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.
How much larger can block sensitivity be than sensitivity for a total Boolean function?
For a total Boolean function , a block of coordinates is sensitive at if flipping every bit in that block changes . Let count sensitive singletons and be the maximum number of pairwise disjoint sensitive blocks. Define and .
This campaign seeks larger exponents for which there exists an infinite family of total Boolean functions , indexed by , satisfying
Here denotes a quantity tending to zero as . Higher is better. The classical exponent is , and Huang's bound gives a ceiling of .
OpenAI's construction achieves an exponent strictly greater than .
One sufficient way to establish an exponent is to find a single total Boolean function with and . Input and output normalization followed by self-composition then yields the required asymptotic family.
Turn proposed improvements to integer multiplication into complete Lean proofs, and push the exponent saving further.
Harvey and van der Hoeven established an algorithm in 2021. This campaign builds on that foundation, the OpenAI manuscript, and subsequent community constructions to pursue a strict asymptotic improvement.
For two -bit integers, the target is
A positive beats asymptotically; larger is better. Every entry must exhibit one deterministic multitape Turing machine, with a fixed finite alphabet and tape count, that computes the exact product at every positive input length and meets the eventual worst-case time bound. The tracked number measures an asymptotic exponent saving.
Classical algorithms solve 3SUM in time. In a 2026 breakthrough, Alman and Vassilevska Williams gave a deterministic algorithm, refuting the integer 3SUM hypothesis. How low can the exponent go?
Building on existing Lean formalizations, this campaign tracks upper bounds for 3SUM on polynomially bounded integers, using a word RAM with -bit words, and pursues smaller exponents.
Classical algorithms solve all-pairs shortest paths in time. In a 2026 breakthrough, Alman and Vassilevska Williams refuted the APSP conjecture with a deterministic algorithm. How low can the exponent go?
Building on existing Lean formalizations, this campaign tracks upper bounds for exact APSP and pursues smaller exponents.
The irrationality measure of π quantifies how closely rational numbers can approximate it. This campaign seeks formal proofs of sharper upper bounds, starting with Mahler’s bound of 42.
The sharp Hlawka inequality for Schatten -norms is a cousin of the triangle inequality: it relates the norms of three matrices to the norms of their pairwise sums and their total sum. For complex diagonal matrices, an exact formula for the best possible comparison constant has been proved in Lean for every real . We conjecture that the same formula holds for all .
What is the smallest cutoff for which this formula holds for every real ?
References:
Is every odd number a sum of primes? This campaign tracks formalized proofs of the smallest that suffices.
Schnirelmann (1930) showed some finite works. Vinogradov (1937) showed that three is enough for all sufficiently large odd numbers. Tao (2012) proved unconditionally. Helfgott (2013) proved that every odd number greater than is a sum of three primes, though the proof is still unrefereed. Ideally, we can formalize this statement here. Note that three is optimal: is neither prime nor + prime.
Schoolbook matrix multiplication takes operations. The exponent is the infimum of all such that two matrices can be multiplied in arithmetic operations; trivially , and is conjectured but open.
Strassen gave the first nontrivial bound, , in 1969, and introduced the laser method in 1986 to reach . Coppersmith and Winograd's 1990 bound of stood for two decades. Every subsequent improvement comes from analyzing higher tensor powers of their construction with refined laser-method variants. That line reached in 2025, and the current record is , from August 2026. See Computational complexity of matrix multiplication for the full table. Can we formalize these results and even improve on them?
Erdős asked, repeatedly and with a rising price tag, for an asymptotic formula for the largest subset of that contains no arithmetic progression of a given length. He offered 1000 dollars for it in [Er97c] and 10000 dollars in [Er81, p.4], where he called the question "probably enormously difficult"; elsewhere he described it as "probably unattackable at present". Most of modern additive combinatorics — the density increment method, the triangle removal lemma, Gowers uniformity norms, the arithmetic regularity lemma — grew out of attempts on this single question, and the answer is still unknown, even in the first non-trivial case .
Timeline.
Every upper bound in this list is still astronomically far from Behrend's lower bound, and no candidate asymptotic formula has been proposed for any .
Fix an integer . A non-trivial -term arithmetic progression is a list of natural numbers with common difference ; the requirement is what "non-trivial" means, and it forces the terms to be distinct. A finite set is -AP-free if it contains no such progression. Write
The mission takes its formal definition of verbatim from the formal-conjectures entry for this problem, so that the goal below is literally the statement recorded there. In that development a set is called free of progressions of length when every subset of it that is an arithmetic progression of length forces . Progressions of length and count as trivial, so under that convention every set is free of them and ; the interesting range begins at . Every statement in this mission that depends on the convention carries an explicit hypothesis on .
On that range, is non-decreasing in both and , satisfies , and hence, by Fekete's subadditivity lemma, converges. Szemerédi's theorem is the statement that the limit is ; the whole difficulty of this mission lies in how fast it goes to .
This is erdos_142.variants.lower of the formal-conjectures file for Erdős 142, reproduced binder for binder, over that file's own definition of .
The headline theorem in that file, erdos_142, states with the comparison function left as an answer(sorry) placeholder, and the same is true of its variants.upper and variants.three. Those are not closed propositions and cannot serve as a mission goal: the literal request of Erdős Problem #142 — "prove an asymptotic formula for " — has no known right-hand side for any , which is exactly why the file leaves a hole there. variants.lower is the one formalizable target in the file, and it is also the strongest precisely-stated form the problem page attaches to #142: Erdős offered 5000 dollars for (essentially) exactly it, as recorded under Erdős Problem #3. It is known for — it follows from Bloom–Sisask 2020, and a fortiori from Kelley–Meka 2023 — trivial for , where , and open for every . It fixes no constants, so no future improvement can invalidate it.
Erdős remarked in [Er80, p.92] that even this separation between consecutive progression lengths is not known. Here [Er80] is the erdosproblems.com bibliography key for Erdős's 1980 paper; it is a citation, not a pointer to Erdős Problem #80, which is an unrelated question about books in graphs. This statement has no counterpart in formal-conjectures: the file for #142 contains only the , and variants above, and the only two files in that repository that mention at all are the ones for #142 and #139.
Proving for all yields, by a standard summation argument, Erdős's conjecture that every with contains arbitrarily long arithmetic progressions — the 5000-dollar Erdős Problem #3, of which the Green–Tao theorem on primes is the best-known special case. Below that threshold, quantitative bounds on control the density at which progressions must appear in any concrete set, and are the input to results on progressions in the primes, in sumsets, and in sparse random subsets of the integers.
Formalization status is uneven, and this mission is designed around that gap. Mathlib already contains the theory in a usable form: the predicate ThreeAPFree, the Roth number rothNumberNat, its subadditivity, and a complete formalization of Behrend's construction (Behrend.roth_lower_bound). Mathlib does not contain Roth's theorem, Szemerédi's theorem, or any of the modern upper bounds; to the best of current knowledge none of Roth, Szemerédi, Gowers, Green–Tao, Kelley–Meka or Leng–Sah–Sawhney has a machine-checked proof anywhere. The formal-conjectures entry states the problem but proves nothing: every declaration in it is a sorry. Two of this mission's targets are taken from that repository — the goal from its file for #142, and the Szemerédi milestone from its file for #139, which uses the same ; those are the only two files there that mention . The milestones therefore split cleanly: the first six are reachable now on top of Mathlib, and the last five are open formalization projects of independent value.
Every known upper bound for runs a density increment: if of density has no -term progression, find a long subprogression on which has density , and iterate. The bound this produces is governed entirely by two quantities — how large the increment is, and how much of the interval survives one step. For the increment is extracted from an inverse theorem for the Gowers -norm, and the best available correlation bounds there are quasipolynomial in ; iterating a quasipolynomial increment cannot do better than , which is nowhere near . Reaching requires an increment with polynomial dependence on together with a subprogression of polynomial length, and that combination is currently available only for , through the sifting and almost-periodicity machinery of Kelley–Meka. No soft or averaging argument can substitute: Behrend's construction shows the truth at is , so the answer is not a power of and cannot be produced by any argument whose output has that shape.
The mission's definition file Erdos142Basic carries two layers, and every statement in the mission is written against them.
The source definitions, ported verbatim. IsAPOfLengthWith, IsAPOfLength, IsAPOfLengthFree and r are the declarations of the formal-conjectures entry, transcribed unchanged into the mission's namespace: a set is an arithmetic progression of length with first term and difference when it has exactly elements and equals ; it is free of length- progressions when every progression of length inside it forces ; and is the supremum of over subsets free of length- progressions. The ground set is Finset.Icc 1 N, and the supremum is sSup over ; the file proves the two facts that make it a genuine maximum (le_r and r_le).
An elementary handle. HasAP k A is ∃ a d, 0 < d ∧ ∀ i < k, a + i * d ∈ A, and APFree k A its negation. This form carries no cardinality side condition in and is what a solver actually wants to induct on. The first milestone is exactly the bridge between the two layers.
Two consequences of the source convention are worth stating plainly, because the prose is silent about them. Length- and length- progressions are trivial, so every set is free of them and ; monotonicity of in therefore holds only from onward, and the corresponding milestone carries that hypothesis. Asymptotic statements use Asymptotics.IsLittleO and Filter.atTop over with real-valued casts, and real division is Lean's, so (N : ℝ) / Real.log N is at ; this is invisible to atTop.
A trivializing formalization is ruled out by construction: one milestone asserts rothNumberNat N, pinning this development against Mathlib's independently written definition of the Roth number, so a vacuous or mis-quantified notion of progression-freeness cannot survive. That milestone, the bridge milestone above it, and the monotonicity milestone have all been checked to be provable before this proposal was drafted.
A full development needs: discrete Fourier analysis on , Bohr sets and their regularity, the arithmetic regularity lemma, Gowers uniformity norms and the inverse theorem for them, and — for the lower bounds — sphere-counting in high-dimensional boxes (already in Mathlib via Behrend). All of this is reusable well beyond this mission. Contributions of any kind are welcome, including partial results: quantitative bounds weaker than the cited ones, the case of a general- milestone, and reusable Fourier-analytic infrastructure are all valuable even when they do not close a milestone.
FormalConjectures/ErdosProblems/142.lean — the source of the goal statement and of the definition of . https://github.com/google-deepmind/formal-conjectures/blob/main/FormalConjectures/ErdosProblems/142.leanAn elliptic curve over is a smooth cubic curve with a rational point. Its rational points form a finitely generated abelian group (Mordell, 1922), so for an integer , the rank. No algorithm is known that decides, for a given curve, whether , i.e. whether there are infinitely many rational points. The Birch and Swinnerton-Dyer conjecture predicts from an analytic object, the Hasse–Weil -function : it asserts that equals the order of vanishing of at . It is one of the seven Millennium Prize Problems of the Clay Mathematics Institute; the official formulation is Andrew Wiles' problem description, The Birch and Swinnerton-Dyer Conjecture (2000). This mission formalizes that statement, its weak form, and the results Wiles lists as known.
Timeline.
A Weierstrass equation over is
with discriminant ; in Lean, WeierstrassCurve ℚ. It is an elliptic curve when (Mathlib's typeclass IsElliptic). Its rational points are the rational solutions together with the point at infinity , an abelian group under the chord-and-tangent law (W.toAffine.Point). The rank is the rank of this group as a -module,
the in .
The Hasse–Weil -series is built prime by prime. For each prime take a Weierstrass equation for that is minimal at (integral coefficients, with the -adic valuation of as small as possible) and reduce it modulo ; put when the reduction is smooth (good reduction). The local factor is
and , convergent for by Hasse's bound. In Lean this is Mathlib's WeierstrassCurve.LSeries W s, defined by exactly this recipe (WeierstrassCurve.LFunction is the arithmetic function , an Euler product of local factors computed on a model minimal at each prime); where the Dirichlet series does not converge, Mathlib's LSeries takes the junk value . This is the complete -series of Wiles' Remark 1; it differs from the incomplete product over in Wiles' display by finitely many factors holomorphic and non-zero at , so both have the same order of vanishing there.
An -function of is an entire function with for (BSD.IsLFunction W Λ). By the identity theorem there is at most one; by modularity there is exactly one. The order of vanishing of at is the with , ; in Lean, analyticOrderAt Λ 1, valued in , with value exactly when vanishes identically near .
BSD.birch_swinnerton_dyer)For every elliptic curve over there is an entire agreeing with on such that
This is Wiles' Conjecture (Birch and Swinnerton-Dyer): with and . Open.
BSD.weak_birch_swinnerton_dyer)There is an -function of with if and only if is infinite. Wiles: "In particular this conjecture asserts that is infinite." Open.
BSD.mordell): is a finitely generated abelian group.BSD.lSeriesSummable): converges for . Wiles: "this Euler product is then known to converge for ."BSD.exists_isLFunction): has an -function. Wiles: Hasse's conjecture, "now been proved" by Wiles, Taylor–Wiles and Breuil–Conrad–Diamond–Taylor.BSD.birch_swinnerton_dyer_of_analyticOrderAt_le_one): if an -function of vanishes to order at most at , its order equals the rank. Wiles: "If with and or , then the conjecture holds."A bridging lemma, BSD.isLFunction_unique, records that an -function of is unique when it exists.
The result itself. The conjecture makes the finiteness of decidable from and, in its refined form, gives an effective procedure for finding generators (Manin, 1971). Conditionally on it, Tunnell (1983) characterises the congruent numbers, the areas of right triangles with rational sides, a problem open since the tenth century. It is the prototype of the conjectures of Tate, Deligne, Beilinson and Bloch–Kato relating ranks of arithmetic groups to orders of vanishing of -functions.
Formalizing it. None of the statements in this mission has a machine-checked proof. Mathlib provides the objects: the group law on , minimal models and reduction types over discrete valuation rings, and the Hasse–Weil -series as a Dirichlet series (2025–2026). It does not contain Mordell's theorem (no theory of heights), Hasse's bound, modularity, or the continuation of . On this platform, earlier library entries named birch_swinnerton_dyer are retired placeholders whose formal statements reduce to trivialities such as ; they carry a notice saying so and are not formalizations of the conjecture. This mission gives the first faithful statement against Mathlib's own -series. Two published platform results bear directly on the milestones: the descent step WeierstrassCurve.Affine.Point.addGroup_fg_of_finiteIndex (finite index of implies finite generation) reduces milestone 1 to the weak Mordell–Weil theorem, and WeierstrassCurve.modularity_of_semistableModel from the platform's Fermat's Last Theorem development proves modularity of semistable curves for a notion of modularity defined through eigenform coefficients; relating that notion to WeierstrassCurve.LSeries would give milestone 3 for semistable curves.
Neither side of the equation is computable in general. On the algebraic side, descent bounds the rank from above by the rank of a Selmer group, but the gap is the Tate–Shafarevich group Ш, which is not known to be finite; the obvious plan, compute the Selmer group and show it has the rank of , founders on Ш. On the analytic side one can certify or numerically but cannot certify an exact zero, and the only known bridge from -values to rational points, the Heegner point construction, produces at most one independent point. This is why milestone 4 stops at order and the conjecture is not known for a single curve of rank . Iwasawa theory (Kato, Skinner–Urban) relates -adic -functions to Selmer groups but yields -adic, not Archimedean, orders of vanishing.
The formalization adds its own obstacles: milestone 1 needs heights and the weak Mordell–Weil theorem (Kummer theory over number fields, finiteness of class groups and units); milestone 2 needs Hasse's bound, i.e. the degree of the Frobenius endomorphism; milestones 3 and 4 rest on modularity, Galois representations, modular curves and Euler systems.
WeierstrassCurve ℚ with IsElliptic (); no minimality or integrality of the model is assumed. Mathlib's -series passes to a minimal model at each prime internally, and the point group depends only on the curve, so every statement is invariant under change of Weierstrass equation.Module.finrank ℤ W.toAffine.Point: for a finitely generated abelian group, the in ; for a group of infinite rank Mathlib's finrank is , a case milestone 1 excludes.WeierstrassCurve.LSeries, with all Euler factors including the bad primes, and junk value where the Dirichlet series diverges. BSD.IsLFunction constrains only on ; milestone 2 shows the series is genuine there, and the bridging lemma shows is then unique.analyticOrderAt Λ 1 : ℕ∞; equating it with a natural number asserts in particular that near .No trivializing formalization. The existential cannot be chosen freely: it must agree with the honest, non-zero Dirichlet series on a half-plane, so it is unique, and is excluded by the finite value of the rank. Without IsElliptic the statements would concern singular cubics, whose point group is or ; the hypothesis is required, not decorative.
Out of scope. The refined conjecture (the leading coefficient in terms of Ш, the regulator, the real period and the Tamagawa numbers), the finiteness of Ш, number fields and abelian varieties, and the functional equation of .
Infrastructure needed and welcome contributions. Heights on and the weak Mordell–Weil theorem; Hasse's bound and the multiplicativity of ; a bridge from Mathlib's WeierstrassCurve.LSeries to the -series of a weight-two newform, so that existing modularity results yield milestone 3; Heegner points and Kolyvagin's Euler system for milestone 4; and the bridging lemma, provable now from the identity theorem. Decompositions of every milestone and lemmas about WeierstrassCurve.LFunction (its values at primes, multiplicativity, independence of the model) are welcome.
Our goal
This project aims to formalize the Poincaré conjecture in Lean, following the approach in Kleiner and Lott's Notes on Perelman's Papers.
Important references
Poincare-Conjecture and DifferentialGeometry are important references for this project, providing existing work on proof planning and foundations in differential geometry. We thank the authors and contributors of both projects. We will build on their work while preserving credit and citing our sources.
OpenGA's role
OpenGA focuses on manual review, curation and reuse: checking existing code, adapting it to the required versions, and organizing reusable definitions and theorems in the library.
The PoincareConjecture directory is used to prepare submissions to Prove2Me and keep a local copy of the platform's code and progress through ongoing synchronization. Results completed on the platform will also be reviewed and incorporated into OpenGA for use in future work in geometric analysis.
We thank the Prove2Me team for running the platform and exploring collaboration between humans and AI in mathematical formalization. We are honored to take part.
The discrete-time Riccati equation is the central object of linear-quadratic optimal control — the design equation behind LQR/LQG controllers in every modern control stack. Proposition 4.4.1 of Bertsekas, Dynamic Programming and Optimal Control, Vol. I (3rd ed., 2005, §4.1) packages its asymptotic theory: under controllability and observability the Riccati iteration converges to the unique positive semidefinite solution of the algebraic Riccati equation and the resulting closed loop is stable. Alongside it, Lemma 4.2.1 of §4.2 develops K-convexity, the analytical engine behind Scarf's optimality of inventory policies — a foundational result of operations research. Neither the Riccati asymptotics nor K-convexity exists in Mathlib.
Matrices , , , . The Riccati operator (BertsekasRiccatiMap)
is controllable if has rank (BertsekasControllablePair); is observable if is controllable (BertsekasObservablePair). Separately, is -convex (BertsekasKConvex, Def. 4.2.1) if for all , , .
with — BertsekasDP.riccati_convergence_stability (goal). Milestones: Lemma 4.2.1(a)–(d) (kconvex_of_convex, kconvex_combination, kconvex_expectation, kconvex_sS_structure), culminating in the structure theorem for continuous coercive -convex functions.
The Riccati result is the mathematical license behind steady-state LQR design: it guarantees the design equation has one meaningful solution, that iterating the finite-horizon recursion finds it, and that the resulting feedback is stabilizing. Formally it would seed a Mathlib-adjacent theory of matrix fixed-point iterations, positive semidefinite order, and spectral-radius stability. The K-convexity milestones are self-contained real analysis, each of independent reuse value for inventory theory; part (d) is the engine of -policy optimality. All results are classical and proved in the book; the formal work is new.
The Riccati proof interleaves monotonicity of on the psd cone, boundedness from controllability (a steering argument), positivity from observability, and stability extracted from the fixed-point identity via a Lyapunov argument — several pieces of matrix analysis (psd order, congruence, Schur-type manipulations, spectral radius vs. convergence of powers) that must be built or located in Mathlib. The naive route of diagonalizing fails: nothing is symmetric about . For Lemma 4.2.1(d), the difficulty is that is not convex: the minimizer structure must come from the K-convexity inequality applied at carefully chosen points, plus continuity and coercivity.
Real matrices over Fin n; Matrix.PosSemidef/PosDef; matrix inverse is Mathlib's total inverse (zero on singular input — harmless here since along the relevant iterates, which the proof must establish); convergence in the entrywise topology; eigenvalues via spectrum ℂ of the complexified matrix, all strictly inside the unit circle. Rank-based controllability exactly as Def. 4.1.1. K-convexity is stated for all real ; note is forced whenever it is satisfiable (), and the expectation milestone is stated for finitely supported disturbances (integrability automatic).
The Pontryagin Minimum (Maximum) Principle is the fundamental necessary condition of optimal control, in continuous use since 1956 across aerospace guidance, robotics, and mathematical economics. Chapter 3 of Bertsekas, Dynamic Programming and Optimal Control, Vol. I (3rd ed., 2005) develops it from the dynamic programming side: the HJB sufficiency theorem (Prop. 3.2.1), an envelope lemma (Lemma 3.3.1), the Minimum Principle itself (Prop. 3.3.1), and its discrete-time counterpart (Prop. 3.3.2). Mathlib's optimal-control coverage is currently near zero — no HJB equation, no adjoint equations, no maximum principle — which makes this the mission with the largest gap between textbook maturity and formal coverage in the series.
Minimize, over admissible pairs, the cost
with continuously differentiable (BertsekasCTModel). Admissible controls are piecewise continuous on — formalized as: bounded image and continuous off a finite set (BertsekasPiecewiseContinuousOn) — and state trajectories are continuous, satisfying the ODE off a finite set (BertsekasCTAdmissibleFrom, parametrized by an arbitrary start ). The Hamiltonian is (BertsekasHamiltonian).
For an optimal admissible pair : there exist an adjoint and a constant with
away from finitely many times — BertsekasDP.pontryagin_minimum_principle (goal). Milestones: Prop. 3.2.1 (hjb_sufficiency_of_continuous), Lemma 3.3.1 (envelope_gradient_lemma), Prop. 3.3.2 (discrete_minimum_principle).
The HJB milestone carries the hypotheses that and are jointly continuous — the consequence of the §3.1 standing assumptions that its proof uses. An earlier version without any regularity hypothesis was disproved: with a discontinuous running cost the cost integrand need not be integrable, and the library's integral of a non-integrable function is .
The Minimum Principle converts an infinite-dimensional optimization into a two-point boundary value problem — the basis of shooting methods and of every "bang-bang" analysis. None of it exists in Mathlib; even the HJB verification theorem would be new. The discrete-time milestone is self-contained multivariable calculus and gives early value; the envelope lemma is reusable well beyond control theory. The results are classical (Pontryagin et al. 1962; the book's Chapter 3); the formal proof of Prop. 3.3.1 will need an honest variational argument — the book's own HJB-based derivation is explicitly informal.
For the goal: the classical proofs go through needle variations and a separation argument, or through regularity of the value function — neither is in Mathlib. The book's derivation assumes differentiability of the optimal value function, which is not a hypothesis of the statement; a formal proof must either supply a rigorous variational argument or add intermediate lemmas as new platform problems (sketching is encouraged). For the HJB milestone, the work is differentiating along a trajectory that satisfies the ODE only off a finite set, then integrating.
States and controls in EuclideanSpace ℝ (Fin n) / (Fin m); gradients in Mathlib's gradient; the ODE and adjoint via HasDerivAt off a finite exceptional set; costs via intervalIntegral. Piecewise continuity includes boundedness of the image, so the cost integrand of an admissible pair is genuinely integrable — the junk-value escape (non-integrable integrand ⇒ integral 0) is closed. Fixed initial state, fixed terminal time, free terminal state; time-independent dynamics (so the Hamiltonian is constant, per the book's remark that time-varying systems lose constancy). is an arbitrary set — no compactness or convexity is assumed in the goal.
If is algebraic and , is transcendental? Guy Diaz asked this in 2004 and it is still open. Note it is , not — the latter would follow at once from Hermite–Lindemann. The whole difficulty is that itself may be transcendental while only its modulus is constrained.
Write for the algebraic numbers in and
for the logarithms of algebraic numbers. In 2004 Guy Diaz asked, and conjectured, that no non-zero element of has algebraic modulus. He states it as
« Soit avec ; alors est transcendant. »
The statement fits on one line and needs no machinery beyond and . It has been open for twenty-two years.
It is not a curiosity. Diaz records that it follows from Schanuel's conjecture and also from the strong four exponentials conjecture, so it sits underneath two of the standard pillars of transcendence theory while being far more concrete than either. Anything that settles it settles a case of both.
The mission decomposes into work that can be done now, without any open input.
Two milestones are conditional theorems — "Schanuel implies Diaz", "strong four exponentials implies Diaz". Diaz asserts both implications in a single sentence and does not write out either derivation; as far as I can establish, neither has been written out anywhere. Each is a short, self-contained argument that any solver can attack today. Both are stated here without axioms: Schanuel, the strong four exponentials conjecture and Hermite--Lindemann are all Prop-valued definitions in the mission's definition bundle, so a conditional milestone takes its hypothesis explicitly and nothing is assumed silently.
A third milestone is the elementary geometry of the configuration — the coordinate axes, which turn out to be exactly the degenerate branch where and are -linearly dependent.
The remaining two milestones are classical theorems that the platform's Mathlib does not have: Hermite--Lindemann and the six exponentials theorem. The first is needed by the four-exponentials route and by the axis case. The second is the proved member of the family this conjecture lives in, and the distance between it and the strong four exponentials conjecture is a fair measure of how far the known machinery falls short.
Only the top node needs genuinely new transcendence.
One structural remark that shapes the whole ladder: Hermite--Lindemann is a special case of the goal, not just an input to it. If is algebraic then is algebraic, hence so is , and the goal applied to gives that is transcendental. Diaz's conjecture is therefore strictly stronger than Hermite--Lindemann, and no route to it can avoid that node.
| 1873, 1882 | Hermite, then Lindemann: is transcendental for algebraic . In particular every non-zero element of is itself transcendental, so a counterexample would be a transcendental number with algebraic modulus and algebraic exponential. |
| 1934--35 | Gelfond and Schneider settle Hilbert's seventh problem. |
| 1966 | Lang's Introduction to Transcendental Numbers records Schanuel's conjecture, and gives the six exponentials theorem (also Siegel, unpublished; Ramachandra 1968). The four exponentials conjecture stays open, and still is. |
| 1966 | Baker's theorem on linear forms in logarithms. |
| 1997 | Diaz studies the companion condition , assertion (4-1), p. 237. |
| 2000 | Waldschmidt's Diophantine Approximation on Linear Algebraic Groups states the conjecture at p. 399, credited to Diaz 1997, and records the relevant four-exponentials configuration with , at p. 15. |
| 2004 | Diaz states the modulus question, §5.1, p. 550. On p. 551 he asks the accompanying methodological question: how could the non-holomorphic maps and enter a transcendence proof at all? |
| 2026 | A machine-checked negative result on a class of strategies (see below). The conjecture itself is untouched. |
For a candidate one has with algebraic, hence
So is not independent data: complex conjugation on is a rational function of the generator, determined by the ring structure. Three consequences follow, all formalised at https://github.com/carlok/diaz-modulus-lean: a ring homomorphism fixing and carrying to any other transcendental point of the same circle automatically intertwines conjugation; such a homomorphism exists whenever both points are transcendental over the base; and no vanishing-coefficient statement over separates a candidate from an ordinary complex number placed on the same circle.
The practical consequence for solvers: accumulating algebraic relations between and until they collide cannot settle this. A successful attack has to introduce information that is not a rational function of over — which is precisely Diaz's own methodological question, still open.
Mathlib/NumberTheory/Transcendental/Lindemann/AnalyticalPart.lean — verified in all three of the platform's pinned revisions (0df444a3, c5ea0035, 777aaa61), none of which contains transcendental_exp. Hence the choice to carry it as a Prop and give it its own milestone rather than assume it. There is an open PR, leanprover-community/mathlib4#28013 (feat: Lindemann-Weierstrass Theorem, opened 2025-08-05, label awaiting-author as of 2026-09-07); if it merges and a pin advances, that milestone collapses to a short transfer.Algebra.trdeg has almost no computational API. It is cardinal-valued, with transcendence bases and lift_cardinalMk_eq_trdeg, but nothing that evaluates the degree of an explicitly adjoined finite set. The Schanuel milestone will want a lemma of the shape "if with transcendental over then ". That is worth splitting off as a child in its own right; it is reusable well beyond this mission.A -packing in a graph is a collection of pairwise vertex-disjoint paths on three vertices. Determining the largest such packing is NP-hard even in restricted graph classes, so structural hypotheses that force an optimal packing are of independent interest in graph factor theory. The present question asks whether 3-vertex-connectivity and cubicity force the strongest possible packing whenever the vertex count permits a perfect partition.
A. Kelmans attributes the broader packing problem to 1984. In Problem 1.10 of Packing 3-vertex Paths in Cubic 3-connected Graphs, the question is whether every cubic 3-connected graph satisfies . Theorem 3.1 of that paper proves that the divisible-order factor statement is equivalent to several apparently stronger deletion and prescribed-edge statements; it does not prove the open claim itself. OPG-46613 records the divisible-order form targeted here.
A 2026 candidate analysis in the Vibe Mathing problem repository investigated a tempting sufficient route: find a perfect matching whose complementary 2-factor has every cycle length divisible by three. Candidate C01 explains why that condition would yield a -factor. Candidate C02 gives an explicit proposed family of order that has -factors but is claimed not to satisfy the stronger matching condition. These candidate claims have computational and partial Lean checks, but no complete Lean kernel proof; they are milestones here, not declarations that the original problem or the candidate family has already been formally established.
All graphs are finite and simple. A graph is cubic when every vertex has exactly three neighbors. It is 3-vertex-connected here when it has at least four vertices and deleting any set of at most two vertices leaves a connected induced graph.
A -factor is represented by a natural number , together with a bijection
such that, in every block, positions and are adjacent and positions and are adjacent. The path is not required to be induced: an ambient edge between positions and is allowed because the two selected path edges still form a copy of .
A 2-factor is a spanning 2-regular subgraph. It is called divisible when every one of its connected components has order divisible by three. A divisible matching complement is a perfect matching such that the relative complement is a divisible 2-factor.
The explicit graph is defined on . Its first nine vertices form the fixed Petersen-minus-one-vertex brick from C02; the remaining vertices form the stated cycle-and-opposite-chord brick with three joining edges. The full adjacency relation is part of the Lean definition rather than an external data file.
For every finite simple graph ,
This is the OPG-46613 target. Cubicity forces the order to be even, so within this domain divisibility by three is equivalent to divisibility by six.
The mission also formalizes the part of Kelmans's Theorem 3.1: the divisible-order factor claim is equivalent to the assertion that deleting any specified 3-vertex path leaves a -factor. Two route lemmas state that divisible 2-factors split into -factors and that, in cubic graphs, divisible 2-factors are equivalent to divisible perfect-matching complements.
The C02 milestones ask first for the complete 18-vertex statement and then for the full family:
This separates a sufficient method from the root conclusion. It is not a counterexample to OPG-46613 because every in the proposed family explicitly satisfies the desired conclusion.
A proof of the main goal would settle the divisible-order form of a long-standing path-packing problem. Through Kelmans's equivalences it would also control several deletion and prescribed-edge variants for cubic 3-connected graphs. A disproof would require a graph satisfying all domain hypotheses but lacking a -factor; the C02 family does not claim this.
Formalizing the candidate boundary is useful even before the root is resolved. It turns a route exclusion into a checkable theorem and prevents a search campaign from silently assuming that every relevant graph possesses a divisible complementary 2-factor. The definitions of noninduced -factors, vertex connectivity by deletion, perfect matchings, 2-factors, and component-order divisibility are intended to be reusable in later graph-factor work.
The perfect-matching route is attractive because the complement of a perfect matching in a cubic graph is 2-regular. The obstruction is that its cycles need not have lengths divisible by three. The C02 candidate family is designed to expose exactly that gap: a persistent 5-cycle is claimed to occur in every complementary 2-factor even though an unrelated -factor exists. Consequently, proving the main theorem cannot simply assume that a favorable perfect matching always exists.
The formal difficulty is also semantic. Connectivity must mean vertex connectivity, the complement must be relative to on the same vertex set, component sizes must refer to the 2-factor rather than the ambient graph, and must remain noninduced. Weakening any of these points can create a materially different or vacuous theorem.
The development targets Lean 4.33.1 and Mathlib revision 0df444a360eaa60ab8c11dca51a86af692955474. Graphs use SimpleGraph on finite vertex types. Degree is the cardinality of the actual neighbor subtype. Three-vertex-connectivity explicitly quantifies over all finite deletion sets of cardinality at most two and includes a four-vertex order guard.
The main theorem is universe-polymorphic and does not hard-code a finite graph enumeration. The family includes . The factor structure uses a bijection, so disjointness and coverage cannot be discharged by duplicate or omitted vertices. Ambient chords do not invalidate a block, while both required consecutive adjacencies must be genuine graph edges. The candidate family statements remain open theorem goals ending in sorry; the shared definition module itself is sorry-free.
Welcome contributions include proofs of the model lemmas, the finite statement, the general C02 family, Kelmans's equivalence, or decompositions of the root theorem into faithful reusable lemmas. Numerical enumeration alone is supporting evidence and should not be presented as a kernel proof.
14b8dc64ac2d89c98cf3a2bbb2fcba76ced0df6a. https://github.com/vibemathing/problem-opg-46613-cubic-p3-partition/blob/14b8dc64ac2d89c98cf3a2bbb2fcba76ced0df6a/research/artifacts/candidates/opg46613-c01/proof.md14b8dc64ac2d89c98cf3a2bbb2fcba76ced0df6a. https://github.com/vibemathing/problem-opg-46613-cubic-p3-partition/blob/14b8dc64ac2d89c98cf3a2bbb2fcba76ced0df6a/research/artifacts/candidates/opg46613-c02/proof.mdThe smooth four-dimensional Poincaré conjecture asks whether a smooth manifold with the topology of the four-sphere must also have its standard smooth structure, up to diffeomorphism. The distinction is between the existence of continuous coordinates and the compatibility of differentiable coordinates. The mission concerns this precise sphere question, listed as open in Problem 4.1 of K3 — A New Problem List in Low-Dimensional Topology. It does not treat a collection of algebraic obstructions as an existing proof of the conjecture. Baykur–Kirby–Ruberman, Problem 4.1
Let be the unit sphere in , with its standard stereographic smooth structure. A homeomorphism is a continuous bijection with continuous inverse; a diffeomorphism is a smooth bijection with smooth inverse. A smooth atlas is a collection of local Euclidean coordinates whose transition maps are smooth.
The manifold is compact and Hausdorff, has no boundary, and is equipped with a specified smooth atlas modeled on . The given atlas is arbitrary: it is not defined by transporting the standard structure from .
For a homeomorphism , let denote the atlas transported from the standard sphere along . A structomorphism for the smooth structure groupoid is a homeomorphism whose coordinate expressions belong to that groupoid. The predicate requires, for every given smooth atlas on such an and every such , a structomorphism between and . It does not require that structomorphism to be the identity. These are the conventions of the source definitions, not additional uniqueness assumptions. [Shin, SPC4.lean, lines 53–81 and 211–221]
For every manifold with the preceding hypotheses, the goal is
This is the source predicate . Its conclusion asserts the existence of a diffeomorphism; it does not assert that a particular supplied homeomorphism is smooth.
The atlas formulation has the exact equivalence
The source supplies a proof of this equivalence without invoking Freedman's theorem or assuming the conjecture as an unconditional fact. It is a reformulation, not a solution. Its foundations include the correspondence
where is the smooth coordinate-change groupoid for the common model. [Shin, SPC4.lean, lines 334–365; Bridge.lean]
Write for the following compact Hausdorff, boundaryless instance of Freedman's topological theorem:
where denotes homotopy equivalence and only topological manifold charts are assumed. This is established mathematics, but a proof in the present formal development remains a target. If denotes the analogous smooth conclusion from a homotopy equivalence, the relation to the main goal is recorded with its hypothesis visible:
Explicit standard-disk foundations form another track. For every , they concern the manifold-with-boundary structure on , its boundary set , and the smooth collar
The collar is a closed embedding, has image
and satisfies , using the boundary inclusion. Its image is a neighborhood of every boundary point in the disk. A companion interface characterizes a map from a manifold with corners into the disk as precisely a continuous map whose inclusion into Euclidean space is . These targets concern the actual disk smooth structure. [Shin, Disk.lean, lines 1076–1141 and 1263–1318]
For each integer , let be the closed unit disk in and let be any homeomorphism of its boundary. The twisted double identifies the boundary point in a left copy of the disk with in a right copy. With the quotient topology, the target is
This statement is published as SP4Gluing.twistedSphere_homeomorphic. The theorem and its supporting continuity and injectivity lemmas have accepted Lean proofs contributed by carlok. All three accepted proofs have also been checked locally with their proved dependencies. It concerns these explicit topological quotients, not arbitrary homotopy spheres or a prescribed smooth structure.
For every regional chart base point, the open-bicollar and left-interior transitions are smooth in both directions. Right-interior-to-seam smoothness requires smooth ; the reverse requires smooth . The single compatibility target concerns exact overlap sources, combining four source results internally. It provides neither a global smooth-manifold instance nor smooth standardness. [Shin, Hemisphere.lean, lines 2439–3577]
A proof of the main goal would identify every smooth structure in its stated sphere class with the standard one, up to diffeomorphism. A proof of the transported-atlas equivalence instead locates the same unresolved comparison in a different formal language. The distinction matters: constructing a smooth structure by transport is not the same as identifying an arbitrary pre-existing one.
The bridge, explicit disk atlas, and stated collar properties have accepted kernel-checked Lean proofs. The clean atlas equivalence also has a proof with no admitted theorem among its axioms. The conjecture remains open, and Freedman's topological theorem remains unproved in this formal development despite its published mathematical proof.
The topological two-disk gluing result identifies the homeomorphism type of these quotients for every boundary homeomorphism and every disk dimension at least one. The accepted formalization supplies a global topological comparison for this explicit quotient. It does not resolve the comparison with a prescribed smooth structure or recognition of general smooth four-manifolds.
Four supporting algebraic tracks concern orbit coinvariants, homology dimension budgets, finite-support shift rigidity, and Laurent-polynomial positivity. Their source results arose in route-specific obstruction studies. As of 6 September 2026, all eleven theorem targets in these algebraic tracks have accepted Lean proofs. The five additional formal proofs were contributed by wamlart: orbit augmentation, region homology budgets, two-corner homology budgets, the Laurent mass threshold, and mass-two positivity. No theorem currently connects their completion to a proof or disproof of . They are exploratory tools, not established milestones in a proof of the main goal.
A homeomorphism can transport the standard atlas, but that observation does not compare the transported atlas with the one already specified on the manifold. Treating those two atlases as equal would remove the central mathematical question by changing its hypotheses.
Likewise, topological recognition does not supply a smooth recognition theorem. Standard disk and collar constructions establish local models; they do not establish a smooth gluing or recognition theorem for an arbitrary prescribed smooth structure, a recognition theorem for arbitrary smooth balls, or a smooth Schoenflies theorem. The missing global comparison cannot be replaced by successful finite algebraic tests or by constructing a standard local chart.
The sphere goal quantifies over Type in universe zero, exactly as in the source. It uses real four-dimensional Euclidean chart models, compactness, the Hausdorff condition, and smoothness of order . Boundaryless manifolds are built into that model. No orientation, fixed parametrization, or identity-map uniqueness is imposed.
The geometric foundations use charted spaces, structure groupoids, models with corners, homotopy equivalences and diffeomorphisms. Disk results include every , so their dimensions are . The boundary-set identification does not by itself construct a general induced smooth boundary structure. Nor is smoothness asserted for a radial clamp across its nonsmooth locus.
The separate source assertion SPC4Ball is not treated as equivalent to the sphere goal: the required formal boundary, capping and gluing bridge is absent. The transported-annulus product diffeomorphism is not a current target; its chart instances serve only as constructor support. No unconditional implication is taken through the source's admitted Freedman declaration. Gaussian coupling, transport defects, partition incidence and merge-score results remain outside this mission because no mathematical dependency on them has been established.
R. İnanç Baykur, Robion C. Kirby and Daniel Ruberman, eds., K3 — A New Problem List in Low-Dimensional Topology, Mathematical Surveys and Monographs 295, American Mathematical Society, 2026, Problem 4.1, pp. 191–192. Author PDF.
Michael Hartley Freedman, The topology of four-dimensional manifolds, Journal of Differential Geometry 17 (1982), 357–453, Theorem 1.6, p. 371. DOI; primary-article scan.
Stephen Smale, Generalized Poincaré's Conjecture in Dimensions Greater Than Four, Annals of Mathematics 74 (1961), 391–406, Theorem A. DOI; primary-article scan.
Ryan Shin, SPC4.lean, Bridge.lean and Disk.lean, unpublished source files, 2026; no public manuscript URL available. SHA-256, respectively: b17fdb932034e5211d0db8171c08e2b3a182016bceaecdd2deb49c39d6bfd5cc, e8ea6b66f6bd675ca272e862e0825ab2db1f8bb792eaffe1b9e8f5d89024d302, 889a9eccf9d2350aee7051ab7b6895e565f9f1a0c84e7120fb45c15acae0097e.
Ryan Shin, Hemisphere.lean, unpublished Lean source file, 2026, declaration twistedSphereHomeoSphere; source SHA-256 c48843d2c4ec6987acfd7f7ab3a92bfed990376206142e74712795b4e9399828. Published topological two-disk gluing target; the recovered local construction is checked; the accepted proof and its two supporting lemmas were contributed by carlok.
Two orthonormal bases of C^d are mutually unbiased when every transition amplitude has squared modulus 1/d. At most d+1 such bases can coexist, and complete families are known in prime-power dimensions through finite-field constructions. Dimension six is the smallest famous composite case where existence of the complete seven-base family remains unknown.
This mission turns CUHK-Shenzhen AI Math Problem 16, Existence of complete sets of mutually unbiased bases, into an auditable Lean campaign. The objective is not merely to transcribe notation: it is to expose the mathematical model, the capstone, and a smaller attack surface as separate artifacts that other formalizers can inspect and reuse.
Construct seven 6 by 6 unitary-column matrices whose every distinct pair has all transition amplitudes of squared modulus 1/6. The baseline milestone constructs three pairwise mutually unbiased bases, a known lower bound that tests all matrix conventions.
Solving this target would settle the precise finite or analytic core represented by the Lean statement and would create reusable infrastructure in quantum information theory, mutually unbiased bases, finite fields, Hilbert spaces. Even a rigorous disproof is valuable: several entries in this collection deliberately ask whether an attractive extrapolation is true, and Lean forces a counterexample to satisfy every side condition. The mission therefore treats theorem proving and model criticism as equally legitimate research outcomes.
The equations are a large coupled system of polynomial equalities over complex phases, modulo substantial gauge symmetry. Numerical near-solutions do not certify exact existence, while nonexistence would require a global obstruction beyond currently known bounds. Dimension six lacks the finite-field structure that supplies complete prime-power constructions.
Formalize standard gauge reductions: fix the first basis to the identity and dephase transition Hadamard matrices. Verify a three-basis tensor-product construction. Then encode additional bases through complex Hadamard matrices and study algebraic constraints, Gröbner-style eliminations, semidefinite bounds, or exact certificates. Computational searches may guide conjectures, but uploaded proofs must convert numerical evidence to exact algebraic identities or certified inequalities.
The Lean target is exact: column orthonormality is U-adjoint times U equals identity, and mutual unbiasedness uses Mathlib complex norm squared. Seven bases are indexed by Fin 7. No quotient by phase, permutation, or global unitary is built into the statement, since these symmetries preserve the predicate and can be used within proofs.
The natural-language source remains authoritative for motivation, while the Lean declaration is authoritative for what Prove2Me will verify. The mission description calls out restrictions where the current formal target is a finite-dimensional core, a fixed interpretation of informal terminology, or one sharpened subquestion from a broader classification problem. Those restrictions should not be silently generalized in a proof claim.
Publish an exact three-basis construction in dimension six, then formalize dephasing and obstruction lemmas for extending a partial family.
The capstone is marked as the mission's main item and is never duplicated as a milestone. Definitions precede theorem statements in the proposal order. A milestone is considered complete only when its own exact statement is proved; proving a nearby theorem with stronger-looking prose but mismatched quantifiers, signs, supports, dimensions, or asymptotic constants does not complete it.
The CUHK-Shenzhen AI Math Problems page added this problem on June 23, 2026. At the drafting date, August 31, 2026, the status and target corrections described above were checked against the source page and the cited primary material.
A contribution may prove the displayed theorem or refute it by constructing data satisfying every Lean hypothesis while negating the conclusion. Informal changes of model do not count: any proposed correction must be submitted as a separately reviewed statement with an explanation of which source ambiguity or false implication it repairs. Definitions must remain computational or mathematically constrained; fields that simply assume the desired conclusion are not acceptable. Every proof must compile against the mission's pinned Mathlib revision, use no sorry, and expose a top-level theorem solution when submitted to Prove2Me.
The main theorem is intentionally separated from a smaller milestone. Contributors should preserve that dependency order, publish reusable lemmas rather than monolithic tactics, and report whether a lemma is analytic, algebraic, combinatorial, or infrastructure-only. Numerical evidence, external computer algebra, and exhaustive search are welcome for discovery, but a final certificate must be replayable by Lean. If an external result is invoked, its hypotheses must be represented in the formal statement or proved in the dependency tree.
The files were built locally with Lean 4.30.0 and Mathlib revision c5ea00351c28e24afc9f0f84379aa41082b1188f, the supported Prove2Me environment at drafting time. The mission definition file is ordered before all theorem files, and each theorem imports exactly that public definition module or Mathlib. Independent blind read-backs accompany the draft items so reviewers can compare what the Lean code literally says with this mathematical description. Human confirmation remains required before the public proposal can be submitted for moderation.
Pontryagin's principle as presented by Luenberger is the decisive necessary condition in continuous-time optimal control. It converts an optimization over functions into a pointwise comparison of a Hamiltonian, coupled to the original state equation and a backward costate equation. Luenberger derives the minimum-Hamiltonian convention from vector-space multiplier ideas and a first-order comparison principle. Formalization is especially valuable here because the printed theorem contains a standard but consequential regularity oversight: it asserts a condition at every time even though controls are only piecewise continuous and the cost is an integral. This mission preserves the intended theorem while replacing that false pointwise claim by the mathematically canonical almost-everywhere statement.
Fix t₀ < t₁, a finite-dimensional Euclidean state space OCState n, a Euclidean control space OCControl m, and a permitted-control set Omega. A state-control pair (x,u) is admissible when x t₀ = xInit, the state is absolutely continuous on the interval, the control is almost everywhere strongly measurable and lies in Omega almost everywhere, the differential equation x' = F(x,u) holds almost everywhere in the interior, and the running cost is interval integrable. An optimal pair globally minimizes the interval integral among all admissible pairs.
The dynamics F and running cost ell are continuous jointly in state and control and continuously differentiable in the state variable. Their state derivatives Fx and ellx vary continuously. A global Lipschitz estimate controls changes of F in both state and control. Because an a.e. measurable control need not be bounded, the optimal control is explicitly assumed to have an a.e. norm bound on the compact interval, matching the boundedness inherited from the source's piecewise-continuous model. The operator-valued paths Fx (x₀ t) (u₀ t) and ellx (x₀ t) (u₀ t) are also assumed interval integrable along the optimum. Together these hypotheses provide the measure-theoretic regularity needed for the adjoint and state perturbations. The Hamiltonian uses Luenberger's minimum convention,
The root VectorSpaceOpt.pontryagin_minimum_principle asserts the existence of an absolutely continuous costate lambda with terminal value lambda t₁ = 0. Almost everywhere it satisfies the weak inner-product form of
and almost everywhere on the control interval it satisfies
Two milestones capture source dependencies. control_state_lipschitz_estimate is the Grönwall stability estimate used on p. 263 to control the state response by the integral distance between controls; it explicitly assumes interval integrability of both the state-difference norm and the control-difference norm, so Mathlib's totalized integral cannot hide a nonintegrable input. adjoint_lagrangian_comparison formalizes §9.6, Proposition 1: under an implicit state equation, differentiability in the state, Lipschitz dependence of the state solution, and an adjoint identity, the objective difference agrees with a frozen-state Lagrangian difference up to an explicit filter-level little-o remainder.
This is the flagship analytic mission of the continuation. It connects finite-dimensional differential calculus, Bochner integration, absolute continuity, ODE constraints, adjoints, and localized control variations in one reusable theorem. The definitions form a minimal control framework that can support terminal costs, endpoint constraints, and alternative maximum-principle conventions later. The corrected a.e. conclusion also demonstrates a central benefit of formalization: informal conventions about representatives of controls and isolated time values must be resolved before a theorem can be accepted.
The weak inner-product adjoint equation avoids introducing a coordinate transpose and remains invariant under the Euclidean-space representation. That choice makes the result immediately reusable in later vector-space treatments of transversality and endpoint multipliers.
The difficulty is very high. Mathlib supplies finite-dimensional calculus, interval integration, absolute continuity, measure-theoretic almost-everywhere statements, and Grönwall tools, but not an assembled Pontryagin framework. The mission must coordinate a state-solution stability estimate, state differentiability of the dynamics and cost, existence and regularity of the backward costate, and Hamiltonian comparison against arbitrary admissible values. The control is measurable rather than globally continuous, so every pointwise expression must be placed under an a.e. quantifier where appropriate. The proposition milestone additionally requires a precise little-o interface instead of an unnamed asymptotic remainder.
The proposal covers §9.6, Proposition 1 and Theorem 1, with the regularity inherited from the surrounding discussion made explicit. Both the optimal state and the costate are absolutely continuous. Admissible controls are a.e. strongly measurable, which is a broader measure-theoretic proxy for the source's piecewise-continuous controls and is compatible with integral objectives; the root additionally requires the optimal control to be essentially norm bounded on Icc t₀ t₁, restoring the compact-interval boundedness used by the source. The maps F, ell, Fx, and ellx are jointly continuous; state derivatives are supplied by HasFDerivAt; a uniform Lipschitz bound is stated; and both derivative coefficients along the optimal path are interval integrable. The separate Grönwall milestone requires its state and control norm differences to be interval integrable. The interval is required to have positive length.
There is a documented source erratum. The sentence on printed p. 263 states Hamiltonian minimality for every t, while the proof on p. 264 chooses a neighborhood on which a purported strict violation persists. That step requires continuity at the selected time. Moreover, changing a piecewise-continuous control at a single isolated time changes neither its a.e. class, the state equation, nor the integral cost. Therefore no condition can be forced at an arbitrary jump value. The Lean root uses an a.e. conclusion on Icc t₀ t₁; an alternative source-faithful repair would assert the inequality at every continuity point of u₀. The mission does not claim existence of an optimal pair, compactness of Omega, endpoint constraints, nonsmooth dynamics, or a sufficiency theorem.
The simplex method walks along edges of a polytope from vertex to vertex. Whether any pivot rule could ever make that walk short in the worst case is governed by a prior, purely geometric question: how far apart, in the edge graph, can two vertices of a polytope be? Warren Hirsch conjectured in 1957 that the diameter of a -dimensional polytope with facets is at most . Half a century of upper bounds stalled at quasi-polynomial, and Santos disproved the conjecture itself in 2012 — but only by a constant factor. The surviving question, the subject of the Polymath 3 project, is the polynomial Hirsch conjecture: is the diameter bounded by a polynomial in and ?
Work in . An H-polytope is a set cut out by finitely many linear inequalities: given vectors and reals , it is
where is the standard inner (dot) product — so each condition is one linear inequality, with normal vector and offset . Throughout, is assumed nonempty and bounded. The parameter counts the inequalities in the given description; since every polytope with facets admits a description by exactly inequalities, bounds stated in terms of over all descriptions are equivalent to bounds in terms of facet counts.
A vertex of is an extreme point. Two vertices are adjacent when the segment is an extreme subset of ; for a polytope the convex extreme subsets are exactly the faces, so this says precisely that is a one-dimensional face — an edge. The combinatorial diameter of is the diameter of the graph of vertices and edges. Throughout, "diameter at most " is expressed as: every two vertices are joined by a walk of steps, each step staying put or crossing an edge — a form that is monotone in and asserts connectivity of the graph (Balinski's theorem) as part of the claim.
Every polynomial in and is dominated by some and conversely, so this is exactly polynomiality, with no committed degree — the form that survives any future sharpening of constants or exponents.
Six classical results over the same definitions: the Hirsch bound in dimension (Klee; Klee–Walkup); Larman's bound ; Naddef's bound for -polytopes; the Kalai–Kleitman bound ; Todd's bound for full-dimensional with ; and — in the other direction — the Santos counterexample: a nonempty bounded H-polytope whose diameter exceeds .
A polynomial diameter bound is necessary for any pivot rule of the simplex method to run in polynomial time in the worst case: if vertices can be super-polynomially far apart, no edge-following algorithm can connect them quickly. A refutation would close off one of the main hoped-for routes to a strongly polynomial linear programming algorithm (Smale's ninth problem). The conjecture is also the test question of polyhedral graph theory: the Kalai–Kleitman argument uses so little about polytopes that it holds for far more general set systems, and Eisenbrand, Hähnle, Razborov, and Rothvoß (Math. OR 2010) showed such abstractions admit almost-quadratic lower bounds — so a proof of the conjecture must use geometry the abstract setting lacks, and a disproof must beat the abstraction barrier's constructions with actual polytopes.
None of these results has been formalized in any proof assistant; Mathlib has extreme points and faces of convex sets, but no polytope combinatorics — no vertex-edge graph, no diameter, no facet counting. This mission builds that layer: an H-polytope model, adjacency via faces, and walk-based diameter bounds, against which both the upper-bound ladder and the Santos disproof can be machine-checked. The Kalai–Kleitman proof is one page from first principles and is the natural summit; the Santos construction is a concrete finite object whose verification is a different, computational kind of challenge.
The naive approach — walk toward the target vertex by always improving some linear objective — is exactly the simplex method, and proving any polynomial bound on such walks is open for every known pivot rule; monotone variants of the diameter question have exponential lower bounds. The obvious inductive strategy (bound the diameter by recursing on facets) is precisely what Kalai–Kleitman optimizes, and it provably cannot go below quasi-polynomial without using metric or topological properties of actual polytopes, by the abstraction lower bound above. On the other side, making diameters large is blocked by the wedge/spindle calculus only producing constant-factor violations. The problem sits in a genuine gap: no technique on either side is known to reach polynomial.
The Lean model commits to: ambient space EuclideanSpace ℝ (Fin d); the polytope as Hpoly a b = {x | ∀ i, ⟪a i, x⟫ ≤ b i} for a : Fin n → EuclideanSpace ℝ (Fin d), b : Fin n → ℝ, with nonemptiness and Bornology.IsBounded as explicit hypotheses (boundedness is essential: Klee–Walkup's unbounded counterexample would otherwise trivialize the Santos milestone); vertices as Set.extremePoints ℝ; adjacency as u ≠ v ∧ IsExtreme ℝ P (segment ℝ u v); and diameter bounds as the walk predicate DiamLE, whose stationary steps make it monotone in the bound. Real-exponent bounds enter through Real.logb and the natural floor. In larman_bound and the two Hirsch-form bounds the subtraction is natural-number (truncated) subtraction, which only weakens nothing: the stated forms are true as written for all in scope. The dimension parameter is the ambient dimension; lower-dimensional polytopes are included, and every milestone is stated so as to remain true for them, with todd_bound requiring full-dimensionality ((interior P).Nonempty) as in its source.
Welcome contributions: any milestone in any order (dimension_three_bound for cases and structural lemmas about Adj and DiamLE are natural entry points, and kalai_kleitman_bound is the summit); reusable infrastructure — polytopes have finitely many extreme points, faces of H-polytopes, Balinski connectivity — published as platform theorems; and, as a separate expedition, the explicit Santos or Matschke–Santos–Weibel polytope. Statements about unbounded polyhedra, the simplex method itself, and subexponential pivot rules are left to future missions.
AI generated but i think correct. I think the milestones make it really annoying but the central theorem looks correct.
The matrix-multiplication exponent measures the asymptotic number of field operations needed to multiply two square matrices. A bound means that, for every , two matrices can be multiplied using arithmetic operations. Matrix multiplication is a central benchmark in algebraic complexity and a primitive for many algorithms in linear algebra, graph theory, and symbolic computation.
After Strassen showed that , a sequence of tensor constructions reduced the exponent further. Schönhage's asymptotic sum inequality made it possible to exploit simultaneous matrix products rather than a single square product. In 1990, Don Coppersmith and Shmuel Winograd combined an explicit low-border-rank tensor with a block extraction argument based on Salem--Spencer sets. Their basic analysis gave ; coupling the random weights in the tensor square sharpened this to , hence the exact rational consequence .
This mission formalizes that historical Coppersmith--Winograd result. It follows the source tensor and its actual block restrictions, while excluding placeholder “laser values” that are not backed by extracted direct sums of matrix-multiplication tensors.
For a field , an order-three tensor is represented by three finite-dimensional -vector spaces and an element of their tensor product. The matrix-multiplication tensor
encodes multiplication of an matrix by a matrix. A restriction applies one linear map to each tensor leg. A degeneration permits those maps to depend polynomially on a formal parameter and selects their first nonzero coefficient. Thus a degeneration from the diagonal tensor is a border-rank certificate .
The Coppersmith--Winograd tensor with parameter is
It has border rank at most . Its coordinates carry three classes, indexed by , and its six nonzero block types are
The first three blocks are matrix-multiplication tensors with dimensions , , and ; the other three are scalar products. Tensor powers therefore contain many typed rectangular matrix products. The laser method selects a large family with disjoint coordinate blocks and applies Schönhage's asymptotic sum inequality to all surviving products simultaneously.
For every field ,
The Lean goal has the same quantified proposition and the same matMulExp definition as the existing Schönhage-bound mission; only the theorem identifier and rational endpoint change.
The development records the characteristic-free order-three degeneration
and the exact matrix-product dimensions associated with every supported type sequence in . These statements identify the algebraic input before any asymptotic counting is used.
For , the tensor-square grading and the coupled-weight pruning must produce the direct sums and asymptotic inequality stated in Section 8 and in the coupled-constituent lemma on journal pp. 270--272. The final numerical milestone certifies the rational endpoint from exact inequalities, rather than treating the decimal as a proof object.
The result was the strongest matrix-multiplication bound for roughly two decades and introduced the tensor family that underlies the classical laser-method line of work. A formal proof supplies a checked bridge from an explicit border-rank identity to an exponent bound whose combinatorial extraction is substantially more delicate than the earlier Schönhage examples.
The formalization also produces reusable infrastructure. The order-three CW degeneration is an explicit polynomial-family test case over arbitrary fields. The six block identifications and type-count formulas can be reused in analyses of tensor powers. A faithful extraction predicate, stated through actual restrictions to direct sums of MMObj tensors, separates sound laser arguments from formulas that count incompatible or coordinate-sharing blocks as independent.
The mathematical bound is known. The open work is its machine-checked reconstruction in Lean. The border-rank theorem, per-type matrix-product restriction layer, tensor-square support invariant, balanced block calculation, Salem--Spencer set theorem, and exact numerical endpoint are already proved. The unrestricted value/rank bridge, the coupled-constituent extraction, and the full Section 8 auxiliary inequality remain the substantive frontier.
The main difficulty is not expanding or evaluating a decimal logarithm. A tensor power contains exponentially many typed terms, but most share variables. They cannot all be placed in a direct sum, and counting all joint type sequences overestimates the usable matrix products. The source hashes coordinate blocks into a large progression-free set and prunes collisions so that the surviving blocks are genuinely independent.
The improvement adds a second layer. It begins with , regroups variables into five classes, couples weights that were independent in the simpler analysis, and estimates a nontrivial central block by a further extraction. A formal proof must track the direction of every restriction, the exact multiplicities of all block types, and the loss introduced by pruning. Replacing exponential surviving-block counts by a polynomial number of blocks, or using joint entropy without the marginal compatibility constraints, changes the mathematical claim and is outside the mission.
The mission uses the existing TensorObj, MMObj, TensorObj.Restrict, Degenerates, tensorAsymptoticRank, matMulExp, and matMulExp_strassen declarations in the Mathlib environment pinned by the earlier matrix-multiplication mission. Tensor dimensions and type counts are natural numbers; exponent and optimization inequalities are real-valued. All top-level bounds quantify over an arbitrary field, matching the integral polynomial identities used by the construction.
Laser statements must exhibit, directly or through a faithful reusable predicate, restrictions from a tensor power to a finite direct sum of concrete matrix-multiplication tensors. The number and dimensions of the summands remain part of the witness. A constant-valued “laser functional,” a vacuous witness hypothesis, or a capacity definition that discards the exponential number of surviving blocks does not satisfy the mission.
Welcome contributions include restriction composition lemmas, tensor-power block equivalences, multinomial and entropy estimates with all marginal constraints, formal Salem--Spencer pruning, exact real-inequality certificates, and the coupled central-block value lemma. Every milestone should cite the corresponding equation, table, or lemma in the primary paper.
The whole series so far lived in discrete time on finite state spaces. Chapters 20–21 of Levin–Peres–Wilmer, Markov Chains and Mixing Times (AMS, 2009) lift both restrictions. Running the jumps of a chain at the arrivals of a rate-one Poisson clock produces the continuous-time chain, whose transition semigroup — the heat kernel — converges to stationarity for every irreducible chain, with no aperiodicity hypothesis: continuous time washes out periodicity. On countable state spaces, existence of a stationary distribution is no longer automatic, and the trichotomy of transience, null recurrence, and positive recurrence replaces it; the convergence theorem survives exactly on the positive-recurrent class. The chapter's crown jewel — and this mission's goal — is Pólya's theorem: simple random walk on the lattice is recurrent in dimensions one and two and transient in dimension three and higher. "A drunk man will find his way home, but a drunk bird may get lost forever."
Continuous time (Ch. 20). For a finite chain , the heat kernel at time is defined by Poissonization,
the law at time of a walk taking -steps at Poisson arrival times ( as a matrix exponential). With , the continuous distance and mixing time are and . The lazy version of a discrete chain is ; from Mission VII, the spectral gap is with the largest eigenvalue . The product chain on a product of coordinate spaces picks a uniform coordinate and updates it by that coordinate's chain.
Countable state spaces (Ch. 21). A chain on a countable state space is a function with nonnegative entries and rows summing to one (as convergent series); -step probabilities are defined recursively, and trajectory probabilities are countable sums of path weights. The first return time to is ; a state is recurrent when (tails tend to zero), positive recurrent when moreover (tails summable), and null recurrent when recurrent but not positive recurrent. A stationary distribution is a nonnegative summing to one with (as convergent series). Simple random walk on steps from to one of its nearest neighbours uniformly at random.
Pólya's theorem (§21.2, Examples 21.8–21.9), the capstone of Chapters 20–21:
The results. Theorem 20.1 explains why laziness and aperiodicity pervade the discrete theory — periodicity is an artifact of the discrete clock. The product-chain theorem 20.7 is the cleanest instance of the paradigm (independent coordinates mix in relaxation time ) and the template for the hypercube cutoff of Mission XI. Chapter 21's trichotomy is the backbone of applied Markov chain theory — queueing, branching, renewal — and Kac's lemma with the convergence theorem 21.14 is the standard equipment of any probability course. Pólya's theorem is one of the most celebrated results of twentieth-century probability, the birth of the random-walk-in-dimension- paradigm.
Formalizing them. Mathlib has no continuous-time Markov chains, no Poissonization, and no recurrence/transience theory (its PMF random walks stop far short). The countable-state layer built here — summable stationary equations, tail-sum return times, the recurrence dichotomy — is the missing infrastructure for formalized applied probability; Pólya's theorem is a famous target in its own right, and the half has never been formalized in any assistant to our knowledge.
The heat kernel is an infinite series of matrices: convergence (dominated by the Poisson weights), the semigroup property, and the interchange of the series with matrix products and limits must all be established by hand over tsum. Theorem 20.1 avoids aperiodicity by the number-theoretic fact that the Poisson distribution smears over residue classes — formally, the continuous chain is automatically aperiodic because for . The product-chain bounds need the machinery of Mission VII applied coordinatewise and a careful union bound; the lower bound is a Gaussian-free second-moment argument. On the countable side, everything is series bookkeeping in the absence of Fintype: the recurrence dichotomy is a generating-function (renewal) identity handled through partial sums; Kac's lemma is a mass-transport double-count over trajectories; and Theorem 21.14 needs an aperiodicity-based coupling on a countable product space, the technical summit of the mission. Pólya's theorem itself combines a local central-limit-type estimate for the return probabilities (, obtained by Stirling in and by a comparison argument in higher dimension) with the dichotomy of Proposition 21.3.
Chapter 20 lives on finite state spaces: the heat kernel is a tsum over of Poisson weights times matrix powers (summability is provable, not assumed), continuous distance is a supremum over states, and the continuous mixing time is an sInf over nonnegative reals (junk if the set were empty — excluded under the theorems' hypotheses). Discrete-vs-continuous comparison (Theorem 20.3) is stated with eventual thresholds (), matching the book's asymptotic phrasing. Chapter 21 lives on a Countable type: stochasticity and stationarity are HasSum statements, -step powers are defined recursively with tsum convolutions, return-time tails are countable sums of path weights over finite horizons, and recurrence/positive recurrence are the tail-limit and tail-summability conditions above — measure theory never enters. Pólya's theorem is stated for the origin of with the walk defined by nearest-neighbour steps; the and halves are separate conjuncts of one statement.
How fast does a Markov chain forget its starting point? For a reversible chain the complete answer is coded in the eigenvalues of its transition matrix: the largest eigenvalue is always , and the size of the gap between and the rest of the spectrum is the chain's fundamental time constant — a large gap means fast mixing, a small gap means slow mixing. Chapters 12–13 of Levin–Peres–Wilmer, Markov Chains and Mixing Times (AMS, 2009) develop this spectral theory and culminate in the discrete Cheeger inequality of Jerrum–Sinclair and Lawler–Sokal, which says that the spectral gap (an analytic quantity, defined below) and the bottleneck constant (a geometric quantity from Mission IV, also recalled below) control each other:
A chain mixes rapidly exactly when its state space has no bottleneck. This inequality is the backbone of the Markov-chain approach to approximate counting and of spectral graph theory at large; alongside it the chapters provide Wilson's method — the sharpest general technique for mixing-time lower bounds — and the comparison machinery that transfers spectral estimates between chains.
All chains live on a finite state space . A chain with transition matrix and stationary distribution is reversible when the detailed balance equations hold; reversibility is the standing assumption of both chapters. The yardsticks of the series are the total variation distance , the worst-case distance to stationarity , and the mixing time , with ; we write .
The spectral vocabulary: an eigenfunction of is a nonzero with , where ; the number is then an eigenvalue. Out of the spectrum one forms
Functions on carry the weighted inner product — the geometry, denoted , in which a reversible is self-adjoint — and the Dirichlet form
the average squared variation of along the chain's transitions. Finally, from Mission IV: the bottleneck ratio of a set of states is , the conditional probability at stationarity of escaping in one step, and the bottleneck constant is .
Theorem 13.14, the discrete Cheeger inequality: for a reversible irreducible chain,
The results. Theorems 12.3–12.4 sandwich the mixing time between and — the fundamental equivalence of spectral and mixing estimates for reversible chains, prerequisite for the cutoff criterion of Mission XI. The Cheeger inequality converts isoperimetry into spectral bounds; it is the mathematical core of the Jerrum–Sinclair program of polynomial-time approximate counting, and its graph version underlies expander theory. Wilson's method produced the sharp lower bounds for adjacent transpositions and hypercube-type chains; the comparison lemma is the engine behind the shuffle bounds cited in Mission V (§16.1).
Formalizing them. Mathlib has the spectral theorem for symmetric matrices but nothing connecting spectra to Markov chains: no spectral gap, no relaxation time, no Dirichlet forms, no Cheeger inequality in any form. A formalized discrete Cheeger inequality would be a landmark reusable well outside this series (spectral graph theory, expanders); the eigenvalue and Rayleigh-quotient layer built here is what Missions IX (tree relaxation, block dynamics) and XI (cutoff criterion) consume.
Everything routes through one change of basis: conjugating by the diagonal matrix with entries produces a matrix that is symmetric precisely because the chain is reversible, so Mathlib's spectral theorem applies — but transporting the resulting eigenbasis back to , keeping track of orthonormality with respect to the weighted inner product, is a genuine formal-linear-algebra project; nothing about it is deep, all of it is fussy. The definitions of and as suprema over the set of non-unit eigenvalues (finite, and nonempty once ) must be reconciled with the eigenbasis enumeration before any variational argument runs. The upper half of Cheeger is direct from the variational characterization — test it on the indicator function of a bottleneck set , recentred to have mean zero; the lower half is the hard half: the standard proof takes an optimal , decomposes it over its level sets , and applies Cauchy–Schwarz twice, and formalizing that level-set sweep is the main effort of the mission. Wilson's method needs a supermartingale-style iteration of the eigenfunction estimate; its constants are exact, so the inequalities cannot be rounded.
Eigenvalues are defined by real eigenvectors (); for reversible chains this captures the whole spectrum, and all statements assume reversibility wherever the book does. and are suprema of explicit sets of reals; on a one-point space these sets are empty and the supremum takes a junk value, so the affected statements carry the explicit hypothesis , matching the book's implicit assumption of a non-degenerate chain. with total inverse. Theorem 12.3 carries an explicit absorbing the rounding of a real-valued bound to an integer time. The cycle eigenvalue statement exhibits eigenvalues (existence of eigenfunctions); completeness of that list is not asserted. The variational characterization asserts both the minimization identity and its attainment, so it can be used in either direction.
Welcome contributions: the symmetrization API (conjugation by ), Rayleigh-quotient lemmas, level-set (layer-cake) infrastructure — all reused by Missions IX and XI.
Missions II–III produce upper bounds on mixing times. Whether such a bound is sharp is a different question: an bound on a chain that actually mixes in steps hides the truth. Chapter 7 of Levin–Peres–Wilmer, Markov Chains and Mixing Times (AMS, 2009) develops the standard toolkit of lower bounds: the counting and diameter bounds (a chain cannot spread faster than its transition graph allows), the bottleneck ratio (a chain cannot mix faster than it crosses its worst cut), and distinguishing statistics (a chain is far from stationarity as long as some statistic separates from by several standard deviations). The bottleneck bound — closely related to the conductance of the chain and, via Mission VII, to the Cheeger inequality — is the single most important obstruction result in the subject: it is how slow mixing (torpid mixing of Ising at low temperature, in Mission IX) is proved.
For a chain with stationary distribution , the edge measure is , the bottleneck ratio of a set of states is
and the bottleneck ratio of the chain is . The maximal one-step out-degree is ; the diameter is measured in the graph joining when . For a statistic and distribution , and are the finite-sum expectation and variance, and denotes the pushforward of under .
This is Theorem 7.3, the bottleneck-ratio lower bound, the chapter's central theorem.
The counting bound for chains with uniform stationary distribution (§7.1.1, display (7.2)); the diameter bound: any two states satisfy for (§7.1.2, display (7.3)); Proposition 7.8 (a statistic separating means by standard deviations forces ); Lemma 7.9 (projection under a statistic does not increase TV distance); Proposition 7.13 (the lazy hypercube walk satisfies ); and Proposition 7.14 (the top-to-random shuffle needs shuffles, matching the upper bound of Mission III).
The results. Together with Mission III this pins the top-to-random shuffle at — the first sharp mixing result of the series, and the prototype of the cutoff phenomenon formalized in Mission XI. Proposition 7.13 similarly matches the hypercube upper bound and feeds the cutoff analysis. The bottleneck bound is used in Mission IX to prove exponentially slow mixing of the mean-field Ising model at low temperature, and its two-sided refinement is the Cheeger inequality of Mission VII.
Formalizing them. Mathlib has no notion of conductance/bottleneck ratio of a chain, no distinguishing-statistic method, and no mixing-time lower bound of any kind. The pushforward and variance infrastructure over finitely supported distributions is elementary but new, and reusable wherever second-moment methods appear (Wilson's method in Mission VII).
The bottleneck theorem's proof is short but exact: it hinges on the identity for conditioned on , followed by a telescoping estimate of ; the formal cost is manipulating conditioned measures and one-sided TV sums (Remark 4.3 from Mission II). For Proposition 7.8, the second-moment argument runs through Chebyshev on both distributions plus optimization of a threshold — the constants are exact, not asymptotic, so the formal inequalities must be done carefully. Proposition 7.13 requires the binomial mean/variance computation for Hamming weight under both and , including the negative-correlation bound for unrefreshed coordinates. The naive route to a lower bound — "the chain has not left a small set, so it is far from " — is precisely the counting bound and is too weak for the sharp results; the statistics method is what closes the gap.
is an infimum over the subtype of nonempty sets with ; on a one-point space this subtype is empty and the infimum takes a junk value, making the goal trivially true there (the bound carries content only for , as in the book). The counting bound divides by with total division ( gives a trivially true statement). The diameter bound is stated for arbitrary pairs of states through SimpleGraph.dist of the transition graph, which subsumes the book's diameter formulation. Propositions 7.13 and 7.14 are stated for all integer times (resp. ), using monotonicity of instead of evaluating at a real-valued time — this avoids floor artifacts while keeping the book's content. Proposition 7.14 quantifies " large, then large" exactly as the book's iterated limit.
Welcome contributions: monotonicity of in ; conditioned-measure lemmas; variance API for distExp/distVar.
The Convergence Theorem of Mission II says an irreducible aperiodic chain mixes geometrically, but with constants coming from a crude Doeblin decomposition — useless for actual chains, whose state spaces are exponentially large. Chapters 5–6 of Levin–Peres–Wilmer, Markov Chains and Mixing Times (AMS, 2009) develop the two classic probabilistic techniques that give useful upper bounds: coupling — run two copies of the chain jointly so that they meet quickly, and read a TV bound off the meeting time — and strong stationary times — random times at which the chain is exactly stationary, independent of the time. The flagship application is the top-to-random shuffle: repeatedly take the top card of a deck of cards and reinsert it at a uniform position; the deck is well mixed after shuffles, with error at most .
A Markovian coupling of a chain (with the stay-together convention (5.2)) is a chain on pairs whose coordinate marginals are both and which moves diagonal states to diagonal states. The coupling time is the hitting time of the diagonal; its tails are expressed with the trajectory calculus of Mission I.
A randomized stopping time is presented by its stopping rule: for each time and trajectory prefix , a number , the conditional probability of stopping at given the trajectory so far and no earlier stop. A strong stationary time for the chain started at is an almost surely finite such with
i.e. independent of . The separation distance is .
The mission also fixes the concrete chains it bounds: the lazy walk on the discrete torus , the Metropolis chain on proper -colorings of a graph, the Glauber dynamics of the hardcore model with fugacity , and the top-to-random shuffle on decks of cards (states are arrangements, i.e. permutations; position is the top).
Let ,
for the top-to-random shuffle on cards — display (6.16) of the book, the chapter's flagship bound, proved by combining the strong stationary time with the coupon collector tail of Mission I.
Theorem 5.2 and Corollary 5.3 (the coupling bound: , hence ); Theorem 5.5 ( for the lazy torus walk); Theorem 5.7 (Metropolis colorings, : mixing in ); Theorem 5.8 (hardcore Glauber, : mixing in ); Proposition 6.1 with Example 6.7 ( is a strong stationary time); Lemma 6.11 (); Lemma 6.13 (); Proposition 6.10 ().
The results. The coupling bound is the single most used upper-bound technique in the subject: Missions VIII (path coupling), IX (Ising) and XI (cutoff examples) all instantiate it. Strong stationary times and separation distance return in Mission XI (separation cutoff) and underlie perfect sampling in Mission XIII. The three concrete bounds (torus, colorings, hardcore) are the standard first applications and give the first polynomial mixing results of the series; the colorings and hardcore chains are the objects of intense ongoing research on sampling thresholds.
Formalizing them. Nothing here exists in Mathlib. The novel infrastructure is the stopping-rule formalization of randomized stopping times over trajectory prefixes — measure-theory-free, but expressive enough for the strong stationarity identity — and the Markovian-coupling predicate on pair chains. Both are reused later in the series (Matthews method, cutoff, CFTP).
The coupling bound itself is short once Proposition 4.7 (Mission II) is available; the work is in the applications. For the torus, the coordinatewise coupling requires assembling one-dimensional couplings and bounding the coupling time by a sum of one-dimensional meeting times — the formal bookkeeping of "couple coordinate by coordinate" is the real cost, and the constant absorbs it. For Theorem 5.7 and 5.8 the argument is a grand coupling over all colorings/configurations simultaneously; the formal statements quantify only over the resulting bound, but a solver must build the coupling. For Proposition 6.1, the crux is the induction "given cards under the original bottom card, all orders are equally likely" — an exchangeability argument that must be carried through the stopping-rule encoding. Lemma 6.11 is where the definition of strong stationarity does its work; the naive attempt to prove Proposition 6.10 directly from the coupling characterization fails, which is exactly why separation distance is introduced.
Couplings of chains are transition matrices on with marginal conditions stated row by row; the stay-together convention is part of the predicate, matching (5.2). Stopping rules take the trajectory prefix (which includes the starting state), so times "depending on the starting position" are covered; strong stationarity packages the stopping rule bounds, almost-sure finiteness (), and the product identity. The colorings chain lives on the subtype of proper colorings; the hardcore chain is the Glauber dynamics of Mission II restricted to the subtype of hardcore configurations (transitions never leave it). Mixing-time upper bounds carry an explicit for integer rounding where the book's real-valued display would otherwise be false for the integer-valued . The torus statement fixes ; for near the display is false as stated in the book.
Welcome contributions: interface lemmas between setAvoidTailProb of the pair chain and the two coordinates; the taboo-matrix form of coupling-time tails; exchangeability infrastructure for the deck chains (reused in Mission V).
Two quadratic functions can be compared losslessly. The S-procedure says that, when the constraint is strictly feasible, the implication
holds if and only if a single nonnegative multiplier certifies it as a matrix inequality, for some . It is a cornerstone of control theory, trust-region methods and robust optimization, and a rare case in which a nonconvex problem has zero duality gap. The route runs through the theory this mission builds from Boyd & Vandenberghe §5.8–5.9 and Appendix B: strong alternatives for convex inequality systems, cone-program strong duality under a generalized Slater condition, semidefinite programming duality, the LMI theorems of alternatives, and the hidden convexity of the joint range of two quadratic forms.
Log-concave functions are the meeting point of convex analysis and probability: densities of Gaussian, exponential, uniform and Wishart distributions are all log-concave, and countless facts of applied probability flow from one structural theorem — integrating out variables preserves log-concavity. This mission builds the convex-analysis spine of Boyd & Vandenberghe's Convex Optimization (Chapters 2–3) — separation and supporting hyperplanes, dual cones, the first- and second-order differential characterizations of convexity, Fenchel conjugacy — and climbs to Prékopa's theorem via the Prékopa–Leindler inequality, a landmark of Brunn–Minkowski theory absent from Mathlib.
Value decomposition — approximating the value of a joint state by a sum of per-agent local values — is a staple of multi-agent dynamic programming and reinforcement learning, from index policies for restless bandits to modern MARL architectures, yet it is normally used without justification. Chen and Peng (arXiv:2506.02385) supply one. They show a multi-agent MDP admits an exact value decomposition precisely when its transition matrix is not entangled — a notion built in direct analogy with quantum entanglement — and then turn that qualitative characterisation into a quantitative one: a measure of Markov entanglement bounds the decomposition error in general. This mission formalizes that core theory. The goal is Theorem 6, the general N-agent bound in the occupancy-weighted norm; the milestones are the equivalence between separability and exact decomposition, the perturbation machinery that carries a one-step transition error into a value-function error, and the extensions to shared global state and shared rewards. The paper's restless-bandit application, which needs mean-field machinery of its own, is left to a second mission in the series.
The Monge optimal transport problem on the real line with the classical distance cost famously fails to have a unique solution. Juillet (2019) restored uniqueness by considering the strictly concave power costs with and letting : the limit selects a distinguished optimal plan, the excursion coupling, built from the level sets of the difference of the cumulative distribution functions. This mission formalizes the completed-graph construction, the generalized Banach indicatrix identities of Bertoin-Yor, the alternating crossing structure of almost every level, and the marginal identities for the crossing counting measures. It culminates in Propositions 3.5-3.6: every monotone transport plan is concentrated on the paired routes, and the marginals uniquely determine the coupling carried by those routes, including in the presence of atoms.
This mission formalizes the key implication 3=>4 in Juillet's Main Theorem.
How much flow can be sent from a source to a sink through a network with arc capacities — and what certifies that no more is possible? This mission formalizes §7.4-7.5 of Bertsimas & Tsitsiklis. The circulation calculus of §7.4 supplies the two structural tools: the flow decomposition theorem (Lemma 7.1 — every nonzero nonnegative circulation is a positive combination of simple circulations with only forward arcs, with integer when is integer) and the optimality criterion for the minimum cost network flow problem (Theorem 7.6 — a feasible flow is optimal if and only if there is no unsaturated cycle with negative cost). Section 7.5 then formulates the maximum flow problem ( s.t. , , for , ), defines augmenting paths (Definition 7.2: on forward arcs, on backward arcs) and the Ford–Fulkerson algorithm, and proves integer invariance and finite termination for integer capacities (Theorem 7.8). The goal is Theorem 7.10:
(a) if the Ford–Fulkerson algorithm terminates because no augmenting path can be found, the current flow is optimal;
(b) the value of the maximum flow equals the minimum cut capacity
— the archetypal combinatorial min-max theorem, which the book notes can also be read as LP duality (pp. 311-312).
Sometimes reward during learning is irrelevant — a pharmaceutical company running phase-II trials only cares about identifying the best treatment, as quickly and as reliably as possible. Chapter 33 of Lattimore–Szepesvári formalizes fixed-confidence best-arm identification: a policy together with a stopping time and a recommendation must be sound (wrong with probability at most ) while minimizing . The information-theoretic complexity is : every sound strategy needs , and the Track-and-Stop algorithm — the goal theorem — achieves exactly. The mission also covers the fixed-budget counterpart, sequential halving.
When rewards are binary — a click or no click, a cure or no cure — the subgaussian machinery of Missions I–III is not tight: the variance of a Bernoulli arm degrades near the boundary of , and the correct exponential rate is governed by the binary relative entropy rather than a squared distance. Chapter 10 of Lattimore–Szepesvári develops Chernoff's tail bound in its information-theoretic form and the KL-UCB algorithm, whose upper confidence bounds are level sets of . The goal theorem shows KL-UCB attains
— asymptotic optimality with exactly the constant demanded by the lower bound of Mission VII, strictly improving subgaussian UCB on every Bernoulli instance.
Every lower bound in bandit theory rests on one question: how hard is it to tell two probability measures apart from a sample? The answer is quantified by the relative entropy , and the sharpest elementary tool is the Bretagnolle–Huber inequality: for any event , — no test can distinguish from with total error probability below . This mission formalizes Chapter 14 of Lattimore–Szepesvári: the Bretagnolle–Huber inequality (the goal theorem, proved via Le Cam's inequality ), Pinsker's inequality , and the closed-form divergences between Gaussians and Bernoullis. These half-page inequalities power every impossibility result in Missions VII, XI and beyond.
No problem in mathematics carries more weight than the Riemann hypothesis. In his single eight-page paper of 1859, 'On the Number of Primes Less Than a Given Magnitude,' Bernhard Riemann linked the seemingly erratic distribution of the primes to the zeros of the analytic continuation of the zeta function ζ(s), and conjectured that every nontrivial zero lies exactly on the critical line where the real part equals 1/2. The truth of this statement would pin down the error term in the prime number theorem and tame the fluctuations of the primes around their expected count, and hundreds of theorems already stand proven only 'conditional on RH,' waiting for it to be settled. David Hilbert placed it in his eighth problem in 1900, alongside Goldbach and the twin primes; in 2000 the Clay Mathematics Institute named it one of the seven Millennium Prize Problems, with a million-dollar reward. G. H. Hardy proved in 1914 that infinitely many zeros lie on the critical line, and trillions more have since been verified by computation to do so — overwhelming evidence that is nonetheless not a proof. After more than 160 years it remains unresolved. This mission takes Mathlib's own definition of the hypothesis as its target.