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?
An additive question about the primes asks how many of them are needed to represent every integer. Shnirelman's constant is the least such that every natural number greater than is a sum of at most primes; that such a exists at all is Shnirelman's theorem (1930). The even Goldbach conjecture would give , and is close to equivalent to that claim, but Goldbach is open, so every bound on has come from the circle method together with explicit numerical input.
The history is a sequence of shrinking bounds, each one effective and each one resting on a numerical verification available at the time:
For a real number write . The von Mangoldt
function equals when is a prime power and
otherwise; it is Mathlib's ArithmeticFunction.vonMangoldt.
The paper does not work with the sharp-cutoff exponential sum but with a smoothed variant. For a piecewise smooth and a modulus , set
The modulus is a technical device: taking restricts the sum to odd and saves a factor of two in the explicit constants. Because of that restriction it is , not , that gets approximated by a rational .
Two explicit cutoffs are fixed. The Lipschitz cutoff
has unit mass and is supported on ; it is chosen because it factorises the Type II sums. The -normalised cutoff
is supported on and symmetric, .
Throughout, denotes a quantity of magnitude at most — an explicit bound, not an asymptotic one. Two numerical constants are fixed once and for all: and .
The goal fixes no constants and no thresholds, so no later improvement can invalidate it.
The milestone list is the paper's own attack path, in its numbering: the two numerical verifications (Theorems 1.5, 1.6) and the short-interval prime bound (Theorem 8.1) that together settle ; the apparatus (Lemma 4.4, Proposition 4.10) and Vaughan-type identity (Lemma 4.11) feeding the minor-arc bound (Theorem 5.1) and hence the main exponential sum estimate (Theorem 1.3); the major-arc analysis (Proposition 7.2); and the circle-method core (Theorem 8.2).
The result itself. Theorem 1.4 lowers Shnirelman's constant from to and removes the Riemann hypothesis from Kaniecki's conditional "five primes". Its durable content, however, is not the headline but the explicit exponential sum estimate of Theorem 1.3: a bound on with constants small enough to be useful for between and , a range where the asymptotically superior estimates of Vinogradov, Chen–Daboussi and Ramaré carry constants too large or too ineffective to apply. That estimate is the reusable object; it has been improved since (Helfgott–Platt) but not superseded in method.
Formalizing it. Status honesty matters here. Theorem 1.4 is closed mathematics, and as a statement it was superseded within a year by Helfgott's ternary Goldbach theorem, which gives three primes for every odd and hence five a fortiori. Neither Tao's theorem nor Helfgott's is formalized anywhere, and this mission does not claim to be attacking an open problem: the work is formalizing a known, fully explicit proof. That proof happens to be an unusually good formalization target, because every constant in it is written down.
The platform already hosts the surrounding infrastructure. The CircleMethod namespace
carries a large verified development of Hardy–Littlewood apparatus following Vaughan, and
the ThreePrimes namespace carries a machine-checked proof of Vinogradov's three primes
theorem conditional on Siegel–Walfisz. This mission sits directly downstream of both and
should import from them rather than rebuild.
The obvious route — deduce five primes from three primes — fails on the range where it is needed. Vinogradov's theorem is asymptotic, and the best effective threshold is ; below it the theorem says nothing, and is far beyond any possible exhaustive check. So the entire difficulty lives in the window , which must be handled by a circle-method argument carrying explicit constants at every step.
Within that window the specific obstruction is the minor arc . A direct Plancherel bound on the side costs a factor of , which is more than the argument can afford; Montgomery's uncertainty principle cuts the loss to roughly , and only a large-sieve estimate on prime pairs brings it down to a bounded factor of . On the side, Theorem 1.3 must be non-trivial across the whole window, which is why the refinements (1.10)–(1.12) for near and near exist at all. Neither bound alone suffices; the proof closes only because both are pushed to explicit constants simultaneously.
The goal is stated over as a Multiset ℕ of cardinality at most whose
members are all Nat.Prime and whose sum is . A multiset, not a list or a finset:
repetition is essential () and order is not. "At most five" is not "exactly
five" — is a sum of one prime and cannot be a sum of five, since the least sum of
five primes is . A formalization asserting exactly five primes is false, not merely
weaker.
The goal admits no trivializing reading: the empty multiset has sum , and the cardinality bound is on the multiset itself, so no prime can be counted with multiplicity zero to evade it.
Everything else in the mission is stated with explicit constants and bounds
rather than asymptotic notation, matching the paper: becomes
outright. Sums over are unrestricted sums against a compactly supported cutoff, not
sums over Finset.range. Real powers are Real.rpow. The two cutoffs and
the sum are published as mission definitions; solvers should use them
verbatim rather than re-deriving equivalent forms.
Three of the milestones are honest dead weight for a solver to attempt directly, and are listed so the dependency graph is truthful rather than because they are tractable. Theorem 1.5 (all zeroes of up to height lie on the critical line) and Theorem 1.6 (every even number up to is a sum of two primes) are finite, decidable statements that Lean can express and that are true, but each represents a verified computation of a scale no current proof assistant can replay — Theorem 1.6 alone is cases. Theorem 8.1 is quoted from Ramaré–Saouter and itself depends on Theorem 1.5. They are leaves that will stay open; a solver's effort is far better spent on the analytic milestones, and the circle-method core (Theorem 8.2) can be closed independently of them.
A complete development additionally needs the smoothed Vaughan identity bookkeeping, the large sieve in Siebert's form, the von Mangoldt explicit formula with a zero sum (Proposition 7.1), and Bourgain's trick of taking one of the three summands of size . The exponential sum machinery is reusable well beyond this mission — it is the standard input to every explicit Goldbach-type result. Contributions to any milestone are welcome independently, and a formalization of Helfgott's theorem that closes the goal by a different route would be an entirely acceptable solution.
Markov chain Monte Carlo turns hard integration problems into long simulations: to estimate an expectation one runs a Markov chain with stationary distribution and reports the sample average . The ergodic theorem guarantees , but honest error bars require more: a central limit theorem
On general state spaces this is famously delicate - a merely ergodic chain with a square-integrable functional can fail the CLT, so the classical theory trades convergence rates (drift, minorization, geometric or polynomial total-variation rates) and mixing conditions (-, -, -mixing) against moment conditions on . This mission formalizes G. L. Jones's survey "On the Markov chain central limit theorem" (Probability Surveys, 2004): the drift-condition CLTs of Meyn-Tweedie and Jarner-Roberts, the classical mixing CLTs of Ibragimov-Linnik, Doukhan-Massart-Rio and Billingsley, the characterizations via uniform integrability and boundedness in probability, and their assembly into the summary theorem: six practically checkable regimes - from polynomial ergodicity with bounded functionals to uniform ergodicity with second moments - each of which guarantees the CLT for every initial distribution. The stationarity, total-variation and mixing infrastructure is general state space and reusable well beyond this mission.
This mission seeks a Lean proof that every odd natural number greater than 1 is the sum of at most three primes. It follows from Helfgott's ternary Goldbach theorem for odd numbers greater than 5, together with the small cases 3 and 5, each of which is itself prime.
For every natural number n with Odd n and 1 < n, construct a multiset of at most three prime natural numbers whose sum is n. Repetition is allowed and order is irrelevant. Examples include 3 = 3, 5 = 5, 7 = 2 + 2 + 3, and 9 = 3 + 3 + 3. The primes need not all be odd.
The goal uses the same Multiset ℕ representation and the same hypothesis 1 < n as Every Odd Number Greater Than 1 is the Sum of at Most Five Primes. The cardinality bound changes from s.card ≤ 5 to s.card ≤ 3. No custom definitions are needed.
The target is unconditional and covers every odd natural number greater than 1. At most three is essential: 3 and 5 cannot be sums of exactly three primes. All summands must satisfy Nat.Prime, and multiplicities count toward the cardinality bound. The initial proposal contains the goal with an open proof, ready for formalization.
A proof may combine a formalization of Helfgott's theorem, which supplies exactly three primes for odd n > 5, with singleton multisets for n = 3 and n = 5. Establishing Helfgott's result requires verified proofs of the analytic and computational ingredients of the chosen argument.
H. A. Helfgott, The ternary Goldbach conjecture is true, 2013, revised 2014. The mission's at-most-three formulation also includes the elementary cases n = 3 and n = 5.
The source defines a two-variable integral on strictly positive-definite real matrices. Its numerator is the absolute bilinear form of A minus B on two unit vectors, while the denominator uses the quadratic forms of A and B. The desired inequality says that componentwise matrix addition is nonexpansive for this quantity, with the larger of the two input distances controlling the output. The surface measure normalization is immaterial because the same constant multiplies every distance.
This mission turns CUHK-Shenzhen AI Math Problem 1, Positive definite matrix integral inequality, 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.
For every positive dimension and every four positive-definite matrices A, B, C, and D, prove d(A+B,C+D) is at most max(d(A,C),d(B,D)). The first milestone fixes dimension one, where the sphere and every matrix entry can be analyzed explicitly.
Solving this target would settle the precise finite or analytic core represented by the Lean statement and would create reusable infrastructure in matrix analysis, positive definite matrices, integral inequality. 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 absolute value prevents a direct cancellation argument, and the denominators couple each integration variable to a different matrix. Positive definiteness gives pointwise positivity but does not immediately compare the ratios after addition. A successful proof must find a convexity, change-of-measure, or projective-metric mechanism that survives the double integral.
Promising routes include reducing by congruence to normalized matrices, studying the scalar inequality on each pair of directions, and interpreting the denominator as a density change on the sphere. The dimension-one case should reveal the sharp scalar inequality. Numerical experiments in dimensions two and three may identify equality cases, but the Lean proof must ultimately derive every bound from positivity and measurable integration.
The Lean model uses finite matrices, Mathlib positive definiteness, the canonical sphere measure obtained from polar decomposition, and an explicit iterated integral. It does not assume symmetry through an unchecked flag: positive definiteness is the Mathlib predicate. Integrability obligations and zero-denominator issues must be proved from positive definiteness.
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.
Establish the dimension-one specialization, including any exact evaluation of the two-point sphere integral needed by the proof.
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 May 28, 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.
Every time a streaming service guesses what you would rate a film you have never seen, it is solving a matrix completion problem: fill in the missing entries of a vast user-by-item table from the few that are observed. The question became famous during the Netflix Prize (2006-2009), and it looks hopeless - infinitely many matrices fit the observed entries - until one assumes the structure that makes recommendation possible: the table is essentially low rank, because tastes are governed by a few latent factors. In their landmark 2009 paper 'Exact Matrix Completion via Convex Optimization' (Foundations of Computational Mathematics), Emmanuel Candes and Benjamin Recht proved that an n-by-n matrix of rank r can be recovered exactly, with high probability, from only about n^1.2 * r * log n randomly observed entries - not by the NP-hard route of minimizing rank, but by minimizing the nuclear norm, a convex surrogate (the sum of the singular values) solvable efficiently. The proof, in the lineage of Candes-Romberg-Tao compressed sensing, turns on two ideas: an incoherence condition ensuring the singular vectors are spread out rather than spiky, and a dual certificate witnessing optimality, whose existence rests on delicate random-matrix concentration. It transformed a practical engineering puzzle into rigorous theory and seeded a decade of work across machine learning, signal processing, computer vision, and sensor localization. This mission formalizes the Candes-Recht exact-recovery theorem in Lean, decomposed into its dual-certificate construction and the probabilistic concentration reductions at its core.
A number field has a unit group which, by Dirichlet's unit theorem, is free of -rank modulo roots of unity. Fix a prime and embed the units diagonally into the units of the completions of at the primes above . The topological closure of the image is a finite free a -module modulo roots of unity, and its -rank can in principle be smaller than : units that are independent over may become dependent -adically. Leopoldt's conjecture asserts that this never happens.
The conjecture controls how many independent -extensions a number field has. Iwasawa showed that if is the maximal -abelian -ramified extension of , then , where is the defect defined below. So a positive defect means extra -extensions beyond the ones accounted for by the archimedean places, and for a totally real field it means a non-cyclotomic -extension exists. Non-vanishing of the -adic regulator is also what makes -adic -functions and -adic class number formulas behave as their complex analogues do.
Timeline of what is actually proved, under which hypotheses:
Beyond the abelian case the conjecture is open. This mission takes the CM claim as its target.
Let be a prime and a number field with ring of integers and units .
Let be the set of primes above , a finite set. For write for the completion and for its valuation ring. Set
the group of semilocal units at , and let
be the diagonal embedding, whose -component is the completion map. Define the -adic closure of the global units
where and the product of the two subgroups is taken inside the abelian group . Finally, the Leopoldt defect of at is
the difference between Dirichlet's unit rank and the free -rank of . The defect is always non-negative, and it is positive exactly when units that are independent over satisfy a -adic relation after the diagonal embedding.
A number field is CM when it is a totally complex quadratic extension of its maximal real subfield . For CM fields a positive defect is equivalent to the vanishing of the -adic regulator of .
This is Theorem 1 of arXiv:1105.4544. It fixes no constants and no auxiliary choices, so it is stable under any later improvement of the argument.
The last is Remark 1.A of the source, attributed there to Laurent: a defect is inherited by finite extensions, because the -adic relations among -generators of the units are preserved under the embedding of unit groups.
The result itself. Leopoldt's conjecture for CM fields would pin down for every CM field and, via the totally real subfield, would rule out non-cyclotomic -extensions of the totally real fields underlying them. It would remove a standing hypothesis from results in Iwasawa theory and -adic -functions that are currently stated conditionally on Leopoldt. Without it, the -rank of the -ramified Galois group is only known to lie in a range.
Formalizing it. Nothing in this area is formalized today. Mathlib has Dirichlet's unit theorem, the archimedean regulator, CM fields, and the completions of a number field at its finite places, but no -adic regulator, no -adic logarithm, and no Iwasawa theory. This mission first pins down a machine-checked statement of the conjecture itself — which is where the mathematical content of Theorem 1 sits, since the theorem is one sentence long — and then attacks it. Because the target is an unrefereed argument, a serious attempt to formalize it is also a test of it: a step that cannot be closed localizes a gap, and a milestone that turns out to be unprovable is itself the finding.
The obvious approach is transcendence theory, and it is the one that works in the abelian case: a -adic relation among units is a vanishing linear form in -adic logarithms of algebraic numbers, and Baker-type lower bounds forbid it. This is exactly Ax's reduction and Brumer's theorem. It stalls immediately beyond abelian fields, because the argument needs units whose Galois structure is explicit — for abelian fields the cyclotomic units supply them, and in general nothing does. Waldschmidt's is the limit of what the transcendence route has delivered in general, and it has not been improved by that route. The source therefore abandons transcendence entirely and argues in Iwasawa theory, constructing a CM -extension of a field where the conjecture is assumed to fail and deriving a contradiction from the classes of primes that split completely in it. That route needs the structure theory of -modules, - and -invariants, Tate cohomology of class group limits, and the vanishing of — none of which exists in Lean.
The development commits to the following conventions, all of them visible in the definition file.
is the subtype of height-one primes of with , and carries a Finite instance. is the dependent product over of the unit groups of the valuation rings adicCompletionIntegers, so it is a commutative topological group. is defined by the intersection displayed above rather than as a topological closure: the source gives both descriptions, and the intersection is the one that needs no choice of topology on . The two can differ by a finite subgroup, which does not affect the -rank.
is defined as the largest for which admits a continuous injective homomorphism into . Continuity is not decoration: as abstract groups embeds into for every , so the topological requirement is what makes the rank the intended one; and since is compact and is Hausdorff, such an injection is automatically a closed embedding. For a closed subgroup of , which is isomorphic to a finite group times , such injections exist exactly for . The cut-off at is carried only so that the supremum ranges over a visibly bounded set of naturals rather than falling back on a junk value; since the -rank of the whole semilocal unit group is already , it never binds.
The defect subtracts in , hence truncates. Since the -rank never exceeds the -rank, truncation is never triggered and is equivalent to the two ranks being equal.
One trivializing formalization is worth ruling out. The goal is not vacuous: it is neither provable nor refutable by unfolding the definitions, and it has genuine content whenever , that is for every CM field other than the imaginary quadratic ones, where Dirichlet's rank is and the statement is trivially true.
A complete development needs, beyond what Mathlib supplies: the -adic logarithm on the units of a local field and the resulting -adic regulator; the Iwasawa algebra acting on inverse limits of -class groups along a -extension, with - and -invariants and the decomposition of Definition 1 of the source; CM -extensions; and Tate cohomology of these modules. All of that is reusable well beyond this mission — it is the missing foundation of Iwasawa theory in Lean. Contributions of any of these pieces as definitions, and of the three supporting targets as theorems, are welcome independently of the goal.
This Textbook project develops a reusable Lean library around Martin Aigner and Günter M. Ziegler's Proofs from THE BOOK. It combines results imported from the existing proof_in_the_book repository with precise contribution targets from the sixth edition (2018). The aim is to preserve mathematical meaning, reuse existing proofs, and make the remaining work accessible to other contributors.
The original import contains 156 distinct platform-accepted results. Euclid, the original main theorem, is retained as a completed milestone when the project goal moves to the sixth-edition extension. Every one of the repository's 40 chapter topics has accepted results. Each result certifies its actual Lean statement, including its hypotheses; this does not certify every argument or every theorem in a chapter. Some proofs reuse Mathlib, while others were developed in the repository. Their source and proof notes retain that distinction.
The imported source snapshot is 873d52e0c88cd351f594221e70c3c5b3559777a9. Imported results use Lean 4.30.0 and Mathlib c5ea00351c28e24afc9f0f84379aa41082b1188f. Immutable public source links are used only where the linked source matches the verified artifact. Compatibility changes, unsuccessful attempts, and verification evidence are retained in the integration project.
The live goal is the explicit conjunction of the 21 linked sixth-edition extension targets. Its reduction connects these targets to the goal, so proving the remaining children advances the project. This goal is deliberately narrower than “every theorem and every proof in the book”; the unlinked topology tasks below are additional formalization work.
New milestones explicitly marked 6th ed. cover Chapters 7 (spectral theorem and determinants), 15 (round circles and links), 35 (finite Kakeya), 37 (permanents and entropy), and 45 (probabilistic counting). They include the precise definitions and boundary conditions needed to state the results. Compiled Open targets are requests for proofs, not proved results. The spectral theorem has a direct Mathlib proof; community results are reused under their actual statements and with attribution.
Two Chapter 15 tasks intentionally remain unlinked mathematical milestones: the full non-equivalence assertion for the depicted Borromean, Tait, and trivial links, and the Fox-coloring invariance bridge for equivalent link diagrams. These invite formalization of the diagrams and the topology bridge as well as proof. The separate modular Fox calculations do not by themselves establish ambient non-equivalence.
The crossing-lemma target is the universal good-drawing form: actual injective edge arcs and exact finite intersection records appear in its interface. It does not assume the desired crossing bound. The Ramsey target preserves the real exponent for odd k. The related public Erdős–Ramsey result with a rounded exponent is identified as a supporting result, not as proof of that full target.
Older milestones use the repository's chapter labels. Repository Chapters 1–21 match the bundled fourth edition; Chapter 22 inserts Van der Waerden's permanent theorem, and Chapters 23–40 correspond to fourth-edition Chapters 22–39. The sixth edition has 45 chapters, so these organizational labels are not sixth-edition chapter numbers. New milestones give sixth-edition numbers and printed source pages explicitly.
Some existing formalizations preserve narrower statements or additional premises. Examples include repository Chapter 13's dihedral-angle conclusion, Chapter 28's Dilworth lower-bound result, and the geometric premises in Chapter 36. Read the actual linked theorem and its description before reusing it. A chapter title or the former Euclid main theorem is not a completion certificate for the collection.
Choose an Open linked theorem and inspect its definitions, exact binders, Mathlib revision, and prior attempts. Reuse a compatible existing result when it proves that statement; preserve the original contributor's attribution. Submit a matching proof for verification. For an unlinked milestone, first formalize and review the source statement and its definitions. These are known textbook results awaiting formalization or proof in this project, rather than claims of new unresolved mathematics.
Source repository: https://github.com/xiangyazi24/proof_in_the_book
Book: Aigner and Ziegler, Proofs from THE BOOK, Sixth Edition (2018), https://doi.org/10.1007/978-3-662-57265-8
The Collatz conjecture, also called the problem, asks whether one elementary iteration rule has the same long-term behavior for every positive integer. It belongs to number theory and discrete dynamical systems: the rule is deterministic and trivial to compute for any fixed input, but no argument is known that controls every orbit. The problem has served as a test case for methods involving congruences, stopping times, probabilistic models, computation, and arithmetic dynamics. Jeffrey Lagarias's survey, The Problem and Its Generalizations, organized much of the classical theory and explains why strong results about large classes of starting values do not settle the universal statement (Lagarias 1985).
The problem has a long record of partial results. By 1985, the literature already included results on stopping-time densities, possible cycles, and divergent trajectories, summarized by Lagarias. In 2019, Terence Tao proved that for every function tending to infinity, the minimum value attained by the orbit of is at most for almost all positive integers , where “almost all” is measured using logarithmic density (Tao 2019). This is a strong statement about typical orbits, but it does not cover every starting value. Computational verification has also been pushed to very large finite ranges; David Barina describes algorithms and verification methods for this task in Convergence Verification of the Collatz Problem (Barina 2021). A finite verification bound, regardless of size, leaves all larger starting values outside its scope.
For a natural number , define the Collatz step by
Write for the result of applying exactly times, with . The forward orbit of is therefore
The familiar orbit beginning at , for example, starts . Reaching is the relevant event; after that point the usual map continues around the cycle .
The mission goal is the universal assertion
The existential index may be zero, so the case is included directly. The hypothesis excludes , whose behavior under the total natural-number definition of is irrelevant to the conjecture.
The goal is the existing public prove2.me theorem collatz_conjecture, rather than a new
copy. Its statement follows the Collatz declaration in the
Formal Conjectures collection.
A proof would classify every positive-integer orbit with respect to reaching . It would simultaneously rule out an orbit that escapes forever without visiting and any nontrivial cycle disjoint from . Partial density results and finite computations establish neither universal exclusion.
The formalization goal is to make the universal quantifiers, parity split, finite iteration, and boundary cases explicit in Lean 4. Supporting contributions can isolate reusable facts about iterates, stopping times, accelerated odd-only maps, residue classes, and finite certificates. Such components may also support formal work on related piecewise-affine integer dynamical systems, while every contribution remains tied to a precisely stated theorem.
Individual trajectories can be computed, and many families of inputs can be reduced by elementary parity arguments, but the map combines contraction and expansion. Even steps halve the current value, while odd steps replace it by the larger value . Local information about a bounded initial segment of an orbit does not supply a uniform bound on all later values or on the time required to reach .
Statistical control of most inputs also leaves exceptional inputs unresolved. Likewise, excluding cycles up to a finite length does not exclude longer cycles, and checking all inputs below a finite threshold does not constrain every larger input. The mission therefore requires statements whose quantifiers genuinely cover all positive natural numbers; a large finite computation or an almost-everywhere theorem cannot by itself close the goal.
The existing Lean statement works over ℕ. Its local collatzStep definition branches on
the proposition that is even, uses natural-number division by on the even branch,
and uses on the odd branch. Iteration is represented by the standard finite function
iterate notation. The theorem quantifies over a positive starting value and asserts the
existence of a finite iterate index at which the value is exactly .
The positivity hypothesis is essential: the total function sends to , so including would make the universal statement false. The mission does not replace the universal quantifier by a fixed numerical bound, and it does not encode a predetermined stopping-time limit. A complete solution must account for every positive starting value.
Useful supporting formalizations include exact relations between the classical and accelerated maps, composition laws for finite iteration, stopping-time predicates, cycle exclusion statements, descent criteria, and checked finite ranges. Each supporting theorem should state its own hypotheses and trust boundary explicitly. Computational artifacts are welcome when their finite scope is stated precisely and their result is connected to a Lean consumer through a checked certificate or another accepted verification boundary.
The -server problem was introduced by Manasse, McGeoch, and Sleator (STOC 1988 / J. Algorithms 1990) as a common generalization of paging, weighted caching, and related sequential decision problems, and their -server conjecture has since become the central open question of competitive analysis. The conjecture asserts that a single ratio — exactly — governs deterministic online server management on every metric space.
Fix a metric space with distance function , and a number of servers . A configuration records where the servers stand: it is a function assigning to each server a point . Moving the servers from configuration to configuration means server travels from to ; the movement cost is the total distance traveled,
A request sequence is a finite list of points of , presented one at a time; write for the list of the first requests (so is the empty list).
A deterministic online algorithm is a rule that, for every finite request sequence , specifies a configuration — where the servers stand after serving the requests of in order. In particular is the initial configuration, before any request arrives. Two points about this way of modeling an algorithm:
Running on produces the configurations , and its cost is the total movement along this trajectory:
For comparison, an offline schedule for starting at a configuration is any sequence of configurations in which places a server at the request , for each — chosen with the whole of known in advance. The optimal offline cost is the infimum, over all such schedules, of the total movement .
Finally, is -competitive if there is a constant — depending on the algorithm, hence possibly on the metric space and the initial configuration, but never on the request sequence — with
The goal fixes no algorithm: any -competitive construction settles it. This is the weakest stable form of the conjecture — it survives every improvement in constants or techniques short of a disproof.
The milestones are the classical results between the trivial and the conjectured, each an existence or impossibility statement over the same definitions: the lower bound on any space with at least points; the conjecture for ; for spaces of exactly points; for the real line; the upper bound of the Work Function Algorithm on every space; the conjecture for spaces of exactly points; the conjecture for three servers in the Manhattan plane — the one settled case over a genuinely two-dimensional continuum (Bein–Chrobak–Larmore 2002; reproved by the unifying potential of Coester–Koutsoupias 2021); Coester–Koutsoupias's 2021 result that the Work Function Algorithm itself — not just some algorithm — is -competitive for three servers on trees, stated over an explicit formalization of the WFA; and the 2023 Bubeck–Coester–Rabani refutation of the randomized analogue: there are -point spaces on which every randomized algorithm is -competitive, stated over a mixed-strategy model of randomized online algorithms.
A proof of the conjecture would close the founding problem of competitive analysis and pin down the exact power of determinism in online optimization over arbitrary metrics; a disproof would separate general metric spaces from every special class where the ratio is known tight. Either outcome recalibrates the field's standard model of adversarial request sequences.
None of these results — not even the lower bound — has a machine-checked proof, and online algorithms as a subject are absent from Mathlib. This mission builds the base layer: a faithful model of online service systems (configurations, online algorithms as prefix functions, offline schedules, competitiveness), the classical possibility and impossibility results over it, and, at the top, the Koutsoupias–Papadimitriou bound, whose potential-function argument is self-contained but delicate. The model is reusable for paging, weighted caching, metrical task systems, and the randomized -server problem.
The obvious first idea — the greedy algorithm, moving the nearest server to each request — is not competitive for any constant, already on three points of the line: two nearby points can ping-pong one server forever while a server parked slightly farther away never moves. Every known competitive algorithm must sometimes move a server other than the nearest one, and the whole difficulty of the conjecture is quantifying exactly how much such foresight-free hedging can achieve. The Work Function Algorithm's analysis via a potential over offline work functions loses a factor of two for reasons nobody has been able to remove; on the lower-bound side, no metric space is known where the deterministic ratio exceeds .
The Lean model commits to: configurations as functions Fin k → M (labeled servers — equivalent in cost to the unlabeled multiset model, since offline can permute labels for free); algorithms as total functions List M → (Fin k → M) with the service constraint, so a step may move several servers (the standard laziness reduction makes this equivalent to one-move-per-request); costs in ℝ via Metric.dist; the offline optimum as an sInf over schedules, which agrees with the attained minimum on finite spaces; and the additive-constant form of competitiveness, quantified as ∃ a, ∀ σ.
Two conventions guard against trivialization. The additive constant is quantified before the request sequence — allowing it to depend on would make every algorithm -competitive. And the lower-bound milestone requires distinct points (Finset.card = k + 1); on spaces with at most points the conjecture is trivially true and the lower bound false.
Three further definitional layers extend the model. The work function workFunction C₀ σ C is the sInf of (schedule cost + final move to C) over schedules serving σ from C₀, and the Work Function Algorithm WFA is defined on finite spaces with k ≥ 1 servers: after each request it moves to a configuration containing the request minimizing (movement cost) + (work function of the history including the request), a minimizer existing by finiteness and ties broken by a fixed arbitrary choice — matching the standard definition with its "ties broken arbitrarily" (our fixed choice is one admissible instance). A tree is a finite metric space carrying a tree graph whose weighted path lengths realize the metric — exactly "the set of vertices of a tree" of the sources. A randomized algorithm is a mixed strategy: a probability measure over an index type together with a deterministic algorithm per outcome and measurable per-sequence cost; its expected cost is a lower Lebesgue integral in , and -competitiveness from demands every outcome start at and one additive constant work for all request sequences.
Welcome contributions: proofs of any milestone in any order (the lower bound and the -point case are the natural entry points); alternative algorithms for milestones already closed; and infrastructure lemmas about moveCost, schedules, and work functions published as reusable platform theorems.
A braid on strands is the everyday object it sounds like: strings hanging between two horizontal plates, each string descending monotonically, no two strings meeting. Emil Artin turned this picture into algebra in 1925 by showing that braids form a group under concatenation and that this group has a finite presentation with generators. The braid groups sit at the crossroads of low-dimensional topology (they are the mapping class groups of punctured discs, and closures of braids produce every link), of algebra (they are the prototypical Artin–Tits groups, torsion-free and orderable), and of representation theory and mathematical physics through the Burau, Lawrence– Krammer and Temperley–Lieb representations.
This mission formalizes the braid-group development of a 2023 master's dissertation, Alexsander Andrey Gomes Tarcha's Um Estudo Introdutório da Teoria de Tranças (UNESP, Rio Claro), whose capstone is Teorema 3.15: the braid group on strands admits Artin's presentation. The dissertation builds the group structure on equivalence classes of geometric braids (Teorema 3.9), shows that the Artin generators generate (Teorema 3.11), derives the braid and commutation relations (Proposição 3.14), establishes the presentation (Teorema 3.15), and closes with two structural properties: the full twist is central (Proposição 3.16) and embeds in for (Proposição 3.17).
Work in the plane . The ordered configuration space
carries the subspace topology of , and the symmetric group acts on it by permuting coordinates. The unordered configuration space carries the quotient topology; its points are the -element subsets of the plane. The base configuration is , and denotes its class in . The geometric braid group is
a loop of -point configurations being exactly a geometric braid, and homotopy of loops being exactly the equivalence by elementary moves used in the dissertation.
The elementary half-twist , for , is the loop that rotates the two base points and by the angle about their midpoint , leaving the other points fixed:
It returns to the base configuration at with the two moving points interchanged, so it is a loop in and defines a class in .
The abstract braid group is the group presented by generators subject to
This is the statement the dissertation actually proves: the map of its proof is defined on generators by , and the work consists in showing that it is a well-defined homomorphism which is surjective and injective. Asking only for an abstract isomorphism would leave the generators unconstrained; naming their images is what makes the presentation usable downstream.
Artin's presentation is what makes the braid groups computable: the word problem, the Burau and Lawrence–Krammer representations, the Markov moves on braid closures, and the Garside normal form all start from generators and relations, while the topological side supplies the meaning of those generators. A formalization that only exhibits an abstract isomorphism cannot be used to compute with a given geometric braid; the version stated here transports each half-twist loop to a generator word, which is what downstream work needs.
On the formalization side, the geometric model (configuration spaces and their fundamental groups) and the algebraic model (a presented group) are already available on the platform in this environment, and the abstract form of Artin's theorem is already stated there as an open problem. What this mission adds is: the elementary half-twist as an explicit, machine-checked loop in — this definition is proved sorry-free here, including the injectivity of the moving configuration at every time and the continuity of the path; the sharpened goal that fixes the isomorphism on generators; and the dissertation's supporting results, none of which is currently on the platform. None of the milestones or the goal has a machine-checked proof yet.
Surjectivity of — every braid is a product of half-twists — is a compactness-and-general- position argument in the dissertation: cut the braid into finitely many slabs in which a single crossing occurs. Turning that into a formal proof requires the homotopy-theoretic substitute, since "general position" is not available for free: a loop of configurations must be subdivided and each piece pushed to a standard crossing.
Injectivity is harder and is the step where a naive approach fails. It is not enough to check that the relations hold; one has to know that they are all the relations, i.e. that a word whose braid is null-homotopic is a consequence of the braid relations. The dissertation follows the classical route through elementary moves on braid diagrams (its Figuras 3.22–3.26), which formalizes as a long case analysis. The standard modern alternative is the Fadell–Neuwirth fibration together with an induction on ; its inductive step needs the exact sequence of the fibration , which is itself substantial work.
The plane is ; configurations are injective tuples indexed by Fin n; the unordered
configuration space is the quotient by the coordinate-permutation action with the quotient
topology; the base configuration is (not ). Braid generators are
indexed by Fin (n-1), the index standing for the book generator ; truncated
natural subtraction means the degenerate values give the trivial group, and the
statements are asserted for all including those cases. The abstract braid group is the
presented group on Fin (n-1) modulo the normal closure of the commutation and braid relators.
The half-twist rotates counterclockwise. The mirror symmetry fixes the base configuration and exchanges the two orientations, so the goal statement does not depend on this choice; a solver may use either convention internally.
The goal cannot be satisfied trivially: it asks for a group isomorphism whose values on the generators are the prescribed classes of explicit loops, so neither the identity on a presented group nor an abstract counting argument suffices.
Contributions welcome beyond the milestones: the Fadell–Neuwirth exact sequence for the plane, the pure braid group as the kernel of the map to , the exponent-sum homomorphism, and torsion-freeness of . The half-twist definition published with this mission is reusable for any further work on braids in this environment.
The matrix-multiplication exponent measures how the arithmetic complexity of multiplying square matrices grows with the ir dimension. Known upper bounds come from constructing large independent matrix products inside tensor powers whose asymptotic rank is controlled. Improving the extraction, rather than finding a lower-rank starting tensor, has driven several recent advances.
Alman, Duan, Vassilevska Williams, Xu, Xu, and Zhou improve the combination-loss analysis by allowing all three variable directions to be treated differently. Their original fourth-power computation gives the bound . The mission targets the slightly weaker rational endpoint , keeping the historical result distinct from the later AlphaEvolve numerical improvement incorporated into the latest manuscript. More Asymmetry Yields Faster Matrix Multiplication, version 2, SODA 2025.
Fix an arbitrary field . The matrix-multiplication tensor represents multiplication of an matrix by a matrix. A tensor's rank is the least number of pure tensors summing to it. The existing Lean definition matMulExp K is the infimum of for integer dimensions , with value at the excluded dimensions and . This definition, and the existing equivalence with the Strassen-preorder exponent, remain unchanged.
The source tensor is the literal fourth power of the Coppersmith–Winograd tensor. The public parenthesization is . Its asymptotic rank is at most . Its canonical coarse components are indexed by triples with . This is the fourth-power, recursion-level-three specialization described in Section 7, not the eighth-power specialization used by the later optimization note. More Asymmetry, Section 7.
A complete split distribution records frequencies of entire fine-grade words, rather than only the marginal split at the next recursion step. At level , these words have length over the alphabet . Three such distributions describe the X-, Y-, and Z-variable blocks. A restricted constituent power keeps only blocks approximately consistent with those distributions, in maximum-coordinate distance at most a specified . An interface tensor is a tensor product of these restricted constituent powers. The approximation tolerance and all three distributions are part of the interface. More Asymmetry, Definitions 3.4–3.6 and 4.1.
The goal is the unconditional field-uniform statement
Its binders and exponent definition match the existing Schönhage and Stothers goals; only the declaration name and endpoint differ. No optimizer result, characteristic condition, distribution, or assumed value surplus is a hypothesis of the root.
The compact proposal has four milestones and the root, totaling five review items. The milestones concern literal fine-to-coarse source restrictions; the fourth-power rank budget; an actual strict six-symmetrized value surplus at the chosen parameter; and the conditional implication from that surplus to the exponent bound. Existing proved source and rank theorems are reused. The open surplus target contains the new complete-split extraction and exact numerical obligations, which are described separately in the proof outline rather than hidden in an opaque certificate definition.
The chosen internal parameter is , so
The substantive value target is the existence of a real such that the actual source has six-symmetrized -value at least in the existing finite-witness semantics. The strict slack leaves room to translate limiting extraction rates into strict lower bases. Neither the existence of that surplus nor a completed exact numerical certificate is claimed at proposal time.
This formalization would capture a new structural improvement, not a re-optimization of the same DWZ square data. Its distinguishing feature is sequentially obtaining the necessary ownership properties for X, then Y, then Z, while preserving more useful fine blocks. The resulting complete-split and interface-tensor theory is also the mathematical foundation for the later AlphaEvolve optimization. More Asymmetry, Sections 2, 4–6; Dupont et al., Section 2.
The known mathematical result is not an open conjecture. The open work is its machine-checked reconstruction. The earlier square and Stothers roots are marked Proved. The newer DWZ fourth-power root has an accepted reduction but remains Open. Its literal fourth source, rank budget, sixfold-symmetry bridge and entropy-certificate infrastructure can be reused independently of that unfinished endpoint. A proof of the numerical DWZ bound alone would not imply the smaller bound targeted here.
The old hashing interface guarantees both coarse X- and Y-block uniqueness. The new method initially requires only coarse X-block uniqueness. Fine Y-block compatibility and usefulness must then establish the ownership needed for the subsequent Z-stage. Applying a theorem whose hypotheses already demand coarse Y uniqueness would discard the new method's essential advantage. Six coordinate permutations create six regions whose parameters and output interfaces must remain consistent. More Asymmetry, Section 4.1 and Figure 1.
Removing incompatible fine blocks creates holes. The relevant repair theorem concerns holes in all three modes and a quantitative supply of broken interface copies. It cannot be replaced without proof by the older square-specific Z-only repair interface. The global and recursive stages also carry subexponential losses and approximation tolerances; their limiting order must be explicit. Numerical feasibility is a separate obligation: floating-point parameters and optimization success are not exact normalization, marginal, entropy, or logarithm proofs. More Asymmetry, Theorem 4.2, Theorems 5.3 and 6.4, and Section 7.
The environment is pinned to Mathlib 777aaa61dcd2a1258d2b4962dbe983ede4d23b2e and Lean v4.29.0-rc3. The development reuses TensorObj, MMObj, restrictions, degenerations, tensor powers, existing tau-value predicates, and matMulExp. The root is uniform over arbitrary fields. Source relations remain target-first: a restriction of A from B is written Restrict A B. A collection of overlapping constituent restrictions must not be relabeled as an external direct sum.
Complete split distributions, simultaneous three-mode projections, interface tensors, region permutations, and explicit finite extraction maps form reusable infrastructure. Exact rational profiles require compatible lengths; approximate profiles require their stated tolerance and limiting argument. No constant-valued replacement for tensor value, vacuous witness hypothesis, or certificate that merely assumes the desired extraction is admissible.
The authors' released code and parameter archive is the provenance source for the original computation. Versioned archive and witness hashes belong to the companion source audit. The optimization program need not be formalized: an exact certificate checker must establish its own normalization, support, marginal and interval conditions. Contributions to complete-split interfaces, sequential ownership, three-mode repair, recursive extraction, entropy certificates, and finite source-to-exponent bridges all advance this mission.
The matrix-multiplication exponent measures how the arithmetic cost of multiplying square matrices grows with their dimension. An improvement in this exponent is relevant both to algebraic complexity and to algorithms whose running times depend on matrix multiplication. This mission formalizes a known improvement using the fourth power of the Coppersmith–Winograd tensor; it does not claim a new mathematical record.
Duan, Wu, and Zhou identify a loss that arises when constituent tensors are analyzed independently although some of their finer components can coexist inside a shared variable block. Their asymmetric-hashing method recovers part of this combination loss. The paper's headline result concerns the eighth power. Its separate fourth-power computation reports in Table 3, printed page 78. The present target is the slightly weaker exact rational endpoint . Duan–Wu–Zhou, Faster Matrix Multiplication via Asymmetric Hashing.
Fix an arbitrary field . The matrix-multiplication tensor encodes multiplication of an matrix by a matrix. Its tensor rank is the smallest number of pure tensors whose sum is that tensor. The existing Lean definition matMulExp K takes the infimum of over integers , with the value at the two excluded small dimensions. This definition is reused without alteration.
A restriction applies a linear map separately to each of a tensor's three variable spaces. A degeneration allows polynomial families of such maps and takes an appropriate leading coefficient. The order of the Lean relation is target first: Restrict A B means that is obtained from . A direct sum uses disjoint variable spaces; a collection of overlapping restrictions does not constitute a direct sum.
The Coppersmith–Winograd tensor has border rank at most . This mission fixes and uses the literal tensor , whose asymptotic-rank budget is . Its standard coordinate partition has 45 coarse components indexed by nonnegative integers . Each coarse component consists of ordered products of square components, whose grades sum to . Duan–Wu–Zhou, Sections 3 and 6–8.
A restricted-splitting value pair consists of a lower value bound and a prescribed distribution on finer Z-variable blocks. In a tensor power, Z-blocks with the wrong empirical split distribution are removed before measuring value. Sixfold symmetrization, using all permutations of the three modes, is part of this definition. Keeping the scalar and discarding the prescribed distribution loses information required by the recursion. Duan–Wu–Zhou, Definition 3.9, Equation (3), and Definition 8.1.
The goal is precisely
It has the same field quantification and exponent definition as the completed Schönhage and Stothers goals. Only the name and rational endpoint change. No distribution, optimizer, characteristic restriction, or unproved value bound is a hypothesis of this goal.
The supporting targets concern the literal fourth-power source; prescribed-splitting component values; the recursive and global extraction inequalities of Equations (34) and (25); an exact certificate for the released fourth-power computation; and the value-to-exponent implication of Theorem 3.2. The proof outline distinguishes stable formal statements from source-level tasks whose complete Lean interfaces still require development. It does not turn an unspecified certificate into an assumption that the desired extraction exists.
The compact milestone list contains four precise statements: the literal fine-to-coarse product restriction; the fourth-power asymptotic-rank bound; existence of a strict six-symmetrized value surplus; and the conditional implication from that surplus to the goal. Together with the root, these are five review items. The first, second, and fourth milestones are marked Proved. The surplus remains Open. An accepted root reduction links the surplus to the proved capstone; it is a proof sketch, not a proof of the exponent bound. Recursive component extraction and exact numerical certification remain substantial work inside that open target.
The planned internal parameter is . Thus . The substantive value obligation is a strict surplus over for the actual fourth-power source, with asymptotic losses absorbed by choosing strict lower rates. The exact certificate must establish this surplus; neither its existence nor its numerical slack is presently claimed as proved.
The result would extend the formalized Stothers endpoint to an asymmetric fourth-power bound. More importantly, it would provide restricted-splitting interfaces that can support subsequent higher-power and more-asymmetric analyses. The mathematical improvement is already established in the cited paper. The task here is to reconstruct its argument with machine-checked statements, concrete tensor maps, and exact numerical bounds.
The earlier square and Stothers mission roots are marked Proved. Reusable infrastructure includes polynomial degenerations, tensor powers, direct-sum value witnesses, hashing and hole-repair lemmas, the literal fourth-power grading, and the final exponent bridge. Two additional literal fourth-power support/restriction bridges and an additive entropy certificate with directed-log inputs are also marked Proved. These statuses do not imply that the new restricted-value recursion or numerical witness is already formalized.
The central difficulty is retaining the correct dependence between each value bound and its prescribed split distribution. The released fourth-power data contains consumer-specific copies of square value pairs. Equal coarse grades do not justify identifying their chosen distributions. The 21 positive fourth-power components use the six-region recursion, whereas the 24 components with a zero coordinate require the boundary merging argument. Duan–Wu–Zhou, Equation (34), Section 7.3, and released implementation.
Global hashing must additionally control competitors with the same marginals, shared Z-blocks, missing fine blocks, and subexponential losses. An isolated restriction into each constituent is insufficient to establish a simultaneous extraction. Numerical optimization presents a separate issue: floating-point normalization and approximate maximum-entropy computations are not exact feasibility or entropy proofs. Exact marginal constraints, positivity domains, and directed error bounds must all be checked.
The environment is pinned to Mathlib 777aaa61dcd2a1258d2b4962dbe983ede4d23b2e and Lean v4.29.0-rc3. The development reuses TensorObj, MMObj, Degenerates, HasTauValueAtLeast, the six-symmetrized value infrastructure, and matMulExp. All endpoint theorems remain uniform over arbitrary fields. Finite profiles use exact integer counts; rational distributions must have compatible unbounded lengths before an asymptotic statement is invoked. Real limiting rates are represented with explicit strict slack where the existing finite-witness predicate does not guarantee endpoint attainment.
No constant-valued replacement for tensor value, opaque witness carrying its desired conclusion, or external direct sum substituted for overlapping source blocks is admissible. New definitions must specify the actual coordinate projections and restrictions they represent. The authors' optimizer is used to find candidate data, not trusted as a proof oracle. Contributions to restricted-power semantics, consumer-specific square pairs, boundary merging, recursive extraction, exact entropy bounds, and source-to-exponent bridges are all directly relevant to the goal.
power4_dup_2.371919.mat. Authors' release.The basic UCB regret bound of Mission II is logarithmic but not tight: its leading constant is eight times the information-theoretic limit, and its worst-case rate carries a spurious . Chapters 8–9 of Lattimore–Szepesvári close both gaps. A refined confidence schedule yields the asymptotically optimal — exactly matching the instance-dependent lower bound of Mission VII for Gaussian noise. The MOSS index achieves minimax regret , matching the lower bound up to a constant. These two theorems are the gold standard for finite-armed stochastic bandits.
The Cook-Levin theorem states that CNF SAT is NP-complete. This mission formalizes the theorem over a multi-tape Turing machine model in Lean 4.
Prove CookLevin.cook_levin_theorem:
under the decider and reduction hypotheses.
A positive integer is perfect when it equals the sum of its proper divisors: , , then , , and so on. Every perfect number anyone has ever exhibited is even. Whether an odd one exists is one of the oldest unsettled questions in mathematics, and it is unsettled in a strong sense: there is no heuristic consensus that odd perfect numbers should be absent for a structural reason, only an accumulating list of conditions any example would have to meet.
The even side of the question is completely resolved. Euclid (Elements IX.36) showed that if is prime then is perfect; Euler proved the converse, so even perfect numbers correspond exactly to Mersenne primes. Nothing comparable is known on the odd side, and the literature instead consists of increasingly severe necessary conditions.
A timeline of what is actually proved about a hypothetical odd perfect number :
None of these results, alone or together, rules out an odd perfect number.
For write for the sum of all positive divisors of . Then is perfect exactly when
equivalently when the divisors of other than itself sum to . The function is multiplicative: whenever , and for a prime power. The quantity is the abundancy index of , so a perfect number is one of abundancy index exactly .
Write for the number of distinct prime divisors of . In Lean, is n.primeFactors.card, and perfection is Mathlib's Nat.Perfect n, which unfolds to ∑ i ∈ n.properDivisors, i = n ∧ 0 < n — the positivity clause is part of the definition, so is not perfect.
Every perfect number is even; equivalently, no odd perfect number exists. This is the weakest statement that settles the question, and it fixes no constants, so no future numerical improvement can invalidate it.
The milestones are the unconditional theorems of the literature listed above, each stated for a hypothetical odd perfect number :
The result itself. A proof of the goal would complete the classification of perfect numbers begun by Euclid: together with the Euclid–Euler theorem, every perfect number would be for a Mersenne prime . A disproof — an explicit odd perfect number — would be an object with at least ten distinct prime factors and more than decimal digits, and would immediately settle a long list of dependent questions about the abundancy index, about the distribution of the values of , and about the multiperfect numbers.
Formalizing it. Only the even half of the theory is currently formalized: the Euclid–Euler theorem is available in Mathlib's Archive (Archive/Wiedijk100Theorems/PerfectNumbers.lean, as Nat.eq_two_pow_mul_prime_mersenne_of_even_perfect and Theorems.perfect_iff_even_and_mersenne), and the main library carries the divisor-sum API around Nat.Perfect in Mathlib/NumberTheory/Divisors.lean, but nothing about the odd case. None of the milestones above is in Mathlib; formalizing them builds the missing -arithmetic infrastructure — factor chains, abundancy estimates, and the parity analysis of on odd numbers — that any attack on the goal, or any future formalization of the computational bounds, will need.
The obvious approach — take Euler's form and push the congruence conditions until they conflict — does not terminate. There is no known local obstruction: the equation has no contradiction modulo any fixed integer, so no congruence argument can close the problem. The known results are all of a different type: they exclude configurations of the prime factorization by finite case analysis on factor chains, and each analysis leaves infinitely many admissible configurations. Increasing weakens the constraints rather than strengthening them, which is why the lower bounds on have advanced by one prime factor per decade at very high computational cost. The upper bound makes the search space finite for each fixed , but astronomically so.
The development is stated over ℕ with Mathlib's Nat.Perfect, so positivity is built into the hypothesis and no separate 0 < n assumption appears. Oddness is Odd n, the number of distinct prime divisors is n.primeFactors.card, and Euler's form is stated with explicit residues p % 4 = 1, k % 4 = 1, together with ¬ p ∣ m and n = p ^ k * m ^ 2. No custom definitions are introduced; everything rests on Mathlib's Nat.sigma / Nat.Perfect API.
One caution on the shape of the milestones. Each is stated conditionally, for an assumed both perfect and odd, so each would follow trivially from the goal theorem. The point of the milestones is precisely that they are proved unconditionally in the literature: a submission is expected to reproduce (or improve on) the published argument, not to derive the statement from an unproved conjecture. Since the goal is itself open on the platform, no admissible proof can take that shortcut.
Contributions welcome: any of the milestones, the supporting multiplicativity and abundancy lemmas needed for them, and reusable infrastructure for on odd numbers. Sharper published bounds — larger values of , the improved Nielsen bound , the Ochem–Rao size bound — are also in scope and are strictly stronger than the milestones listed.
A learner repeatedly chooses one of slot machines, observes only the reward of the chosen arm, and wants to earn almost as much as the best arm in hindsight. This is the stochastic multi-armed bandit, the canonical model of the exploration–exploitation dilemma. This mission formalizes the model (environments, policies, regret, and the regret decomposition ) and the two classical algorithms of Chapters 6–7 of Lattimore–Szepesvári: Explore-Then-Commit and the Upper Confidence Bound algorithm built on the optimism principle. The goal theorem is the instance-dependent UCB regret bound — logarithmic regret with explicit constants, the single most cited result of bandit theory — together with its distribution-free companion .
Wikipedia's pages on open problems are, for many mathematicians, the first contact with a conjecture: a one-paragraph statement, a short history, a list of partial results. The Formal Conjectures library (Google DeepMind, Apache-2.0) turned a large part of that material into Lean 4 statements, so that the conjectures can be attacked — and, just as importantly, stated unambiguously — by machine.
This mission ports a coherent slice of that material to Prove2Me. It is deliberately a portfolio mission: the goal theorem is the Bateman–Horn conjecture, the strongest single statement in the collection, and the milestone list gathers the other conjectures and the landmark theorems that surround them. Some milestones are genuine steps toward the goal (the Bunyakovsky conjecture is literally the one-polynomial case); most are independent open problems from other fields, grouped here because they share a source, a level of difficulty, and a need for faithful formal statements. A reader should not assume that proving a milestone advances the goal theorem. The mission's value is that every statement in it has been written against the same Mathlib revision, checked to compile, and documented well enough to be attacked.
A rough timeline of the collection's landmarks:
The goal theorem concerns prime values of polynomials. Fix a finite set of distinct polynomials. Say that satisfies the Bunyakovsky condition if its leading coefficient is positive, , and is irreducible over ; say that satisfies the Schinzel condition if for every prime there is an integer with — i.e. no fixed prime divides the product at every argument.
For a prime let be the number of residue classes at which some vanishes, let , and let
The Bateman–Horn constant is the (conditionally convergent) Euler product
The other groups use their own vocabulary, each fixed in a definition item of this mission: Kakeya sets in and over ; Mills' property ; Wagstaff primes and Catalan–Mersenne numbers; polynomial self-maps and their Jacobian matrix; nontrivial closed invariant subspaces; linear extensions of a finite poset; Catalan's constant; and an explicit two-symbol Turing machine model with its maximum-shifts function .
The goal theorem is the Bateman–Horn asymptotic: under the Bunyakovsky and Schinzel hypotheses, exists and is positive and
Weaker statements in the same direction appear as milestones, first of all Bunyakovsky's conjecture: under the same hypotheses with , takes prime values infinitely often. The remaining milestones are listed in the milestone panel and are grouped by subject: Diophantine equations (Brocard, Pillai, Lebesgue–Nagell, Catalan/Mihăilescu), Mersenne-type primality (New Mersenne, infinitude of Mersenne primes, Catalan–Mersenne), prime-representing constants (Mills), geometric measure theory (Kakeya in , Kakeya over , Falconer), operator theory (invariant subspace problem and Read's counterexample), group algebras (Kaplansky's zero-divisor and idempotent conjectures), affine algebraic geometry (the two-variable Jacobian conjecture), irrationality and transcendence (, all odd zeta values, Zudilin's theorem, , , , Catalan's constant), order theory (the – conjecture), and computability (Radó's theorem).
The results themselves. Bateman–Horn is the quantitative form of Schinzel's hypothesis H: it contains the twin prime conjecture, the infinitude of primes of the form , and Bunyakovsky as special cases, and it is the standard heuristic behind prime-counting predictions. The other targets are each the headline question of their area: whether every bounded Hilbert-space operator has an invariant subspace; whether group algebras of torsion-free groups are domains; whether Kakeya sets must have full dimension. The solved milestones (Mihăilescu, Davies, Dvir, Zudilin, Read, Saito, Radó) are landmarks whose formal proofs would be significant library contributions in their own right.
Formalizing them. None of the open statements is expected to fall here; the concrete deliverable is a set of faithful, compiling, reusable statements plus formal proofs of the solved milestones, most of which are not in Mathlib today. Several are realistically in reach: the finite-field Kakeya bound (Dvir's polynomial method is short), the elementary fact that and cannot both be algebraic, and Radó's diagonal argument.
For Bateman–Horn, the obstruction is visible already for , : sieve methods bound from above by a constant times the conjectured main term and produce almost-primes, but the parity problem blocks every known sieve from producing a single prime value of an irreducible quadratic. The conditional convergence of the Euler product is a second, smaller trap: the product over must be taken in order, so any reformulation as an unordered infinite product changes the statement.
Each other group has its own obstruction, and they do not transfer: the parity problem says nothing about Kakeya, where the difficulty is that dimension is not stable under the natural compactness arguments, nor about the invariant subspace problem, where the known counterexamples on show that no soft argument can work.
Conventions this mission commits to, all fixed in the definition items:
ℤ[X]; primality of a polynomial value is primality of its
absolute value, and the counting function ranges over natural numbers .IsMulTorsionFree).Contributions welcome: proofs of the solved milestones; sharper variants; and additional faithful statements from the same source library, which contains far more than fits in one mission.
Provenance note. The Lean statements in this mission are adaptations of the Formal Conjectures library (Apache-2.0), rewritten to depend only on Mathlib and on this mission's own definition items, and checked to compile against the platform's Mathlib revision. Each draft item carries a read-back; those read-backs are non-blind — they were written by the same agent that drafted the statements, and each says so in its first line. They are documentation, not independent testimony.
The braid group is one of the places where group theory, low-dimensional topology and knot theory meet. Artin introduced it in 1925 (E. Artin, Theorie der Zöpfe, Abh. Math. Sem. Univ. Hamburg 4 (1925), 47–72) and returned to it in 1947; since then it has become standard equipment in the study of links (closed braids and Markov's theorem), of mapping class groups of punctured surfaces, and of configuration spaces. Birman's Braids, Links, and Mapping Class Groups (Annals of Mathematics Studies 82, Princeton University Press, 1974) is the classical reference that develops all three subjects from the braid group outwards, and its Chapter 1 is the foundation on which the rest of the book rests.
The chapter's structure is itself the reason to formalize it first: everything later in the book — the closed-braid picture of links, Markov's theorem, the Magnus representations, the mapping class group of the punctured sphere — is phrased in terms of the group and of the presentation established here. A mission that fixes faithful Lean definitions of the configuration spaces and of the abstract braid group therefore fixes the vocabulary for the whole series.
Timeline of the results collected here: Artin (1925) gave the presentation and the characterization of braid automorphisms of a free group; Chow (1948) determined the centre; Fadell–Neuwirth (1962) introduced the configuration-space fibrations, and Fadell–Van Buskirk (1962) used them to give the proof of the presentation reproduced by Birman.
Write for the Euclidean plane, identified throughout with the complex numbers . For let
be the ordered configuration space of points in the plane, topologized as a subspace of . The symmetric group acts on it by permuting coordinates; the quotient
with the quotient topology, is the unordered configuration space. A point of is an unordered set of distinct points of the plane. The base configuration is , and all fundamental groups below are taken at or at its image.
The braid group of the plane is : a loop is a motion of points of the plane returning to the same set of points, and homotopy classes of such motions compose as braids. The pure braid group is , the subgroup of motions returning each point to its own starting position.
Separately, let denote the abstract group given by generators subject to
These are equations (1-1) and (1-2) of the book (p. 11). Geometrically interchanges the -th and -st points along a semicircle.
The group of motions of points of the plane is the group with generators and the two families of relations above: the relations are not only valid but defining.
The milestone list follows the chapter: the covering-space description of the projection (Proposition 1.1, p. 11), the Fadell–Neuwirth exact sequence (Theorem 1.4, p. 14), the semidirect-product decomposition of the pure braid group (Corollary 1.8.1, p. 24), the faithful representation of by automorphisms of a free group (Corollary 1.8.3, p. 25), the centre of (Corollary 1.8.4, p. 28, due to Chow), and Artin's algebraic characterization of the braid automorphisms (Theorem 1.9, p. 30).
Theorem 1.8 is what makes the braid group computable: with defining relations in hand one can combine braids into the normal form of Corollary 1.8.2 and solve the word problem, represent braids by automorphisms of a free group, and pass to the link-theoretic material of Chapters 2 and 5 where braid words, not motions, are the objects manipulated. Corollary 1.8.3 turns braids into concrete data — a braid is determined by what it does to the generators of a free group — and Theorem 1.9 says exactly which endomorphisms arise this way; both are the algebraic engine behind the conjugacy-problem and Magnus-representation chapters.
For formalization the state of play is that Mathlib has free groups, presented groups, the fundamental groupoid and fundamental group, covering maps and fibre bundles, but no braid groups and no configuration spaces: nothing here can be assembled from existing declarations. The mission therefore produces reusable infrastructure — configuration spaces of the plane, the symmetric-group quotient, the Artin presentation, the Artin action on a free group — as well as machine-checked proofs of results that are classical but, as far as the mission's search of the library showed, not yet formalized in Mathlib.
The generators and relations are easy to write down and easy to verify in ; what is hard is completeness, i.e. that no further relations are needed. The naive route — draw the braid, push it into a normal form by hand — is exactly what a formal proof cannot do. The Fadell–Van Buskirk argument reproduced by Birman instead runs an induction on driven by the fibration : its homotopy exact sequence gives a split extension of by a free group, presentations are assembled along the extension, and finally the covering with deck group transfers the answer from the pure braid group to the full braid group. Each of those steps needs genuine algebraic topology — local triviality of the projection, exactness of the homotopy sequence, freeness of of a punctured plane — which is where the formalization work actually lies.
The plane is . is the subtype of injective functions
; is its quotient by the equivalence "differ by
precomposition with a permutation", with the quotient topology. Base point: the configuration
, i.e. , and its image. Fundamental groups are Mathlib's
FundamentalGroup at those base points. Braid generators are indexed by
with -based indices ( stands for ), and free-group generators by
; the abstract braid group is a PresentedGroup on that index set. Truncated
subtraction makes the generator set empty for , so and are trivial, as
intended. Two milestones are stated with the shift (i.e. for the projection
) to avoid truncated subtraction in the maps.
Two conventions are worth flagging because they weaken what the Lean text asserts relative to the prose. First, the goal asserts the existence of some isomorphism ; it does not pin the isomorphism down on the geometric generators of Figure 2, since those loops are not part of the formal development. Second, Artin's representation is formalized as the existence of a homomorphism from to the automorphism group of the free group whose value on each is the explicit endomorphism of equation (1-14), together with its injectivity; Theorem 1.9 is then stated for an arbitrary such , given as a hypothesis, and is non-vacuous precisely because Corollary 1.8.3 supplies one.
No trivializing formalization is available: the goal is an isomorphism statement between two groups that are both defined independently of it, and the degenerate cases (both sides trivial) are genuine special cases of it, not the content.
Infrastructure a complete development needs, all reusable: freeness of of a punctured plane, local triviality of the Fadell–Neuwirth projection, the homotopy exact sequence of a fibration in the range needed, presentations of split extensions, and the transfer of a presentation along a regular covering. Contributions of any of these as standalone lemmas are welcome, as is a formalization of the geometric generators (1-9) that would let the goal be strengthened to pin the isomorphism on .
In 1915, George D. Birkhoff proved the existence of a retrograde periodic orbit in each bounded component of the planar circular restricted three-body problem and asked whether its double cover bounds a disk-like global surface of section. Such a surface turns a three-dimensional flow into a two-dimensional return map and was intended as a route to a direct periodic orbit (Birkhoff 1915; Liu--Salomão, Section 1.4). McGehee obtained the corresponding section in the small-mass perturbative regime in 1969, while modern contact and symplectic methods recast the question in terms of regularized energy hypersurfaces and Reeb dynamics (Joung--van Koert, Introduction).
In 2012, Hryniewicz established the global-section criterion later quoted by Joung and van Koert: on a dynamically convex star-shaped hypersurface, the proposed binding orbit must be unknotted with self-linking number −1 (Joung--van Koert, Theorem 1.3; Hryniewicz). In 2025, Joung and van Koert combined that criterion with validated orbit and convexity computations for and (Theorems 1.2 and 1.5). In May 2026, Liu and Salomão proved the conjecture at every subcritical energy for mass ratios sufficiently close to , in fact obtaining rational open books bound by every retrograde orbit in that regime (Theorem 1.16). Their June 2026 Hill result covers every subcritical energy in Hill's lunar problem, which is a limiting model rather than a finite-mass instance of the circular restricted problem (Liu--Salomão 2026). These results leave the universal finite-mass, all-subcritical statement below as the open target.
Two primaries of masses and , with , are fixed in rotating coordinates at and . For a massless particle with phase coordinates , the Hamiltonian is
This is equation (1.1) of Joung--van Koert. Let be the smallest collision-free critical value, where lies between the primaries. The subcritical range is ; there are then two bounded physical components, one around each primary (Liu--Salomão, Section 4).
The mission labels the primary at . With complex Levi-Civita variables and , the inverse position map is , and the regularized Hamiltonian is
On the collision-free domain, , and its zero level regularizes collision with the labeled primary (Joung--van Koert, equation (2.2)). The selected component is anchored at . Below , it is a star-shaped three-sphere, invariant under the free antipodal deck map , and it double-covers the corresponding Moser-regularized component (Joung--van Koert, Proposition 2.4).
For every , every , and every complete flow on generated by and commuting with the antipodal map, prove
Here consists of and a quotient period with , with no earlier positive time reaching either or . Its physical projection is required to be a -symmetric, simple, collision-free loop of winding around the labeled primary. Traversing it twice gives a least-period closed orbit upstairs. This records the geometric retrograde orbit used in the Birkhoff-conjecture formulation; it does not impose the stronger pointwise astronomical monotonicity test distinguished in Joung--van Koert, Definition 2.1, Proposition 2.2, and Remark 2.3.
The rational page is encoded by a smooth immersive disk lift . Its lift is embedded, its interior is transverse to , and its boundary is the closed double lift. After passing to the antipodal quotient, the interior remains embedded and the only nontrivial fibers are antipodal boundary pairs; hence the boundary maps exactly two-to-one onto the prime quotient orbit. Every nonbinding quotient trajectory must meet the page interior at arbitrarily large positive and negative times, matching the recurrence clause in the standard definition of a global surface of section (Hryniewicz, Definition 1.1).
A global surface of section replaces the continuous three-dimensional regularized flow, away from its binding, by the iterates of a two-dimensional first-return map. Periodic points, invariant sets, and recurrence of that map encode periodic and recurrent trajectories of the original system. This is why Birkhoff connected the conjecture to the existence of a direct orbit, and why later work uses such sections to obtain global dynamical consequences (Birkhoff 1915; Joung--van Koert, Introduction). A proof across all finite mass ratios and all subcritical energies would close the gap between the known perturbative, near-equal-mass, and narrow validated regimes.
Existence of a -symmetric geometric retrograde orbit is not the unresolved step: Birkhoff's shooting argument supplies one in each bounded component for every and every energy below (Liu--Salomão, Theorem 5.1). The difficult assertion is global. One must produce a disk with the correct two-fold boundary behavior, prove transversality at every interior point, and prove that every other trajectory returns to it indefinitely in both time directions. Known proofs obtain these conclusions from convexity, dynamical convexity, and pseudo-holomorphic-curve machinery only in restricted parameter ranges (Joung--van Koert, Theorem 1.5; Liu--Salomão, Theorem 1.16).
The Lean model uses total real-valued extensions of the displayed Hamiltonians, but every physical assertion carries explicit collision-free or denominator guards. The first critical value is initially an infimum; a separate theorem row proves nonemptiness, boundedness below, and attainment at an inner Lagrange point. The energy component is selected by a concrete regularized collision point, the physical mass range is strict, and the headline theorem assumes an actual Flow together with its Hamiltonian-generator and antipodal-equivariance properties. These choices prevent singular derivatives, an unintended component, an empty critical set, or an arbitrary dynamics from satisfying the goal vacuously.
The antipodal quotient in Lean is presently the topological quotient by the explicit deck relation. The formal rational-page predicate is therefore a cover-lift encoding: continuity, the real-action laws, exact quotient fibers, primeness, and global returns are stated downstairs, while smoothness, immersion, and transversality are stated on the Levi-Civita lift. It does not install a smooth atlas or explicit Moser coordinates on the quotient, and it asks for one rational page rather than a full open-book fibration. The theorem concerns one labeled primary; it does not simultaneously assert the analogous result on the other bounded component. The Hill limiting problem and the pointwise astronomical sign condition are not part of the headline conclusion.
All theorem rows are Lean declarations ending in by sorry. Successful elaboration verifies that the statements are syntactically and type-theoretically coherent; it is not evidence that the open theorem has been proved. Supporting rows isolate analytic facts, regularization identities, component geometry, quotient descent, the known retrograde-orbit theorem, and the parameter ranges already covered in the cited literature.
The matrix-multiplication exponent measures the asymptotic arithmetic cost of multiplying square matrices. An upper bound means that, over the field under consideration, two matrices can be multiplied using field operations for every . It is a central benchmark in algebraic complexity and controls the exponent of many algorithms that use matrix multiplication as a subroutine.
Coppersmith and Winograd's 1990 analysis of the square of their tensor established . That number remained the record for roughly two decades. Stothers' 2010 thesis first obtained a smaller exponent by analyzing the fourth tensor power, and Davie and Stothers later supplied a self-contained journal treatment. Their Theorem 5.3 and numerical parameters give ; see Davie--Stothers, printed pp. 367--368. The result is the first historical step below the classical tensor-square barrier and is the natural next capstone after a formal proof of the bound.
This mission formalizes the Davie--Stothers fourth-power argument at the exact rational endpoint . It concentrates on the new mathematical layer introduced by the fourth power: five non-matrix constituents, their recursive value estimates, and the two-dimensional same-marginal ambiguity in the final distribution count.
For a field , an order-three tensor represents a bilinear map. The matrix-multiplication tensor
encodes multiplication of an matrix by a matrix. Restrictions apply linear maps to the three tensor legs; degenerations permit polynomial families of maps. A direct sum of matrix-multiplication tensors has disjoint variable blocks and can be converted into an exponent inequality by Schönhage's asymptotic sum inequality.
The Coppersmith--Winograd tensor has border rank at most and a three-class coordinate partition. Its square decomposes into fifteen coarse constituents with . Davie--Stothers square this decomposition again. The fourth power has forty-five constituents with indices summing to eight, grouped into ten symmetry classes represented by
The first five classes are rectangular matrix-multiplication tensors. The last five require recursive value bounds. With , the paper writes
and states the five lower bounds in Lemma 5.1. The final fourth-power extraction assigns frequencies to the ten symmetry classes. Their coordinate marginals are encoded by the matrix in Equation (5.2); its kernel is the two-dimensional space displayed immediately after that equation.
The paper's bounds are limiting exponential rates and may carry subexponential losses in their finite Salem--Spencer extractions. Prove2Me's HasTauValueAtLeast predicate instead records a constant-relative finite witness. The source-faithful formal statements therefore assert attainment of every fixed nonnegative base strictly below each displayed limiting rate, rather than unjustified attainment of the limiting endpoint itself. This downward-closed form retains the complete asymptotic conclusion and is exactly what the final strict numerical surplus needs.
For every field ,
The source's computed endpoint is strictly smaller, giving slack for an exact rational certificate. The Lean goal has exactly the same field quantification and matMulExp definition as the existing Coppersmith--Winograd mission; only the theorem identifier and endpoint change.
The mission records the canonical nine-grading of and the ten symmetry classes of Table 1. It formalizes all five clauses of Lemma 5.1 for , , , , and in every-strict-lower-base form; Equation (5.2) and the stated basis of ; Lemma 5.2's entropy minimization along that kernel; Theorem 5.3's downward-closed fourth-power value inequality; and the Table 2 numerical specialization. The final milestones connect the resulting tau-value surplus to the border-rank budget and transfer the Strassen-preorder exponent bound to matMulExp.
Mathematically, this theorem is the first improvement obtained by passing from the square to the fourth power of the Coppersmith--Winograd tensor. It establishes the recursive constituent pattern used by the later eighth-, sixteenth-, and higher-power analyses. In particular, the five formulas in Lemma 5.1 are the first complete catalogue of genuinely recursive fourth-power constituents.
For formalization, the mission creates a reusable representation of higher-power CW gradings and their symmetry orbits. It also forces a distinction between a locally chosen joint type and all other types with the same marginals. Lemma 5.2 is the exact finite-dimensional entropy correction needed when the marginal map has nontrivial kernel. That infrastructure can be reused by later refined-laser and complete-split missions.
The result is known mathematically. The open task is a machine-checked reconstruction. Prove2Me already contains the CW tensor, its characteristic-free border-rank degeneration, its canonical square grading and constituent restrictions, the Salem--Spencer layer, direct-sum tau-value witnesses, the asymptotic sum inequality, and the exponent bridge. The exact optimizer identity for the profile is also proved. The remaining frontier is to connect the literal fourth-power constituents to finite direct-sum extractions, then assemble all five value estimates and the final kernel-corrected distribution count.
The fourth power contains 225 ordered products before symmetry grouping. A formal proof must show that each claimed constituent is the literal block of and that its recursive decomposition uses the correct variable spaces. Replacing a sum of overlapping blocks by an external direct sum would make the value bound artificially strong.
The five non-matrix classes have different feasible frequency polytopes. Their optimizer formulas are valid only after the corresponding nonnegativity and normalization conditions are checked. The class already has a nontrivial same-marginal family. At the global level the map has a two-dimensional kernel, so marginal counts alone do not determine a unique joint distribution. Ignoring that kernel removes the entropy penalty and invalidates Theorem 5.3.
Finally, Table 2 contains decimal witnesses obtained numerically. A formal proof must replace floating-point evaluation by exact rational parameters and certified bounds for logarithms and real powers, while retaining strict slack at .
The development uses environment 777aaa61dcd2a1258d2b4962dbe983ede4d23b2e and the existing TensorObj, MMObj, restriction, degeneration, HasTauValueAtLeast, tensorAsymptoticRank, matMulExp_strassen, and matMulExp declarations. Top-level theorems quantify over an arbitrary field. Finite block indices and symmetry classes use finite types; frequency vectors and entropy inequalities use real numbers; exact finite profiles use natural numbers before passing to cofinal asymptotics.
The capstone specializes to and the fourth tensor power. Generic grading, orbit, multinomial, entropy, and optimizer lemmas are welcome when they shorten later missions. Every value theorem must ultimately be backed by restrictions or degenerations to direct sums of concrete matrix-multiplication tensors. An opaque value functional, a constituent definition that is an external sum rather than the source block, or a numerical hypothesis that assumes the desired endpoint is outside scope.
Contributions are welcome for the literal nine-grading, symmetry-orbit classification, the five constituent extractions, exact address factorizations, optimizer feasibility, the kernel calculation and Lemma 5.2, exact Table 2 arithmetic, and the final exponent assembly.
Machine scheduling asks how to assign jobs to machines over time. In many applications a job also needs additional scarce resources while it runs: a tool, a skilled operator, a memory bank, a channel. Adding such resources can turn a problem with a polynomial algorithm into an NP-hard one. Błażewicz, Lenstra and Rinnooy Kan (DAM 1983) extended the standard three-field classification of scheduling problems (Graham, Lawler, Lenstra and Rinnooy Kan 1979) with a resource field . They then drew the complete borderline between easy and hard problems for unit-time jobs, identical or uniform machines and the makespan criterion. Their Fig. 2 marks each problem type as polynomially solvable or NP-hard.
This mission formalizes the two hardness results of that classification that come from graph partition problems (Theorems 2 and 3, p. 15). Two identical machines are easy under any resource constraints (Theorem 1, after Garey and Johnson 1975). Theorems 2 and 3 show that a third identical machine, or two machines of different speeds, already makes the problem strongly NP-hard, once the number of unit resources is part of the input.
There are jobs and machines . Each machine processes at most one job at a time, and each job runs on one machine without interruption. Machine has a speed , and every job has unit execution requirement , so it takes time on . Identical machines () are the case ; uniform machines () allow arbitrary speeds.
There are resources . Resource has a positive integer size , the amount available at any time. Job needs a nonnegative integer amount of throughout its execution. A schedule assigns each job a machine and a start time . Its completion time is , and it is being executed at every time with . A schedule is feasible when:
The makespan is .
The resource type means three things: the number of resources is part of the input, every size is , and every requirement satisfies . A unit resource is therefore a conflict: two jobs that both need it can never run at the same time. The problems here have no precedence constraints. and ask for a feasible schedule of minimum makespan. Their decision versions ask, for a threshold , whether a feasible schedule with exists.
The source problems are two graph problems on a graph with :
Both are NP-complete (Garey and Johnson 1979, problems GT11 and GT13).
The construction of p. 15 introduces one job per vertex and one unit resource per nonadjacent pair , required by and only.
Formally: if the language of PARTITION INTO PATHS OF LENGTH 2 is NP-hard, then the language of unary codes of yes-instances of the decision version of is NP-hard. The two speeds are arbitrary positive integers.
The results. Theorems 2 and 3 are two of the minimal NP-hard problems in the paper's classification. Together with Theorem 1 they place the borderline exactly: with unit resources whose number is part of the input, two identical machines are polynomial, while three identical machines, or two machines of different speeds, are strongly NP-hard. Strong NP-hardness rules out pseudo-polynomial algorithms unless P = NP, and it carries over to every more general resource type and machine environment in Fig. 1 and Fig. 2. Section 4.1 of the paper also derives hardness for and from these instances.
Formalizing it. The results are classical and proved on paper, but the paper's proofs are one sentence each ("Clearly", "It is easily seen"). No machine-checked proof exists, and the platform has no model of resource-constrained scheduling with real-valued time. This mission produces that model. It also produces a precise statement of strong NP-hardness on top of Cook's Turing-machine definitions, and the first formal NP-hardness reductions from graph partition problems to scheduling.
The scheduling half of each equivalence depends on the real-time model. On two uniform machines of speeds 2 and 1, jobs take time and , so jobs on the fast machine start at half-integers or anywhere else. The resource constraint must hold at every real time, not at a finite set of checkpoints. An argument that treats time as integer slots applies to the triangle case but does not transfer to the paths case.
The complexity half needs polynomial-time computability of the construction on Cook's one-tape Turing machines, on encoded strings that include malformed inputs. It also needs closure of polynomial-time reductions under composition, which the imported complexity layer states but does not prove.
Fin n, Fin m, Fin l), so are q 0, q 1.CookPvsNP_defs.CubicP3Partition.P3Factor, a spanning non-induced -factor.Welcome contributions: proofs of the two equivalences, polynomial-time computability of the construction on Cook's machines, and a general composition lemma for polynomial-time reductions. The composition lemma is reusable for every hardness mission built on CookPvsNP_defs.
Several classical min-max theorems of combinatorial optimization say that a discrete maximization problem and a continuous minimization problem have the same optimal value, and that both have integral optimal solutions when the data are integral. Edmonds' polymatroid intersection theorem (1970), Fujishige's Fenchel-type duality for submodular functions (1984), Frank's discrete separation theorem for a submodular/supermodular pair (1982), and the potential characterizations of weighted matroid intersection (Frank's weight splitting theorem, 1981; Iri and Tomizawa's criterion for the assignment problem, 1976) are instances. Murota's paper Convexity and Steinitz's exchange property, 1996 places all of them under one theorem: a Fenchel-type min-max formula for a pair of an M-concave and an M-convex function, with integrality on both sides.
Timeline:
Let be a finite nonempty set. For , is its characteristic vector; for , are the sets of coordinates where is positive or negative, , and .
A finite integral base set is a finite nonempty such that for and some has . These are exactly the integer points of integral base polytopes of submodular systems. is the convex hull of .
A function has the exchange property (EXC), and is called M-concave, if for and some has and
A function is M-convex when is M-concave.
For and the concave conjugate and convex conjugate are
and the concave closure and convex closure are and ; they are finite exactly on and .
The primal problem maximizes over ; the relaxed primal problem maximizes over ; the dual problem minimizes over . A maximum over an empty family is .
If and satisfy (EXC), then
with (P1) a finite dual infimum forces , and (P2) if all values are finite and equal and the infimum is attained. If are integer-valued, the infimum may be taken over and is attained there when finite.
The formula gives, in one statement, the integrality of an optimal solution of the relaxed primal problem (the essential content of the first half, as the paper observes on p. 296) and of the dual problem. The paper presents it as a unification of two groups of theorems: Edmonds' polymatroid intersection theorem, Fujishige's Fenchel-type duality and Frank's discrete separation theorem on one side, and Iri and Tomizawa's potential characterization for independent assignment with its extensions by Fujishige and Frank (weight splitting) on the other. In the paper it yields the primal and dual separation theorems (Theorems 6.8, 6.9) and the convolution results (Theorems 6.10, 6.11), and it is the prototype of the Fenchel-type duality of discrete convex analysis.
All results here are proved in the literature; none is known to be formalized. Mathlib has no submodular base polytopes, no matroid intersection theorem and no discrete convex analysis. A formal proof of Theorem 6.4 would also require formal proofs of the two cited results, Frank's discrete separation theorem and the M-concave intersection theorem, which the paper uses without proof.
Lemma 6.3 is polyhedral convex duality and holds for any functions. The content is equality with the integral problem: the relaxed maximum over the polytope must be attained at an integer point. For general finite sets it is not, and the intersection of two integral polytopes generally has fractional vertices. Both the integrality of (Edmonds) and the existence of an integral optimal potential depend on the exchange structure; a direct argument from the definitions of conjugates does not see it. The dual integrality claim, that can be taken integral, is again specific to (EXC) and fails for general concave extensions.
Lean conventions, all in namespace SteinitzExchange.Duality:
[Fintype V] [DecidableEq V] [Nonempty V]; integer vectors are V → ℤ, real vectors V → ℝ; finite sets of integer vectors are Finset (V → ℤ).(V → ℤ) → ℝ used only at points of . M-convexity of is (EXC) for fun x => -ζ x; lives on and on , which are distinct sets in general.⨅/⨆ over and are evaluated only on the convex hulls, where they equal the paper's values; off the hulls they carry a junk value instead of , which no statement uses.EReal, as suprema and infima of coerced reals, so no occurs. EReal's supremum of the empty family is , the paper's convention. The dual infimum is never a real ⨅ (which would return when unbounded and make (P1) meaningless).V → ℤ.Formalizations that would trivialize the goal are excluded: an unrestricted real infimum for the dual, a convex closure built from instead of , a single base set for both functions, and a relaxed maximum taken over all of instead of .
Needed infrastructure: finite convex hulls and polyhedral Fenchel duality, submodular base polytopes and their integrality, Frank's separation theorem, and the valuated intersection theorem. The submodular-system layer (Theorem 2.1, Theorem 6.5) is reusable beyond this mission. Contributions to any milestone, including proofs of the two cited theorems, are welcome.
Linear optimization over the bases of a matroid, over the integer points of a polymatroid, or over the flows of a network is well understood: the greedy algorithm is exact, the feasible sets are the integer points of polytopes described by submodular functions, and min-max theorems of Edmonds and Frank hold with integrality. Nonlinear objectives on the same sets are much less uniform. Valuated matroids (Dress and Wenzel, 1990; see Murota 2003) showed that a quantitative form of the Steinitz exchange axiom is exactly what keeps the greedy algorithm exact for a nonlinear weight. Kazuo Murota's paper Convexity and Steinitz's Exchange Property (Adv. Math. 124 (1996) 272–311) extends this exchange axiom from matroid bases to the integer points of arbitrary integral base polytopes, names the resulting functions M-concave, and proves that they are the discrete counterpart of concave functions. The paper is the starting point of discrete convex analysis (Murota, Discrete Convex Analysis, SIAM 2003), which is now used in auction theory (gross-substitutes valuations are M♮-concave), inventory and resource allocation, and combinatorial optimization.
This mission covers the first of the paper's three characterizations of M-concavity: the Extension Theorem (Theorem 4.6).
Let be a finite nonempty set. For , is the characteristic vector of . For , , , , and .
A finite integral base set is a finite nonempty such that for and there is with (axiom (B1)). Examples are the incidence vectors of the bases of a matroid. Its convex hull is an integral base polytope; in general, an integral base polytope is the convex hull of some finite integral base set.
A function satisfies the exchange property (EXC), and is called M-concave, if for all and there is with , and
The local exchange property (EXC) asks only, for with , for some and some with the same conclusion.
For , , and . For any , the concave conjugate is and the concave closure is , a concave function that is finite exactly on . A function extends if on .
For a finite integral base set and ,
The Extension Theorem identifies a combinatorial axiom with a convex-analytic property: M-concave functions are exactly the restrictions to lattice points of concave functions on the base polytope whose linear perturbations are all maximized on integral base polytopes. It is the reason the M-concave class supports a convex-analysis-style theory at all: local optimality implies global optimality, maximizers of linear perturbations are well behaved, and conjugacy (the paper's Theorems 5.3 and 6.4, separate missions of this series) can be developed. Theorem 3.1 on its own is widely used to verify M-concavity in applications, since it reduces the exchange axiom to pairs at distance four.
All results here were proved in 1996. To our knowledge none of them has a machine-checked proof; Mathlib has matroids on sets but no integral base sets in , no M-concave functions and no concave closure of a function on a finite set. A formal proof of this chain would be a first formal development of discrete convex analysis.
The equivalence of (EXC) with its local version (Theorem 3.1) is not a routine induction on : the exchange inequality for a far pair does not follow from the inequalities along a path of distance-4 pairs, because the exchange partner must be chosen consistently with the prescribed . For the "if" direction of Theorem 4.4, knowing that every maximizer set is an integral base set says nothing directly about the values of at non-maximizing points; turning this global information on maximizers into the local inequality (EXC) requires a supporting hyperplane of the concave closure at a well-chosen point and the integrality of the intersection of an integral base polytope with a box (a cited result on submodular systems). Theorem 4.6 then needs the concave closure to agree with on (Lemma 4.5), which fails for general .
All declarations live in the namespace SteinitzExchange.Extension. The ground set is a type V with [Fintype V] [DecidableEq V] [Nonempty V]; integer vectors are V → ℤ, real vectors V → ℝ, and toReal embeds the former into the latter. is a Finset (V → ℤ). A function is a total (V → ℤ) → ℝ whose values are only ever read at points required to be in . is Mathlib's convexHull ℝ of the image of . Pinned readings:
Trivializing formalizations are ruled out: the extension must agree with on and be concave on , the argmax is over and not over , and an integral base polytope is never empty.
A complete development needs basic facts on integral base sets (the equivalence of (B1) with the simultaneous exchange (B2), , and the paper's cited Theorem 2.1 relating them to submodular functions), the representation (4.3) of the concave closure as a maximum of convex combinations, and supporting hyperplanes of polyhedral concave functions. The layer of integral base sets and M-concave functions is reusable for the two other missions of this series and for any later formalization of discrete convex analysis; contributions of general-purpose lemmas about it are welcome.
The Riemann zeta function at integers splits into two very different worlds. At even arguments Euler's formula shows every is a rational multiple of , hence irrational and even transcendental. At odd arguments almost nothing is known. The single exception is , proved irrational by R. Apéry in 1978 (Astérisque 61 (1979), 11–13). For every other odd argument the arithmetic nature is open to this day: no individual value is known to be irrational.
What is known are localisation results, which assert that an irrational number occurs somewhere in a finite or infinite list of odd zeta values without saying where.
All objects below are those of the source note, in its own notation.
Fix odd integers and with , and positive integers subject to and
For each integer put and for , and consider the rational function
together with the linear form
Condition (1) gives , so the series converges.
Two arithmetic quantities control the denominators of . Write for the least common multiple of , put for , and set
the product running over primes, where is the integer-valued, nonnegative, -periodic function
The growth of is governed by the saddle points, the zeros of
and by the auxiliary function
Writing for the zero with of largest real part, the two competing constants of the method are
with the logarithmic derivative of the gamma function.
The goal fixes no witness: the statement is satisfied as soon as one of the four values is irrational, and remains the honest form of what the source proves. It is deliberately weaker than the (open) statement that each is irrational, and weaker than any claim identifying which of the four is irrational.
The milestones follow the source's own numbering: Lemma 1 (the linear form and its denominators), the prime-number-theorem asymptotics of , Lemma 2 (the saddle-point asymptotics of for ), the small-values criterion for display (4), Lemma 3 (the criterion ), and the numerical verification of at , , , , for , where and .
The result itself. Together with Apéry's theorem it gives the smallest list of small odd zeta values known to contain an irrational number, and it fixes the current record of the Ball–Rivoal hypergeometric method: the same machinery yields quantitative lower bounds for the dimension of the -span of odd zeta values, and any improvement of the arithmetic factor or the saddle-point estimate propagates directly to those bounds.
Formalizing it. The result is proved mathematically; nothing here is open. What is missing is a machine-checked proof. Mathlib contains the Riemann zeta function, the gamma function, and the prime number theorem, but not Apéry's theorem, not the Ball–Rivoal construction, and not the Chudnovsky–Rukhadze–Hata arithmetic method. A complete development produces reusable infrastructure: integrality of very-well-poised hypergeometric sums, the / denominator-saving mechanism, saddle-point asymptotics for a Barnes-type complex integral, and the standard linear-form irrationality criterion.
The obvious route — exhibit explicit rational approximations to a single and estimate them — fails, and that failure is the content of the field: no construction is known that separates a single odd zeta value. Zudilin's construction instead produces one real sequence that is simultaneously a -linear form in ; irrationality of some coefficient's argument then follows from the two-sided estimate, but the argument is blind to which one.
The three hard steps are independent of one another. First, integrality: the coefficients of have denominators controlled by , and the extra factor — a product of prime powers extracted from the -function — must be divided out; this is a delicate -adic valuation count. Second, asymptotics: the exact exponential rate of comes from a complex integral over a vertical line, evaluated by the saddle-point method at a zero of a degree- polynomial with no closed form. Third, the final comparison is a numerical inequality between two transcendental-looking constants that must be certified rigorously, including a Stieltjes integral of a piecewise-constant function against the digamma function.
Statements are formalized over the reals, with for an integer represented by the convergent series (zetaR); a bridging statement identifies it with Mathlib's riemannZeta at natural arguments, so the goal theorem may be stated with riemannZeta as it already is in the platform library. Admissible parameter sets are a structure carrying , , the sequence , and the hypotheses of the source, so no theorem quantifies over parameters the source excludes. R is a real-valued function of a real variable built from Real.Gamma, and is the tsum of its -st iteratedDeriv at natural arguments; convergence is a separate milestone rather than a silent assumption, so that the value is not asserted to exist by fiat. is the infimum over of the integer-valued expression above, a finite product over primes with (the integer form of ), and the Finset.lcm of . The Stieltjes integral is written as , which agrees with the Riemann–Stieltjes integral because is continuously differentiable on ; uses the principal branch of the complex logarithm.
The saddle point is not defined by a choice function: every statement that mentions it takes it as a parameter together with the hypotheses "root of the polynomial", "positive imaginary part", "maximal real part among such roots", and the two side conditions and of Lemma 2. No milestone is vacuous: for the concrete parameter set of the source such a exists, with .
Contributions of any size are welcome, including partial infrastructure: -adic valuation lemmas for products of factorials, asymptotics of Finset.lcm, saddle-point estimates, and interval-arithmetic machinery for the final numerical comparison.
Call a set of reals a Sidon set when all its pairwise sums are distinct: if with all four in the set, then .
The goal. There is an absolute constant such that every finite set of positive reals contains a Sidon subset with .
This is the lower bound half of Erdos problem 530, which Riddell posed and which asks for the order of the largest guaranteed Sidon subset. That problem is open: it asks whether the guarantee is asymptotically , and the constant is not known. What is settled is the order, by Komlos, Sulyok, and Szemeredi, Linear problems in combinatorial number theory, Acta Math. Acad. Sci. Hungar. 26 (1975) 113-121, as a case of a general theorem about linear equations. Erdos had previously observed the cube-root lower bound and the matching upper bound from . A second and much shorter proof is in Bailleul and Riblet, arXiv:2605.03181.
A one-paragraph argument gives : take a Sidon subset of maximum size, and note that every outside it satisfies or for elements of , so .
That cube root is not a weak first attempt, it is the ceiling for any argument that only counts. An arithmetic progression of length has additive energy of order , so a probabilistic argument cannot see the difference between it and a generic set. Getting from to requires using the structure of the set, and that is what both published proofs do.
Compress, then pigeonhole against a known Sidon set.
An arbitrary finite set of reals has no arithmetic to work with, so first move it into : a finite set spans a finite dimensional -vector space, and a generic rational functional separates its points while preserving every relation . Then squeeze the resulting integers into an interval of length comparable to their number, keeping a constant fraction of them and keeping the property that a Sidon subset of the image lifts to one of the original. Finally intersect with a translate of the Erdos-Turan Sidon set, which has about elements inside . A set of size inside meets some translate of a Sidon set of size in order points, and that intersection is Sidon.
The two proofs differ only in the compression step, and the mission carries both.
The 1975 route compresses in four lemmas driven by a remainder map: choose a modulus dividing no difference, dilate so that the remainders are small, and observe that a small remainder map preserves . Finding the modulus needs a prime counting bound.
The 2026 route replaces all four with one averaging lemma over a real rotation parameter , keeping the elements whose fractional part of is below , where no carry occurs. No prime counting appears anywhere.
Every item is stated in Mathlib primitives alone, so the mission needs no definition items. The Sidon condition, the Erdos-Turan construction, and the reduction relation of the 1975 route are all written out at each use.
The published 2026 proof finishes with Singer's 1938 covering of by Sidon sets. Mathlib has no perfect difference sets, so the mission uses averaging over translates instead. It does the same job at the same order and gives a worse constant, which costs nothing because the goal asserts only that some exists.
Two lemmas of the 1975 paper are deliberately absent. A local formalization of Lemma 2 and Lemma 6 turned out to be false as stated, machine-checked in both cases, so neither is offered here as a milestone. Those are errors in that rendering rather than in the paper, and the 2026 route reaches the goal without either. Lemma 1' is absent for the same practical reason: the 2026 route does not need it.