Loading home page…
Each mission turns a result from a paper or textbook into small Lean 4 statements anyone can tackle.
Campaigns group missions around a shared mathematical goal. Each one tracks a quantity, such as an upper or lower bound. Have a good candidate in mind? Ping us on Slack, Zulip, or WeChat.
Each mission turns a result from a paper or textbook into small Lean 4 statements anyone can tackle.
Campaigns group missions around a shared mathematical goal. Each one tracks a quantity, such as an upper or lower bound. Have a good candidate in mind? Ping us on Slack, Zulip, or WeChat.
Classical algorithms solve all-pairs shortest paths in time. In a 2026 breakthrough, Alman and Vassilevska Williams refuted the APSP conjecture with a deterministic algorithm. How low can the exponent go?
Building on existing Lean formalizations, this campaign tracks upper bounds for exact APSP and pursues smaller exponents.
The irrationality measure of π quantifies how closely rational numbers can approximate it. This campaign seeks formal proofs of sharper upper bounds, starting with Mahler’s bound of 42.
The sharp Hlawka inequality for Schatten -norms is a cousin of the triangle inequality: it relates the norms of three matrices to the norms of their pairwise sums and their total sum. For complex diagonal matrices, an exact formula for the best possible comparison constant has been proved in Lean for every real . We conjecture that the same formula holds for all .
What is the smallest cutoff for which this formula holds for every real ?
References:
Is every odd number a sum of primes? This campaign tracks formalized proofs of the smallest that suffices.
Schnirelmann (1930) showed some finite works. Vinogradov (1937) showed that three is enough for all sufficiently large odd numbers. Tao (2012) proved unconditionally. Helfgott (2013) proved that every odd number greater than is a sum of three primes, though the proof is still unrefereed. Ideally, we can formalize this statement here. Note that three is optimal: is neither prime nor + prime.
Schoolbook matrix multiplication takes operations. The exponent is the infimum of all such that two matrices can be multiplied in arithmetic operations; trivially , and is conjectured but open.
Strassen gave the first nontrivial bound, , in 1969, and introduced the laser method in 1986 to reach . Coppersmith and Winograd's 1990 bound of stood for two decades. Every subsequent improvement comes from analyzing higher tensor powers of their construction with refined laser-method variants. That line reached in 2025, and the current record is , from August 2026. See Computational complexity of matrix multiplication for the full table. Can we formalize these results and even improve on them?
The irrationality measure is the supremum of the for which has infinitely many rational solutions . Every irrational number has (Dirichlet), almost every real number has , and it is conjectured that . Known upper bounds:
The campaign's first proved value is Mahler's . This entry records Chudnovsky's bound.
The campaign template with the value filled in: PiIrrationality.UpperBound (19.8899945 : ℝ), i.e. .
Value. The bound is quoted in the literature as (e.g. Hata 1993), a truncation. This entry rounds the last digit up to so that the goal follows from the published constant.
Chudnovsky determined the exact asymptotic behaviour of the Hermite-type contour integrals behind Mahler's approximations, which sharpens the resulting exponent.
Each step down the list replaces Mahler's approximations with a sharper family. Formalizing would build reusable explicit machinery: integral constructions of rational approximations to , bounds on their common denominators via prime-number estimates, and the standard lemma turning a sequence of good approximations into an irrationality-measure bound.
The irrationality measure is the supremum of the for which has infinitely many rational solutions . Every irrational number has (Dirichlet), almost every real number has , and it is conjectured that . Known upper bounds:
The campaign's first proved value is Mahler's . This entry records Mignotte's bound.
The campaign template with the value filled in: PiIrrationality.UpperBound (20.6 : ℝ), i.e. .
Value. The paper's abstract states for all , which gives exactly as stated. The paper also proves for (explicit), so follows from the same source; this entry uses the table value .
Mignotte refined Mahler's method of explicit rational approximations to (Hermite's approximation formulae for the exponential and logarithm) and sharpened the estimates that turn their size and denominators into an irrationality measure.
Each step down the list replaces Mahler's approximations with a sharper family. Formalizing would build reusable explicit machinery: integral constructions of rational approximations to , bounds on their common denominators via prime-number estimates, and the standard lemma turning a sequence of good approximations into an irrationality-measure bound.
This mission formalizes Y. Lodha and J. T. Moore, A nonamenable finitely presented group of piecewise projective homeomorphisms, Groups Geom. Dyn. 10 (2016) 177–200 (doi:10.4171/GGD/347; arXiv:1308.4250v3, whose page numbers are used): the group generated by three explicit piecewise projective homeomorphisms of the line is nonamenable and finitely presented, the first torsion-free finitely presented counterexample to the von Neumann–Day problem.
A discrete group is amenable when it has a finitely additive invariant probability measure on all its subsets. A group containing a nonabelian free subgroup is not amenable, and von Neumann and Day asked whether the converse holds. The counterexamples found before Monod's work are built from torsion groups by elaborate inductive constructions. Monod (2013) found nonamenable groups without free subgroups among piecewise projective homeomorphisms of the line. Lodha and Moore isolate in Monod's group a subgroup with three explicit generators and nine explicit relations.
Timeline.
The generators act on the real line: , and , are the piecewise projective maps of p. 2 (aFun, bFun, cFun). As homeomorphisms of the projective line (a, b, c) they generate (G0), inside the group where the published Monod bundle defines (Monod.Hpp).
Lodha and Moore move to infinite binary sequences through the continued-fraction map (Phi), under which , , become functions , , of sequences (Proposition 3.1). There and are and acting on the sequences that extend . is the group generated by all and , the group generated by the and the with not constant, and the five families of relations (1)–(5) among them. Products are taken left to right, as in the paper.
Section 5 rewrites words in the generators by explicit substitutions into standard forms and sufficiently expanded standard forms, and tracks them through strings in , , , ; these notions form the second definitions bundle.
ConnesFeldmanWeiss.exists_nonsingular_generator_of_isAmenableRel) as two milestones; Theorems 2.1 (Zimmer) and 2.2 (Carrière and Ghys) as printed; the group ; and the identities and orbit comparison of p. 4.The result. settles the finitely presented von Neumann–Day problem with a group that is torsion-free, has explicit generators and relations, and acts by piecewise projective maps, so its elements can be described by labeled tree diagrams much as those of Thompson's group . It shows that shares the combinatorics of without its unresolved amenability question.
Formalizing it. Before this mission none of the paper was formalized. The Monod mission's milestones supply the setting, and the case of Carrière and Ghys that Monod uses is already proved there by an elementary argument (Monod.not_isAmenableRel_mob).
Nonamenability is a short reduction to Theorem 2.2, which in general is deep. Finite presentation is the bulk: one must show that every word that evaluates to the identity can be reduced to an -word by the substitutions of §5, through a well-founded ordering on standard forms (Lemma 5.6) and an analysis of how acts on binary expansions (Lemmas 5.9–5.11).
Lean representation and conventions.
List Bool (finite) and Stream' Bool (infinite). is explicit; and are defined by the recursion of p. 5, digit by digit.Stream' Bool, so that products are left to right as in the paper. Statements about , , take products in the opposite of the homeomorphism group for the same reason.a, b, c are the homeomorphisms that agree with the formulas on , and toSeqGroup turns a bijection of sequences into a group element. Both fall back to the identity for a function that is not a homeomorphism or a bijection. Every generator is in fact one, so the fallback is never reached, and a trivial group would make the goal false.Matrix.ProjectiveSpecialLinearGroup, with the quotient topology), as on p. 4; a class acts on the projective line by the Möbius map of either of its matrices, through the published Monod bundle.What is left out, and deviations.
CountableOrbit.exists_perm_rel_iff_exists_zpow_eq is the underlying fact).LodhaMoorePrinted.printed_relations_four_and_nine_ne); the milestone uses the translations of the relations in , that they come from.LodhaMoorePrinted.eq_of_step_singleton_y_neg_one), and allow commuting and for any exponents, as the proof of Lemma 5.6 does (with commuting only for positive exponents, Lemma 5.6 fails: LodhaMoorePosCommute.not_forall_exists_derives_sufficientlyExpanded).What a development needs. Monod's mission supplies , its lack of free subgroups, the elementary non-amenability argument for with dense, and the passage from an amenable group to an amenable orbit relation. The theorem of Connes, Feldman and Weiss is published and proved (ConnesFeldmanWeiss.exists_nonsingular_generator_of_isAmenableRel); it gives the hard direction of the equivalence. The presentation of Thompson's group is published by the Cannon–Floyd–Parry mission on the two presentations of Thompson's group . Proofs of any milestone are welcome.
This is the third mission of the series on Assumptions of Physics by G. Carcassi and C. A. Aidala (book, v3.0, 2025), formalizing the order-theoretic core of Part II, Chapter 3, "Properties and quantities". The chapter explains when the possibilities of an experiment can be labelled by numbers: a domain can be described by a quantity exactly when its possibilities already carry a linear order whose order topology is the natural topology. It then shows that integer-valued quantities correspond to sparse orders and decidable domains, and real-valued quantities to dense, complete, separable orders. The mission imports the definitions of mission I (Assumptions of Physics I), which must be launched first.
For an experimental domain with possibilities and natural topology (mission I), a property with values in a topological space fully characterizes if it is a homeomorphism . A quantity is a property whose value space is linearly ordered and carries the order topology. A linear order on is a natural order if its order topology equals . A linear order is sparse if every chain between two elements is finite and dense if between any two elements there is an infinite chain; it is complete if every non-empty bounded subset has a supremum.
These results say that numerical labels are not added to experimental domains from outside: an integer or real quantity can be assigned only when the domain already has the corresponding order structure, and that order is fixed by narrowness of verifiable statements. Theorem 3.51 is a classical characterization of real intervals that the book takes without proof. The results are proved informally in the book (3.51 is only sketched there); no machine-checked formalization of the domain-level statements is known to the drafters.
Theorem 3.9 needs transport of a linear order along a homeomorphism and the fact that order isomorphisms are homeomorphisms of order topologies. Theorem 3.51 needs the uniqueness of Dedekind completions of a countable dense order and must handle every kind of endpoint behaviour of a contiguous subset of . Proposition 3.46 must cover finite as well as infinite domains: the book's proof uses a bijection with , which exists only for countably infinite possibility sets.
Quantities are types Q with Mathlib's LinearOrder, TopologicalSpace and OrderTopology; full characterization is Nonempty (D.Possibility ≃ₜ Q); a natural order is a LinearOrder structure on D.Possibility whose Preorder.topology equals the natural topology. "Contiguous subset" is Set.OrdConnected. For continuous quantities the subset carries its own order topology, as in Definitions 3.6 and 3.52. In Theorems 3.44 and 3.46 the value type ranges over Type, which is enough because sparse orders are countable. Sections 3.3 and 3.6 (references and their ordering, statement (3) of Theorems 3.44 and 3.53, Theorem 3.38) are left for a later mission: they need a separate formal theory of references.
This is the second mission of the series on Assumptions of Physics by G. Carcassi and C. A. Aidala (book, v3.0, 2025), formalizing Part II, Chapter 2, "Domain combination and relationships". The chapter asks when the outcome of one experiment can be inferred from another (e.g. temperature from the height of a mercury column), and shows that such inference relationships between verifiable statements correspond to causal relationships between possibilities, which are continuous maps of the natural topologies. It builds on the definitions of the first mission (Assumptions of Physics I), which must be launched first because this mission imports its definition file.
Statements are truth sets over the possible assignments of a fixed logical context; an experimental domain , its possibilities , verifiable sets and natural topology are as in mission I. An inference relationship from to is a map with ; depends on if one exists, and two domains are equivalent if each depends on the other. A causal relationship is a function between possibilities with . The combined domain of a countable family of domains is generated by all their statements under finite conjunction and countable disjunction.
Theorem 2.10 is what justifies describing experimental relationships by functions between possibilities rather than by maps between all finite-precision statements, and Corollary 2.11 identifies equivalence of experimental domains with homeomorphisms that respect the statements. Later chapters use these to transport structure between equivalent domains. The results are proved informally in the book; no machine-checked formalization is known to the drafters.
The forward direction requires showing that each possibility of lies inside exactly one possibility of and that preimages of verifiable sets are verifiable. The converse is subtler: Definition 2.7 does not require continuity, and the book's Corollary 2.8 ("all causal relationships are continuous") does not hold in general. For example, with , and , the identity on possibilities is a causal relationship but . The goal therefore includes continuity of explicitly. That is the hypothesis the book's proof of the converse actually uses.
Domains are ExperimentalDomain Ω on a common type Ω; dependence is ExperimentalDomain.DependsOn (existence of an equivalence-preserving map, which here is the inclusion ), causal relationships are predicates IsCausalRel on functions between the possibility types, and topological notions are Mathlib's (Continuous, ≃ₜ). The combined domain ExperimentalDomain.combined takes a family over an arbitrary countable index type. Theorem 2.12 (transport of structure) is informal in the source and is not formalized here. Propositions 2.15–2.28 are left out: the residual possibility depends on the choice of basis, and Proposition 2.18 appears to need a stronger independence hypothesis than Definition 2.17 provides. They are candidates for a later mission.
We formalize the equivalence between Turing machines and the WordRAM model of computation. Turing machines are the standard model for studying computability, but algorithms are rarely described in terms of tape operations. WordRAM is much closer to assembly, with memory accesses, arithmetic instructions, branches, and loops. The goal is to connect this familiar way of expressing algorithms to the foundations of computability. This will also bring us closer to one day formalizing Fine Grained Complexity.
The formal target is halting equivalence through simulations in both directions, with the stated memory bounds and a family of word widths, each fixed during a run.
A basic question of combinatorial geometry asks when a family of sets can be pierced (or stabbed) by few points. For intervals on the real line the answer is classical: if every two of finitely many closed intervals intersect, one point meets all of them, namely the rightmost left endpoint. This is the one-dimensional case of Helly's theorem. The situation changes as soon as the sets are allowed to have holes. Unions of two intervals can intersect pairwise without any point being common to three of them, so no single point suffices, and it is not obvious that any bound depending only on the number of holes exists.
This mission formalizes the answer given in Section 8.6 of Matoušek and Gärtner's Understanding and Using Linear Programming (Springer, 2007): pairwise intersecting unions of intervals can always be pierced by points. The section uses the result to illustrate a general method of combinatorics, in which a linear programming relaxation of a covering problem is bounded through LP duality and then rounded. The same scheme, a bound on the fractional transversal number followed by a rounding step, appears across discrete geometry and combinatorial optimization.
Timeline.
Fix an integer . A -interval is a union of closed intervals on the real line,
The numbers and are the endpoints of . A finite family of -intervals is pairwise intersecting if for all . A set of real numbers is a transversal of if every contains a point of .
More generally, for a finite set and a system of subsets of : a transversal is a set meeting every member; the transversal number is the smallest size of a transversal; a matching is a subsystem of pairwise disjoint members, and the matching number is the largest size of a matching. The fractional transversal number is the optimal value of the linear program
and the fractional matching number is the optimal value of
This is the book's theorem with its constant .
The result. Theorem 8.6.1 shows that the piercing number of pairwise intersecting -intervals is bounded by a function of alone, and that this function is polynomial. The section also states, without proof, the extension for arbitrary finite families of -intervals. Upper bounds of this kind feed into piercing and hitting-set questions for families with bounded "complexity", and the chain is the standard frame in which such bounds are proved.
Formalizing it. The theorem, both lemmas and the duality chain are proved in the literature and in the book. None of them is on the platform. The work consists of formalizing the book's proof: a double-counting argument, LP duality for the pair of fractional programs together with the rationality of an optimal basic solution, and a rounding step. The general-set-system milestone is reusable for any transversal problem, independent of -intervals.
The obvious generalization of the one-dimensional argument fails: for no point need be common to all members, so there is no single extremal endpoint to choose, and a greedy piercing procedure has no control over how many points it uses. The difficulty is to obtain a bound that does not depend on the size of the family. In the book's route the counting statement of Lemma 8.6.2 holds only for equal weights, while the fractional programs produce arbitrary real weights, and the passage between the two, as well as the passage from a fractional transversal of small total weight to an actual finite set of points, are the steps that need care.
A -interval is stored as data: two functions left, right : Fin d → ℝ with left k ≤ right k, together with the set toSet . Components are indexed . Endpoints are those of the given components, so they depend on the representation, as in the book's proofs. Families are Finsets of such data; Lemma 8.6.2 uses a Fin n-indexed sequence, since the proof of Lemma 8.6.3 applies it to a sequence with repetitions. The hypotheses (the book's definition) and, in Lemma 8.6.2, are explicit. The quantity is real division. Transversal sizes are cardinalities of a Finset ℝ bounded by .
For set systems, is a finite type and a Finset (Finset V) with nonempty members; without this assumption no transversal exists and both fractional programs degenerate. The numbers and are expressed through optimal feasible solutions, not as infima or suprema, so no junk value of an empty or unbounded set is involved. is an sInf over that is attained under the nonemptiness assumption, and is a maximum over the finite family of matchings.
A trivializing formalization is ruled out: the pairwise-intersection hypothesis is satisfiable by nonempty families, the transversal is required to meet the actual sets , not a representation artifact, and the bound and are the book's constants, not weakened ones.
Needed infrastructure: finite sums over Finset ℝ, LP duality for a finite primal–dual pair in inequality form (or a direct proof of the chain), rationality of an optimal vertex, and a left-to-right sweep over a sorted finite set of reals. Contributions of a general LP duality statement for set-system relaxations are welcome and reusable.
A deep-space probe sends a vector encoded as , and up to about 8% of the transmitted numbers may be corrupted arbitrarily. Section 8.5 of Matoušek and Gärtner's Understanding and Using Linear Programming (Springer 2007, DOI 10.1007/978-3-540-30717-4) shows that decoding reduces to finding a sparse solution of an underdetermined linear system , and that under suitable conditions this sparse solution is found exactly by a single linear program. The same problem arises in signal processing (sparse representations in redundant wavelet dictionaries) and in computer tomography, and it is the core of what became known as compressed sensing.
Timeline, as recorded in the book's references:
Let be a real matrix with and . The support of is . For an integer , a sparse solution of is an with and . The -norm is .
Basis pursuit is the optimization problem
which is equivalent to the linear program
The matrix is BP-exact for if for every : whenever has a solution with at most nonzero components, is the unique optimal solution of (BP). The crosspolytope is , the kernel of is , and . For with , the cone at is , and is good for if .
For and :
This is the book's geometric characterization of exact recovery, and the statement on which the known probabilistic proofs are built.
With , and an matrix of independent entries, there is a constant such that for every
The book states this without proof. It is included as a separate theorem, not a milestone of the goal.
Lemma 8.5.4 converts an algorithmic property, that an linear program returns a prescribed sparse vector for every right-hand side, into a purely geometric property of the kernel of relative to the low-dimensional faces of the crosspolytope. With milestone 5 it becomes the statement that avoids a finite family of cones, which is where union bounds over faces and estimates for random subspaces enter. Observation 8.5.1 separates what is information-theoretically possible (uniqueness of sparse solutions) from what is computationally achievable by linear programming; finding a sparse solution directly is NP-hard in general. Theorem 8.5.2 is the quantitative payoff: a fixed fraction of arbitrary gross errors can be corrected by solving one linear program.
All of these results are proved in the literature; Lemma 8.5.4, Observation 8.5.1 and the milestones are elementary, and Theorem 8.5.2 rests on Donoho's polytope-neighborliness analysis. The platform has a related formalization of Wainwright's restricted nullspace property (Theorem 7.8 of High-Dimensional Statistics, namespace HighDimStat.SparseLinear), which fixes a support set rather than characterizing exactness for all -sparse vectors through the crosspolytope. A machine-checked proof of Theorem 8.5.2 with the constants and is, to our knowledge, not available anywhere; it would require substantial Gaussian and high-dimensional geometry infrastructure.
For the goal and milestones the difficulty is bookkeeping, not ideas: the scaling between a sparse solution and the boundary point , the case , and the fact that BP-exactness quantifies over all right-hand sides while the geometric side quantifies over boundary points of the crosspolytope.
Theorem 8.5.2 is of a different order. A union bound over the faces of dimension reduces it to bounding the probability that a random -dimensional subspace meets one cone nontrivially, and getting that probability small enough to beat the combinatorial factor with the stated numerical constants is the hard part. Rough asymptotic estimates do not give at .
Vectors are functions Fin n → ℝ (the book's indices become ) and matrices are Matrix (Fin m) (Fin n) ℝ. The -norm is written out as , since Mathlib's norm on Fin n → ℝ is the sup norm. The support is a Finset of indices. Optimality in (BP) and (BP′) is stated against every feasible point; no infimum is taken, so an empty or unbounded feasible set cannot create a spurious optimum. "Every or fewer columns" ranges over finsets of distinct column indices, column being Aᵀ j. The hypotheses and of Lemma 8.5.4 are kept as on the page, although the equivalence does not use them; is also the standing assumption of §8.5 needed for .
In Theorem 8.5.2 the random matrix has the product law of independent gaussianReal 0 1 entries, the constant is quantified before , and measurability of the BP-exact event is part of the conclusion, so the bound concerns a genuine probability rather than an outer measure.
A trivializing formalization is ruled out: BP-exactness requires uniqueness among all minimizers for every right-hand side, not just optimality of , and the crosspolytope condition is an equality of sets, not an inclusion that alone would satisfy.
All definitions live in one module (MatousekLP.SparseRecovery.BasisPursuit); the and support vocabulary is reusable for later sparse-recovery missions. Contributions are welcome on every milestone, on the goal, and on the infrastructure towards Theorem 8.5.2 (Gaussian measures on matrix spaces, measurability of the BP-exact event, the face structure of the crosspolytope).
A binary error-correcting code is a set of -bit words chosen so that the words stay distinguishable after a few bits have been corrupted in transmission. A code can correct any errors exactly when every two of its words differ in at least positions. The more words the code has, the more information each transmitted block carries. So the central quantitative question of coding theory is how large a code of given length and minimum distance can be. Codes are used in every technology that transmits or stores data, from disks and phones to deep-space probes.
In 1973 Philippe Delsarte showed that an upper bound on this maximum size is the optimum value of an explicit linear program (Delsarte, An algebraic approach to the association schemes of coding theory, Philips Res. Repts. Suppl. 10, 1973). The bound was far stronger than the classical volume argument and remains a standard tool. This mission formalizes the self-contained proof of the bound in §8.4 of Matoušek and Gärtner's textbook (Springer 2007). That proof follows Best, Brouwer, MacWilliams, Odlyzko and Sloane (IEEE Trans. Inform. Theory 24, 1978). The mission also covers the step of Delsarte's original argument that the book isolates as a lemma.
Timeline.
A word is , and a code is any set . The Hamming distance is the number of positions with . The weight is the number of ones in . The word is the entrywise sum modulo 2. For , the restricted distance counts only the differing positions that lie in .
A code has distance if for all distinct (Definition 8.4.1). The quantity is the maximum of over all codes with distance .
For the Krawtchouk numbers are
The distance distribution of a code is
The Delsarte linear program has variables . It maximizes subject to:
For Delsarte's original argument, is the matrix whose entry is when and otherwise. The weights are .
The goal is stated against every upper bound of the objective on the feasible set. No particular optimum value is fixed, so the statement covers every and at once.
The Delsarte bound turns an extremal problem over the subsets of the cube into a linear program with variables. For it gives , while the sphere-packing bound gives . Many entries of the standard code tables rest on this bound or its refinements. The positive semidefiniteness in Lemma 8.4.7 is the starting point of the semidefinite programming bounds of Schrijver and of later work. The same framework also underlies the linear programming bounds for spherical codes and sphere packings.
The theorem is classical and fully proved in the literature. Neither Mathlib nor this platform has a formal statement or proof of it. Mathlib has Hamming distance and binomial coefficients, but it has no , no Krawtchouk numbers and no LP bound for codes. This mission would produce the first formal statement and proof. It would also produce reusable identities on Krawtchouk sums and character sums over .
Two of the program's constraints are immediate once is defined: , and for . The difficulty lies in the Krawtchouk constraints. They do not follow from counting pairs at a single distance. They require a sign-weighted count over all words of weight , and the sum must then be regrouped by the distance of each pair. That regrouping identifies a count of words, split by how many ones they share with a fixed word, with the Krawtchouk number. Formally this is an exchange of finite sums together with a binomial counting identity, and the index bookkeeping, including the range , has to be exact.
The obvious attempt proves the inequality one distance class at a time. It fails because the individual terms have no sign. Only the whole sum is nonnegative.
Fin n → Bool, with bit as true. The book's positions become 0, …, n-1. Codes are Finsets of words, and is Mathlib's hammingDist.Finset.sup over the finite family of codes with distance . This family contains the empty code, so the maximum is attained.Fin (n+1) with no index shift. The constraints are imposed for , so they are vacuous for .Matrix.PosSemidef over .No trivialization. The goal is not stated as "" with a real supremum, which Lean would evaluate to on an empty or unbounded set. Its hypothesis ranges over upper bounds of a feasible program: is always feasible, so the hypothesis is never vacuous.
Contributions welcome. Useful lemmas include:
These are reusable for other LP and SDP bounds in coding theory.
A two-player zero-sum game models any situation in which one party's gain is exactly the other party's loss: a military allocation in the spirit of Colonel Blotto, a sealed-bid contest, rock–paper–scissors. The central question is what each player should do when the opponent is also reasoning about them. John von Neumann answered it in 1928 with the minimax theorem (von Neumann 1928): each player has a strategy guaranteeing the same number, the value of the game, whatever the opponent does. The theorem underlies modern game theory, robust decision making, and the analysis of online learning algorithms, where regret bounds are routinely derived from it.
Section 8.1 of Matoušek and Gärtner's Understanding and Using Linear Programming (Springer 2007) presents the theorem as an application of linear programming duality. This mission is the sixth of a series formalizing the capstone results of the book.
Alice has pure strategies and Bob has . A real payoff matrix records Alice's gain, and Bob's loss, when Alice plays her th and Bob his th pure strategy. A mixed strategy of Alice is a probability vector , , ; a mixed strategy of Bob is a probability vector . When the players randomize independently, Alice's expected payoff is
The worst-case payoffs are
over mixed strategies. A mixed strategy of Bob is a best response against if it minimizes ; a mixed strategy of Alice is a best response against if it maximizes it. A pair is a mixed Nash equilibrium (Definition 8.1.1) if each is a best response against the other. Alice's is worst-case optimal if ; Bob's is worst-case optimal if .
The proof in the book passes through three linear programs: the dual of (8.1), which for a fixed maximizes subject to ; program (8.2), the same with as variables subject to , ; and program (8.4), which minimizes subject to , , .
For every payoff matrix with : worst-case optimal mixed strategies exist for both players; for any worst-case optimal of Alice and of Bob, the pair is a mixed Nash equilibrium; and there is a single number , the value of the game, with
for every such pair. The third clause is what distinguishes the theorem from the existence of some saddle point.
The theorem gives a complete prescription for zero-sum play: a worst-case optimal strategy secures at least the value against any opponent, and a worst-case optimal opponent holds the player to at most the value, so both players can announce their strategies in advance without loss. With Lemma 8.1.2(ii) it yields a characterization: a pair of mixed strategies is a Nash equilibrium if and only if both are worst-case optimal. The minimax equality is used downstream in online learning (regret-to-value arguments), in robust optimization, and in Yao's principle for randomized algorithms.
The mathematics is classical and proved; what this mission adds is a machine-checked version in the book's own formulation. The platform already has AGT.zero_sum_minimax (Algorithmic Game Theory I), which proves the existence of a saddle point, and the general FamousTheorems.sion_minimax_theorem. Neither states that every pair of worst-case optimal strategies is an equilibrium with a common value, and neither exhibits the LP route: the dual of (8.1), the programs (8.2) and (8.4), and their duality. The mission records that route statement by statement, so that it can be reused as a worked instance of LP duality.
Lemma 8.1.2 is routine; the entire content is the reverse inequality . The obvious attack, maximizing directly, fails because is a minimum of linear functions and hence not linear, so its maximization is not a linear program as written. The obstacle is removed only by an appeal to LP duality in the proof, together with the facts that the simplices are nonempty and compact, and that the relevant programs are feasible and bounded so that optima exist. None of this is supplied by the pure-strategy structure of the game: pure Nash equilibria need not exist (rock–paper–scissors has none).
Pure strategies are indexed by Fin m and Fin n, with the book's standing assumption carried as hypotheses 1 ≤ m, 1 ≤ n by every theorem; the book's indices become . Mixed strategies are Mathlib's stdSimplex ℝ (Fin m), the payoff is x ⬝ᵥ (M *ᵥ y). is the real sInf and the real sSup of the payoffs over the opponent's simplex; milestone 1 states that these are attained. A mixed Nash equilibrium is defined in the verbal form of Definition 8.1.1 (mutual best responses). Worst-case optimality is defined against all mixed strategies, never as a saddle-point condition, so the goal is not circular with Lemma 8.1.2(iii). LP optimality is stated as "feasible and at least as good as every feasible point", so no supremum over a possibly empty or unbounded feasible set is used.
The book's clause that worst-case optimal strategies "can be efficiently computed by linear programming" is algorithmic and is not part of the formal statement; there is no complexity model. A goal asserting only the existence of worst-case optimal strategies, or only the existence of some equilibrium, would drop the theorem's third clause and is ruled out: the common value is quantified before all pairs of worst-case optimal strategies.
A complete development needs compactness of the standard simplex, continuity of the bilinear payoff, and a strong duality theorem for linear programs in the form of the programs (8.2)/(8.4); the latter is reusable across the whole series. Proofs by other routes (Sion's theorem, a separating hyperplane argument, fixed points) are welcome for the goal; the LP milestones stand on their own as statements about the programs.
Every finite algorithm for linear programming rests on one structural fact: if a linear program has an optimum at all, it has one at a point singled out by finitely many linear conditions. The simplex method walks between such points, and exact complexity analyses, sensitivity analysis and integrality arguments all start from them. Chapter 4 of J. Matoušek and B. Gärtner, Understanding and Using Linear Programming (Springer, 2007, DOI 10.1007/978-3-540-30717-4), establishes this fact for linear programs in equational form, in the definitions that the rest of the book (the simplex method of Chapter 5, duality in Chapter 6, the applications in Chapter 8) uses.
This mission is the second of a series formalizing that book. It fixes the book's notion of a basic feasible solution and of a vertex, and targets the theorem that optimal solutions exist whenever the program is feasible and bounded, and can then be chosen basic.
A linear program in equational form is
where is a real matrix, , , and means every coordinate of is nonnegative. A feasible solution is an satisfying both constraints; the set of them is . An optimal solution is a feasible with for every feasible . The objective is bounded from above if some real satisfies for all feasible .
Throughout Section 4.2 the book assumes that has columns and rank (its rows are linearly independent). For , denotes the matrix formed by the columns of with indices in . A basis is an -element set for which is nonsingular, i.e. its columns are linearly independent. A basic feasible solution is a feasible for which some basis has for every .
A point is a vertex of if and some nonzero satisfies for every : is the unique maximizer over of a nonzero linear function.
For of rank with ,
Both parts are one theorem, as in the book. Part (i) says optimal solutions fail to exist only for the two obvious reasons, infeasibility and unboundedness; part (ii) says an optimum can always be found among basic feasible solutions.
Theorem 4.2.3 gives a finite, if impractical, algorithm for linear programming: enumerate the at most sets , solve , and keep the best nonnegative solution. It is the correctness backbone of the simplex method, which visits basic feasible solutions in a smarter order, and it is the source of the book's claim that a feasible and bounded linear program has an optimal solution. Theorem 4.4.1 identifies this algebraic notion with the geometric corners of the feasible polyhedron, which is what makes statements such as "the LP relaxation has an integral vertex" in later chapters meaningful.
All of these results are classical and fully proved in the book. The value of formalizing them here is the definition layer: later missions of this series (Bland's rule, the central path, the scheduling application) state their results about bases and basic feasible solutions in exactly these definitions, and a proved Theorem 4.2.3 in this form lets them import the existence of an optimal basic solution instead of re-deriving it. Related facts are already machine-checked on Prove2Me in the formulation of Bertsimas and Tsitsiklis (Introduction to Linear Optimization I and II: minimization over polyhedra , extreme points, basic solutions as active linearly independent constraints). Those statements concern a different presentation of the program and a different notion of basic solution; connecting them to the equational-form statements here is itself a welcome contribution.
The obvious argument for part (i), "a continuous function on a closed set bounded above attains its supremum", fails: the feasible set is usually unbounded, and a linear function bounded above on an unbounded closed convex set need not obviously attain its supremum without using the polyhedral structure. The existence of an optimum is exactly the nontrivial content of part (i); compactness is not available.
For milestone 1, the delicate direction is the converse: a set of linearly independent columns indexed by must be completed to an -element basis, which requires the rank- assumption. For Theorem 4.4.1, the direction from vertex to basic feasible solution is not local: a vertex is defined by an optimization property, while basicness is a statement about the support of the point.
All items live in the namespace MatousekLP.BFS and share one definition module, MatousekLP.BFS.EquationalForm. Conventions:
Fin n → ℝ, matrices Matrix (Fin m) (Fin n) ℝ; the book's indices are 0, …, n-1;A *ᵥ x = b, is 0 ≤ x (pointwise), is c ⬝ᵥ x;Finset (Fin n); " nonsingular" is linear independence over of the family of columns of indexed by the elements of , together with B.card = m;m ≤ n and A.rank = m on every theorem;Set.extremePoints; the book's remark on p. 55 that the two coincide is not used as a definition;A formalization in which "optimal" were defined through sSup of the objective over the feasible set would make part (ii) trivially true or false on unbounded programs; the definitions here rule that out. Dropping the rank hypothesis would make part (ii) false (no basis exists when the rows are dependent), so it is not optional.
Reusable infrastructure: the column-restriction and basis vocabulary, the support set , and the extension of a linearly independent set of columns to a basis of the column space are needed again in the simplex chapter. Proofs of any milestone, and bridges to Mathlib's Set.extremePoints or to the Bertsimas–Tsitsiklis statements on the platform, are welcome.
Almost every screening, auction and regulation model asks the same preliminary question: which allocation rules can be made incentive-compatible by some choice of payments? In the one-dimensional models of auction theory and nonlinear pricing the answer is monotonicity: higher types must receive higher allocations. Many applications are not one-dimensional, though. Examples are multi-object auctions, multi-product pricing, and lotteries over several outcomes. For those, a characterization that uses no structure at all is needed. Rochet (1987) gave one: an allocation rule is implementable exactly when it is cyclically monotone, a condition that originates in Rockafellar's characterization of subdifferentials of convex functions. Later work on dominant-strategy implementation, the "weak monotonicity" literature of algorithmic mechanism design, and revenue equivalence all build on it.
This mission formalizes Chapter 5 of Börgers, An Introduction to the Theory of Mechanism Design (Oxford University Press, 2015): all nine numbered results of the chapter.
Timeline. Rockafellar (1970, Theorem 24.8) characterized the cyclically monotone maps between vector spaces as the subgradient selections of convex functions. Rochet (1987) extended the idea to arbitrary alternatives and types with quasi-linear utility and proved that implementability is exactly cyclical monotonicity. Krishna and Maenner (2001) proved revenue equivalence on convex type spaces with utilities convex in the type. Bikhchandani, Chatterji, Lavi, Mu'alem, Nisan and Sen (2006) showed that for finitely many alternatives, weak monotonicity (the two-type case of cyclical monotonicity) already suffices on rich, order-based domains. Saks and Yu (2005) proved the same on convex domains.
A designer and one agent choose an alternative from a set . The agent has a type in a nonempty set . With utility function , her payoff from when she pays is . Neither nor carries any structure.
A direct mechanism is a decision rule and a transfer rule . It is incentive-compatible if for all . A decision rule is implementable if some makes it incentive-compatible. It is weakly monotone if for all pairs of types. It is cyclically monotone if for every finite sequence of types with ,
A complete and transitive order of induces a partial order on types: if values every -higher alternative strictly more, relative to an -lower one, than does, and neither type distinguishes -indifferent alternatives. The type set is one-dimensional if any two distinct types are -comparable, and bounded if all utility differences lie in for some . It is rich if, for some reflexive and transitive relation , every function with is some type's utility function. A mechanism is individually rational with outside option if every type does at least as well as with and no payment.
for arbitrary , nonempty and .
Rochet's theorem turns the existence of payments, an infinite system of linear inequalities in unknowns , into a condition on the decision rule alone. It underlies the characterization of implementable rules in multidimensional screening, the taxation principle, and the dominant-strategy characterizations of Chapter 7 (applied agent by agent). Propositions 5.4–5.6 recover the "monotone allocation" results of the one-dimensional chapters from it. Proposition 5.8 is the general form of the payoff-equivalence lemmas used for optimal auctions.
All results are classical and proved on paper, except Propositions 5.7 and 5.8, whose proofs the book omits and refers to the literature. None of them is formalized on Prove2Me. The platform's algorithmic-game-theory series has the weak-monotonicity half in a multi-agent valuation model (types are valuations ), not the abstract-type statement, and has no cyclical-monotonicity or Rochet result.
Necessity is a two-line telescoping argument. Sufficiency needs a transfer rule built from the decision rule, and the first idea fails: prices attached to alternatives chosen pair by pair (which weak monotonicity supplies) need not be globally consistent. Figure 5.1 of the book gives a three-type example that is weakly monotone but not implementable. The transfer must come from a supremum over all finite chains of types starting at a fixed type. The supremum is finite only because of cyclical monotonicity, and no finiteness, compactness or boundedness is available. Proposition 5.8 needs an envelope argument along segments in without differentiability. Proposition 5.7 needs a combinatorial argument that uses richness of the domain.
Alternatives and types are arbitrary Lean types A, Θ with Nonempty Θ, and the utility is u : A → Θ → ℝ. A cycle of length is a map Fin (m+1) → Θ with equal first and last entries, and its summands are indexed by Fin m. Relations are predicates A → A → Prop. For Propositions 5.3 and 5.8, types form a subset S of Ω → ℝ (resp. Fin n → ℝ) used as a subtype. Lotteries are stdSimplex ℝ Ω, and the subgradient inequality is required only at points of S.
The explicit statements are fixed as follows:
Two statements are corrected from the page, each with a counterexample to the literal version recorded in its item:
Both directions of Rochet's theorem are required. The necessity half alone, or a version with finite , finite or bounded utilities, is a different and much weaker theorem and does not close the goal.
The development needs finite telescoping sums, suprema of sets of reals (sSup with an explicit bounded-above argument), convex functions on sets and one-dimensional convex analysis (Proposition 5.8). The definitions file is reusable for Chapters 6–8 of the series. Contributions of alternative proofs, for example Proposition 5.6 through Rochet's theorem, are welcome.
Assumptions of Physics by Gabriele Carcassi and Christine A. Aidala (book, v3.0, 2025) is a programme to derive the mathematical structures of physical theories from explicit physical requirements. Part II, "Physical Mathematics", begins (Chapter 1) by making precise what it means for a statement to be experimentally verifiable, and shows that a single physical requirement (only countably many tests can be run in an indefinite amount of time) is enough to force the familiar structures of point-set topology onto the space of outcomes of any experiment. This mission formalizes that chapter. It is the first mission of a series on the book; all declarations live in the namespace AssumptionsOfPhysics so that later missions can build on them.
A logical context is represented by its set of possible truth assignments, and a statement (up to logical equivalence) by its truth set . Negation, conjunction and disjunction are complement, intersection and union; the certainty is and the impossibility is ; " is narrower than " means , and are compatible when .
An experimental domain is a family of statements that contains and , is closed under finite conjunction and countable disjunction, and has a countable basis : every element of is obtained from by finite conjunctions and countable disjunctions. Its theoretical domain is the closure of under negation, finite conjunction and countable disjunction. A possibility is a non-impossible that, for every , is either narrower than or incompatible with it; denotes the set of possibilities. The verifiable set of a statement is , and the natural topology on is the topology generated by . A domain is decidable if it is closed under negation.
The chapter's results identify the open sets of a topology with verifiable statements and its points with complete experimental answers (possibilities). Second countability and the axiom are thereby derived rather than assumed, and the cardinality bound limits which mathematical objects can carry experimental meaning. Later chapters of the book (domain combination, properties and quantities, ensemble spaces) rely on these facts. The results are proved informally in the book; no machine-checked formalization of them is known to the drafters. A formalization fixes the precise hypotheses under which they hold (for instance, whether a basis must be countable in Propositions 1.46, 1.48 and 1.60) and provides a reusable library for the rest of the series.
The individual statements are elementary, but several of the book's proofs are informal about two points that a formal proof must handle. First, the possibilities must be shown to cover the space of assignments and to be atoms of ; the book argues through minterms of a countable basis, which needs a "disjunctive normal form" for countably generated families. Second, the natural topology is defined via arbitrary unions while experimental domains are only closed under countable disjunction; showing that every open set is still of the form (Proposition 1.57) requires a second-countability / Lindelöf-type argument rather than direct closure.
Statements are subsets s : Set Ω of an arbitrary type Ω (possibly empty); the experimental domain is the structure ExperimentalDomain Ω, whose field stmts is the family . Generation by finite conjunction and countable disjunction (FinConjCountDisj) includes the empty conjunction and the empty disjunction ; generation with negation (NegFinConjCountDisj) includes . Possibilities form the type D.Possibility, which carries the natural topology as an instance; topological notions (SecondCountableTopology, T0Space, T1Space, DiscreteTopology) are Mathlib's. The primitive notion of verifiability (Axiom 1.27) is not modelled separately: membership in is what all results of the chapter use. Statements involving "a basis" quantify over every basis (countable or not), as in the source. Contributions of reusable lemmas, in particular a disjunctive-normal-form lemma for countably generated families of sets, are welcome.
This is the fourth mission of the series on Assumptions of Physics by G. Carcassi and C. A. Aidala (book, v3.0, 2025), formalizing the axiomatic core of Part II, Chapter 4, "Ensemble spaces". The chapter proposes three physically motivated axioms (ensemble, mixture, entropy) that every space of statistical states should satisfy, covering classical probability distributions and quantum density operators alike, and derives from them structure that is usually postulated, for example that mixtures can be "un-mixed" (cancellativity). That is the first step towards embedding ensembles in a vector space. Unlike missions II and III, this mission does not depend on earlier missions.
An ensemble space is a , second countable topological space with a continuous mixing operation (, ) that is idempotent, commutative and associative, and a continuous entropy . The entropy is strictly concave, with equality iff , and bounded above by for a universal function . Two ensembles are orthogonal, , when this bound is saturated, and mixtures preserve orthogonality. An ensemble is a component of if with ; two ensembles are separate if they have no common component. The mixing entropy is .
Cancellativity is what allows affine combinations with negative coefficients, the origin, in this framework, of the vector-space embedding of ensembles (Theorem 4.94) and of negative quasi-probabilities such as Wigner functions. It holds in classical and quantum statistics, and here it is derived from continuity and strict concavity of the entropy instead of being postulated. The results are proved informally in the book; no machine-checked formalization is known to the drafters.
The convex-space axioms are stated in a two-sided associativity form, so every rearrangement of mixtures must be derived from it. The book's proof of cancellativity first propagates the equality from one coefficient to all of by an iteration , and then uses a limit together with continuity of mixing and of the entropy. Strict concavity has to be applied only to non-trivial coefficients.
The structure EnsembleSpace I E bundles Axioms 4.4, 4.7 and 4.55 for a topological space E; mixing coefficients are elements of Mathlib's unitInterval. Real coefficient expressions in the associativity axiom pass through clampI, the projection , and lie in on the stated domain. The universal function is a parameter. Orthogonality is saturation of the upper bound for every . Strict concavity is required for only, since at equality is automatic. The book's Proposition 4.67 uses for , which follows from universality of (any space with two distinct ensembles forces it); the milestone carries this as an explicit hypothesis. Items 3 and 4 of Proposition 4.116 in the book use the normalization from Theorem 4.59; item 3 is stated with and item 4 is omitted. Hull operators, the vector-space embedding (Theorem 4.94), boundedness of lines (Theorem 4.105), the entropic geometry and the standard classical/quantum models (Propositions 4.5, 4.9, 4.56) are left for later missions.
Chapter IX of von Neumann and Morgenstern's Theory of Games and Economic Behavior asks when a game played by many participants is really several separate games played side by side. The authors' motivation (41.1) is methodological: the general theory of the -person game becomes unmanageable as grows, and one way to gain insight into large games is to isolate classes of games that can be analysed exactly. The first such class consists of games whose players fall into groups that have no dealings with each other — the book's example is the internal economies of two countries whose connections are disregarded (41.2.4). Such a game is the composition of its constituents, and the question of the chapter is how to recognise a composite game from its characteristic function alone and how far a given game can be decomposed.
The answer (§43) is a structure theorem. The groups of players that can be split off form a Boolean algebra of sets; its atoms, the minimal splitting sets, form a partition of the set of players, the decomposition partition ; and every splitting set is a union of blocks of . The book remarks (41.3.3) that the splitting condition (41:7) is exactly Carathéodory's criterion of measurability, transported from measures to characteristic functions. The mission formalizes §43, together with the criterion (42:G) of §42 on which it rests.
Let be a finite set of players. A characteristic function is a real number for every subset (every coalition, including the empty set and ). Write . From 42.4.1 on the book works in the domain of constant-sum games, whose characteristic functions are, by (42:D), exactly the functions satisfying
For with complement , the game is decomposable with respect to and if there are constant-sum games on the players and on the players with for all — formula (41:3). The -constituent is the game on with for (41:4).
A splitting set (43.1) is a satisfying (41:6),
The game is indecomposable if and are its only splitting sets (43.3.1). A minimal splitting set is a splitting set none of whose proper subsets is splitting (43.3.2), and is the system of all minimal splitting sets. The game is inessential (42:F) if it is strategically equivalent to the zero game, i.e. for all , for some reals (the transformation (42:5)).
For every satisfying (42:6:a)–(42:6:c):
The goal combines the partition property and the characterization of all splitting sets; it is the book's own summary of §43.3 and does not presuppose that is a partition.
In attack order: the criterion (42:G) (decomposability (41:6) (41:7)); the closure properties (43:A) (complements), (43:B) (, ), (43:C) (intersections and unions); (43:D) (splitting sets of a constituent) and (43:E) (a constituent is indecomposable iff its set is minimal); (43:F), (43:G) separately; (43:I) (a minimal splitting set is disjoint from, or inside, any splitting set); the restatement (43:H*) ( splits iff every block of lies inside or outside ); and the two extreme cases (43:J) ( = all singletons iff the game is inessential) and (43:K) ( iff the game is indecomposable).
The decomposition partition is canonical: every constant-sum game splits uniquely into indecomposable constituents, and (43:E) identifies them as the constituents on the blocks of . The two extreme cases (43:J), (43:K) show that inessentiality and indecomposability are opposite ends of one scale. Chapter IX uses this structure in §§44–47, where solutions of decomposable games are related to solutions of their constituents ((46:A)–(46:I)); a formal decomposition partition is the prerequisite for that later work, and a candidate follow-up mission.
The results are classical and proved in the book. The mission's contribution is a machine-checked version: a formal definition layer for splitting sets of a set function on a finite set, the Boolean-algebra closure, and the atomic decomposition. The combinatorial core — that the sets satisfying a Carathéodory-type additivity condition form a Boolean algebra of a finite set, whose atoms partition it — is reusable outside game theory (for instance for finitely additive decompositions of set functions). No machine-checked version of these results is known to exist; they are formalized here for the first time as far as a search of the platform shows.
The individual steps are elementary, but the obvious argument for the key closure property (43:C) fails: to show that is splitting one cannot simply add the identities (41:6) for and for , since a pair , is not of the form those identities control, and may be nonempty — the book's footnote on p. 354 singles out overlapping splitting sets as the case its proof is really about. Likewise (43:D) is not a tautology: that a set self-contained within a self-contained set is self-contained in the whole game has to be proved (footnote 1, p. 355). Formally, the main work is bookkeeping of set identities and the passage between subsets of (players of the constituent) and subsets of .
ι with decidable equality (the book's ; in Chapter IX players are also named ). Coalitions are Finset ι, and are the complement Sᶜ in , and is a function Finset ι → ℝ.IsConstantSum), the chapter's domain from 42.5.3 on ("in the remainder of this chapter we will continue to consider constant-sum games", p. 353). is arbitrary: the statements are not restricted to zero-sum games, which would be a weaker special case. (43:K) additionally assumes nonempty ([Nonempty ι], the book's ); every other statement holds without it. (43:E) assumes , since the book's constituent is a game and has at least one player.↥J, ↥Jᶜ; the -constituent is restricted to subsets of ↥J. Sums of sets are unions; "disjunct" is Disjoint.decompositionPartition v is the set of minimal splitting sets; that it is a partition is proved, not assumed. An aggregate of minimal splitting sets is a finite family A, its sum A.sup id; the empty aggregate gives .Finset ι and their atoms, which would shorten (43:F)–(43:H).Consider the classical error-correcting problem. An input vector (the plaintext) is encoded as by a coding matrix with , and an unknown, arbitrary vector of errors corrupts the result, so that only is observed. Can be recovered exactly, and by an algorithm whose running time is polynomial in ? Candès and Tao (2005) answer both questions at once: if a matrix annihilating satisfies a restricted orthonormality condition, then is the unique solution of the convex program , which is a linear program, whenever at most entries of are corrupted, whatever their positions and values. Read for the matrix alone, the same theorem says that minimization (basis pursuit) returns the sparsest solution of an underdetermined linear system. That statement is the mathematical core of compressed sensing, and the restricted isometry constants introduced in this paper became the standard tool of the field.
Timeline. Donoho and Huo (2001), followed by Elad–Bruckstein, Donoho–Elad and Gribonval–Nielsen, proved the equivalence of and minimization for matrices formed by concatenating two orthonormal bases, for sparsity of order , through incoherence. Candès, Romberg and Tao (2004) and Candès and Tao (2004) obtained recovery with overwhelming probability for random matrices at sparsity of order . Donoho (2004) showed for Gaussian matrices that a constant, unspecified fraction of nonzero entries can be tolerated. The present paper (December 2004, published 2005) gives a deterministic sufficient condition, , valid for every matrix, and specializes it to Gaussian matrices with explicit numerical values of the tolerable fraction. Later work, for instance Candès (2008) with the condition , sharpened the sufficient condition; those later results are not part of this mission.
Let be a real matrix with columns , and let be the linear span of these columns. For an index set and real coefficients , write . A vector is supported on when for all ; with this convention is just the product . Norms are the Euclidean norm and the norm .
Definition 1.1. For an integer , the -restricted isometry constant is the smallest quantity such that
for all of cardinality at most and all real coefficients . The -restricted orthogonality constant is the smallest quantity such that
for all disjoint with and . The paper writes for . These numbers measure how far the columns of are from an orthonormal system when only linear combinations of at most columns are considered.
The two optimization problems are
A vector is the unique minimizer of one of these problems when it is feasible and every other feasible vector has a strictly larger objective value.
Let be a real matrix of full rank with , and a real matrix with . Let satisfy
If where is supported on a set of size at most , then is the unique minimizer of .
Let satisfy (1.10) for , and let be supported on a set with . Then is the unique minimizer of with .
Theorem 1.5 is the companion of Theorem 1.4 for the decoding problem, and the mission's milestones are the four lemmas the paper proves on the way: Lemma 1.2 (the numbers control the numbers), Lemma 1.3 (uniqueness of sparse representations under ), and the two dual sparse reconstruction properties, Lemma 2.1 ( version) and Lemma 2.2 ( version).
The result. The guarantee is deterministic and uniform: one condition on , checkable in principle from the matrix alone, ensures that a single linear program recovers every sufficiently sparse vector, with no probability of failure. In the decoding reading, a fixed fraction of the ciphertext can be corrupted arbitrarily and the plaintext is still recovered exactly by convex optimization. The paper shows in its Section 3 that Gaussian matrices satisfy (1.10) with overwhelming probability at explicit values of , and in Section 5 that the same hypothesis yields near-optimal recovery of compressible signals from few measurements; both are consequences of the deterministic core formalized here.
Formalizing it. The theorems are proved in the paper, and no machine-checked proof of them exists. Prove2Me holds a formalization of a different restricted-isometry sufficient condition taken from a textbook (HighDimProb.SparseRecovery.rip_implies_exact_recovery); it uses a different definition of the isometry constant and a different hypothesis, so nothing there can be reused as is. This mission produces the definitions of and exactly as in Definition 1.1, the dual-certificate lemmas, and the two theorems, in a form that later missions on compressed sensing can import. The probabilistic Theorem 1.6, Lemma 3.1 and Corollary 1.7, and the compressible-signal Theorem 5.1, are not targets: see the scope section for why.
The whole proof rests on a dual certificate: a vector with for and for . Given such a , the argument of Section 2.2 is a short chain of inequalities. The first idea every newcomer has is ; this interpolates the signs on and, by restricted orthogonality, its inner products off are small in an sense, but not in the sense required. That is exactly Lemma 2.1: the bound holds only outside an exceptional set of at most indices. Lemma 2.2 removes the exceptional set by an infinite alternating iteration, prescribing values on the previous exceptional set while keeping the values on fixed, and summing a geometrically convergent series.
Two points deserve attention from solvers. First, the paper's proof of Lemma 2.2 prescribes values on sets of size up to () at each step, while the per-step factors it quotes, , are what Lemma 2.1 gives for a set of size ; a proof of the printed constant in (2.4) has to account for this, and the hypothesis of Theorem 1.4 leaves room for a proof with slightly worse per-step factors. Second, Lemma 2.1 is printed with in its bound on the exceptional set, while the inequality (2.3) its proof establishes gives ; the mission states the lemma with , which coincides with the printed form in the case used by Lemma 2.2.
Matrices are Matrix (Fin p) (Fin m) ℝ; a coefficient vector on is a vector in Fin m → ℝ supported on the finite set , and is F.mulVec c. The Euclidean and norms and the inner product are explicit finite sums, so every statement can be checked by hand against the paper. is the span of the columns.
The constants and are the infimum of the set of nonnegative (resp. ) satisfying the defining inequalities for all admissible sets and coefficients. This set is nonempty, closed and bounded below, so the infimum is attained and is the paper's smallest quantity; on the paper's domain the smallest such quantity is nonnegative, so the extra clause only fixes a harmless value in degenerate cases such as . The definitions are total in , and each theorem carries the paper's domain conditions (, and , or as needed) as explicit hypotheses. The hypotheses are satisfiable, since a matrix with orthonormal columns has , so none of the statements is vacuous.
"Unique minimizer" is a strict inequality against every competitor. "Full rank" for the matrix with is injectivity of ; both are standing assumptions of the paper's Section 1.1 and appear as hypotheses of Theorem 1.5. In Lemma 2.1, "a constant depending only on " is a positive function of the real number , quantified before all other data.
Out of scope, with the reason for each: Theorem 1.6 refers to a threshold "given in Section 3.5", which the paper does not contain, and to "overwhelming probability" with unspecified constants; Lemma 3.1 is proved only for and "large enough", with an unspecified threshold and an term quoted from the literature; Corollary 1.7 rests on Theorem 1.6; Theorem 5.1 has an unspecified constant and is explicitly not proved in the paper. A future mission can add these once precise statements are fixed.
Contributions that are welcome: proofs of the four milestone lemmas and of the two theorems; reusable lemmas on the attainment and monotonicity of the constants, on the Gram matrix and its inverse under , and on the duality inequality of Section 2.2. Statements that weaken the hypotheses (for instance to ) belong to a separate mission.
In a Walrasian pure exchange economy, agents trade a fixed stock of commodities, and a price vector is a general equilibrium when aggregate excess demand vanishes. Existence of equilibrium (Arrow–Debreu, 1954) says nothing about how prices reach it. The classical tâtonnement model of Samuelson (1947), , is not derived from any optimization principle, and Scarf (1960) gave economies in which it is not globally stable; see also Smale's survey Dynamics in General Equilibrium Theory (JSTOR 1817235) and the chaotic tâtonnement examples of Bala–Majumdar (JSTOR 25054664).
Lindgren (doi:10.3390/analytics1010003) proposes instead that the economy as a whole chooses a price path by dynamic programming: it minimizes a running cost combining a quadratic transaction cost for price changes and the agents' aggregate minimal expenditure. From the resulting Hamilton–Jacobi–Bellman (HJB) equation the paper derives an evolution equation for the price velocity and a condition under which the value function acts as a Lyapunov function: the equilibrium is approached when price adjustments are large enough. This mission formalizes those derivations.
There are commodities and agents. Prices are vectors , and the paper's implicit summation is written . Agent has an expenditure function (minimal cost of reaching a fixed utility level), and the market weighs agents with constants ; the aggregate expenditure is
The economy controls the price velocity and minimizes the cost functional (eq. (7))
whose value function is . The Hamiltonian (eq. (8)) is
the optimal policy (eq. (9)) is , and the HJB equation (eq. (10)) reads
Here always denotes the gradient with respect to prices. Shephard's lemma identifies the Hicksian demand of agent with . For the stability analysis the paper runs time forward, which reverses the sign of the HJB equation: .
If is and solves the time-reversed HJB equation, and the price path follows the optimal policy , then on any interval on which
the function is strictly decreasing; if moreover , it is strictly positive on .
The paper's contribution is the claim that price dynamics derived from an optimization principle are nonlinear and only conditionally stable, with stability requiring sufficiently fast price changes; the author connects this to volatility clustering in financial time series. The derivations in the paper are formal calculations with the regularity of left implicit. Formalizing them pins down exactly which smoothness assumptions each step needs (for instance, eq. (12) uses equality of mixed partial derivatives, hence a value function), and which facts are imported from outside (the HJB equation itself, Shephard's lemma). The resulting statements are reusable calculus facts about HJB equations with quadratic control cost.
Each step is a short computation on paper; the formal difficulty is in the calculus infrastructure: partial derivatives of functions on , symmetry of second derivatives, the chain rule along a curve, and turning a pointwise negative derivative into strict monotonicity on a closed interval. The HJB equation is taken as a hypothesis on rather than derived from the definition of the value function, because the paper asserts it without proof and a rigorous derivation would require viscosity-solution theory.
All declarations live in the namespace LindgrenPriceDynamics. Prices are functions Fin l → ℝ; partial derivatives are Fréchet derivatives applied to standard basis vectors, and time derivatives are one-variable derivatives in the time argument. The value function is a function J : ℝ → (Fin l → ℝ) → ℝ whose joint regularity is stated for the uncurried map on ℝ × (Fin l → ℝ). The standing assumption is kept; positivity of and is not needed by any stated conclusion and is not imposed. Prices are not restricted to the positive orthant. The goal's large-velocity hypothesis is satisfiable (e.g. , , with small on a bounded interval), so the goal is not vacuous.
This mission formalizes N. Monod, Groups of piecewise projective homeomorphisms, Proceedings of the National Academy of Sciences 110 (2013) 4524–4527, doi:10.1073/pnas.1218426110: the groups of piecewise projective homeomorphisms of the line are non-amenable and have no free subgroups whenever .
The paper opens with the Banach–Tarski paradox and von Neumann's notion of amenability: "Tarski readily proved that amenability is the only obstruction to paradoxical decompositions. However, the known paradoxes relied more prosaically on the existence of non-abelian free subgroups. Therefore, the main open problem in the subject remained for half a century to find non-amenable groups without free subgroups" (p. 1). That problem, the so-called von Neumann conjecture, was answered by Ol'shanskii around 1980, with Tarski monsters. Monod's groups give "straightforward torsion-free counter-examples", "so simple that many additional properties can be established" (p. 1).
Monod's groups are close relatives of Thompson's groups: Thurston's model identifies Thompson's group with piecewise maps of the line with rational breakpoints (p. 2). Whether is amenable is a notorious open problem, and whether is amenable is Monod's Problem 12 (p. 2).
The projective line is OnePoint ℝ, on which acts through by Möbius transformations (mob, using Mathlib's action on OnePoint). For a subring of (A : Subring ℝ; is ⊥, is ⊤), P A is , the set of fixed points of hyperbolic elements (trace of absolute value greater than ).
A homeomorphism of is piecewise in with breakpoints in (IsPiecewiseProjOn A E f) when, off some finite subset of , it agrees near every point with a Möbius transformation from . Monod's (Gpp) is the group generated by the homeomorphisms piecewise in , with breakpoints anywhere, and (Hpp) is its stabilizer of (fixInf). For a subring , (G A) is the subgroup of generated by its elements that are piecewise in with breakpoints in (IsPiecewiseProj A), and (H A) is its stabilizer of ; is H ⊥. GRat is the subgroup of generated by its elements piecewise in with breakpoints in , and HRat its stabilizer of : the rational-breakpoint variants of and (p. 2).
Amenability is Garrido.IsAmenable (a finitely additive left-invariant probability measure on all subsets), and "no non-abelian free subgroup" is Chou.NoFreeSubgroupOfRankTwo; both are published definitions, in the bundles Garrido_Amenability and Chou_Classes. Co-amenable subgroups (IsCoamenable), inner amenability (IsInnerAmenable) and pointwise stabilizers (fixSubgroup), all on p. 3, are defined in the bundle in the same style.
A relation is amenable for a measure (IsAmenableRel μ R, p. 2) when it has a left invariant mean in the sense of Connes–Feldman–Weiss: a positive, unital map from bounded measurable functions on to functions on , linear up to -null sets and invariant under the partial transformations of . volP1 is the Lebesgue measure class on .
The goal is Theorem 1, "The group is non-amenable if " (p. 1), introduced as "the main result of this article". The proof (p. 2) passes to a countable dense subring of , compares the orbits of and on (Proposition 9), and concludes from two facts about measured equivalence relations: the orbit relation of an amenable group's action is amenable, and, by a theorem of Carrière and Ghys, the orbit relation of on is not.
The milestones are, in the paper's order: consists exactly of the elements of piecewise in with breakpoints in ; ; preserves orientation, is left-orderable and torsion-free; Proposition 9; the countable dense subring; the orbit relation of a measurable action of an amenable group is amenable; the orbit relation of on is not amenable (Carrière–Ghys, external); Lemma 13 and Theorem 14 leading to Theorem 2 ( has no free subgroups); Corollary 3; Proposition 6 (bi-orderability); Lemma 16, Proposition 7 (co-amenability of pointwise stabilizers), Proposition 15 and Proposition 5 (inner amenability); and Thurston's identification of the rational-breakpoint variants of and with and .
The result. Theorem 1 and Theorem 2 together make , for instance , a torsion-free counterexample to the von Neumann conjecture, with finitely generated examples (Corollary 3). The groups are concrete enough to carry many further properties (Propositions 5–7).
Formalizing it. Nothing on amenability of groups of homeomorphisms of the line, or on measured equivalence relations, is in Mathlib. Amenability and Følner's theorem are on this platform from Garrido I, the Banach–Tarski paradox from Garrido II, Brin–Squier's theorem from its own mission, and Thompson's and (CannonFloydParry, CannonFloydParry_T) from the Cannon–Floyd–Parry missions.
The algebraic half, Theorem 2 and Propositions 5–9, follows Brin–Squier and elementary dynamics on the circle. The analytic half is the passage through measured equivalence relations in the proof of Theorem 1. The mission defines amenability of a relation as Connes–Feldman–Weiss do, by an invariant mean valued in , which is the form under which an amenable group's orbit relation is amenable without extra set-theoretic hypotheses. The step taken from the literature, that the orbit relation of on is not amenable for countable and dense, rests on Carrière–Ghys's theorem and on Zimmer's theory of amenable actions (Adams–Elliott–Giordano). The milestone is proved (Monod.not_isAmenableRel_mob) by an elementary route that needs neither: a ping-pong argument in that contradicts an invariant mean directly.
OnePoint ℝ and acts through Matrix.SpecialLinearGroup (Fin 2) A; since acts trivially the orbits are those of .OnePoint ℝ, each defined as the subgroup generated by the maps the paper describes; the milestones state that is exactly its set of such maps and that .volP1).The Hlawka inequality for Schatten -norms is a cousin of the triangle inequality: it relates the norms of three matrices to the norms of their pairwise sums and their total sum. The question is how large a comparison constant is needed to make this inequality hold.
This mission extends the best possible constant for complex diagonal matrices from to every real . The result is proved in Lean. The constant and its formula are unchanged from the foundation mission: the largest comparison constant required by the cyclic family of three diagonal matrices. For each exponent, it works for every triple of diagonal matrices, whatever their size, and no smaller constant does.
The mission started from a supplied pen-and-paper proof. Lowering the cutoff took more than replacing 256 with 90: several estimates in the original argument had to be strengthened. The research note proves the bound for real entries first, then transfers it to complex entries and shows that the constant cannot be improved. The goal theorem below gives the exact formula and statement.
This is the second step of the sharp diagonal Hlawka campaign, and it reuses the foundation's definitions and supporting results. The campaign invites further improvements below 90, keeping the same formula.
The broader question of optimal constants for Schatten norms appears in Audenaert and Kittaneh’s Problem 7. Extending the sharp diagonal constant to general matrices is a separate challenge.
79aa498bfcf7b22bd91d771fb32ec278e2d4704b. Source libraryA Markov chain Monte Carlo sampler is often assembled from simpler parts. A practitioner who has several proposal mechanisms for a Metropolis–Hastings sampler can combine them in two ways. Either each drives its own Metropolis–Hastings kernel and the sampler picks kernel with probability at each step, or the mixture is used as a single proposal inside one Metropolis–Hastings kernel. Both samplers leave the target invariant, so the choice is about efficiency.
Section 4 of Tierney (1998) settles the comparison: when both samplers use the maximal acceptance probability, the second never does worse in terms of asymptotic variances of sample-path averages. The statement that carries this is Proposition 5, an ordering of kernels in Peskun's off-diagonal order; the variance comparison then follows from Theorem 4 of the same paper, the general-state-space extension of Peskun (1973).
Timeline. Peskun (1973) introduced off-diagonal domination for finite state spaces and showed that the Metropolis–Hastings acceptance probability is maximal in that order. A version of Proposition 5 for discrete chains appears in the appendix of Tierney (1991) and in the rejoinder of Besag, Green, Higdon and Mengersen (1995). Tierney (1998) states and proves it for general state spaces, using the measure-theoretic description of Metropolis–Hastings kernels from §2 of the same paper.
Let be a measurable space and a probability measure on it, the target. A proposal kernel is a Markov kernel on . Given a measurable acceptance probability , the Metropolis–Hastings kernel is
where is the point mass at (mhKernel Q α).
Put and . With and (canonDensity), let
(canonR, canonRatio). The set is symmetric, and are mutually absolutely continuous on and mutually singular off it (Proposition 1 of the paper). The Metropolis–Hastings acceptance probability is
(alphaMH π Q), and the kernel with is the maximal Metropolis–Hastings kernel for (maxMHKernel π Q).
For kernels on , dominates off the diagonal, (OffDiagDominates π P₁ P₂), if for -almost every , for all . For a countable family of kernels and weights , the mixture is the kernel (mixKernel β K).
Let be a finite or countable family of proposal kernels and with . Let be the maximal Metropolis–Hastings kernel for and the maximal Metropolis–Hastings kernel for . Then
Both sides use maximal kernels: uses of the mixture proposal, each its own , and the same weights form both mixtures.
A companion item states the maximality of (§3, p. 7): every measurable acceptance probability whose kernel is reversible satisfies -a.e., so the maximal kernel dominates every reversible Metropolis–Hastings kernel with the same proposal.
The result. Proposition 5, combined with Theorem 4 of the paper (off-diagonal domination orders asymptotic variances of reversible kernels), shows that for every function with finite variance the asymptotic variance of under the mixture-proposal sampler is at most that under the mixture of samplers. Per-iteration cost can be higher for the mixture proposal, since then needs the densities of all components; Proposition 5 isolates the statistical side of that trade-off. The maximality companion states the fact behind the name "maximal kernel": is the largest acceptance probability that keeps a Metropolis–Hastings kernel reversible.
Formalizing it. The paper's proof is a computation of about six lines with Radon–Nikodym densities. A formal version must make explicit what the computation leaves implicit: that , defined from one dominating measure, has the same density form for every symmetric dominating measure; that the measure inequality on passes to the kernel-level statement with one null set for all ; and that the mixture proposal and the mixture of kernels are handled as countable sums of kernels. As of September 2026 neither Mathlib nor this platform has a machine-checked version of Proposition 5, of the maximality of , or of reversibility of the Metropolis–Hastings kernel on a general state space; only finite-state Metropolis chains have been formalized on the platform.
The obvious argument works pointwise with densities: write every kernel as a density against a common reference measure and compare of sums with sums of minima. On a general state space there is no common reference measure given in advance, and is only defined up to -null sets, through a Radon–Nikodym derivative with respect to , a measure that differs for and for each . The step that needs care is relating these different versions: the densities of the against a common symmetric , the density of , and the transpose densities , which are densities of only because is symmetric.
The second difficulty is the passage from measures to kernels. The inequality between measures on gives, for each fixed , the kernel inequality for -almost every , with a null set that depends on . The order requires one null set for all , and the diagonal must be removed, which needs the diagonal to be measurable.
The formalization is in Lean 4 with Mathlib, in the namespace TierneyMH.Mixture. The state space is a type E with a σ-algebra; π is a probability measure; proposal kernels are Markov kernels Kernel E E. Acceptance probabilities and densities take values in (ℝ≥0∞); a general is assumed measurable with . is π ⊗ₘ Q, its image under Prod.swap, detailed balance is Kernel.IsReversible. Mixtures are indexed by a countable type ("a sequence", which includes finite families), with weights in ℝ≥0 and HasSum β 1.
Added hypotheses, both labelled in the statements: singletons are measurable (implicit in the paper's and ), on the goal and the maximality companion; and, on the goal only, the σ-algebra of is countably generated. The second is an addition to the paper: it is what makes the exceptional null set in uniform over in the passage from the measure inequality to the kernels. It is not assumed in the measure-level milestones.
is one fixed version, built from Mathlib's rnDeriv exactly as in the proof of Proposition 1 (with , not an arbitrary dominating measure), and all statements are insensitive to the version. The ratio is set to 1 on the null subset of where is infinite, so that and hold everywhere, as Proposition 1 asks.
Trivializations ruled out: is the indicator of times , never an arbitrary acceptance function or a single shared by all components; compares , not (on the rejection masses differ and the comparison is false); and the conclusion is about the Metropolis–Hastings kernels themselves, not about the measure identity alone. All hypotheses are satisfiable, for instance on = Bool with uniform, two proposals and and weights .
Needed infrastructure, reusable for other Metropolis–Hastings results: Radon–Nikodym calculus for product measures and their transposes, countable sums of kernels, and a monotone-class argument over a countable generating family. The Metropolis–Hastings kernel, , and off-diagonal domination are defined identically in the companion missions I (detailed balance, Theorem 2) and II (Peskun ordering, Theorem 4) of this series. Proofs of milestones in any order, and proofs of the goal from the milestones, are welcome.
The discrete logarithm problem modulo a prime asks, given a prime , a generator of the multiplicative group modulo , and a nonzero residue , for the exponent with . Its presumed classical hardness underlies Diffie–Hellman key exchange, ElGamal encryption and the Digital Signature Algorithm. The best classical algorithm known when Shor wrote, Gordon's adaptation of the number field sieve, runs in time .
In §6 of Polynomial-Time Algorithms for Prime Factorization and Discrete Logarithms on a Quantum Computer (SIAM J. Comput. 26(5), 1997; doi:10.1137/S0097539795293172, arXiv:quant-ph/9508027), Shor gave a quantum algorithm that uses two modular exponentiations and two quantum Fourier transforms and outputs, with constant probability, a pair from which can be computed. The quantitative core of that analysis is a single number: the circuit produces a "good" output with probability at least . This mission formalizes that bound and the three estimates it is assembled from.
Let be a prime and a generator of , so that are all the nonzero residues. Fix the unknown with and put . Let be the power of with .
The Fourier matrix is the matrix with entries for (§4, eq. (4.1)). Rows index input basis vectors and columns output basis vectors.
The algorithm uses three registers: two holding numbers and one holding a nonzero residue modulo . It starts from the state
(preFourierState), applies to each of the first two registers (finalState), and measures all three registers. The probability of observing is the squared modulus of its amplitude (outcomeProb).
For integers and , the symmetric residue is the residue of modulo in (symmRes). Put
An observed state is good (IsGood) when
Goodness depends only on .
The constant is the one the page carries forward. The goal fixes no threshold on : it is stated for every prime that admits a power of two strictly between and .
The result. The bound is what turns the circuit into an algorithm. Repeating the circuit times in expectation yields a good output, and from a good pair one reads off an equation that determines modulo divisors of (§6, eqs. (6.18)–(6.20)). Together with the quantum Fourier transform circuit and reversible modular exponentiation, this places the discrete logarithm modulo a prime in quantum polynomial time. Every later analysis of quantum attacks on discrete-logarithm cryptography starts from this success probability or a sharpened version of it.
Formalizing it. The result has been proved since 1994–1997 and is textbook material; it is not open. As far as is known, no machine-checked proof of Shor's discrete-logarithm analysis exists. The paper's proof of eq. (6.17) replaces a sum by an integral with an error term whose constant is not given, yet states for every prime. A formal proof must therefore either control that error explicitly or find another argument, and so settles a point the paper leaves informal. Numerically, the smallest value of over good states is about for all primes , so the unconditional claim is not in doubt for small . The page also contains two small slips, recorded under Formalization scope; a complete development pins down exactly what is true.
The exponential sum (6.4) runs over pairs satisfying a congruence modulo , while the phases are taken modulo . The two moduli are unrelated: is a power of two and is arbitrary. Eliminating through the congruence introduces a floor function , and the resulting phase is not linear in . The obvious estimate treats the sum as a geometric series in and bounds it by its first-order phase; this fails because the floor term perturbs every phase by an amount of size up to . Condition (6.11) only keeps this perturbation within of the main phase; it does not remove it. The per-state bound must survive this perturbation uniformly in , and , including small primes where the paper's integral approximation gives no explicit control.
The count of good pairs needs a separate argument about how often a multiple lies within of a multiple of when is large.
Fin q × Fin q × (ZMod p)ˣ → ℂ. The first two registers range over ; the third over the units modulo .finalState is defined this way from (6.1) and . It is not typed in as the closed form (6.3) or (6.4). A formalization that defined the final state by (6.4) directly would make milestone 1 trivial, and is ruled out.Fact p.Prime). The generator is encoded as orderOf g = p - 1. is a parameter, with . is given by q = 2 ^ l together with . No large- threshold is added anywhere.x⁻¹ ^ b in the unit group. is computed in and inside and the congruences, and as natural-number subtraction only where makes it exact. is real.Needed infrastructure: finite exponential sums and their modulus, the symmetric residue and its basic properties, and counting multiples in residue classes of . The exponential-sum estimates of milestones 1 and 2 are reusable in the order-finding analysis of §5 of the same paper. Proofs of any milestone, of the normalization , and of auxiliary lemmas about symmRes are welcome.
Many problems in statistics, signal processing and machine learning minimize a sum of a smooth loss and a nonsmooth regularizer: least squares with an or penalty, and constrained problems in which the regularizer is the indicator of a nonconvex set. The proximal gradient method (also called forward–backward splitting) is the standard first-order algorithm for such problems. Each step takes a gradient step on the smooth part and then applies the proximal mapping of the nonsmooth part, which for many nonconvex regularizers (hard thresholding, projection onto sparse vectors) has a closed form.
For a smooth part whose gradient is -Lipschitz, the classical analysis allows any constant step size , and every cluster point of the iterates is stationary; Li and Pong cite Bredies and Lorenz (Minimization of non-convex, non-smooth functionals by iterative thresholding, preprint, 2009) for this. Attouch, Bolte and Svaiter (Math. Program., 2013) added convergence of the whole sequence when has the Kurdyka–Łojasiewicz property. When is nonconvex, however, is governed by the most negative curvature of as much as by the most positive one, and the admissible step sizes can be much smaller than the convex part of alone would require.
Li and Pong (SIAM J. Optim., 2015; preprint arXiv:1407.0753v6) show that the concave part of imposes no restriction on the step size: it suffices to bound the curvature of after it has been offset by a convex function. This mission formalizes that result, Theorem 4 of their paper. It is the fourth mission of a series on the paper; the first three treat its results on the alternating direction method of multipliers.
Work in with the Euclidean inner product and norm . The problem is
under the paper's standing assumptions: is twice continuously differentiable with a bounded Hessian ; is proper (never , finite somewhere) and closed (lower semicontinuous); and for every and the proximal problem has a minimizer. Neither nor is assumed convex.
A vector is a regular subgradient of at (with ) if for all near , for every . The limiting subdifferential collects the limits of regular subgradients at points with . A point is stationary if
Given a step size and an arbitrary starting point , the proximal gradient method generates by
Any minimizer may be selected. A cluster point of is the limit of a subsequence .
The step-size condition involves a convex function and a constant with
where is the Loewner order on symmetric linear maps.
Suppose is twice continuously differentiable and convex, , (44) holds, and is generated by (43) with . Then
and every cluster point of , if one exists, satisfies .
The goal does not assert that a cluster point exists, nor that the whole sequence converges; both are false without further assumptions.
In the order of the paper's proof:
The result. For a difference of convex functions with being -Lipschitz, (44) holds with and , so the step size may be taken in whatever the curvature of . For an indefinite quadratic the admissible range becomes instead of , and for a concave quadratic every positive step size is admissible. Because the method is a descent method under this rule, its iterates stay in a sublevel set of , so the sequence is bounded whenever is coercive. The same estimates feed the whole-sequence convergence argument for Kurdyka–Łojasiewicz functions.
Formalizing it. The theorem is proved in the paper; to the best of current knowledge it has no machine-checked proof. Formalizing it requires the limiting subdifferential of an extended-real-valued function, its closedness property (3), and a Fermat rule for a smooth-plus-nonsmooth sum, none of which is in Mathlib. These are reusable for any nonconvex first-order method analysed through cluster points.
The descent part rests on (45), a descent inequality for whose Lipschitz constant is read off from a two-sided Hessian bound; the familiar descent lemma is stated for alone and does not apply, since may have a much larger Lipschitz constant than .
The stationarity part is where the naive argument fails. Passing to the limit in (47) needs not only but also , because the limiting subdifferential is closed only under -attentive convergence. Lower semicontinuity gives one inequality; the other must come from the minimizing property (43) compared against . The objective may be at , so summability of the steps has to be extracted without assuming a finite starting value.
The space is EuclideanSpace ℝ (Fin n). and are real-valued; takes values in EReal, and every objective value is compared in EReal, never through EReal.toReal. The Hessian is the derivative of the gradient map, a continuous linear self-map; the Loewner order is Mathlib's partial order A ≤ B ↔ (B - A).IsPositive, and both sides of (44) are kept. The regular subgradient is encoded in its -neighbourhood form, and the limiting subdifferential requires all three convergences , , . Stationarity is . The update (43) is a relation on sequences: minimizes the bracket over all of , with no uniqueness and a free starting point. A cluster point is the limit of for a strictly increasing .
Trivializing formalizations are ruled out: (44) is not replaced by " is -Lipschitz", which is the classical special case ; , boundedness of the sequence and existence of a cluster point are not assumed; and a limiting subdifferential without is not used, since that would make stationarity a weaker statement.
Contributions welcome: the closedness (3) and the Fermat rule behind (47) for the limiting subdifferential, a descent lemma from a two-sided Hessian bound, and the telescoping and limit arguments of the proof.
The alternating direction method of multipliers (ADMM) splits a problem of the form into a sequence of simpler subproblems, one in which the nonsmooth term enters only through its proximal map and one in which only the smooth term appears. For convex problems its convergence theory is classical. In signal processing and statistics, however, the method is routinely run on nonconvex models, such as - or -regularized least squares, where is nonconvex and possibly discontinuous and convex theory does not apply.
Li and Pong (arXiv:1407.0753, SIAM J. Optim. 25(4), 2015) gave a convergence analysis of a proximal variant of the ADMM for this nonconvex setting. Their Theorem 1 shows that every cluster point of the iterates is a stationary point. That statement is only informative if cluster points exist. Theorem 2, the subject of this mission, gives conditions on , and under which the whole sequence of iterates is bounded, so that cluster points exist and Theorem 1 applies.
Let . The data are:
The augmented Lagrangian is
and the Bregman distance of is . A sequence is generated by the proximal ADMM if, from arbitrary ,
For a linear self-map , write , and write , for the semidefinite and definite order of symmetric maps. Assumption 1 asks for with (so is surjective), bounds , maps with , with , a bound , and with
Suppose Assumption 1 holds and, with the same and , there is with
Suppose that either (i) is invertible and , or (ii) and . Then
The milestones are the numbered displays of the paper's proof:
The result. Theorem 2 supplies the existence of cluster points that Theorem 1 assumes. The two together give an unconditional statement: under Assumption 1, (29) and either coercivity condition, the proximal ADMM has a cluster point and every one of them is stationary. The hypotheses cover the models that motivate the paper. Least squares with a coercive nonconvex regularizer falls under case (i) with , and a strongly convex quadratic with a regularizer that is bounded below and a general surjective falls under case (ii) (Examples 4–6 of the paper). Boundedness is also a standing hypothesis of the paper's Theorem 3, the Kurdyka–Łojasiewicz argument for convergence of the whole sequence.
Formalizing it. The result has been proved since 2015. As far as a search of the platform shows, neither it nor the underlying Lyapunov-type estimates for the ADMM has been machine-checked. This mission formalizes the known proof. The estimates (20), (30) and (31) are shared with the stationarity analysis of the same algorithm, so they serve any later formal work on nonconvex ADMM variants.
The obvious approach is to bound the iterates by the monotone quantity of Eq. (30). That quantity involves , which contains and is not bounded below a priori, so its decrease alone does not bound anything. The dual term has to be absorbed. It is controlled through and the last primal step, and the part involving is then paid for out of itself. Condition (29) exists to make exactly this trade possible, which is why it couples to the of Assumption 1. The two cases then extract boundedness in opposite orders: (i) goes from through to using invertibility of , and (ii) goes from through to . In case (i) the lower bound on that the argument needs is not assumed and must itself be derived from coercivity and lower semicontinuity.
EuclideanSpace ℝ (Fin n) and EuclideanSpace ℝ (Fin m), and is a continuous linear map with Mathlib's adjoint. , and every inequality containing them live in EReal, stated additively so that no extended-real subtraction occurs.Ruling out trivial versions. A formalization that bounds only , fixes or to an example's values, lets (29) use a fresh , adds a lower bound on in case (i), or assumes minimizers that make the sequence constant proves a different, weaker theorem, and is not the target.
Definitions needed. Proper and closed extended-valued functions, the Hessian as fderiv of gradient, the augmented Lagrangian, the Bregman distance, the proximal-ADMM relation and Assumption 1 are all provided. They mirror the definitions of the companion mission on cluster points of the same algorithm. A solver will need standard facts beyond them: first-order optimality for a differentiable function, the mean-value bound from the Hessian sandwich, and strong convexity of the -subproblem. Proofs of individual milestones are welcome independently.
Approximate policy iteration and policy-gradient methods stop when they can no longer find a direction of improvement. Kakade and Langford (ICML 2002) asked what such a stopping point guarantees. Their algorithm, conservative policy iteration, halts at a policy for which no policy can improve much on as measured under a restart distribution ; the quantity that is small is the optimal policy advantage . Theorem 6.2 of the paper translates this local condition into a global statement: the performance of is close to optimal, with a loss controlled by how well covers the states an optimal policy visits.
The bound is the origin of the distribution mismatch coefficient , which reappears in the analysis of approximate dynamic programming (concentrability coefficients, Munos 2003), of conservative and trust-region methods, and of the convergence of policy gradient methods (Agarwal, Kakade, Lee, Mahajan 2021), where it governs the rate. The performance difference lemma (Lemma 6.1) used in its proof has become a standard tool of reinforcement learning theory.
A finite Markov decision process has a finite nonempty state set , a finite nonempty action set , transition probabilities (for each a probability distribution over ), a reward function with , and a discount factor . A stochastic policy is, for each state , a probability distribution over actions. A state distribution is a probability vector on .
The normalized value function is , where , and . The state–action value is and the advantage is . The discounted future state distribution from is
and the performance of from is .
The policy advantage of with respect to and is : the expected advantage of over on the states itself visits. Its maximum over all stochastic policies is (Definition 4.3). An optimal policy satisfies for every policy and every state . For nonnegative on , (p. 5).
If and is optimal, then for every state distribution
The goal states both inequalities and the outer bound. The evaluation distribution is arbitrary and unrelated to the restart distribution ; taking , the start distribution, gives Corollary 4.5 (p. 5).
For any policies , and any starting distribution ,
The states are weighted by the future state distribution of the new policy , the advantage is that of the old policy .
Theorem 6.2 is the quality guarantee for conservative policy iteration: combined with the paper's Theorem 4.4 (the algorithm stops with after polynomially many calls), it bounds the suboptimality of the returned policy for any target distribution, independently of the size of the state space except through the mismatch coefficient. It also explains the role of the restart distribution: a more uniform makes small. Lemma 6.1 is used throughout later theory, from trust-region policy optimization to the global convergence of policy gradient methods.
Both results are proved in the paper, with short arguments. The contribution of this mission is a machine-checked version of the infinite-horizon discounted statement in the paper's normalization, with the ratios handled exactly, including states where a denominator vanishes. Neither the discounted performance difference lemma for stochastic policies nor the distribution mismatch bound is known to be formalized in Mathlib; a finite-horizon performance difference identity has been formalized separately and is a different statement.
The mathematics is short; the difficulty is in the infinite-horizon bookkeeping. The value function and are infinite series, and Lemma 6.1 relates the series of two different policies: its natural one-line argument uses the Bellman equation for , which is not the definition here, together with interchanges of infinite sums over time with finite sums over states and actions, each of which needs summability. Theorem 6.2 then needs two facts that are not stated as results in the paper: that equals (the supremum over policies is attained by a greedy policy, and ), and that . Reading the ratio with real division would give a false statement when a denominator is zero; the statement avoids this.
States and actions are finite nonempty types; policies and kernels are real-valued functions π s a (the paper's ) and P s a s' (the paper's ), with their distribution properties as explicit hypotheses. The published definitions IsTransitionKernel, IsPolicy, InducedTransition, OccupationDist, InducedReward and PolicyValue from the Foundations of Machine Learning series are reused; is times PolicyValue, the defining series. is the supremum of the policy advantages over stochastic policies, which is the paper's maximum. Optimality of is relative to stationary stochastic policies, the paper's policy class; the existence of an optimal policy (the paper's "well known result", p. 2) is not part of this mission.
Every hypothesis is explicit: rewards in with , , a kernel, and stochastic policies, and state distributions. Each bound is stated multiplicatively: "" is " for every with for all ". When some no such exists and the bound is empty, which matches ; no full-support assumption is made on or . The hypothesis is on the supremum itself, not on the closed form , which is a step of the proof; a formalization that assumed the closed form, or that divided by in real arithmetic, would not be this theorem. The proof of the theorem uses only that is a policy; optimality is kept as a hypothesis because the paper states it.
The proof on p. 7 twice writes ; the inequality it uses, and the one stated on p. 5, is . This slip is in the proof, not in the statement. Pages are PDF pages; the paper has no printed page numbers.
Useful reusable infrastructure: summability and Bellman equations for the normalized discounted value, as a probability distribution with , and attainment of by a greedy policy. Contributions of any of these as separate lemmas are welcome.
Johnson's 1954 paper in Naval Research Logistics Quarterly is the starting point of machine scheduling theory. Its first section solves the two-machine flow shop: items must pass through machine 1 and then machine 2, and an explicit ordering rule minimizes the total elapsed time. Its second section treats three machines. There the problem "loses some of the nice structure of the two-stage case" (p. 65), and the general three-machine problem was later shown to be strongly NP-hard (Garey, Johnson and Sethi, 1976). Johnson nevertheless identifies a restricted case, in which the middle machine is dominated by the first (or the last), where the two-machine rule still gives an optimal schedule. That case, and the structural facts behind it, are the content of this mission.
The three-machine results are still the reference point for polynomially solvable flow shops and for lower bounds in branch-and-bound methods for the general problem.
Timeline.
There are items and three machines. Item needs processing time on machine 1, on machine 2 and on machine 3, in that order. Each machine handles at most one item at a time, and processing is not interrupted.
A schedule assigns each item start times . It is feasible when all start times are at least on machine 1, the processing intervals of distinct items on the same machine do not overlap, and , . The three machines may process the items in different orders. The total elapsed time (makespan) is .
An ordering lists the items, being the item in position . Its as-soon-as-possible schedule processes the items in the order on every machine and starts each item on each machine as early as the rules allow. For an ordering, with positions , Johnson defines
the sums running over the items in the first (resp. ) positions.
Johnson's three-stage rule says that item definitely precedes item when
and calls them indifferent under equality. An ordering is consistent with (IV) when no item placed later is definitely preferred to an item placed earlier.
If every is at least every , then an ordering consistent with (IV) exists, and for every such ordering the as-soon-as-possible schedule of is feasible and satisfies
the "maximum walk" of p. 68. 3. Special case (p. 67). If then , so the makespan is . 4. (III) (IV) (p. 67). Interchanging the items in positions changes and only at , and the interchange is strictly worse for the diagonal terms exactly when (IV) holds. 5. Lemma 4 (p. 67). Relation (IV) is transitive, except when the middle item is indifferent to both others. 6. Mirror case (p. 68). The conclusion of Theorem 2 also holds when every is at least every .
The result. Theorem 2 gives an exact method for a class of three-machine flow shops, in a problem that is strongly NP-hard in general. Lemma 3 says that, for three machines, permutation schedules are dominant; Johnson's example on p. 65 shows this fails for four machines. The closed form of milestone 2 expresses the makespan of any ordering as a longest path in a grid, the device behind most later flow-shop lower bounds.
Formalizing it. All results are proved on paper, some tersely: Lemma 3's proof is two lines and cites the wrong lemma, Lemma 4 is proved by reference to Lemma 2, and the mirror case is asserted without proof. A search of Mathlib and of the platform catalog found no machine-checked proof of any of them. The mission produces a checked account of the three-machine flow shop, including the comparison against all feasible schedules rather than only permutation schedules, and pins down the exact form of the hypotheses (see below).
The interchange argument of the two-machine case does not transfer directly. For a general ordering the makespan involves , and interchanging adjacent items changes terms that depend on everything placed earlier; the page notes that "the decision is not independent of what precedes the interchanged elements". The hypothesis is what makes nondecreasing along the ordering, collapsing the double maximum to the diagonal. A second obstacle is that (IV) is not a total preorder: ties break transitivity, so passing from "no adjacent pair can be improved" to "optimal" needs the all-pairs consistency and the tie exception of Lemma 4. Finally, Lemma 3 is a statement about arbitrary start-time schedules, so the reduction to orderings must handle machines whose orders differ.
Items are Fin n; processing times are real-valued functions A B C : Fin n → ℝ, assumed positive in each theorem that is about schedules (the paper's standing assumption, p. 61). A schedule is three start-time functions; feasibility is spelled out as above with non-overlap written as a disjunction of inequalities. The makespan is the maximum of the machine-3 completion times together with , so the empty instance has makespan . An ordering is an Equiv.Perm (Fin n) with σ k the item in position k; positions are 0-based, so the Lean K u, H v are the paper's , . Statements with maxima over positions assume .
Hypotheses made explicit or corrected:
Optimality in the goal is against every feasible schedule. A formalization that compares only orderings with each other, or that defines the objective as the closed form , would drop Lemma 3's content and is ruled out: the makespan is the latest completion time of a start-time schedule. The existence clause keeps the optimality clause from being vacuous.
A complete development needs finite sums over initial segments of Fin n, Finset.sup', and permutation manipulations (adjacent transpositions, bubble-sort arguments). The feasibility model and the closed form are reusable for other flow-shop results; contributions of general lemmas on adjacent interchanges of permutations are welcome.