Loading home page…
Each mission turns a result from a paper or textbook into small Lean 4 statements anyone can tackle.
Campaigns group missions around a shared mathematical goal. Each one tracks a quantity, such as an upper or lower bound. Have a good candidate in mind? Ping us on Slack, Zulip, or WeChat.
Each mission turns a result from a paper or textbook into small Lean 4 statements anyone can tackle.
Campaigns group missions around a shared mathematical goal. Each one tracks a quantity, such as an upper or lower bound. Have a good candidate in mind? Ping us on Slack, Zulip, or WeChat.
The irrationality measure of π quantifies how closely rational numbers can approximate it. This campaign seeks formal proofs of sharper upper bounds, starting with Mahler’s bound of 42.
The sharp Hlawka inequality for Schatten -norms is a cousin of the triangle inequality: it relates the norms of three matrices to the norms of their pairwise sums and their total sum. For complex diagonal matrices, an exact formula for the best possible comparison constant has been proved in Lean for every real . We conjecture that the same formula holds for all .
What is the smallest cutoff for which this formula holds for every real ?
References:
Is every odd number a sum of primes? This campaign tracks formalized proofs of the smallest that suffices.
Schnirelmann (1930) showed some finite works. Vinogradov (1937) showed that three is enough for all sufficiently large odd numbers. Tao (2012) proved unconditionally. Helfgott (2013) proved that every odd number greater than is a sum of three primes, though the proof is still unrefereed. Ideally, we can formalize this statement here. Note that three is optimal: is neither prime nor + prime.
Schoolbook matrix multiplication takes operations. The exponent is the infimum of all such that two matrices can be multiplied in arithmetic operations; trivially , and is conjectured but open.
Strassen gave the first nontrivial bound, , in 1969, and introduced the laser method in 1986 to reach . Coppersmith and Winograd's 1990 bound of stood for two decades. Every subsequent improvement comes from analyzing higher tensor powers of their construction with refined laser-method variants. That line reached in 2025, and the current record is , from August 2026. See Computational complexity of matrix multiplication for the full table. Can we formalize these results and even improve on them?
In Witten's cubic open string field theory (Witten 1986) the interaction glues half-strings together, and in the usual center-of-mass variables the action contains infinitely many time derivatives. Such a theory has no evident initial value formulation, which obstructs a Hamiltonian treatment and a direct discussion of causality.
Erler and Gross (2004) show that after a unitary change of basis in which the string field depends on the lightcone component of the string midpoint (and on transverse center-of-mass coordinates), the cubic vertex contains no derivatives with respect to lightcone time. This reduces to five linear relations among the Neumann coefficients of the three-string vertex, the midpoint identities (A.6)–(A.10) of the paper. One of them, (A.8), is a closed numerical identity: a specific infinite series built from Neumann coefficients equals , where is the zero-mode Neumann coefficient. This mission formalizes that identity and the chain of intermediate results the paper uses to prove it (Appendix B), together with a divergence statement from Section 2 explaining why other midpoint bases fail.
Define real constants () by the expansion
For real the left side is , so is the -th Taylor coefficient of at (e.g. ). The even Neumann vector and the vector are
In Lean these are ErlerGross.neumannA, ErlerGross.neumannMEven (with neumannMEven n ) and ErlerGross.betaVec. Two auxiliary objects appear in the proof: the (B.3) terms
(ErlerGross.b3Term) and the -basis integrand
(ErlerGross.kappaIntegrand), which arises from the continuous spectrum of the Neumann matrices (Rastelli–Sen–Zwiebach 2001).
formalized as: the series converges absolutely (Lean HasSum) to .
In the paper, (A.8) is one of the relations which, together with (A.6), (A.7), (A.9), (A.10), removes lightcone-time derivatives from the cubic vertex. This is what gives the theory an initial value formulation in lightcone time and makes the Hamiltonian BRST quantization of Section 4 possible. Unlike the other four identities, which are relations between distributions and are verified in the paper's spectral basis, (A.8) is an equality of real numbers. It can therefore be checked completely in Lean.
A complete formalization would produce a machine-checked proof of a Neumann-coefficient identity. It would also add reusable material: Taylor coefficients of , the integral, and digamma-type evaluations of rational series.
The goal defines through Taylor coefficients, which have no closed form. The paper does not sum the series in the mode basis. It moves to the continuous basis of the Neumann spectrum and closes a contour. That step rests on eigenvector expansions and the principal-value distribution , neither of which is in Mathlib. A direct route has to connect the coefficients to the integral , or to the series , some other way. The terms of decay like . The terms of the goal series decay only like , so the goal series converges slowly.
iteratedDeriv.HasSum is unconditional (equivalently absolute) convergence. Every statement asserts convergence, so no statement can hold only because Lean assigns to a divergent tsum.The diagonal Ramsey number is the least such that every red/blue colouring of the edges of the complete graph contains a monochromatic copy of . Ramsey's theorem guarantees that is finite; the question of how fast it grows is one of the central problems of extremal and probabilistic combinatorics. Erdős asked repeatedly ([Er88], [Er93]; see erdosproblems.com/77) for the value of
It is not even known whether this limit exists.
Timeline.
So today, if the limit exists, it lies in .
For consider simple graphs on the vertex set . A red/blue colouring of the edges of is the same as such a graph (the red edges) together with its complement (the blue edges). A -clique of is a set of exactly vertices, any two of which are adjacent in . Define
In the Lean development this is Erdos77.diagonalRamsey k. Small values: , , , , .
The original problem asks for the value of the limit, which is unknown; a goal with a hard-coded value cannot be stated honestly. The goal therefore asserts only that the limit exists (as a real number). Determining remains the ultimate aim; any proof of a specific value would in particular prove this goal.
The result itself. Existence of the limit would say that diagonal Ramsey numbers have a well-defined exponential growth rate — a regularity statement that is currently unknown in either direction. Even the bounds and are the products of decades of work, and the lower bound base has resisted improvement since 1947.
Formalizing it. The goal is open. The milestones are proved results in the literature; the classical ones (Erdős–Szekeres, Erdős 1947) are natural first formalization targets, and the recent upper bounds (CGMS, GNNW) are substantial formalization projects in their own right. The status of existing machine-checked formalizations of these results is not asserted here.
There is no known sub- or super-multiplicativity for that would give existence of the limit via Fekete's lemma: the natural product constructions relate to and only with losses that are too large, and the best lower and upper bounds come from entirely different methods (random colourings versus the book algorithm), so neither side controls the other.
sInf of an empty set of naturals is ; the Erdős–Szekeres milestone shows the set is nonempty, so the infimum is the genuine Ramsey number.atTop filter on ; "" in GNNW is encoded as "for every , eventually with exponent ".Fin n, binomial estimates, the probabilistic method for the lower bounds (Spencer uses the Lovász Local Lemma), and the CGMS book algorithm for the upper bounds. All of these are reusable beyond this mission.A sunflower (also called a -system) with petals is a family of sets whose pairwise intersections are all equal to one common set, the kernel. In 1960 Erdős and Rado proved the sunflower lemma: every sufficiently large family of -element sets contains a sunflower with petals, and they asked how large "sufficiently large" must be (Erdős–Rado 1960). The conjecture that the threshold is only exponential in is one of Erdős' best-known problems in extremal combinatorics; it is listed as Erdős Problem 20, and Erdős offered a $1000 prize for it. Sunflower bounds are used, for example, in Razborov's monotone circuit lower bounds and in the study of set systems with restricted intersections.
Timeline.
The conjecture itself remains open, even for .
Fix natural numbers (the uniformity) and (the number of petals). A family of sets is -uniform if every member of has exactly elements. A subfamily is a -sunflower if and there is a set with for all distinct .
The sunflower threshold is the least natural number such that every -uniform family (over any ground set) with contains a -sunflower.
The constants are left unspecified; only the exponential shape in is asked for. A disproof (the negation of this statement) would equally settle the problem.
A supporting sanity check, , is taken from the source formalization.
A positive answer would show that sunflower-free -uniform families have at most exponential size, the correct order of magnitude by the Erdős–Rado lower bound; this would sharpen every application that currently loses a factor per coordinate, including monotone circuit lower bounds. A negative answer would show the -type bounds of 2019–2021 are essentially the truth.
On the formal side, the Erdős–Rado upper bound has a Lean formalization recorded in the source file; the lower-bound construction and the spread-family / coding arguments behind the Rao and Bell–Chueluecha–Warnke bounds are, as far as this proposal records, not yet formalized. Formalizing them produces reusable infrastructure on spread families and random-subset (or entropy) arguments.
The classical induction on (pick a maximal family of pairwise disjoint members; if it is small, some element lies in many members, recurse on the link) loses a factor of about at each of steps, which is where comes from. The modern arguments replace the recursion by an analysis of spread families, but each still loses a factor per level, and no known technique removes it. The case is already open.
Set (Set α) and sizes are measured with Set.ncard, which returns on infinite sets. Consequently, for only finite members can be "-element", and the condition with only applies to finite families. All targets assume (except the sanity check), so the quirks do not affect them.answer(·) statement.Contributions of general lemmas on sunflowers, spread families and the Erdős–Rado construction are welcome and reusable beyond this mission.
Chapter 3 of Gittins, Glazebrook and Weber, Multi-armed Bandit Allocation Indices (2nd ed., doi:10.1002/9780470980033), asks which of the assumptions behind the index theorem can be dropped and which cannot, using the simplest bandit processes there are: jobs, which pay a single reward when they complete. Along the way it settles three questions that matter on their own. When identical machines run in parallel, which schedule of deterministic jobs minimizes the total completion time (Baker's theorem), and what does the equal-ratio case look like (Theorem 3.3)? When an object is hidden in one of several boxes and each search costs money and may fail, in what order should the boxes be searched (Blackwell's search-index theorem, Theorem 3.6)? And when two bandit processes discount at different rates, is there still an index policy (Nash's Theorem 3.4)? The search theorem is the chapter's example of what the index machinery yields once undiscounted criteria are admitted through the limit ; the scheduling results are the source of the counterexamples that show a second machine breaks the index structure.
Jobs on parallel machines. There are jobs with service times and weights , and identical machines. A schedule assigns each job a machine and a position in that machine's processing order; each machine processes its jobs consecutively. The completion time of a job is the total service time of the jobs on its machine up to and including it; the flow time is and the weighted flow time . The load of a machine is the total service time assigned to it, and is its excess over the average . The SPT list schedule sorts the jobs by increasing service time and deals them out cyclically to the machines. The level of a job is its position counted from the end of its machine's schedule.
The search problem (Problem 3). A stationary object is hidden in one of boxes, in box with probability . A search of box costs and finds the object with probability if it is there. A search policy is a sequence of boxes; after unsuccessful searches of box the posterior probability that the object is there is proportional to , and the search index of the box is , the current probability of finding the object per unit cost. The expected cost of a policy is .
Two discount factors. Bandit process (state space , kernel , reward ) discounts at rate and at rate ; a reward obtained at time is worth or times its face value according to which process produced it. The cross indices are and with the roles exchanged: each is computed from one process's stopping times but with the other's discount factor in the denominator. The book prints the denominator as and compares with at every time; both are corrected here (see the Theorem 3.4 item), since the printed rule is not optimal. The family is the two-armed Markov bandit of the Bandit Algorithms model on the disjoint union .
For prior probabilities summing to one, detection probabilities and costs , a search policy is optimal if and only if at every step it searches a box of maximal current index :
Theorem 3.3, as the identity when ; Theorem 3.4 in discrete time and corrected, that a policy selecting, at time , when and when attains the supremum of the bandit-dependently discounted payoff; Theorem 3.7, that SPT minimizes the flow time on machines and that the optimal schedules are exactly those placing the -th block of longest jobs at level from the end, for some order of the equal jobs.
Theorem 3.6 is the classical solution of the discrete search problem (Blackwell, reported by Matula 1964; Kadane 1969): the greedy rule in probability-per-cost is optimal, and every optimal policy is of that form. The book derives it from the index theorem through an auxiliary family of bandit processes (Problem 3A) and the undiscounted limit (Corollary 3.5), which is why it sits in this chapter; as a statement it is elementary and self-contained, and it is the template for the tax problems and Klimov's model of Chapter 4. Theorem 3.7 and Theorem 3.3 are the positive results about parallel machines that survive the loss of the index structure; Theorem 3.4 shows the index theorem's shape persisting under bandit-dependent discounting, with two twists: each index depends on the other process's discount factor, which is exactly why it does not extend to three processes, and the comparison at time weighs the indices by and , so the rule is not stationary in the states. The printed statement misses the second twist and misnormalizes the first; two one-state bandits paying () and () are best played and then forever, which no stationary rule does.
None of these is machine-checked. Formalizing them gives the platform an optimality theorem for an infinite-horizon search process with an explicit index characterization in both directions, the standard parallel-machine flow-time results with a precise uniqueness clause, and a first statement on the Bandit Algorithms two-armed model with unequal discounting.
For Theorem 3.6 the obvious route, comparing two adjacent searches, gives only that interchanging a pair in the wrong index order lowers the cost; turning that into optimality over all infinite sequences needs that an optimal policy exists (costs are bounded below by zero and the index policy has finite cost), that a policy neglecting a box of positive prior has infinite cost, and that any first deviation from the index rule can be improved by moving a later search forward, which requires tracking how the not-found probability changes along the whole tail. The converse direction is the same interchange run backwards, and the tie case must be handled so that the equivalence is exact. Theorem 3.7's first part follows from writing the flow time as with the level and applying a rearrangement inequality over the multiset of levels, but the multiset of levels itself depends on how many jobs each machine gets, so balancing the machine counts is part of the argument; the uniqueness clause needs both that the multiset is forced and that the pairing of levels with service times is forced by strict monotonicity. Theorem 3.4 is the hardest: the book's proof changes the time scale of each process so that the two share a discount factor, which produces a semi-Markov family, and applies the index theorem there; in discrete time on the Markov model one needs either a discrete analogue of that argument or a direct prevailing-charge proof with two charge scales.
Schedules are assignments of machines and positions with distinct positions on a machine, without idling; the flow-time quantities are finite sums over Fin n. The SPT schedule is defined by the ascending rank of a job (ties broken by index) and carries its own injectivity proof. The search cost is a series in of nonnegative terms, so no summability hypothesis is needed and "infinite cost" is literal; the index is stated unnormalized, , which orders the boxes exactly as the posterior index does. The two-discount family uses the platform's MarkovBanditPolicy 2 (S_A ⊕ S_B) and markovBanditMeasure with the kernel that moves an -state by and a -state by ; the payoff is the round-by-round series , absolutely summable for bounded rewards, and the policy condition is imposed at histories whose current states have the right types (all reachable histories do). Hypotheses: , service times positive; , , , ; countable state spaces, bounded rewards, .
Trivializing readings are excluded: the search "iff" is over all sequences, not a finite horizon; the uniqueness clause is stated in full, with ties resolved by any ranking of the equal jobs; the cross indices are suprema over positive stopping times (denominators at least one), and the two-discount rule weighs the indices by , . Welcome contributions: the rearrangement and level-count lemmas for schedules, the interchange lemma for the search cost, and a discrete prevailing-charge argument for Theorem 3.4.
An initial value problem , , is the standard way a law of motion, a growth model or a circuit equation is written down, and only a small minority of such problems can be integrated in closed form. Single-step methods advance the solution by small increments: Euler's method takes the tangent line at the current point, and the higher-order Runge-Kutta schemes refine the same idea. What justifies them is a pair of theorems: that the problem has a unique solution at all, and that the computed polygon approaches that solution as the step size decreases.
This mission is the seventh in a series formalizing the lecture notes Métodos Numéricos by Sergio Roberto de Freitas (UFMS, 2000). It covers Chapter 9, Métodos Numéricos para EDO's, up to the convergence of Euler's method.
Consider the initial value problem
with defined on a rectangle .
Picard's method replaces the differential equation by the integral equation and iterates it:
With , and , the source states the bound on , where is the exact solution.
Euler's method with step produces , . Its local error is per step and its global error .
The goal theorem is the global error statement: for an initial value problem whose exact solution is twice continuously differentiable on and whose right-hand side is Lipschitz in there, there is a constant such that for every step size and every grid point ,
This is the precise form of the source's assertion .
The milestones are the results the chapter states on the way: local existence and uniqueness for the initial value problem under a Lipschitz condition in (Teorema 9.4.1), the Picard error bound, the convergence of the Picard iterates to the solution, and the one-step Taylor identity behind Euler's method.
The global error bound is what makes Euler's method a method rather than a heuristic: it converts an arbitrary choice of step size into a guaranteed accuracy, and it exhibits the characteristic loss of one order between the local error and the global error that recurs for every single-step scheme. The existence and uniqueness theorem is the prerequisite for all of it — without uniqueness there is no well-defined object for the numerical solution to approximate — and the Picard iteration is both the constructive proof of that theorem and a method in its own right.
The global error proof has to handle the interaction of two error sources: the local truncation error at each step and the amplification of previous errors by the Lipschitz constant, which gives the discrete Gronwall recursion . Carrying that recursion to the closed-form bound, and doing it uniformly in , is the core of the mission. The Picard bound requires the iterates to remain inside the rectangle so that the hypotheses on continue to apply — that is what the choice is for — and an induction on with the factorial denominator.
The unknown is a real function of a real variable and is a function of two real variables. A solution is a function satisfying and having derivative at every point of the relevant interval. The Lipschitz condition in the second variable is stated explicitly, , in place of the source's hypothesis that is bounded; for the global-error goal it is assumed for all real and all in the interval, and in the Picard milestones only inside the rectangle. Uniqueness is stated as agreement of any two solutions on the interval, not as uniqueness of a function on all of , since a solution is unconstrained outside the interval. Euler's iterates and the Picard iterates are explicit recursive definitions; the Picard integral is the interval integral, which is total, so no integrability side condition appears in the definition. The constant in the goal is asserted to exist and to be positive, uniformly over step sizes in ; the restriction merely normalizes the range of steps considered.
Chapter 2's tail bounds mostly rest on moment-generating-function control, obtained either directly (sub-Gaussianity) or through explicit combinatorial arguments (Hoeffding, bounded differences). The entropic method offers a different, more structural route: bound a specific information-theoretic quantity — the -entropy of — and convert that bound mechanically into a tail bound via a short ODE argument (the Herbst argument). This method's real payoff appears once it is combined with the tensorization property of entropy across independent coordinates, which is what lets it handle Lipschitz functions of many independent variables — including cases, such as separately convex functions, that elude the purely martingale-based techniques of Chapter 2. This mission formalizes the entropic method's two foundational entropy-to-tail conversions and its central Lipschitz-concentration application, following Wainwright, High-Dimensional Statistics: A Non-Asymptotic Viewpoint (Cambridge University Press, 2019), Chapter 3.
For (), , the -entropy of a nonnegative random variable is (Eqs. (3.1)-(3.2)). Writing for the moment generating function of , the entropy of has the explicit form (Eq. (3.3)).
A function is separately convex if, for each coordinate , the univariate function obtained by fixing every coordinate but the -th is convex — strictly weaker than joint convexity of itself. is -Lipschitz with respect to the Euclidean norm if for all .
Let be independent, each supported on , and separately convex and -Lipschitz. Then for all ,
If for all ( or ), then for all — the basic entropy-to-sub-Gaussian-tail conversion.
The sub-exponential analogue: if for , then on the same range.
Propositions 3.2 and 3.3 are the two basic entropy-to-tail conversions the entire chapter's entropic method rests on — every subsequent Lipschitz-concentration result in the chapter (including Theorem 3.4 and the more advanced Theorem 3.24) is obtained by first establishing an entropy bound of one of these two forms and then invoking the corresponding proposition. Theorem 3.4 is itself the direct analogue, for independent bounded variables, of Chapter 2's Gaussian Lipschitz concentration (Theorem 2.26) — but crucially requires the extra hypothesis of separate convexity, which the Gaussian case does not need and which cannot be dropped in general.
Formalizing it. No faithful prior art exists on the platform. The one candidate flagged in
BRIEF.md, Talagrand.lipschitz_concentration, was read in full: it is a weighted-Hamming-
distance concentration bound for functions on a finite-alphabet product space Fin n → α,
proved via Talagrand's convex-distance method — a different underlying space (finite alphabet
vs. real-valued bounded coordinates) and a different Lipschitz norm (weighted Hamming vs.
Euclidean) from Theorem 3.4, and not reused here. A search for "log-Sobolev" and "Herbst" turned
up bousquet_herbst_cgf_le_phi_via_herbst/bousquet_herbst_cgf_le_phi_double_integration: these
are abstract calculus lemmas about a generic function satisfying an ODE-type growth
condition (), concluding — a genuinely different statement
shape from Proposition 3.2/3.3's entropy-to-CGF conversions (which conclude a quadratic, not
exponential, bound on ), and not a faithful match. All
three theorems here are drafted as open goals (:= by sorry).
The naive approach to Theorem 3.4 — try to adapt the bounded-differences (martingale) method of Chapter 2 directly — fails, because the bounded-differences method needs to have small coordinatewise oscillation in an absolute sense, while separate convexity alone gives no such uniform bound (a separately convex function can vary arbitrarily fast within the interior of its domain, only its slope is controlled by the Lipschitz condition). The entropic method sidesteps this by working with the -entropy of directly: entropy has a tensorization property across independent coordinates (not itself part of this mission, but what the entropic method's proof of Theorem 3.4 uses) that reduces a multivariate entropy bound to a sum of "one coordinate at a time" contributions, each of which convexity and the Lipschitz condition jointly control — a route with no analogue in the bounded-differences approach.
Separate convexity and Euclidean-Lipschitzness are both restated locally in this chapter's own
sub-namespace (HighDimStat.Concentration), per this book series' rule against importing
another chapter's draft definitions, even though Chapter 2 already defines an
IsLLipschitz for the same Euclidean condition. φ_X'(\lambda)$ (Proposition 3.3) is realized via Mathlib's deriv, a legitimate way to state a hypothesis on a derivative without separately proving differentiability, appropriate at the draft-statement stage. Explicit Integrable`
hypotheses guard the Bochner integral's junk value on non-integrable functions throughout (trap
2), not literal in the book's own propositions but implied by what "the entropy exists" (an explicit qualifier the book itself makes when introducing Eq. (3.2)) means.
Goal substitution, disclosed. BRIEF.md recommends Theorem 3.24 (the two-sided, jointly
convex analogue) as the primary goal, but explicitly names Theorem 3.4 as a fallback "if 3.24's
dependence on the unnumbered transportation-cost inequality (Eq. 3.73, attributed to Samson)
proves too heavy to state faithfully in the time available." Theorem 3.24's proof route depends
on Theorem 3.19 (a general "transportation cost implies concentration" result for an abstract
metric measure space, itself needing a from-scratch formalization of the transportation-cost
inequality (3.58) and the concentration function ) plus the
unproven-in-chapter Eq. (3.73). Building this full stack faithfully was judged to exceed this
chunk's time budget; Theorem 3.4 is drafted instead, using this mission's own budget on
Propositions 3.2 and 3.3 (the two most load-bearing entropy-to-tail conversions of the chapter)
rather than the heavier transportation-cost machinery. Theorem 3.19, Theorem 3.24, and Eq.
(3.73) are all out of scope for this mission and named here as natural follow-on work.
Chapter 7 of Walter Rudin's Principles of Mathematical Analysis (3rd edition, McGraw-Hill, 1976) asks when a limit of functions inherits the properties of its members. Pointwise convergence preserves almost nothing: Rudin's opening examples give continuous with discontinuous limit, and sequences where . Uniform convergence is the hypothesis that repairs this, and the chapter's second half asks the converse question — which functions arise as uniform limits from a given family — answered by the Stone–Weierstrass theorem (Theorem 7.32): an algebra of continuous real functions on a compact set that separates points and vanishes nowhere is uniformly dense in all continuous functions there.
The classical Weierstrass approximation theorem (7.26) — polynomials are dense in — is the special case that made the general theorem worth proving, and is used in Chapter 8 for Fourier series and in Chapter 11 for the density of continuous functions in .
This mission is the seventh in a series formalizing Rudin Chapters 1–11; it uses the compactness results of Mission II, the continuity results of Mission IV and the Riemann–Stieltjes integral of Mission VI.
A sequence converges uniformly to on if for every there is with for all and all — the same for every point. A family is equicontinuous on if a single serves all its members in the definition of uniform continuity; it is pointwise bounded if each orbit is bounded, and uniformly bounded if one bound works for all and all .
A set of real functions is an algebra if it is closed under addition, multiplication and multiplication by real scalars; it separates points on if for in some has ; it vanishes at no point of if for each some has . The uniform closure of on is the set of uniform limits on of sequences from .
Let be compact and let be an algebra of real continuous functions on which separates points on and vanishes at no point of . Then
every continuous real function on is a uniform limit on of members of .
Uniform convergence is the standard hypothesis under which limits commute with continuity, integration and (with an extra condition) differentiation, and Theorems 7.11, 7.12, 7.16 and 7.17 are used throughout the rest of the book; Chapter 8 in particular builds the exponential, trigonometric and Gamma functions as uniform limits and differentiates them term by term on the strength of 7.17. Theorem 7.18 shows how weak pointwise differentiability is as a consequence of continuity: a uniform limit of piecewise-linear functions can fail to be differentiable anywhere. Arzelà–Ascoli is the compactness criterion for families of functions, and it is the standard route to existence theorems for differential and integral equations.
Stone–Weierstrass is the structural theorem of the chapter: it replaces the combinatorial Bernstein-polynomial proof of Weierstrass's theorem with a statement about algebras of functions, applicable to trigonometric polynomials, polynomials in several variables, and Lipschitz algebras alike.
Mathlib contains a Stone–Weierstrass theorem for subalgebras of C(X, ℝ) on compact Hausdorff
spaces, and a version of Arzelà–Ascoli. This mission states the results in Rudin's terms — plain
sets of functions on a compact subset of a metric space, uniform closure defined by
sequences — so that they can be used together with the Riemann–Stieltjes integral built in
Mission VI, which is not part of the library.
Stone–Weierstrass is the one theorem in this mission whose proof is genuinely structural: from the algebra one first produces as a uniform limit of polynomials in (which needs the polynomial approximation of on and so cannot be circular with Theorem 7.26), then maxima and minima of pairs, then functions matching prescribed values at two points, and only then the local-to-global patching over a finite subcover. Each step is short; keeping the uniform closure a lattice and an algebra simultaneously is the bookkeeping burden.
Two hypotheses are easy to lose and both are necessary: an algebra that vanishes at a point cannot approximate functions that do not, and one that fails to separate two points cannot approximate functions that distinguish them.
Conventions fixed by this mission:
TendstoUniformlyOn … atTop; complex-valued sequences are
used where Rudin allows complex values.Rudin.IsFunctionAlgebra, Rudin.SeparatesPointsOn, Rudin.VanishesAtNoPointOn,
Rudin.UniformClosureOn, defined for sets of functions X → ℝ and a compact subset K.
The goal's conclusion is membership in the uniform closure, i.e. the existence of an
approximating sequence from the algebra.Rudin.EquicontinuousOn,
Rudin.PointwiseBoundedOn, Rudin.UniformlyBoundedOn, stated with explicit and
as in Definitions 7.19 and 7.22.An 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.