Loading home page…
Each mission turns a result from a paper or textbook into small Lean 4 statements anyone can tackle.
Campaigns group missions around a shared mathematical goal. Each one tracks a quantity, such as an upper or lower bound. Have a good candidate in mind? Ping us on Slack, Zulip, or WeChat.
Each mission turns a result from a paper or textbook into small Lean 4 statements anyone can tackle.
Campaigns group missions around a shared mathematical goal. Each one tracks a quantity, such as an upper or lower bound. Have a good candidate in mind? Ping us on Slack, Zulip, or WeChat.
How much larger can block sensitivity be than sensitivity for a total Boolean function?
For a total Boolean function , a block of coordinates is sensitive at if flipping every bit in that block changes . Let count sensitive singletons and be the maximum number of pairwise disjoint sensitive blocks. Define and .
This campaign seeks larger exponents for which there exists an infinite family of total Boolean functions , indexed by , satisfying
Here denotes a quantity tending to zero as . Higher is better. The classical exponent is , and Huang's bound gives a ceiling of .
OpenAI's construction achieves an exponent strictly greater than .
One sufficient way to establish an exponent is to find a single total Boolean function with and . Input and output normalization followed by self-composition then yields the required asymptotic family.
Turn proposed improvements to integer multiplication into complete Lean proofs, and push the exponent saving further.
Harvey and van der Hoeven established an algorithm in 2021. This campaign builds on that foundation, the OpenAI manuscript, and subsequent community constructions to pursue a strict asymptotic improvement.
For two -bit integers, the target is
A positive beats asymptotically; larger is better. Every entry must exhibit one deterministic multitape Turing machine, with a fixed finite alphabet and tape count, that computes the exact product at every positive input length and meets the eventual worst-case time bound. The tracked number measures an asymptotic exponent saving.
Classical algorithms solve 3SUM in time. In a 2026 breakthrough, Alman and Vassilevska Williams gave a deterministic algorithm, refuting the integer 3SUM hypothesis. How low can the exponent go?
Building on existing Lean formalizations, this campaign tracks upper bounds for 3SUM on polynomially bounded integers, using a word RAM with -bit words, and pursues smaller exponents.
Classical algorithms solve all-pairs shortest paths in time. In a 2026 breakthrough, Alman and Vassilevska Williams refuted the APSP conjecture with a deterministic algorithm. How low can the exponent go?
Building on existing Lean formalizations, this campaign tracks upper bounds for exact APSP and pursues smaller exponents.
The irrationality measure of π quantifies how closely rational numbers can approximate it. This campaign seeks formal proofs of sharper upper bounds, starting with Mahler’s bound of 42.
The sharp Hlawka inequality for Schatten -norms is a cousin of the triangle inequality: it relates the norms of three matrices to the norms of their pairwise sums and their total sum. For complex diagonal matrices, an exact formula for the best possible comparison constant has been proved in Lean for every real . We conjecture that the same formula holds for all .
What is the smallest cutoff for which this formula holds for every real ?
References:
Is every odd number a sum of primes? This campaign tracks formalized proofs of the smallest that suffices.
Schnirelmann (1930) showed some finite works. Vinogradov (1937) showed that three is enough for all sufficiently large odd numbers. Tao (2012) proved unconditionally. Helfgott (2013) proved that every odd number greater than is a sum of three primes, though the proof is still unrefereed. Ideally, we can formalize this statement here. Note that three is optimal: is neither prime nor + prime.
Schoolbook matrix multiplication takes operations. The exponent is the infimum of all such that two matrices can be multiplied in arithmetic operations; trivially , and is conjectured but open.
Strassen gave the first nontrivial bound, , in 1969, and introduced the laser method in 1986 to reach . Coppersmith and Winograd's 1990 bound of stood for two decades. Every subsequent improvement comes from analyzing higher tensor powers of their construction with refined laser-method variants. That line reached in 2025, and the current record is , from August 2026. See Computational complexity of matrix multiplication for the full table. Can we formalize these results and even improve on them?
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.
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.
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.
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.
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.
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.
How well can an irrational number be approximated by fractions? Dirichlet's pigeonhole argument shows that every irrational has infinitely many fractions with . The irrationality exponent measures how much better than this the best approximations can be: it is the supremum of the exponents for which has infinitely many solutions. Almost every real number has , as do all algebraic irrationals (Roth's theorem), but for specific transcendental constants such as proving any finite bound is hard, and the expected value has been conjectured for decades (recorded, in its -dependent form, in Waldschmidt, Open Diophantine problems, Moscow Math. J. 2004, p. 265). Upper bounds on also control how often integers come close to multiples of , which decides convergence of series such as the Flint–Hills series .
This mission asks for a formal proof that , as stated in an OpenAI preprint dated September 24, 2026 (source). The preprint has not been peer reviewed and its claims have not been independently verified; on the platform the Lean goal is open.
For an irrational real ,
Equivalently, means that for every only finitely many reduced fractions approximate to within . Here is the usual circle constant, Real.pi.
The Lean goal is the conjunction of:
Part 1 is the quantitative form stated in Theorem 1.1; it applies to all numerators and denominators, reduced or not. The threshold is allowed to depend on and is not effective in the source.
The result itself. It settles the value of the irrationality exponent of , previously bounded only by about . It does not claim a uniform bound (equivalently, bounded continued-fraction partial quotients), which remains a different question. As a consequence the preprint derives convergence of the Flint–Hills series (Corollary 1.2, p. 1) and, more generally, that converges if and only if (Corollary 5.2, p. 20).
Formalizing it. The statement is elementary and fully expressible with real numbers and integers, so a formal proof certifies it without definitional subtleties. The proof combines a weighted multivariable interpolation theorem (zero estimates, intersection-theoretic positivity on blowups) with an interpolation-determinant argument. Mathlib has Liouville-type results and continued fractions, but none of the zero-estimate or interpolation-determinant machinery; those would be reusable for transcendence proofs generally. No machine-checked finite bound on is known.
The classical route to bounds on constructs explicit integrals or Padé approximants with small values and controlled denominators; each refinement lowers the bound slightly, and these methods have no visible path to the value . The preprint instead argues by contradiction from a sequence of successively separated exceptional approximations (Section 1.2, p. 2). Two incompatible estimates are needed for one nonzero determinant: an arithmetic lower bound after clearing denominators (Lemma 3.1, p. 13) and an analytic upper bound (Proposition 3.4, p. 16). Nonvanishing requires an interpolation theorem at centers whose locations are not known in advance (Theorem 2.1, p. 4), and a dimension count alone does not give full rank at these special centers; this is where the curve inequality (Proposition 2.3, p. 7) enters.
Real.pi, integers and rationals only; there is no auxiliary definition file.p q with Q ≤ q, using Real.rpow for (here ).sSup in ℝ of the set of with infinitely many rationals r (in lowest terms, r.den ≥ 2) satisfying the strict inequalities. Since the goal asserts the value , the default sSup conventions for empty or unbounded sets cannot make it trivially true: the set must be nonempty, bounded above, with supremum exactly .Welcome contributions: Dirichlet's approximation theorem in the form needed for Part 2, Siegel-type lemmas, and determinant estimates over .
Rational numbers approximate π to different degrees of accuracy. A useful question is how the error depends on the denominator, rather than how many decimal digits a particular fraction happens to match. The irrationality measure records the boundary between exponents that allow infinitely many exceptionally close rational approximations and exponents whose approximations eventually stop. It is a quantitative question: knowing that π is irrational alone does not determine this boundary.
OpenAI's family 017 formalization selects the assertion that this boundary is exactly 2. This mission imports that precise Lean statement and records its upper-bound consequence in the campaign. The source is pinned to commit adc7f1241b42e322a6451854ab7e4b4c146bf78a, so later repository changes do not change the target.
Let be an integer, let be a positive integer, and measure the approximation error by . A real exponent sets the comparison scale . Larger exponents require smaller errors. A bound that holds for every sufficiently large denominator must have a threshold uniform in the numerator, rather than a separate threshold for each fraction.
For a rational number , write for its positive denominator in lowest terms. Define the set
The source's supremum is taken in the real numbers. Infinitely many rational values are required; repeatedly writing one rational number with larger unreduced denominators does not satisfy this condition. The restriction on excludes integers. These conventions are part of the imported proposition.
The campaign goal is the existing shared predicate :
The threshold may depend on , but must work for every numerator and every eligible denominator. This is the goal named PiIrrationality.openai_bound_two and supplies the campaign value 2.
A separate theorem, OAI.PiExponent.main, preserves both conjuncts of the upstream challenge:
The eventual inequality here is non-strict; the campaign formulation uses a strict inequality with a positive epsilon. They express compatible upper-bound conclusions. The supremum clause additionally records the exact value. No conclusion that the exponent 2 itself belongs to is asserted by the supremum equality alone.
A verified solution to the campaign goal would place the upper bound 2 alongside the campaign's existing bounds, using exactly the same definition. A verified solution to the imported source theorem would also establish the explicit real-supremum characterization. Keeping that theorem separate preserves the stronger original statement while allowing the campaign to compare like-for-like upper bounds.
The OpenAI solution entry point supplies proof terms through its project dependencies. The Comparator challenge file intentionally ends with a proof placeholder. This mission imports statements; the upstream proof development has not yet been imported and verified in this mission. An external proof reference does not by itself complete either target here.
Numerically checking many rational approximations cannot establish either target. The eventual bound quantifies over every real exponent above 2 and every sufficiently large denominator, with no finite upper limit. The threshold must also be independent of the numerator. Conversely, the supremum clause concerns infinitely many distinct rational values, so a finite list of strong approximations does not establish it. These are the mathematical obligations that a submitted proof must discharge.
The imported statement uses Mathlib's real number π, real powers, rational coercions, reduced rational denominators, set infinitude, and real supremum. No custom replacement for π or the campaign's upper-bound predicate is introduced. The source first conjunct quantifies over integer denominators but forces them to be at least 2; the campaign definition uses positive natural denominators. The campaign goal imports Definitions.Def_PiIrrationality_UpperBound from its existing foundation.
The original source uses Lean 4.34.1 and Mathlib revision d13f23b723b8a846827a245b89c10fc7d3f11612. This entry targets the campaign's environment. The existing published source theorem is reused without changing its proposition or Mathlib import. Proof porting, supporting lemmas, and a verified connection between the exact source theorem and the shared campaign goal are welcome. Flint–Hills summability is outside this mission's scope, matching the selected upstream statement.
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.
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.
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 -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.
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.
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 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 .
Multiplying two -bit integers is the basic operation underneath division, square roots, base conversion, evaluation of elementary functions to high precision, and polynomial and matrix arithmetic over ; the cost of all of these is usually quoted in units of the multiplication cost . In 1971 Schönhage and Strassen proved on a multitape Turing machine and conjectured that is the true order of growth. The upper half of that conjecture was settled by Harvey and van der Hoeven in 2019 (published 2021), who gave an algorithm achieving in the same machine model.
Timeline (multitape Turing model).
A -tape Turing machine, in the conventions of Montanaro's Computational Complexity lecture notes (§3, §3.4), has the following parts:
In one step the machine reads the symbol under every head, writes a symbol under every head, moves each head by at most one cell (never left of ), and changes state. Once in it stays there unchanged.
For a bit string , written most significant bit first, let be the integer it represents, and for let be the length- binary representation of , padded with leading zeros. The machine is started in with on the input tape. It computes the product if, for every and all , it reaches with the output tape holding exactly followed by blanks. Its running time is the largest number of steps it takes on any pair of -bit inputs. Write
There is one machine that computes the product and has running time
with the natural logarithm. That is, for all , for some constants and .
The milestones are the self-contained mathematical statements behind the Gaussian resampling step of the paper (§4.1–§4.2) and its prime-selection step (§5.2):
The result. Theorem 1.1 makes an unconditional upper bound for integer multiplication on multitape Turing machines, matching the Schönhage–Strassen conjecture. Through standard Newton-iteration reductions it gives the same bound for division and -th roots, and for computing elementary constants and functions to precision . No superlinear lower bound for is known, so the matching lower bound remains open.
Formalizing it. The theorem has a published proof but no machine-checked proof. A formal proof would also check the full chain of reductions (splitting into digits, Chinese-remainder multidimensional convolution, Gaussian resampling, Nussbaumer polynomial transforms, fixed-point error control, and Turing-machine data movement), each with explicit error and cost accounting. The resampling identity and the norm bounds are statements of independent interest in discrete harmonic analysis, and are useful to formalize on their own.
The obvious approach is a Fourier transform over with bits of precision. This leads to recursive estimates of the form , and every such scheme loses a factor that tends to infinity at each level of recursion. Reaching requires every level of recursion to cost a constant factor less than the previous one. That in turn requires transforms of prime length to be replaced by power-of-two transforms at essentially no extra cost, while keeping bits of precision loss per level. In the Turing model, every reshuffling of data also costs time proportional to the data volume times a logarithm, so the reductions must avoid general sorting wherever its cost would dominate.
IntMul_MultitapeModel, which follows the -tape conventions of Montanaro's lecture notes. Tapes are indexed by and begin with . There is a designated state that freezes the configuration. Tape is a read-only input tape and tape is the output tape. The input is , and the output tape must hold exactly followed by the product bits and then blanks. Running time is the number of steps until .IntMul_HvdH_Resampling.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.
Packing congruent circles into a square is a classical problem in discrete geometry: for each natural number , choose a common radius as large as possible while keeping all disks inside the square and preventing overlap. Every exact value requires two logically distinct achievements: an explicit configuration attaining the proposed radius and a proof that no configuration can do better.
The character of those proofs changes sharply with . The first cases admit short geometric arguments; later cases use contact-graph analysis, specialized case divisions, or computer-assisted global optimization with interval arithmetic. Formalizing the resulting constants therefore provides a growing benchmark for extremal geometry, real algebra, finite configurations, and verified computation in Lean.
This is an open-ended formalization mission. It begins with the exact constants currently represented by theorem-backed milestones, but it is not restricted to a fixed terminal value of . Further milestones may be added whenever an exact packing value and its rigorous optimality argument are identified and stated precisely enough for formalization.
A point is a pair of real coordinates. For points and , squared Euclidean distance is
For a real radius , a point lies in the inner square when both coordinates belong to the closed interval . This is exactly the coordinate condition saying that a closed disk of radius , centered at that point, is contained in the unit square.
The predicate requires and a family of centers in the inner square such that the squared distance between every two distinctly indexed centers is at least . Equality is allowed, so tangent disks are admitted. Radius zero is also admitted.
Define
and define the optimal covered-area fraction by
It is often convenient to use the equivalent point-separation constant , the greatest possible minimum pairwise distance among points in the unit square. The conversion is
The Lean definitions use a supremum rather than assuming in advance that an optimal packing is attained.
The mission currently contains theorem-backed milestones for the following values:
| Exact separation or area value | Proof character in the supplied notes | |
|---|---|---|
| , hence | diagonal bound | |
| minimum enclosing square of a triangle | ||
| , hence | convex hull and perimeter | |
| four-cell pigeonhole argument | ||
| case-specific geometric proof | ||
| hand proof and later computer verification | ||
| case-specific geometric proof | ||
| , hence | classical geometric proof | |
| , hence | theoretical grid-optimality proof | |
| , hence | theoretical grid-optimality proof | |
| , hence | theoretical grid-optimality proof |
For rows stated using , the corresponding milestone for uses the conversion formula above. The equalities are claims about the supremum-defined packing constants, not merely about the displayed candidate configurations.
The milestone list is intended to grow. The supplied survey notes classify and as rigorously solved in the cited literature, while distinguishing and as not rigorously closed in the cited 2021 account. Many of the computer-assisted cases do not have a simple radical expression in the supplied notes. Before such a case is linked to a Lean theorem, its primary source must provide a precise candidate value, algebraic characterization, certified enclosure, or optimal-configuration certificate that can be stated faithfully.
A new milestone should identify:
Numerical evidence and strong bounds are valuable, but they must be labeled as bounds rather than exact-value milestones. Conversely, newly published exact results for larger may be added without changing the underlying definitions.
Every exact-value milestone must connect the proposed value to Packable, r_n, and c_n. Constructing a configuration establishes only a lower bound. An upper-bound argument without attainability also does not establish equality. A complete proof must bridge both directions through the supremum definition.
The proof methods may include:
Shortcuts that redefine , , or to equal a desired answer are excluded. The constants must remain consequences of the common geometric model.
The root theorem CirclePackingConstants.c_all is the conjunction of the eleven exact-value milestones currently in the mission, covering . Its proof sketch reduces the root directly to those milestone theorems, so the mission remains open until every current exact value is proved.
The milestone theorems remain separately reusable and independently auditable. When further exact values are added, a successor aggregate theorem can extend the conjunction and become the new root without replacing the shared definitions or invalidating earlier results.
This structure allows elementary cases, historical hand proofs, and computer-assisted certificates to progress independently while remaining part of one cumulative library of exact circle-packing constants.
The Lean model uses ℝ × ℝ for points and an explicit coordinate formula for squared Euclidean distance. Disk containment is represented by inclusive coordinate inequalities. Nonoverlap is represented by a weak squared-distance inequality, so tangency is permitted. The indexing type is Fin n, and the definitions apply to every natural number, including zero.
The definition bundle contains only Point, sqDist, InInnerSquare, Packable, r_n, and c_n. Solvers may introduce normalization maps, separation bounds, explicit configurations, supremum lemmas, contact structures, certificate checkers, and radical or polynomial identities as auxiliary declarations.
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.
This mission develops Chapter 5 of Quantum Computing: Lecture Notes by Ronald de Wolf. The chapter's selected results describe the mathematical guarantees below.
The linked theorem statements and shared definitions specify the register types, oracle access, normalization, and resource conventions. Their source locators and independent readbacks accompany each target.
The period-finding problem: we are given for which there is an unknown with if and only if .
Let be the power of two with and . Let be the unitary on qubits, with read as an -bit number and written in bits, and let be the quantum Fourier transform on the first register. One run of Shor's algorithm prepares
(one evaluation of and two Fourier transforms) and measures the first register in the computational basis, obtaining . Call good if
Then:
So a good outcome determines : continued-fraction expansion of finds the unique fraction with denominator at most near , and its denominator is the period. This is the quantum core of Shor's factoring algorithm.
Formalization Note The state is the shared shorRunState, with (which gives ) and second register qubits. The intermediate measurement of the second register is omitted: it does not change the distribution of the first register. The probability of a good outcome is the total weight of the basis states whose first register is good. The constants and are quantified before , and . The source's per-run constant is not stated (see notes).
These are known mathematical results. Their Lean statements have been checked and reviewed against the cited source; formal proofs remain open for contributors.
Prove the existing statements under their stated hypotheses and definitions. Any correction to a printed source claim remains explicit in its target description. All listed target proofs are currently sorry; no proof is claimed. The mission goal is the designated chapter capstone; the remaining targets are separate milestones. Parts a, b, c and d are merged into their original chapter.