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.
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 Lagrange spectrum describes the asymptotic quality of rational approximation to irrational real numbers. The Markov spectrum is defined through minima of indefinite binary quadratic forms. Freiman determined the exact starting point of the maximal half-line contained in each spectrum.
This mission aims to formalize his theorem that this half-line is , where
The formalization must establish membership of every real number at least , including the endpoint, and show that no half-line starting below is contained in either spectrum.
The sources are Freiman's Russian monograph and an accompanying detailed reconstruction of its proof, with an English translation, exact computational certificates, and verification scripts. The project follows Freiman's continued fraction construction, incorporating the corrections and supplementary arguments established in the report.
The intended result is a complete Lean 4 proof. Its scope includes the equivalence of the classical and continued fraction definitions of the spectra, the infinite constructions that realize spectral values, and the exact finite calculations used in the argument.
Start with README.md and PROOF_GUIDE.md in the package. The files formalization/MISSION.md and formalization/MILESTONES.md describe the scope and proposed stages of the formalization. For reproducing the report, use the PDF and sources contained in the ZIP.
References to the report in the individual source fields use its printed page numbers.
A matching cut is a vertex bipartition whose crossing edges form a matching. The property was introduced under the name decomposability and has links to graph algorithms, stable cutsets in line graphs, and several graph-labeling problems. An Open Problem Garden question asked whether sufficiently large girth forces a matching cut once average degree is bounded.
Feghali, Lucke, Paulusma, and Ries answered that question negatively. Their conference paper appeared at ISAAC 2023, and the version of record was published in Algorithmica in 2025. The paper proves NP-completeness for bipartite graphs of arbitrarily prescribed girth and bounded maximum degree. A central input, Lemma 5, is a stronger structural existence statement: for every girth threshold there is an immune -regular bipartite graph of at least that girth, and it has a perfect matching.
This is therefore a ResearchPaper mission, not a new open-problem mission. Its goal is to formalize the published theorem and its graph-theoretic consequence. Repository candidate constructions and finite arithmetic audits remain separate and are not credited as solving the problem.
For a finite simple graph and a vertex set , the associated cut consists of all edges with one endpoint in and one in . The cut is nontrivial when both shores are nonempty. It is a matching cut when each vertex is incident with at most one crossing edge. A graph is called immune in the cited paper when it has no matching cut.
The girth is the length of a shortest simple cycle; forests have infinite girth. A graph is -regular when every vertex has exactly fourteen neighbors. Bipartiteness is witnessed by a partition into two independent sides. A perfect matching pairs every vertex with one adjacent partner.
The original OPG wording has a literal one-vertex boundary ambiguity: with nonempty shores required, has no matching cut, average degree zero, and infinite girth. The research-paper target avoids that vacuity by constructing connected graphs with at least two vertices, exact degree fourteen, and arbitrarily large finite girth.
The main theorem follows the paper's structural lemma:
The graph may depend on . The existence quantifier does not request an efficient algorithm or a numerical order bound.
A supporting theorem removes the perfect-matching and bipartite fields and records the direct substantive counterexample family:
Thus choosing refutes the intended universal assertion that some girth threshold works for every graph of average degree below .
The theorem shows that large girth and bounded degree do not force matching cuts. The examples are highly nontrivial: they are connected, regular, bipartite, and can have arbitrarily large girth. This separates local tree-like structure from the global expansion that prevents a matching cut.
Within the paper, the immune graphs serve as gadgets for hardness reductions. The journal theorem states that, for every , Matching Cut is NP-complete even for bipartite graphs of girth at least and maximum degree at most . Formalizing Lemma 5 supplies the graph-theoretic core needed to reconstruct that result without forcing this mission to formalize an entire complexity-theory reduction in its first stage.
Large girth alone makes bounded neighborhoods look like trees, and trees have many matching cuts. Immunity must therefore come from global expansion rather than short local cycles. The paper obtains the required family from Lubotzky–Phillips–Sarnak Ramanujan graphs and combines spectral and isoperimetric bounds to show that every nontrivial cut has too many crossing incidences to be a matching.
A formal proof must bridge several exact interfaces: existence of suitable primes, the finite Cayley-graph construction, bipartiteness and regularity, the girth lower bound, the spectral-to-isoperimetric inequality, and Hall's theorem for the perfect matching. None of these can be replaced by a finite sample or an asymptotic slogan.
Graphs are finite and simple. Connectedness is nonempty mutual graph reachability. A simple cycle is a cyclic list of at least three distinct vertices; girth at least means every such cycle has length at least , so forests satisfy every threshold. A matching cut requires both shores nonempty and is encoded by the condition that every vertex has at most one crossing neighbor. A perfect matching is represented by an adjacent involution.
The main theorem explicitly requires at least two vertices, although exact 14-regularity already forces nontrivial order; the redundant bound documents exclusion of the ambiguity. The mission does not claim that the frozen OPG contract was well-posed at order one. It formalizes the paper's substantive counterexample family and the consequence for the intended question.
Candidate files in the associated repository explore alternative bounded-degree constructions and integer counts. They are candidate_only and are not proof dependencies. Contributions should follow the published Lemma 5 and its cited inputs, or provide a separately sourced proof of the same declaration. The later maximum-degree-60 NP-completeness theorem is welcome as a future extension after the finite complexity framework is fixed.
[VM-STATUS-20260908-R05-PROVED]
Status update (2026-09-08): The root theorem
OPG500Counterexample.eight_vertex_counterexampleis now Proved by an accepted Prove2Me submission. All six milestones are proved and the root has zero open leaves. The accepted proof has also been independently rebuilt with Lean 4.33.1 / Mathlib0df444a360eaa60ab8c11dca51a86af692955474. The historical text below describes the mission as it stood before formal closure.
Peripheral cycles occupy a distinguished place in structural graph theory. A cycle is peripheral when it is induced and does not separate the graph after its vertices are removed. Tutte proved in 1963 that the peripheral cycles of a finite 3-connected graph generate its binary cycle space. This theorem links a local, visibly embedded kind of cycle to the global algebraic structure of all cycles.
Weighted geodesic cycles provide a different generating family. Georgakopoulos and Sprüssel proved in 2009 that, for every finite graph with positive edge lengths, every cycle is a binary sum of weighted geodesic cycles whose lengths do not exceed the length of the original cycle. In the same paper they posed Problem 3: can the edges of every finite 3-connected graph be assigned positive lengths so that every weighted geodesic cycle is peripheral? A positive answer would recover Tutte's generation theorem through metric structure.
The present target tests the opposite possibility on one explicitly specified graph with eight vertices. A candidate argument and finite certificates are available in the frozen OPG-500 research repository, but those artifacts are explicitly marked candidate_only: they are neither a published counterexample nor a machine-checked resolution. The purpose of the formal target is to determine whether the proposed universal obstruction survives complete definition, proof, and statement-faithfulness checks.
Let be a finite simple graph. A positive edge-length assignment is a function
such that for every edge . The length of a finite path or cycle is the sum of the lengths of its edges.
A simple cycle is -geodesic when, for every pair of vertices on , at least one of the two – arcs of has length equal to the shortest-path distance between and in . Equivalently, there is no – path in whose length is strictly smaller than both – arcs of . The definition concerns vertices of the cycle and permits ties between shortest paths.
A simple cycle is peripheral when it is induced and deleting all of its vertices leaves a connected graph or the empty graph. This is vertex deletion, not edge deletion.
Fix the graph on vertices . The vertices induce . For each , set and join to exactly the three core vertices other than . The four vertices are pairwise nonadjacent. Thus the frozen edge set is
The labels and edge set are part of the statement and are not interchangeable with earlier candidate labelings without an explicit isomorphism.
Formalize the following statement for the fixed graph :
The existential cycle may depend on . The universal quantifier includes all strictly positive real assignments, including assignments with tied shortest paths. This is the stable target; finite samples and rational specializations are subordinate checks rather than replacements for it.
The development should also formalize the finite weighted geodesic-cycle generation theorem of Georgakopoulos and Sprüssel, the exact 3-connectivity and peripheral-cycle classification of , the required shortest-path and tight-subgraph statements, the finite cycle-space rank statements, and the finite minimum/descent principle used to select a cycle outside a closed binary span. These targets should remain separate declarations so that their assumptions and reuse boundaries are visible.
A proof of the main target would give a negative answer to the finite problem by exhibiting a 3-connected graph for which no positive edge weighting can make all geodesic cycles peripheral. It would not contradict Tutte's theorem: peripheral cycles may still generate the cycle space even though they cannot be made to contain every geodesic cycle for any weighting. The distinction between these two generation mechanisms is part of the mathematical content.
A formal development would add more than a checked final sentence. It would provide reusable definitions for positively weighted finite graphs and vertex-geodesic cycles, a precise treatment of the two arcs between cycle vertices, explicit deletion semantics for peripheral cycles, and finite cycle-space infrastructure. It would also separate purely finite graph facts from statements quantified over arbitrary real weights. The candidate repository currently supplies finite enumeration and abstract Lean fragments, but no existing artifact checks this full dependency chain.
Until the complete main theorem is verified, the eight-vertex graph remains a candidate obstruction and the original problem remains unresolved by this development.
The central difficulty is the universal quantification over real edge lengths. Testing many integer or rational vectors cannot cover it. Shortest paths need not be unique, so an argument that silently perturbs the weights or assumes unique geodesics can change which cycles are geodesic. Every strict and weak inequality must therefore agree with the source definition, including tie cases.
The graph is small but the semantic boundary is not. A formal cycle representation must expose the two cycle arcs for every vertex pair without admitting malformed or repeated-vertex objects. The peripheral predicate must combine inducedness with connectivity after vertex deletion and must classify all cycles, not only a selected family of triangles. Finally, finite cycle-space computations and rank inequalities must be connected to actual paths and weighted geodesicity; a propositional or enumerative certificate alone does not establish that bridge.
The Lean development will use Fin 8 for the vertices of and a SimpleGraph representation for adjacency. Weights will be functions on the edge subtype, so values on nonedges cannot affect the theorem. All weights are real and strictly positive. Paths and cycles are finite and simple; arbitrary walks do not count as target witnesses. Geodesicity is vertex-based and includes tied shortest paths. Peripheral cycles use inducedness and vertex deletion, with a connected-or-empty remainder.
The main theorem must retain the quantifier order “for every weighting, there exists a cycle.” It may not be weakened to rational weights, finitely many tested assignments, nonnegative weights, one selected weighting, edge-geodesicity, or the assertion that only four named core triangles fail to be peripheral. Definitions must be sorry-free, and nontrivial mathematical claims must be theorem declarations with separately checked proofs.
Reusable contributions include finite weighted-path length, shortest-path attainment in finite positive graphs, the equivalence of the two geodesic formulations, cycle-arc APIs, vertex-deletion connectivity, binary edge-vector encodings, and finite descent outside a closed span. Graph-specific finite certificates are welcome only when their checker is represented in Lean or their conclusions are otherwise proved in the kernel.
a41fe59b4535851ea55f6e868e938b9aaf81e924. https://github.com/vibemathing/problem-opg-500-geodesic-cycles/tree/a41fe59b4535851ea55f6e868e938b9aaf81e924A modular form has a complex L-function whose critical values carry arithmetic information. To compare those values in p-adic families, their transcendental period factors must first be removed. The remaining algebraic numbers can then be embedded into a p-adic field. The result sought here is a single bounded measure encoding the critical values of all twists by characters of p-power conductor. This is the existence and interpolation theorem underlying the cyclotomic p-adic L-function (one of the most fundamental objects of Iwasawa theory).
The reference is the famous paper of Mazur, Tate and Teitelbaum, Chapter I, especially §§10–14 (MTT); but for simplicity we are treating only the ordinary case here (not the more general finite-slope case), and not attacking the results later in MTT (exceptional-zero conjectures, etc).
Fix a prime , a positive integer , and a weight . Let be a normalized cuspidal Hecke eigenform of weight on with nebentypus and Fourier coefficients (necessarily algebraic). Fix embeddings and . No condition is imposed. The character is extended by zero on nonunits modulo .
The form is ordinary when . The ordinary root is the root of
with . This convention also covers the case: if , then and the unit root is (MTT I.§12).
A measure means a continuous -linear functional on the continuous functions . It is a bounded p-adic measure, rather than a positive real-valued measure. The Lean representation is Mathlib's AbstractMeasure on (PadicInt p)ˣ.
The two periods and normalize the signed modular integrals. Write
and use for sign . A period system specifies nonzero periods, algebraic normalized values for , and finite generation over of the lattice generated by these values. Period rationality and finite generation are separate mathematical obligations, combining Manin–Shimura rationality with the module-of-values construction in MTT I.§2; see also the explicit treatment of general eigenforms in Williams, §11.7.
The goal is to construct an ordinary root, a period system, and a measure with the following interpolation property. Let be a primitive Dirichlet character of conductor , where , and let . Put . With the positive-exponential Gauss sum , define the algebraic number by
The required identity is
where all algebraic character values in the following expression are transported by :
This is the scalar period-normalized form of MTT I.§14. At both character values at vanish, leaving . At the primitive character is the character of modulus one, and both Euler factors remain. The latter case is included explicitly.
Seven milestones isolate period rationality and its finite lattice; existence and uniqueness of the ordinary root; the distribution relation for polynomial disk moments; uniform boundedness of constant disk masses; unique extension to a measure with every critical polynomial moment; the complex Birch–Mellin identity; and the deduction of interpolation from the two signed measures. Their source locations are recorded individually. The period milestone combines two standard inputs; the boundedness and extension milestones specialize the MTT construction to slope zero.
The result supplies the analytic input for studying p-adic special values and their variation. It also supplies reusable infrastructure for normalized modular integrals, rational period systems, finite-order twists, and bounded measures on p-adic units. The classical existence theorem is known. The work proposed here is to prove the stated Lean theorems and connect the existing Mathlib analytic and algebraic infrastructure. Local compilation establishes that the declarations are well-typed; the mission statements remain unproved targets.
Listing algebraic critical values does not establish that one bounded measure interpolates them. Values on nested residue disks must satisfy compatibility, and ordinary boundedness must control the extension to continuous functions. Polynomial moments of positive degree must agree with that same extension. The unramified character requires its own Euler-factor calculation; simply applying the ramified formula at conductor one loses factors. On the complex side, rationality requires genuine periods of the modular form, not arbitrary chosen scaling constants. These are the obligations represented by the milestones.
The cusp form is Mathlib's analytic CuspForm, with Fourier coefficients tied to its width-one q-expansion. The nebentypus transformation law and every prime Hecke eigenvalue equation are written explicitly. The prime Hecke operator includes both its translated sum and its second term; when the prime divides the level, the second term vanishes. The complex twist is the finite-translate expression for , and its critical L-value is defined by the actual Mellin integral. Neither an arbitrary L-value table nor the desired measure is an input assumption.
The embeddings share the abstract algebraic closure of ; there is no asserted continuous map from to . The algebraic bridge in each interpolation identity is existential and constrained by a complex equality. Test functions are existential continuous maps constrained pointwise to equal the specified character or disk function; this makes their continuity part of the conclusion instead of an unproved definition. All primes, including , are allowed. Natural-number subtractions occur only in theorem contexts with and .
The signed projections use a factor of . Their normalized measures are added, and the period sign is . These conventions fix the powers, sign, Gauss sum, and periods in the displayed interpolation formula. Periods are not asserted to be canonical integral periods; rescaling by algebraic constants changes the normalization. Exceptional-zero derivative formulas, positive-slope distributions, tame-conductor twists, and Iwasawa main conjectures are outside this mission.
Adam McKenna closed this mission on 13 September 2026 following Unit distances in convex polygons, by Liam Kruer, Jensen Kohlmeyer, and Liam Price. Their construction gives strictly convex point sets with Ω(n log log n) unit-distance pairs and arbitrarily large minimum unit-distance degree, answering both questions and the general fixed-k version of Problem 97 negatively.
Paper and complete Lean source. All credit for the counterexample and its formalization belongs to those authors. Adam McKenna prepared the Prove2Me adapters.
Do not start further proof attempts or solver runs for the affirmative conjectures. Existing statements, conditional lemmas, partial proofs, and milestones remain as historical work. The owner has authorized closure assuming the external result is correct; individual theorem pages report Prove2Me verification status.
The mission is to prove the combined open goal
for finite point sets in strictly convex position in the Euclidean plane.
Problem 97 gives the local step needed for Problem 96. Assume Problem 97. Every nonempty convex-independent finite set then has a vertex with at most three neighbors at each positive radius, in particular at radius . Delete that vertex and preserve convex independence. Apply the same step to every subset created by deletion until no points remain. Charge each unordered unit-distance pair to the first endpoint deleted. Each deleted vertex receives at most three charges, so an -point set determines at most unordered unit-distance pairs. This gives the Problem 96 bound and therefore . The package uses this one-way dependency; it does not seek a reverse implication.
Let be finite. Strict convex position means that every point of is an extreme point of the convex hull of . For , the pinned multiplicity at radius counts points with . Problem 97 asks for a point where no radius has four such other points. Problem 96 counts unordered pairs at distance , then takes the supremum over convex-independent -point sets.
The historical progression is part of the setting. Erdős’s 1946 paper posed an earlier three-neighbor version. His 1987 account reports Danzer’s convex nonagon in which every vertex has three equidistant witnesses, and asks about four witnesses. Fishburn and Reeds’s 1992 work gives a 20-vertex convex configuration with the same unit distance at every vertex, placing the local question beside the unit-distance problem.
The Problem 97 target is the canonical statement that every nonempty finite convex-independent has no four-equidistant-point property:
The Problem 96 target is the canonical asymptotic statement
where is the supremum of the unordered unit-distance counts determined by convex-independent -point sets. The bound is asymptotic; the Problem 97 route would give the stronger explicit bound for every natural number .
The package records a formal proof route joining a pinned geometric obstruction to a global extremal bound. A successful Problem 97 proof would immediately settle Problem 96 with the explicit constant , while preserving the combinatorial meaning of the count. It also separates the historical three-neighbor constructions from the still-open four-neighbor assertion.
The source proof reduces Problem 97 to strong induction on . Its counting engine follows Dumitrescu's 2006 isosceles-count method, with the cap-witness refinements used in the source attributed to Nivasch--Pach--Pinchasi--Zerbib (2013). This engine forces every counterexample to have at least nine points; a finite geometric analysis excludes exactly nine points; and the remaining step must produce a removable vertex for every larger minimal counterexample. The removable-vertex statement carries the induction hypothesis that every strictly smaller nonempty convex 4-equidistant set is contradictory. That large-cardinality geometric step remains open, so both headline targets remain open. Finite computational certificates can support local cases but do not replace the universal geometric statement.
Problem 97 is open, so the mission also records the parallel negative route.
The source formalization calls a nonempty convex-independent
finite set with the four-equidistant property a
Problem97.IsCounterexample.
Constructing one such set would refute Problem 97 and therefore refute the
mission's affirmative conjunction, regardless of whether Problem 96 remains
true. The counterexample milestone keeps this resolution path visible beside
the nonexistence proof. A successful witness must use exact coordinates or
exact algebraic data from which Lean verifies both strict convex position and
the four-equidistant property; a numerical approximation or a realizable
incidence pattern alone is insufficient.
Problem 96 has its own negative route. Because its claim is asymptotic, one finite convex configuration cannot refute it. A counterexample must instead give convex-independent point sets at arbitrarily large cardinalities whose unit-distance counts exceed every proposed linear constant. The mission tracks this superlinear-family statement separately, together with a reduction from it to the exact negation of Problem 96. This keeps both possible outcomes visible: a direct or Problem-97-derived linear upper bound, and an explicit family proving that no such bound exists.
The canonical source is pinned at commit
757d852766f377f7c1a0ffeeef6d3526bc0cb7a4. It contains the formal source
statements for Problem 97
and Problem 96.
The source repository reports closed proofs of the conditional bridge to the bound
(conditional three-times bound),
the counting milestone
(nine-point counting bound),
and the exact nine-point exclusion
(exact nine-point exclusion theorem).
The remaining large-cardinality milestone is the
removable-vertex step,
with its minimality hypothesis retained. The current platform mission contains
accepted transfers of the counting argument, the conditional bridge, and the
exact nine-point exclusion, while the removable-vertex step remains open. Its definitions make
convex independence and the positive-radius condition explicit; no theorem is
assumed inside a definition. Singletons and two-point sets are included in
Problem 97, while Problem 96's counting definitions also include the empty set.
The source repository uses Lean v4.27.0; these mission statements target the
platform's v4.33.1. Source-proof transfer and revalidation remain separate work.
The Lean declarations and proofs are this project's own formalization. The
Dumitrescu and Nivasch--Pach--Pinchasi--Zerbib citations record mathematical
provenance; they do not indicate that a paper proof was imported or
machine-checked directly.
These source results establish the intended dependency graph: the P97 universal
root feeds low-unit-degree extraction, strong induction, and then the P96
supremum bound. The platform mission records those contracts and milestones;
it does not claim to have transplanted their proof bodies.
The milestones include the two canonical roots, their conditional bridge, the
|A| ≥ 9 count, the n = 9 exclusion, the |A| > 9 removable-vertex step,
the documented Danzer nine-point three-neighbor example, the parallel goal of
constructing a Problem 97 counterexample, and the superlinear-family route to
a counterexample to Problem 96.
Applying the circle method to an additive problem about primes requires counting primes in arithmetic progressions with an error term uniform in the modulus: the modulus is not fixed in advance, it grows with the size of the numbers being represented. The Siegel–Walfisz theorem is the classical statement of that uniformity, valid for every modulus up to a fixed power of , and it is the one analytic ingredient the standard proof of Vinogradov's three primes theorem cannot do without.
The history is a sequence of partial uniformities:
The von Mangoldt function equals if is a prime power and otherwise. The Chebyshev function counts primes with weights; the prime number theorem is the assertion .
A Dirichlet character modulo is a multiplicative function , supported on the units and taking root-of-unity values there. The principal character is the indicator of the units; a character is quadratic (real) if and , and primitive if it is not induced by a character of a proper divisor of . The Dirichlet -function , defined for , extends meromorphically to , entire except for a simple pole at when is principal.
The two counting functions of the mission are the twisted von Mangoldt sum and the progression sum
related by finite character orthogonality. Write for principal and otherwise. A zero of lying inside the classical zero-free region is an exceptional zero (a Siegel zero); the set of such zeros for a given is the exceptional set , which the results below constrain to have at most one element.
The attack path follows Davenport, Multiplicative Number Theory, 3rd ed., §§14, 18, 20, 21, 22.
(1) zero_free_region (§14, pp. 88–96). There is an absolute such that for
every and every ,
with at most one exception, which is real, lies in , is a simple zero, and can occur only for quadratic non-principal .
(2) pnt_dlvp (§18, pp. 111–114). For some and all ,
(3) psi_char_of_region (§20, pp. 121–125). For a region constant there are
such that, whenever is an exceptional set for with
respect to and ,
(4) siegel (§21, pp. 126–131). For every there is
such that for every real primitive non-principal ,
(5) siegel_zero (§21, second form). For every there is
such that for every real primitive non-principal ,
(6) siegelWalfisz (§22, pp. 132–134). For every there are such
that for all , all , and all with ,
This is literally the platform proposition ThreePrimes.SiegelWalfisz.
A corollary, not a milestone, records the progression form siegel_walfisz_ap: for
and ,
Goal (three_primes, §26). There is such that every odd is a sum
of three primes. It follows from milestone (6) by the existing platform theorem
deducing ThreePrimes.ThreePrimesExistence from ThreePrimes.SiegelWalfisz. The goal
leaves unspecified rather than hard-coding a numeric threshold, so it is not
invalidated by later improvements to that threshold.
Siegel–Walfisz is the standard uniform input downstream of which sit the circle method for ternary Goldbach, the Bombieri–Vinogradov theorem, and much of sieve theory. Without it, the three primes theorem's major-arc analysis has no main term.
Platform status is the reason this mission exists. A complete, machine-checked
formalization of the three primes theorem already exists in the namespace ThreePrimes
(by user tabbott), following Vaughan, The Hardy–Littlewood Method, Ch. 3, and
Davenport §26. It is conditional: it takes Siegel–Walfisz as an explicit hypothesis
ThreePrimes.SiegelWalfisz. Discharging that hypothesis makes the three primes theorem
unconditional, and is the whole content of this mission.
Mathlib contains the analytic continuation of
(DirichletCharacter.LFunction),
its functional equation, the non-vanishing of on ,
Dirichlet's theorem, and the Chebyshev function. It does not contain the zero-free
region for , the explicit formula for , Siegel's theorem, or
Siegel–Walfisz. The platform additionally hosts the
PNT+ project contour
machinery for — Borel–Carathéodory, the
inequality, a zero-free rectangle, and MediumPNT,
. That is a template for the
analogues, not a proof of them, and its error term is weaker than the de la Vallée
Poussin form milestone (2) asks for.
The first idea is to run the argument character by character. It works for complex and breaks for real ones. The positivity device that pushes zeros off compares , and the trivial character at nearby points; when is quadratic, is principal and contributes the pole of at at exactly the height where the putative zero sits, so the inequality degrades from "no zeros" to "at most one zero" and stops there. Every later step inherits that unexcluded zero: milestone (3) can only be stated with the term present, and milestone (6) is exactly the assertion that for this term is small — which Siegel's ineffective bound supplies and nothing effective is known to.
A second shortcut, deducing uniformity from Mathlib's non-vanishing of on together with Dirichlet's theorem, also fails: those results are qualitative, carry no rate, and are not uniform in .
Sums run over with , matching Vino.vmSumChar and
ThreePrimes.SiegelWalfisz; Davenport sums over . The two differ by the single
term , negligible against every error term above. Milestone (2)
alone uses a real argument, via Mathlib's Chebyshev.psi. is Mathlib's
DirichletCharacter.LFunction, so no continuation is reconstructed.
The zero-free region is Davenport.InRegion c q s, namely
; the exceptional zero
is packaged as IsExceptionalSet c χ E: is a subsingleton, every element is a real
zero of in and can exist only for quadratic non-principal ,
and at every of the region outside . Milestone (1) adds
simplicity as for .
Milestone (3) takes the region constant as a parameter rather than importing it
from milestone (1), so the milestones can be attempted in any order. For large the
hypothesis IsExceptionalSet c χ E may be unsatisfiable for some , making the
statement vacuous there — a harmless weakening, not a falsehood, and not a trivializing
reading: milestone (1) produces a definite small with a witness for every
, so instantiating milestone (3) at that discharges the hypothesis rather than
voiding it.
Siegel's theorem is stated for χ.IsQuadratic, χ ≠ 1, χ.IsPrimitive characters, with
the conclusion a lower bound on ; since is real
for real , this is the value itself, not a weakening. The constants in milestones
(4), (5) and (6) are ineffective; the statements are plain existentials, so
ineffectivity is invisible to Lean, but no numeric constant can be extracted from
anything downstream of them.
The principal character is included in the character-form statements, with main term
(if χ = 1 then (N : ℂ) else 0); milestones (3) and (6) therefore contain the prime
number theorem itself and cannot be proved by restricting to non-principal .
Milestone (6) requires strictly, which is what makes a
genuine saving over the trivial ; with allowed it would be
empty.
Beyond the six milestones, a complete development needs Hadamard factorization for as an entire function of order , the zero-counting estimate (§16, pp. 101–103), the truncated explicit formula for (§19, pp. 115–120), Perron-type contour truncation, and the imprimitive-to-primitive reduction . All of it is reusable well beyond this mission, being the standard prerequisite for Bombieri–Vinogradov, Linnik's theorem, and effective Chebotarev. Contributions of these supporting results, of alternative routes to milestone (3) following Montgomery–Vaughan Ch. 11, of the versions, and of sharper constants are welcome.
Mathlib.NumberTheory.LSeries.DirichletContinuation.
docsPolynomial representations provide a concrete way to study modules over Lie algebras: the underlying vector space is a polynomial ring, while the Lie generators act by explicit multiplication, shift, and differential operators. Chen and Tan classify a family of modules over the symplectic Lie algebra that are free of rank one over the universal enveloping algebra of an abelian nilradical. Their paper determines the family, its isomorphism classes, its weight and simplicity criteria, its finite-length behavior at exceptional parameters, and an application to Hamiltonian Lie algebras. This mission packages those headline results into one common Lean target, corresponding to Theorems 1.1--1.3 of Chen--Tan.
The common-family formulation matters. The source does not assert three unrelated existence theorems: one explicit two-parameter family carries all of the classification, simplicity, finite-length, and Hamiltonian consequences. The Lean goal therefore quantifies that family once and requires all headline properties of the same witness.
Fix and the complex symplectic Lie algebra . The relevant maximal parabolic subalgebra has an abelian nilradical . Its enveloping algebra is a polynomial algebra in the root generators, represented formally by a multivariate polynomial ring. A rank-one free -module can consequently be modeled on that polynomial ring.
The definition bundle presents the simple Chevalley generators and their action by explicit operators depending on a scalar and a polynomial parameter . Rather than assuming that these formulas already form a representation, the target asks for a generator presentation satisfying the symplectic Lie relations and for a representation family realizing the formulas. It also formalizes module equivalence, weight spaces, simplicity, Noetherian and Artinian conditions, finite composition factors, and the Shen--Larsson construction for a Hamiltonian Lie algebra.
Prove that for every there is one generator presentation and one family
of -representations on the polynomial ring, free of rank one over the abelian nilradical, satisfying the explicit generator formulas. Prove the source's classification and isomorphism criteria, including that is a weight module exactly when is constant, and the stated simplicity criterion outside the exceptional arithmetic set
For exceptional , prove the Noetherian/Artinian and finite-composition-series conclusions and the weight/nonweight classification of the composition factors. Finally, prove that the canonical Hamiltonian Shen--Larsson construction has the exact degree-weight spaces and the source's simplicity and weight-module consequences. All clauses must be witnessed by the same family .
The result gives a complete algebraic description of a large concrete class of non-highest-weight modules. It separates the generic simple regime from an exceptional finite-length regime and shows how nonweight symplectic modules generate weight modules over an infinite-dimensional Hamiltonian Lie algebra. The explicit formulas make the family suitable for calculation, while the classification prevents duplicate parameter choices from being mistaken for genuinely different modules.
Formalization adds checks that are easy to blur in prose. In particular, the generator formulas cannot be called a Lie representation until the defining relations have been verified, and the same witness must support every later theorem. A completed proof will contribute reusable Lean infrastructure for symplectic root data, polynomial representations, module-theoretic finiteness, exact weight-space descriptions, and Hamiltonian Lie-algebra functors. The paper's proofs are known; the open task is their machine-checked reconstruction.
The first obstacle is structural rather than computational. Checking formulas on individual generators is insufficient: all Chevalley and Serre relations must hold with the correct operator order and signs, after which the action must extend to the full Lie algebra. Classification then requires controlling arbitrary rank-one-free modules, not merely verifying that the displayed examples exist.
The exceptional parameters introduce a second layer. Generic simplicity and exceptional finite length are logically different claims, and the composition-factor statement must be tied to the same parameterized representation. The Hamiltonian application adds another algebra and a tensor construction; exact weight spaces and simplicity cannot be obtained by treating the functor as an opaque interface. The Lean goal deliberately keeps these obligations inside one theorem so that separate convenient witnesses cannot satisfy different portions.
The mission works over with natural rank . The definition bundle uses concrete multivariate polynomials, matrices and linear maps, a presented symplectic Lie algebra, Lie representations, submodules, and tensor products. The exceptional set is expressed with complex coercions, so no accidental natural-number division is involved. The nilradical action, freeness, parameter equivalence, weight-space equalities, simplicity, finite-length properties, and Hamiltonian brackets are transparent propositions in the bundle.
The final theorem is a single conjunction under one existentially quantified presentation and one existentially quantified family . Several convenient corollaries can be projected from it, but they are not independent targets and do not permit different witnesses. The bundle contains no custom axioms or opaque semantic assumptions, and the only admitted term is the main theorem's sorry. Contributions may split the proof into source-numbered lemmas about generator relations, classification, exceptional submodules, or the Shen--Larsson application, provided the shared-family quantifier structure is preserved.
For many natural chains, convergence to stationarity is not gradual: the distance stays near its maximum for a long time and then collapses to zero in a comparatively negligible window. A deck of cards under riffle shuffles is "not at all mixed" for six shuffles and "essentially mixed" after eight. This abrupt transition is the cutoff phenomenon, discovered by Aldous and Diaconis in the 1980s, and Chapter 18 of Levin–Peres–Wilmer, Markov Chains and Mixing Times (AMS, 2009) develops its theory: precise definitions of cutoff and cutoff windows, the product criterion necessary for cutoff, and complete proofs for two model families — the biased walk on a segment and the lazy hypercube walk, the latter with the sharp location and window , in both total variation and separation. Chapter 19 complements this with lamplighter walks: chains on the wreath-product state space of lamp configurations over a moving lamplighter, whose relaxation, mixing, and separation times are governed — beautifully — by the hitting and cover times of Missions VI. Both chapters are formalized in this mission.
A family of chains is a sequence on state spaces with stationary distributions ; all single-chain quantities acquire an index . As before, , , , and . The family has a cutoff when for every
and a cutoff at with window when and the distance at time tends (in the appropriate limsup/liminf sense) to as and to as . The separation distance from is (Mission III), , and a separation cutoff is defined by the same window template with in place of . From Mission VII, is the relaxation time; from Mission VI, and are the maximal hitting and cover times, and the pairwise distance is from Mission II.
The concrete chains: the lazy biased walk on holds with probability and otherwise steps up with probability , down with probability (reflecting at the endpoints); the lazy hypercube walk is the walk of Mission IV on . The lamplighter chain over a graph has states (lamp configuration in , lamplighter position in ); one step randomizes the current lamp, moves the lamplighter one step of the lazy walk on , and randomizes the new lamp. Its stationary distribution is uniform lamps times the walk's stationary distribution.
Theorem 18.3: the lazy hypercube walk has a cutoff at with window — the family's total variation distance undergoes its full collapse in a window of size around .
The results. Cutoff is the deepest phenomenon in the quantitative theory of Markov chains: it says mixing is a phase transition in time. The hypercube is the fundamental example where everything can be computed — the eigenvalue structure of Mission VII delivers the upper bound and a refined distinguishing-statistic argument (Mission IV) the lower — and the location with window is the sharpest statement of the coupon-collector heuristic. The product condition 18.4 is the basic sanity criterion in the ongoing research program of characterizing cutoff. The lamplighter theorems tie together the entire series: hitting times (Mission VI), cover times (Mission VI), relaxation times (Mission VII), and separation (Missions III, XI) all meet in one family of chains that furnishes counterexamples — for instance, families with total-variation cutoff but no separation cutoff.
Formalizing them. Nothing about cutoff exists in any proof assistant. The definitions themselves (families of chains, windows, limsup/liminf in a real parameter) are a formalization contribution: they force precision about quantifier order that informal texts elide. The hypercube cutoff is a landmark target — a sharp two-sided asymptotic statement, not an inequality.
The upper half of the hypercube cutoff needs the full eigenvalue decomposition of the walk ( with multiplicity , via Mission VII's spectral representation) and the bound summed over binomial coefficients; the lower half needs the Hamming-weight distinguishing statistic pushed to second-order precision (mean and variance at time ). Proposition 18.4 converts an eigenfunction with eigenvalue near into a quantitative anti-concentration statement — the formal content of "a bounded ratio forbids abrupt collapse". Theorem 18.2 rests on a central-limit-flavoured estimate for the biased walk's position, done with fourth-moment bounds rather than the CLT. The lamplighter theorems are the heaviest: the upper bounds couple lamp refreshment with the cover-time of the base walk, the lower bounds run separation-distance and eigenfunction arguments, and all four inequalities must hold with universal constants over an arbitrary growing graph family — the statements quantify over the family, so the proofs must too. The asymptotic language throughout (liminf/limsup over , limits in the window parameter ) exercises the filter library in earnest.
Families are dependent functions ∀ n, Matrix (V n) (V n) ℝ over a sequence of finite state-space types. Cutoff and windows are rendered exactly by the book's Eq. (18.3) and §18.1: the window definition uses Filter.liminf/limsup over composed with limits in the real parameter (through ⌊t n + α w n⌋₊, with the natural-floor convention on negative reals). The mixing-time ratio in the cutoff definition uses real division of the natural-valued mixing times (total division: the hypotheses keep denominators eventually positive). The biased walk's stationary distribution is passed as a hypothesis rather than a closed form. In the lamplighter theorems the comparability constants and the threshold are existentially quantified, with the graph family and its connectivity as hypotheses; the lamplighter matrix and its product stationary distribution are explicit definitions. Lemma 19.3 is stated for a single reversible chain at all times .
Every mixing bound in Missions II–IX ultimately leaned on either coupling or the spectrum, and the spectral route demanded reversibility. Chapter 17 of Levin–Peres–Wilmer, Markov Chains and Mixing Times (AMS, 2009) opens a third route: martingales — processes whose conditional expected increment vanishes — and the beautiful evolving-set process of Morris and Peres built from them. The payoff theorem of the chapter bounds the mixing time of any lazy irreducible chain by its bottleneck constant, with no reversibility hypothesis anywhere — an honest strengthening of the spectral route through the Cheeger inequality, whose proof is a martingale analysis of a random sequence of sets growing and shrinking under the chain's flow. The same chapter proves the optional stopping theorem in the exact discrete form the rest of the series consumes, and applies the machinery to sharp return-probability estimates for lazy walks.
Throughout, is a chain on a finite state space with stationary distribution ; , , and as in the earlier missions; . The chain is lazy when at every state.
A martingale adapted to the chain is a family of functions of the trajectory up to time such that the conditional expectation of , given the trajectory so far, equals — for a finite chain, a pointwise finite-sum identity. A stopping time is a -valued stopping rule in the sense of Mission III: whether to stop at time depends only on the trajectory up to .
From Mission IV: the edge measure is , with , and the bottleneck constant is the minimum over sets with of . The evolving-set process is the Markov chain on subsets of in which, from the current set , one draws uniform on and passes to the superlevel set
— states currently receiving a large share of the flow out of are likely to join, states receiving little are likely to leave.
Theorem 17.10 (Morris–Peres), the capstone of Chapter 17: for any lazy irreducible chain — reversibility not assumed —
The results. The optional stopping theorem is the workhorse identity of discrete probability — the earlier missions' gambler's-ruin and hitting-time computations are all instances, and Missions XI–XII cite it again. The Morris–Peres theorem is the strongest known elementary relation between geometry and mixing: for reversible chains it recovers the Cheeger-based bound of Mission VII, but it needs no reversibility, and its proof technique — controlling the root as a supermartingale — introduced evolving sets as a tool that has since produced heat-kernel decay, isoperimetric mixing profiles, and bounds for non-reversible and time-inhomogeneous chains well beyond the book.
Formalizing them. Mathlib's martingale library lives in measure-theoretic generality; this mission's chain-adapted martingales are self-contained finite objects (families of functions on trajectory spaces), so the optional stopping theorem here is independent of, and complementary to, the measure-theoretic one. Evolving sets exist in no proof assistant; the process is a genuinely novel formalization target — a Markov chain whose states are Finsets, defined through interval lengths of a uniform variable.
The optional stopping theorem needs the dominated-convergence step (bounded martingale, a.s. finite time) rendered as an elementary tail estimate — the series must be shown summable and equal to by an exchange of finite sums with a limit. The evolving-set transition probabilities are interval lengths: the probability of passing from to is the length of the set of whose superlevel set is exactly , which the formalization encodes by explicit upper and lower thresholds (a min over and a max over of the clipped ratios ); establishing that these lengths sum to one over , and that the process has the two martingale properties, is delicate finite-order-statistics reasoning. The goal theorem then runs a supermartingale argument on : laziness keeps the thresholds in , an expansion estimate converts the bottleneck constant into a per-step multiplicative decay of , and Lemma 17.12 converts that decay into a total-variation bound. Theorem 17.17 composes the same machinery with a Cauchy–Schwarz step. None of this exists in any library; the auxiliary supermartingale lemmas are welcome as separate contributions.
Martingales, stopping times, and stopped expectations are the trajectory-calculus objects of Missions I and III: finite sums over paths weighted by , with expectations over the stopping time as tsums in (non-summable families sum to ; the a.s.-finiteness hypothesis is the statement that the stopping mass sums to ). The evolving-set matrix is defined by the clipped-threshold formula described above — an explicit real matrix on Finset V — and the goal and lemmas assume positive and lazy exactly where the book does. Theorem 17.17 is stated for the lazy walk on a connected graph with positive degrees, with written out. Real-valued bounds on the natural-valued are direct inequalities on the cast, with no hidden rounding.
The Ising model is statistical mechanics' fruit fly: spins on the vertices of a graph, neighbours preferring to agree, a single parameter — the inverse temperature — tuning the strength of that preference. Chapter 15 of Levin–Peres–Wilmer, Markov Chains and Mixing Times (AMS, 2009) studies the Glauber dynamics for this model and exhibits, on concrete graphs, the phenomenon that made mixing times a subject: a dynamical phase transition. At high temperature (small ) the dynamics mixes in steps on any bounded-degree graph; on the complete graph the same dynamics passes, as crosses an explicit threshold, from mixing to exponentially slow mixing. The chapter also introduces two comparison tools of independent value — the sensitivity of the spectral gap to edge removal, and the block dynamics comparison — and the Kenyon–Mossel–Peres bound for trees, all formalized in this mission.
Spin configurations on a finite graph with vertex set of size and maximum degree are functions assigning to each vertex (encoded over Booleans, ). The Ising model at inverse temperature is the Gibbs distribution
each edge counted once, the normalizing partition function. The Glauber dynamics for picks a uniform vertex and re-samples its spin from conditioned on all other spins — concretely, the new spin at is with probability where is the sum of the neighbouring spins.
The yardsticks are as in the earlier missions: is the total variation distance, , and . From Mission VII: an eigenvalue of a chain is a real with for some nonzero ; is the largest eigenvalue , the spectral gap is , the largest over eigenvalues , and the relaxation time is .
Theorem 15.1, the high-temperature fast-mixing theorem: if then the Glauber dynamics on any graph satisfies
together with its refinement for graphs with all degrees even, where the condition relaxes to .
The results. Theorem 15.1 is the standard fast-mixing criterion for Glauber dynamics, and the model application of the path-coupling technique of Mission VIII. Theorem 15.3 exhibits, in the cleanest possible setting, the correspondence between the static phase transition of the mean-field Ising model and the dynamical transition of its Glauber dynamics — the phenomenon at the heart of Markov-chain approaches to statistical physics. The tree bound of Kenyon–Mossel–Peres and the block-dynamics comparison are the standard tools for spatially structured spin systems; block dynamics in particular is the engine of recursive gap bounds on trees and lattices.
Formalizing them. Nothing about the Ising model, Gibbs distributions, or Glauber dynamics exists in Mathlib. The Gibbs-distribution layer (weights, partition functions, conditional single-site laws with their closed forms) is foundational for any future formalization of statistical mechanics; the phase-transition theorem 15.3(ii) would be, to our knowledge, the first formalized instance of exponentially slow mixing driven by an energy barrier.
The high-temperature theorem is path coupling (Mission VIII) plus the tanh lemma: the one-site coupling of two adjacent configurations contracts the Hamming metric at rate , and every analytic input is in Lemma 15.2 — which is why that elementary lemma is a milestone of its own. The slow-mixing half of Theorem 15.3 runs through the bottleneck bound of Mission IV: the magnetization performs a one-dimensional walk in a double-well free-energy landscape, and the bottleneck at zero magnetization has exponentially small stationary mass — a large-deviations estimate carried out with binomial coefficients. The cycle's lower bound needs Wilson's method (Mission VII) with an explicit eigenfunction. The tree and block theorems are exercises in the comparison technology of Mission VII (Dirichlet forms, canonical paths through block updates); their constants are crude but the inductive structure is delicate. Everything sits on the subtlety that the state space has size , so all "polynomial" bounds are polynomial in , not in the size of the state space.
The Gibbs distribution is defined by explicit finite sums (weight over partition function, total division); no positivity side conditions are needed since the weights are exponentials. The Glauber dynamics is the generic single-site heat bath of Mission II applied to the Ising distribution, so the closed form is a provable lemma, not a definition. Asymptotic statements (, "for sufficiently large ") are rendered with explicit quantifiers and a free precision parameter ; the phase-transition constants are existentially quantified. The tree is encoded as words of length over an alphabet of size ; the block dynamics re-samples a uniformly chosen block from the conditional Gibbs distribution, with the convention that a conditioning of zero mass yields a zero row (total division), which the theorems' hypotheses exclude on the support. The even-degree refinement of the goal is stated as a second conjunct with its own hypothesis.
How many shuffles does a deck of cards need? The question created the modern theory of mixing times: Diaconis and Shahshahani's analysis of random transpositions (1981) and the Bayer–Diaconis "seven shuffles suffice" analysis of the riffle shuffle (1992) are its founding results. Chapters 8 and 16 of Levin–Peres–Wilmer, Markov Chains and Mixing Times (AMS, 2009) treat the four standard shuffles: random transpositions (pick two cards, swap them), the riffle shuffle (cut and interleave, the Gilbert–Shannon–Reeds model), random adjacent transpositions, and the -reversal chain of segment reversals — the last motivated by genome rearrangement, where a chromosome evolves by reversing segments and the mixing time measures evolutionary distance ("from shuffling cards to shuffling genes").
All four chains are random walks on a symmetric group; decks are encoded as in Mission III, an arrangement being a permutation with position on top. Random transpositions have increment distribution , . The lazy adjacent-transposition walk puts mass on the identity and on each . One inverse riffle shuffle assigns each card an independent uniform bit and moves the cards labeled to the top, preserving relative order; the (forward) riffle shuffle is its time reversal, given by transposing the inverse-shuffle matrix (the stationary distribution being uniform). The -reversal chain on circular arrangements indexed by picks a position and a length uniformly and reverses the segment .
for random transpositions on cards (Corollary 8.10), formalized as: for every there is with for all .
Proposition 8.11 (random transpositions lower bound , via fixed points); Proposition 8.13 (riffle shuffle: ); Proposition 8.14 (riffle shuffle: for large , by the counting bound of Mission IV); the random adjacent transpositions upper bound for large (§16.1.2, display (16.4)) and lower bound (§16.1.3, by following a single card); and Proposition 16.2 (the -reversal chain with satisfies , via conserved adjacencies).
The results. Random transpositions at (the constant here is not sharp; the sharp constant is part of the celebrated Diaconis–Shahshahani cutoff) and riffle at are the emblematic mixing results outside of spin systems; the riffle bound is the mathematical content of "seven shuffles suffice" for . The adjacent-transposition walk at order is the basic example where geometry (diameter ) forces polynomial mixing. The -reversal lower bound is the quantitative starting point of the biological application.
Formalizing them. Random walks on symmetric groups and their mixing are entirely absent from Mathlib; so are the combinatorial devices these proofs run on — the Broder stopping time, rising sequences and the Eulerian-number analysis of riffle shuffles, single-card projections, conserved adjacencies. The riffle shuffle formalization via bit strings and the stable-sort permutation Tuple.sort gives a clean combinatorial model reusable for the cutoff analysis of Mission XI.
Corollary 8.10's route is the Broder strong stationary time: mark cards under a card-and-position scheme and prove that, conditioned on the marked set and its positions, the marked cards are uniformly ordered — an exchangeability induction on top of Mission III's stopping-rule framework; then the coupon-collector-style tail with an extra factor. Proposition 8.11 requires the fixed-point statistic: the expected number of untouched cards after transpositions and a second-moment bound, fed into Proposition 7.8. The riffle upper bound runs through inverse shuffles: after inverse shuffles the deck is a uniform stable sort of -bit labels, and mixing reduces to the birthday problem for labels; formalizing "distinct labels imply uniform order" is the crux. The -reversal lower bound needs a second-moment argument for the number of conserved adjacencies with the exact variance bookkeeping of the book. Throughout, the walk-on-group conventions (left vs right increments, forward vs inverse shuffle) are the classic source of silent errors; the formal statements pin them.
All chains are explicit matrices on Equiv.Perm (Fin n) (or Equiv.Perm (ZMod n) for the circular -reversal chain); increments act on the left, matching Mission I's group-walk convention. The riffle shuffle is defined as the transpose-reversal of the explicit inverse-riffle matrix — the two have equal distance to uniformity by Lemma 4.13 (Mission II), which a solver may use rather than re-derive. Asymptotic statements (, "for sufficiently large ") are spelled out with explicit quantifiers; upper bounds carry a where integer rounding requires it. The -reversal family takes the length function as a hypothesis-carrying parameter with , and its lower bound is a genuine limit statement (Tendsto, distance to stationarity tending to ).
Welcome contributions: exchangeability and projection lemmas for deck chains; Eulerian/rising-sequence counting; the single-card chain projection (reused for Mission XI's cutoff examples).
Why do interior-point methods solve convex programs in Newton steps? Nesterov and Nemirovskii's answer is self-concordance: a convex function whose third derivative is controlled by its second, along every line, admits a Newton analysis with absolute constants and no condition number — and the logarithmic barrier is self-concordant. This mission formalizes §9.6 and Chapter 11 of Boyd & Vandenberghe: the self-concordance calculus, the Newton-decrement analysis, the duality gap along the central path, the per-centering work bound , and the crown result — with the aggressive schedule the barrier method reaches duality gap after
centering steps, each of uniformly bounded Newton cost.
Determine the exact second-order term in the least possible largest factor in a factorization of into distinct integers exceeding , with the proposed rational constant .
The final step from bandits to reinforcement learning: actions now change the state of the world. Chapter 38 of Lattimore–Szepesvári studies online learning in an unknown Markov decision process with states, actions and rewards in . The optimism principle of Mission II scales up: UCRL2 maintains confidence sets over transition kernels, solves an extended MDP by extended value iteration, and recomputes only when a state-action count doubles. The goal theorem: with probability , , where is the diameter of the MDP — sublinear regret with no prior knowledge of the dynamics. The matching lower bound brackets the true complexity of tabular reinforcement learning up to .
Randomness appears to enlarge efficient computation, but the Sipser–Gács–Lautemann theorem places every bounded-error probabilistic polynomial-time language at the second level of the polynomial hierarchy, giving one of complexity theory’s foundational limits on the power of randomization.
How well can any algorithm possibly do? Chapters 13–17 of Lattimore–Szepesvári answer with three matching impossibility results. The divergence decomposition identifies the information a policy collects: . Feeding it into the Bretagnolle–Huber inequality of Mission VI yields the goal theorem — the minimax lower bound over Gaussian bandits, showing MOSS (Mission III) is optimal up to a constant. The same machinery gives the instance-dependent bound of Lai–Robbins type: every consistent policy suffers , certifying the asymptotic optimality of the UCB of Mission III and KL-UCB of Mission IV, and a high-probability lower bound showing the Exp3-IX guarantees of Mission V cannot be improved.
Dantzig–Wolfe decomposition and column generation solve large integer programs by replacing a set of "easy" constraints with a description of its feasible points, and then pricing out the points one at a time. For linear programs this rests on the Minkowski–Weyl representation: every point of a polyhedron is a convex combination of its extreme points plus a nonnegative combination of its extreme rays. For integer programs that representation is not enough. Imposing integrality on the convex multipliers of the extreme points of does not give back the integer program, because an optimal integer point may lie in the interior of .
Lübbecke and Desrosiers, in their survey Selected Topics in Column Generation (Operations Research 53(6), 2005), present discretization (Johnson 1989, Vanderbeck 2000) as the true integer analogue of the decomposition principle. Its basis is their Theorem 1: the integer points of a rational polyhedron are generated by finitely many integer points and finitely many integer rays with integer multipliers. The paper states this result and refers its proof to Nemhauser and Wolsey, Integer and Combinatorial Optimization (1988). It underlies the integer master problem (25) of branch-and-price.
Let be an matrix and an -vector with rational entries. The polyhedron is
and its set of integer points is , the points of whose coordinates are all integers. Because , .
The recession cone of is . An integer ray of is a nonzero vector of in this cone. Extreme rays are not required.
In Lean these are polyhedronP D d, integerPoints D d, recessionConeP D and IsIntegerRay D w in the namespace Lubbecke2005.Discretization, with integer vectors cast to real vectors by castVec.
If , there exist a finite set of integer points and a finite set of integer rays of such that
Since the multipliers are nonnegative integers summing to one over , (24) says that is the union, over , of the translates of the monoid generated by the rays. No bound on or is part of the goal.
If , every point of is a vertex of . In this case convexification and discretization coincide.
The result. Theorem 1 converts an integer program into the integer master program (25) over the multipliers , with one column per generating point and per generating ray. When is bounded the rays disappear, exactly one equals one, and (25) is a linear integer program even for a nonlinear cost . The representation is what makes branching on master variables, and the passage between compact and extensive formulations, well defined in branch-and-price.
Formalizing it. The result is classical (Nemhauser–Wolsey 1988, going back to Giles and Pulleyblank and to Meyer's theorem that the integer hull of a rational polyhedron is a polyhedron). On Prove2Me, the real representation (8) is formalized as LinearOptimization.polyhedron_resolution (Bertsimas–Tsitsiklis Thm 4.15) and the integer hull theorem as LinearOptimization.integer_hull_is_polyhedron (Thm 11.3); both are included as reference items. The convexification counterpart of §3.2, that the Lagrangian dual equals the LP over , is LinearOptimization.lagrangean_dual_eq_lp_over_hull. No machine-checked statement of the integer representation (24), with integer multipliers and integer rays, was found on the platform. The mission produces that statement and, once solved, its proof.
The obvious attempt applies the real representation (8) and rounds. It fails twice. First, the extreme points of need not be integral, and an integer point written as a real combination of vertices and rays has no reason to have integer multipliers. Second, the extreme rays of generate the recession cone over , but the integer points of that cone are not in general nonnegative integer combinations of the (scaled) extreme rays; a generating set of the lattice points of a cone must usually contain non-extreme vectors. The finiteness of is also not automatic: itself is typically infinite, and taking trivializes the statement.
Rationality of the data is essential. For , every integer ray has slope below , so finitely many base points and rays generate only points with for some , while contains for every .
Fin n → ℝ; integer vectors are Fin n → ℤ cast coordinatewise. Both sides of (24) are sets of real vectors.ℚ-valued and cast to ℝ. This is an addition: the paper names no field, and the theorem is false for irrational data (see Difficulty). The cited source, Nemhauser–Wolsey, works with rational data.Fin k and Fin l for existentially chosen ; the finiteness is the content of the theorem. The multiplier vector is written as a pair of ℕ-valued vectors.A formalization with real multipliers would be the resolution theorem (8), already on the platform, and one with or infinite would be trivial; both are excluded by the statement.
Useful infrastructure: lattice points of rational polyhedral cones (Hilbert bases, Gordan's lemma), the integer hull theorem, and the real resolution theorem. A proof of Gordan's lemma for rational cones in this vocabulary would be reusable well beyond this mission. Contributions toward any of these are welcome.
In best arm identification with fixed confidence, a learner samples unknown distributions (arms) sequentially and must, as early as possible, name the arm with the largest mean, while being wrong with probability at most a prescribed risk . The problem models adaptive A/B/n testing, clinical and simulation-based selection among alternatives, and the "ranking and selection" problem of operations research and simulation optimization. The quantity of interest is the sample complexity , the expected number of samples a strategy takes before stopping.
Timeline of the question this mission formalizes:
A canonical one-parameter exponential family is a family of laws , , on with density with respect to a reference measure ; is twice differentiable and strictly convex, and has mean . Bernoulli, Poisson and Gaussian laws with known variance are examples. The divergence is the Kullback–Leibler divergence between the members with means and .
A bandit model assigns a member of the family to each arm. The class consists of models with a unique optimal arm . At each round the learner picks an arm as a function of past observations, observes a reward drawn from that arm's law, and at a stopping time recommends an arm. is the number of draws of arm in the first rounds and its empirical mean.
With and the probability simplex, the characteristic time is
and the maximizer are the optimal proportions of arm draws.
Track-and-Stop combines two ingredients:
For and , Chernoff's stopping rule with combined with C-Tracking or D-Tracking satisfies
for every .
Theorem 1 of the same paper shows for every -PAC strategy, and . Theorem 14 with therefore shows that the lower bound is attained: is the exact asymptotic sample complexity of best arm identification in exponential family models, and Track-and-Stop is asymptotically optimal.
The result is proved in the paper. What is not available is a machine-checked proof for exponential families. The platform already holds a Lean development of the Gaussian case following Lattimore and Szepesvári, Bandit Algorithms, Ch. 33, stated for one existentially chosen policy with a different threshold. This mission asks for the universal statement: every run of either tracking rule, for every exponential family, with the paper's thresholds. The tracking lemmas (Lemmas 15, 7, 8) are deterministic combinatorics and reusable by any tracking-based algorithm.
The obvious argument plugs the almost-sure behaviour of Proposition 13 into an expectation. That step fails: almost-sure convergence of does not control , because on the rare events where the empirical means are far from the stopping time may be very large. Theorem 14 needs a quantitative concentration of on events whose complements have summable probability, which in turn relies on the forced exploration guaranteed by the lower bounds on (the concentration step of App. D, Lemmas 19–20).
A second obstacle is the regularity of : the tracking lemmas only transfer convergence of to convergence of through the continuity of on , proved from the characterization of in §2.2 (Proposition 6). The GLR statistic also needs its closed form (7) near , which requires the empirical means to lie in the interior of the mean space.
BanditPolicy, BanditTrajectory, TrackAndStop). uses Kullback–Leibler divergences of the arm laws over the class and takes values in . Trajectory coordinate is round . An arm never drawn has empirical mean .Best arm identification with fixed confidence is the pure-exploration counterpart of the multi-armed bandit problem. A learner faces unknown reward distributions ("arms"), samples them sequentially, and must stop and name the arm with the largest mean, being wrong with probability at most a prescribed . The question is how many samples this requires. It arises in adaptive A/B testing, in the selection of the best of several simulated systems (ranking and selection in simulation optimization), and in clinical trials that must declare the best treatment with a guaranteed error rate.
Lower bounds for this problem were first stated in terms of the gaps between means (Mannor and Tsitsiklis, 2004). Kaufmann, Cappé and Garivier (2016) replaced ad hoc changes of measure by a single "transportation" lemma relating expected sample counts, Kullback–Leibler divergences and the error probability. Garivier and Kaufmann (COLT 2016, arXiv:1602.04589v2) combine this lemma over all alternative models at once, in the spirit of Graves and Lai (1997), and obtain a lower bound whose constant is exactly matched, as , by their Track-and-Stop strategy. This mission formalizes that lower bound (Theorem 1 of the paper, p. 3).
A canonical one-parameter exponential family is given by a reference measure on , an open interval and a function , twice continuously differentiable on with , such that the laws with density with respect to are probability measures for . The mean of is . Bernoulli laws and Gaussian laws of known variance are examples.
A bandit model is a vector ; arm returns i.i.d. rewards with law and mean . Arm is the unique optimal arm if for every . Let be any set of bandit models of the family each having a unique optimal arm, and put .
A strategy consists of a sampling rule (the arm drawn at round depends, possibly with extra randomization, on the first observations), a stopping time of the natural filtration , and an -measurable decision . It is -PAC on if for every , and . is the number of draws of arm among the first rounds.
Write for the divergence between two arm laws, , and for the probability simplex on the arms. The characteristic time is defined by eq. (1):
For , every -PAC strategy on and every ,
The statement fixes no constant beyond those of the paper, and it holds for every , not only in the limit.
For every with ,
This is Lemma 1 of Kaufmann et al. (2016), which the paper quotes without proof; Theorem 1 follows from it for every alternative simultaneously.
Theorem 1 identifies as the exact problem-dependent complexity of fixed-confidence best arm identification: since , it gives , and the paper's Track-and-Stop strategy attains this rate (the subject of mission IV of this series). The bound also explains which proportions of draws an optimal strategy must use: the maximizer of eq. (1) (mission II).
Both results are proved in the literature. Neither is formalized in the paper's generality. The platform holds the textbook form of Lattimore and Szepesvári (Theorem 33.5), which is stated for an arbitrary class with the weaker constant ; for , , so Theorem 1 is strictly stronger. A formal proof here yields the transportation lemma for exponential families on the platform's infinite-horizon bandit model, which later missions (II–IV, and any lower bound by change of measure) can reuse.
The obvious proof applies the finite-horizon divergence decomposition at a deterministic horizon . That fails here: is random and unbounded, the decision is -measurable, and the relevant divergence is between the laws of the stopped observations. The step from a fixed horizon to a stopping time, together with the data-processing inequality that turns the error guarantees under two models into , is the central difficulty. A second, smaller difficulty is to identify the paper's divergence and its means with the measure-theoretic KL divergence and mean of the arm laws of the exponential family.
Lean namespace OptimalBAI.LowerBound. The bandit protocol is the platform's (BanditAlgorithm.BanditPolicy, banditTrajMeasure, IsBanditStoppingTime, IsSoundBAI, baiComplexity); is the platform's bernoulliRelativeEntropy and is trajPullCount. Conventions:
Fin K, 0-based (the paper's arm is index ); trajectory coordinate is round ;A statement with in place of , or restricted to Gaussian arms, is the platform's existing textbook theorem and does not count as this mission's goal; nor does any version that drops the almost-sure stopping clause or truncates or to real numbers.
Needed infrastructure: the transportation lemma at a stopping time (data processing for KL through an -measurable event, Wald-type identity for the stopped log-likelihood ratio), the identities "mean of " and "KL of two family members ", and . All are reusable beyond this mission. Contributions of any of these lemmas, of eq. (2) alone, or of the Gaussian and Bernoulli special cases as stepping stones are welcome.
Graphs are the most basic combinatorial model of pairwise relations: road networks, frequency interference between radio stations, schedules, circuit layouts. Chapter 5 of Keller and Trotter's Applied Combinatorics (appliedcombinatorics.org, CC BY-SA 4.0) introduces the vocabulary of graph theory and proves its first structural theorems: when a graph can be traversed edge by edge (Euler, 1736), when it can be toured vertex by vertex (Dirac, 1952), when it can be colored with two colors, and how far the chromatic number can drift from the size of the largest clique.
Hamiltonicity is the vertex analogue of Euler's edge-traversal problem and behaves very differently: Euler's problem has a simple parity characterization, while deciding whether a graph has a hamiltonian cycle is NP-complete (Karp, 1972). Sufficient conditions are therefore the main tool, and the minimum-degree condition of Dirac (1952) is the first and most cited of them; Ore's condition (1960) and the Bondy–Chvátal closure (1976) refine it.
A graph consists of a finite vertex set and a set of 2-element subsets of , the edges; means and are adjacent. The degree is the number of neighbours of . The mission uses Mathlib's SimpleGraph V with [Fintype V]; "a graph on vertices" means Fintype.card V = n.
AppliedComb.Graphs.IsHamiltonian).IsEulerian).IsIntervalGraph).In the book's order:
The book's proof of Theorem 5.18 uses only the pigeonhole principle, so none of these results lies on its path. The milestones are the chapter's other theorems about the same objects (cycles, degrees, colorings), and they share the goal's definitions. Cayley's formula (Theorem 5.39, labelled trees on vertices) is already on the platform as GYGraphTheory.cayley_tree_formula and is included as a reference item.
Dirac's theorem is sharp: the complete bipartite graph has minimum degree and no hamiltonian cycle. It is the starting point for the theory of degree conditions for hamiltonicity (Ore, Pósa, Chvátal) and for its extremal and random-graph analogues. Euler's theorem gives linear-time recognition of eulerian graphs; Theorem 5.21 characterizes bipartite graphs; Proposition 5.25 shows that local sparsity (no triangles) does not bound the chromatic number; Theorem 5.28 is the first step towards perfect graphs.
All of these results have been proved for a long time. What is missing is their formalization. Mathlib provides SimpleGraph, chromaticNumber, cliqueNum, degree-sum identities, and definitions of eulerian and hamiltonian walks. It contains no Dirac theorem, no converse of the eulerian degree condition, and no interval-graph theory. On the platform, FamousTheorems.two_colorable_iff_no_odd_cycle_6b is stated with odd closed walks rather than odd cycles, and triangle_free_chromatic_number asserts only rather than with exactly.
For Dirac's theorem the obvious approach, induction on (deleting a vertex), fails: deleting a vertex lowers degrees, and the hypothesis is not inherited by the smaller graph. The degree condition is global, and so is the argument that uses it. In Lean the argument also has to reverse and splice vertex sequences while keeping distinctness and every adjacency along the way. The sufficiency half of Euler's theorem has to construct a circuit that uses every edge exactly once, not just show that one exists up to parity. In Theorem 5.21 the obstruction is a cycle with distinct vertices; producing one from a failed 2-coloring takes more work than producing an odd closed walk. Proposition 5.25 needs a concrete infinite family of graphs and exact computation of both invariants. The upper bound is easy, but the lower bound is not.
SimpleGraph V on a Fintype V. The number of vertices is always Fintype.card V, never a free parameter; in Theorem 5.18 the ceiling is (n + 1) / 2 in , with Fintype.card V = n.Walk.IsHamiltonianCycle, which needs at least three vertices: under that notion Theorem 5.18 would be false for . The goal assumes nonempty, as the book's proof does ( positive). Degenerate readings are ruled out: a predicate satisfied by a cycle through only some vertices, or a statement in which is not the number of vertices, would make the goal vacuous or false, and neither is used here.chromaticNumber (-valued) and is cliqueNum; on finite graphs both agree with the book's definitions (pp. 81, 84).The stochastic multi-armed bandit is the basic model of sequential decision making under uncertainty: a learner repeatedly chooses one of actions, observes a noisy reward for the chosen action only, and must balance exploring poorly known actions against exploiting the one that currently looks best. It underlies adaptive clinical trials, online advertising, recommendation, dynamic pricing and many simulation-optimization procedures in operations research.
The standard algorithm is UCB (Auer, Cesa-Bianchi and Fischer, 2002, doi:10.1023/A:1013689704352), which plays the arm with the largest upper confidence bound on its mean. Its confidence widths grow with the current time (or with a horizon fixed in advance), and its guarantee is on the expected regret, which grows like . Lai and Robbins (1985, doi:10.1016/0196-8858(85)90002-8) showed that logarithmic growth of the expected regret cannot be avoided by a consistent algorithm.
Abbasi-Yadkori, Pál and Szepesvári (NIPS 2011) proved a self-normalized concentration inequality for vector-valued martingales that holds uniformly over time. Section 6 of their paper applies it to the -armed bandit. The resulting confidence intervals depend on neither the horizon nor the current time. The UCB variant built on them, UCB(), has pseudo-regret bounded by a constant, independent of the horizon, on a single event of probability at least . This mission formalizes that section.
There are arms with unknown means . Write for the best mean and for the gap of arm .
Randomness lives on a probability space with a filtration . In round the learner plays an arm that is -measurable and receives the reward . The noise is -measurable and conditionally 1-sub-Gaussian:
The noise need not be independent or identically distributed across rounds, and the rewards need not be bounded.
After rounds, is the number of plays of arm and is the average reward received from it. For a confidence level the confidence width is
with when . UCB() plays, in round , an arm that maximizes ; in particular every arm is played once before any comparison is made. The pseudo-regret after rounds is
This is the linear bandit of the paper with the standard basis of as decision set and .
For every , with probability at least , for all simultaneously,
The right-hand side depends only on the gaps, and .
For any adapted choice of arms (not only UCB()) and every , with probability at least ,
The result. Theorem 7 shows that, once a confidence level is fixed, a UCB-type algorithm can stop paying for exploration after finitely many rounds: with probability the total regret over an infinite horizon is bounded. The paper notes that this does not contradict the Lai–Robbins lower bound, which concerns expected regret; on the failure event of probability the regret may grow linearly. Lemma 6 is the practical content behind this: anytime-valid confidence intervals for adaptively sampled means under martingale noise, usable for stopping rules, best-arm identification and any sequential procedure that inspects its estimates at data-dependent times.
Formalizing it. Both results are proved in the paper's appendices (F and G). No machine-checked proof of either is known to exist. The platform already has the self-normalized martingale bound for and unit sub-Gaussian noise (BanditAlgorithm.self_normalized_martingale_bound, listed here as a reference item), and UCB bounds with horizon-dependent widths and in-expectation or pathwise conclusions. Neither is Theorem 7. The mission produces a formal account of time-uniform confidence intervals for adaptively sampled arm means, and of a regret bound that is uniform in the horizon.
Two points separate this from textbook UCB analyses. First, the number of samples of an arm is itself random and depends on past noise, so a fixed-sample concentration inequality with a union bound over times does not give widths that are free of : a union bound over all costs a factor that diverges. The time-uniform event must come from a maximal (self-normalized) inequality applied to the martingale . Second, the regret statement is uniform in with constants depending on the gaps; converting a condition of the form "" into an explicit bound on requires solving an inequality in which appears both polynomially and inside a logarithm, and the explicit constants and must come out of that step.
The Lean development lives in the namespace ImprovedLinBandits.UCBDelta.
Fin d with 0 < d in the goal; means are μ : Fin d → ℝ, is ⨆ i, μ i (the maximum over a nonempty finite type).t + 1 for t : ℕ: the arm I (t + 1) is ℱ t-measurable, the noise η (t + 1) is ℱ (t + 1)-measurable and satisfies Mathlib's HasCondSubgaussianMGF (ℱ t) … (η (t + 1)) 1 P. Values at index are unused.A trivializing formalization is ruled out: the confidence event is not assumed as a hypothesis of Theorem 7, the i.i.d. bandit model is not substituted for the martingale noise model, and no bound on the means or rewards is imposed.
Useful infrastructure for solvers: the self-normalized bound of Theorem 1 in the scalar case (, , , ), a union bound over arms, and elementary inequalities inverting . Lemmas about pull counts and empirical means under adaptive sampling are reusable beyond this mission and are welcome as contributions.
Nonlinear programming algorithms are routinely advertised as finding a local minimum. Most of them only certify first-order conditions (a KKT point), and the natural next question is whether a given feasible point is in fact a local minimum. For smooth problems where the Hessian is nonsingular this is a second-order test, but in the degenerate case the test itself becomes a combinatorial question about a quadratic form restricted to a cone.
K. G. Murty and S. N. Kabadi (Math. Programming 39 (1987) 117–129) showed that this question is intractable already in its simplest instance: deciding whether is a local minimum of a quadratic form on the nonnegative orthant is NP-complete, and so is deciding whether a square integer matrix is copositive. The paper is the standard reference for the hardness of copositivity testing, which matters for copositive programming, for second-order optimality checks in constrained optimization, and for the complexity of local search in nonconvex optimization.
Let be a real square matrix of order and . The matrix is copositive if for every (coordinatewise). The paper considers the quadratic program
and the following questions, each phrased so that "yes" is the interesting answer:
The source problem is subset sum (Problem 5): given positive integers , is there with ? Let be the total number of digits in the data. The paper fixes an integer and a rational with , and defines functions of nonnegative variables :
, a homogeneous quadratic that agrees with on the set
and . The function is a quadratic form in ; the symmetric matrix , with entries computed explicitly from , is the output of the reduction.
For positive integer data and as above, with the matrix of , the following are equivalent:
This is the mathematical content of Theorems 1–3 and §4: a polynomially computable map from subset sum instances to matrices under which every one of these questions has the answer of the subset sum instance.
The result. The equivalence shows that checking local optimality of a feasible point, checking boundedness of a quadratic objective on a cone, and checking copositivity are all at least as hard as subset sum, hence NP-hard. Through (15) the same holds for local minimality and boundedness of a quartic polynomial with no constraints at all. These facts are the standard justification for why nonconvex solvers settle for KKT points, and the copositivity part underlies the hardness of copositive programming.
The formalization. The paper's claims are proved, and have been cited for decades, but the proof as printed is a sketch: several steps are stated as "clearly" or "it can be verified", and one step of the proof of Theorem 1 (p. 125) is false as written. The inequality for fails for slightly above , and the pointwise implication " on " has an explicit counterexample. The equivalence of Problems 6 and 7 itself survives numerical checks. A machine-checked proof of the goal settles the correctness of the reduction with the paper's own constants. No machine-checked proof of these statements exists on the platform.
The combinatorial direction (a subset sum solution gives a point with ) is a computation. The converse direction carries the content, in two places.
First, passing from to trades the linear penalty for a quadratic one. This is harmless on the box but not for , where is negative. The printed argument handles this coordinate by coordinate and is wrong there; a correct argument has to show that no point of with exists unless a point with does, which requires a global use of the size of .
Second, passing from to requires a quantitative gap: if on then with of only polynomially many bits. Lemma 2 provides such a gap for the unit box and integer matrices, but is not the box and has rational coefficients, so the lemma does not apply verbatim.
The remaining equivalences (Problems 1, 2, 3, 4, 11, 12 for a fixed matrix) follow from homogeneity of the quadratic form and the substitution , and are routine.
The data are natural numbers and is rational; all are cast to in and . The index is Fin n, and the variables of are indexed by Fin n ⊕ Fin n with Sum.elim y s. Standing hypotheses: and (the paper's "all positive integers"); in ; and in . The size counts decimal digits. Problem 1 is local minimality relative to the orthant, Problem 11 is unconstrained local minimality, both in the Euclidean topology. Lemma 2 is stated for integer symmetric (as §4 of the paper says, "as before … symmetric"), with Schrijver's encoding size, since the paper does not define "the size of "; the "optimum is or " is stated as a disjunction without an infimum. The milestones on over assume , which the paper assumes tacitly; the goal needs no such hypothesis.
Not formalized: membership in NP (Lemma 1), the polynomial-time computability of and its encoding size, the NP-completeness of subset sum (cited by the paper from Garey–Johnson), Theorem 4, and any of the words "NP-complete" or "NP-hard". The platform's complexity layer (Turing machines over bitstrings) has no subset sum problem and no encoding of rational matrices. The matrix has rational entries; a positive integer multiple of it is the integer matrix of Theorem 3, has the same answer to every question, and the rescaling is not formalized. The §3 standing assumption "D is not PSD" is not imposed; the constructed matrix can be PSD and the equivalence holds regardless.
The goal is about the explicit matrix , whose entries are given in the definitions; it is not about "some matrix whose quadratic form is ", and the constants and are the paper's explicit bounds, not "sufficiently large" or "for some ". A formalization that quantifies existentially over the matrix or the precision would be trivially true and is ruled out.
Contributions welcome: proofs of the matrix identity and the homogeneity arguments (milestones 6–9), a proof of Lemma 2 (which needs a Cramer/Hadamard bound on basic solutions of the linear complementarity system (9)), and a correct proof of the step. The copositivity definitions and milestones 7–9 are reusable for any later work on copositive programming.
Value-at-Risk (VaR) is the standard regulatory measure of downside risk of a portfolio: the loss level that is exceeded only with a prescribed small probability . Computing it requires the full distribution of asset returns, which is rarely known. In practice one estimates a mean vector and a covariance matrix and then assumes a Gaussian distribution, which understates the probability of large losses when returns are heavy-tailed or skewed.
El Ghaoui, Oks and Oustry (Oper. Res. 51(4), 2003) replace the distributional assumption by a worst case: the VaR is computed against every distribution consistent with the known moments. For known mean and covariance they obtain an exact closed form and several semidefinite (SDP) representations of this worst-case VaR. The SDP forms are what make the approach extend to moment uncertainty (moments only known to lie in a set, §2.2 of the paper) and to robust portfolio optimization. The equivalence between the probabilistic statement and the closed form is also a multivariate one-sided Chebyshev bound, related to Bertsimas and Popescu (SIAM J. Optim. 15(3), 2005; working paper 2000).
There are assets. Their returns over one period form a random vector , and a portfolio earns . The paper restricts to an admissible set that does not contain ; only is used.
The distribution of is unknown except for its mean and covariance matrix , with (positive definite). Let be the set of all probability distributions on with these two moments. For a loss level , the loss set is . The worst-case VaR at level is (Eq. (4))
Further notation: (Eq. (8)); for symmetric matrices, means is positive semidefinite and . The second-moment matrix is (Eq. (6))
For , , and , the following five propositions are equivalent:
In particular
The result. Proposition 2 turns the worst-case VaR into a second-order cone function of , so minimizing it over a polytope of portfolios is a second-order cone program (Eq. (12)). The SDP forms 3 and 5 are the basis of the paper's §2.2–§3: they extend, with the moments only known to lie in a convex set, to a single SDP whose value is the worst-case VaR over that set. Proposition 4 gives a deterministic reading: the worst-case VaR is the largest loss when the return vector is only known to lie in an ellipsoid, which connects distributional robustness to robust optimization with ellipsoidal uncertainty.
Formalizing it. The result is proved in the paper, with two imported steps: strong duality for the moment problem (Smith 1995; Bonnans and Shapiro 2000) and a Slater-type strong duality for the one-constraint quadratic condition. No machine-checked version is known. A formal proof would supply these steps with explicit hypotheses and would produce a Lean statement of the multivariate one-sided Chebyshev (Cantelli) bound with tightness over the full moment class.
The matrix equivalences (2 ⇔ 4 ⇔ 5 and 2 ⇔ 3) are Schur complements and finite-dimensional SDP duality. The difficulty is Proposition 1. The upper bound (Cantelli's inequality for ) handles one direction, but the converse requires tightness: for every below the closed form, a distribution on with exactly the prescribed mean and full covariance matrix that puts probability more than on the loss set. A scalar extremal distribution for does not by itself have the right covariance in the other directions, and a Gaussian does not reach the bound. The paper's route through the moment problem instead needs strong duality between a supremum over measures and an infimum over matrices, which is where the positive definiteness of enters.
EuclideanSpace ℝ (Fin n); is the inner product, and matrices are Matrix (Fin n) (Fin n) ℝ. Matrices of size are indexed by Fin n ⊕ Fin 1 and built with Matrix.fromBlocks (the helper bordered A v c is ). is PosSemidef, is PosDef, is (A * B).trace, and is written .HasMeanCov) contains every Borel probability measure on whose coordinates are square-integrable, with mean and centred covariance . It is not restricted to densities or to Gaussians: the Gaussian class gives a different constant, .IsLUB/IsGLB of one real number (no attainment is claimed). The maxima over , over and over the ellipsoid are IsGreatest.An algorithm for linear programming is strongly polynomial if the number of arithmetic operations it performs is bounded by a polynomial in the dimension of the problem alone (the number of variables and constraints), independently of the bit lengths of the numbers in the input. Many combinatorial optimization problems are linear programs over polyhedra of the form whose constraint matrix has entries , but whose objective vector is an arbitrary rational weight vector. Polynomial-time algorithms for such problems (for instance the ellipsoid-based algorithms of Grötschel, Lovász and Schrijver for maximum-weight cliques in perfect graphs, submodular flows, and matroid polyhedra) have running times that depend on the length of .
Frank and Tardos (Combinatorica 1987) remove this dependence once and for all: they replace by an integral objective whose entries have bits and which has exactly the same optimal solutions and the same optimal dual bases as over every such polyhedron. Any algorithm that is polynomial in and in the length of the objective then becomes strongly polynomial. The tool is simultaneous Diophantine approximation, used through the lattice-basis-reduction algorithm of Lenstra, Lenstra and Lovász (Math. Ann. 1982). The technique extends Tardos's strongly polynomial algorithm for linear programs with small constraint matrices (Oper. Res. 1986), which applies only to explicitly given programs.
For write and ; takes the values .
Decomposition. Fix a positive integer . A decomposition of is an expression
It satisfies condition (iii) if for the vector is nonzero and : the coefficients decrease so quickly that each term is negligible against the previous one.
Preprocessing. Given a rational and , the paper's preprocessing algorithm finds a decomposition with , condition (iii), and the size bound (ii)' , and outputs
Linear programs. Let be an matrix with entries in and . The primal program is and the dual program is . A point is -maximal if . A dual basis is a maximal set of row indices of whose rows are linearly independent; it determines at most one with supported on it (the basic dual solution), and it is an optimal dual basis if that exists and is optimal for the dual program.
For every , with , there is with
such that for every matrix with columns and every : (i) is -maximal if and only if it is -maximal; (ii) a set of rows of is an optimal dual basis for if and only if it is one for . The vector depends on only, not on or .
The result gives a general reduction: whenever a class of polyhedra with constraint matrices admits an optimization algorithm that is polynomial in and in the length of the objective, it admits a strongly polynomial one. The paper applies this to maximum-weight cliques in perfect graphs, optimization over submodular flow polyhedra, and matroid polyhedra membership, and its Section 5 applies the same rounding to the integer programming algorithms of Lenstra and Kannan. The subset-sum corollary (milestone 5) is independently useful: every rational weight function on a finite set can be replaced by an integral one with -bit entries that orders all subset sums identically.
All statements of this mission have been proved on paper since 1987. None is formalized on Prove2Me, and Mathlib contains only the one-dimensional Dirichlet approximation theorem. The mission produces a machine-checked version of the exact statements, with the explicit constants of the paper; the complexity claims (operation counts, strong polynomiality) are not part of it.
The goal combines two independent parts. The number-theoretic part (milestones 1–5) needs a multidimensional Dirichlet theorem, an induction producing the decomposition, and exact inequality chains with the constants and . The linear-programming part (milestones 6–7) needs bounds on the entries of inverses of nonsingular submatrices, the existence of optimal dual solutions supported on a dual basis, LP duality and complementary slackness. The obvious first idea, scaling to an integer vector by a common denominator, preserves every sign but gives no bound on in terms of ; the bound is the content of the theorem. Likewise, rounding each coordinate of separately to a fixed precision does not preserve the sign of when is tiny but nonzero.
Vectors are functions on Fin n: the input is rational (Fin n → ℚ) in the goal, in Theorem 3.3 and in the subset-sum corollary, as in the algorithm's input line; it is real in Theorem 3.1, Lemma 3.2 and Lemma 4.1, as on the page. Integral vectors are Fin n → ℤ, and is a Matrix (Fin m) (Fin n) ℤ with every entry in , cast to ; is unrestricted. Decompositions are indexed by as in the paper. is always the explicit sum , compared with in ; of an integer vector is a natural number (supNorm). Sign equality uses SignType.sign and includes the zero case. Condition (iii) is stated multiplicatively together with , which the paper's quotient presupposes; without Lemma 3.2 fails. An optimal dual basis is a maximal linearly independent set of row indices together with an optimal dual solution supported on it.
Two formalizations would make the goal trivial and are excluded: dropping the bound on (a multiple of then works), and letting depend on and (the goal states before ). The assumption on is part of every Section 4 statement.
A complete development needs a multidimensional pigeonhole argument, determinant and adjugate bounds for matrices, and basic LP duality (strong duality, complementary slackness, basic optimal dual solutions); the last two are reusable across linear-programming missions. Proofs of individual milestones, reusable lemmas on LP duality, and alternative proofs of Dirichlet's theorem are all welcome.
Paging is the problem of managing a fast memory that holds pages out of : when a requested page is not in fast memory (a page fault), some resident page must be evicted, and the cost of an algorithm is its number of faults. Practitioners have many eviction rules. Least-recently-used (LRU) performs well on real workloads but can be times worse than the optimal off-line schedule; the randomized marking algorithm of the same paper is -competitive and so has better worst-case guarantees. Fiat, Karp, Luby, McGeoch, Sleator and Young asked in 1991 whether one on-line algorithm can combine the advantages of several given ones, and answered the question exactly: the attainable combinations of ratios are characterized by one inequality (arXiv:cs/0205038, §6).
The question of combining on-line algorithms has since become a theme of its own: combining heuristics with worst-case-safe algorithms, and, more recently, combining machine-learned predictions with robust fallbacks, both ask for the same kind of guarantee against several reference algorithms at once.
A type consists of servers and a finite set of vertices with the uniform metric: two distinct vertices are at distance . This is paging: vertices are pages, the vertices covered by servers are the pages in fast memory, and a server move is a page fault.
A deterministic on-line algorithm of type has an initial configuration of its servers and, after each request , moves servers so that some server covers ; its configuration after a request sequence depends only on that sequence. Its cost on a request sequence is the total distance its servers travel, i.e. the number of server moves.
For algorithms and of the same type and a constant , is -competitive against if there is a constant such that for every request sequence
A sequence of positive reals is realizable if for every type and every deterministic on-line algorithms of that type there is a deterministic on-line algorithm of the same type that is -competitive against for every .
For and positive reals ,
In the order of the paper's proof:
The result. Theorem 6 is an exact characterization, not a bound: the region of simultaneously attainable ratios against arbitrary deterministic paging algorithms is . For example, any two paging algorithms can be combined into one that is -competitive against each, and no better symmetric pair is possible in general. Combined with Theorem 7 of the same paper (not part of this mission), the same region is attainable against randomized algorithms, which is how LRU's practical behaviour and the marking algorithm's worst-case guarantee can be obtained within constant factors by one algorithm.
Formalizing it. The theorem has been proved since 1991; no machine-checked proof is known. A formal proof produces a reusable notion of competitiveness of one on-line algorithm against another, built on the published KServer_model definitions, and a formal account of the scheduling fact at the core of the sufficiency proof.
Sufficiency looks like an averaging argument, but the combined algorithm cannot simulate the and follow one of them: switching between their configurations costs up to per switch, which no additive constant absorbs. The accounting has to charge each of 's faults to a specific move of a specific , and the charge must be injective; the paper's claim that is at least the number of punishments is where this happens, and it depends on how server intervals are matched. The allocation of faults to algorithms is then a deadline-scheduling problem whose feasibility is exactly , and the floor functions make the counting delicate at the boundary. The paper's own definition of punishment only counts intervals that start with a move, so the first faults of (servers on their initial vertices) need separate treatment; they are absorbed by the additive constant.
Necessity needs the right family of hard instances: the algorithms must never move at the same step, which pins the type to .
The Lean development works in the namespace CompetitivePaging.Combining and imports the published KServer_model definitions: KServer.OnlineAlgorithm k M (a configuration map from request prefixes to Fin k → M with a serving condition) and OnlineAlgorithm.cost. Committed conventions:
k : ℕ and any finite M : Type with a metric in which distinct points are at distance ; realizability quantifies over all of them, never over one fixed type;Trivializing encodings are ruled out: realizability is not stated for a single fixed type, the metric is not the metric of Fin n, and the competitive constant is not allowed to depend on the request sequence.
A complete proof needs the construction of the punishing algorithm as a KServer.OnlineAlgorithm (a lazy, injective algorithm whose moves depend on the prefix and on the 's configurations), the injective charging argument, the scheduling lemma, and the explicit shuttle algorithms. The scheduling lemma and the charging lemma are independent of paging and reusable. Proofs of any milestone are welcome, as are alternative statements of the sufficiency construction.