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.
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.
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.
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 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.
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.
Multiplying two binary integers is a basic task in computational complexity. The relevant resource here is the number of individual steps made by a machine whose tapes can only be accessed through moving heads. Harvey and van der Hoeven established an bound in this model. The OpenAI manuscript proposes a positive saving in the exponent of the logarithm. Subsequent constructions explore larger savings. The formalization target is the complete computation and its time bound, including the analytic and implementation arguments needed to connect a finite construction to every input length.
A deterministic multitape Turing machine has a fixed finite alphabet, a fixed finite state set, and a fixed finite number of tapes. Each tape extends in one direction and has one head. A step reads the symbols under the heads, changes state, writes at those positions, and moves each head by at most one cell. The alphabet contains distinct blank, start-marker, zero, one, and separator symbols. Tape zero is the read-only input tape; tape one is the output tape; further tapes are available for work. The halting state freezes the configuration.
An input consists of two bit strings of the same positive length , separated by . The strings are read most significant bit first, with leading zeros permitted. If denotes the represented natural number, the required output is exactly the -bit binary representation of , padded with leading zeros and followed by blanks. All tapes begin with a preserved start marker. Define .
The full target is
This asserts the existence of one machine that computes the exact product correctly for every positive input length, together with constants and such that every pair of -bit inputs, for and , halts within
steps. Constants, alphabet, states, and tape count are independent of the input length. The number is an exact real value. Larger gives a stronger asymptotic saving because .
Each entry supplies its own exact numerical value and identifies the construction that motivates it. Historical and new entries use the same machine definition. A proposed value may be recorded while its complete proof is still open; it becomes a proved record only when the goal has a verified proof. Numerical certificates are supporting results with their own scope, and do not establish a complete machine time bound.
The value
is the headline conditional witness of S. Jain's integer-mult-kappa, round eight, at revision 5868dc7. It is bound by the complex side ().
The repository states that the claim is conditional: it assumes the full upstream multiplication theorem (the OpenAI manuscript and Colkitt's framework) and that stage two is the complement time-reversal of stage one, and it rests on three further interfaces that are stated but not machine-checked there — IceKylin's normal form for alternating residuals, the cost of binary address adapters for the exterior fix-up children, and the row stock of the stopped bit interchange. Its Lean files check only finite rational statements (moment certificates, the stopped mix and the parameter assembly), not the analytic inequalities or the multiplication theorem. It has not had independent review.
Earlier claims appear as milestones: Harvey–van der Hoeven (), OpenAI Theorem 1 (), Colkitt's checkpoint, Jain rounds six and seven, and community PR #62. Each is implied by this goal because decreases in .
A proof for any positive value would give a strict asymptotic improvement over . Such an improvement would contradict the proposed lower bound, while remaining consistent with the known upper bound. The tracked value concerns asymptotic growth; it does not measure the runtime of a practical implementation. No claim about a currently fastest implementation follows from a larger saving.
Formalizing the full target connects exact finite calculations to a uniform algorithm. The community repository explicitly treats the original framework and remaining all-size interfaces as assumptions of its current evidence. In this mission those steps must be proved before the goal can be marked Proved. They are not added as hypotheses that would weaken the full target. Earlier published theorem statements and finite certificates may be reused with their original attribution and proof status.
A finite network certificate can establish a concrete role count or a rational margin, but does not itself supply a machine for every input length. A complete proof must establish correctness of the recursive construction, admissibility of its parameters, precision and error guarantees, and the cost of moving data on tapes. Counts of algebraic operations alone do not account for this last resource. The difficult connection is between these separate contracts and the single uniform machine quantified by the goal.
The goal imports the existing public Definitions.Def_IntMul_MultitapeModel bundle and uses IntMul.KappaBound directly. No alternative machine or cost model is introduced. Natural numbers describe input lengths, head positions, and step counts; real numbers describe the asymptotic constant and exponent. The real power has base at least one. Correctness is required even below the asymptotic threshold. Inputs of length zero and malformed inputs are outside the specified task.
The input and output conventions exclude a machine that merely decides a predicate about the product. The entire output tape must contain the required product and then blanks. Neither failure to halt nor correctness on a finite collection of test inputs meets the target. The work tapes and final head positions are unconstrained. Reusable contributions include machine composition with explicit costs, exact encodings, analytic estimates, and proofs that the finite certificates imply the contracts required by the recursive algorithm. Every such contribution should state its own assumptions and conclusion explicitly.
Multiplying two binary integers is a basic task in computational complexity. The relevant resource here is the number of individual steps made by a machine whose tapes can only be accessed through moving heads. Harvey and van der Hoeven established an bound in this model. The OpenAI manuscript proposes a positive saving in the exponent of the logarithm. Subsequent constructions explore larger savings. The formalization target is the complete computation and its time bound, including the analytic and implementation arguments needed to connect a finite construction to every input length.
A deterministic multitape Turing machine has a fixed finite alphabet, a fixed finite state set, and a fixed finite number of tapes. Each tape extends in one direction and has one head. A step reads the symbols under the heads, changes state, writes at those positions, and moves each head by at most one cell. The alphabet contains distinct blank, start-marker, zero, one, and separator symbols. Tape zero is the read-only input tape; tape one is the output tape; further tapes are available for work. The halting state freezes the configuration.
An input consists of two bit strings of the same positive length , separated by . The strings are read most significant bit first, with leading zeros permitted. If denotes the represented natural number, the required output is exactly the -bit binary representation of , padded with leading zeros and followed by blanks. All tapes begin with a preserved start marker. Define .
The full target is
This asserts the existence of one machine that computes the exact product correctly for every positive input length, together with constants and such that every pair of -bit inputs, for and , halts within
steps. Constants, alphabet, states, and tape count are independent of the input length. The number is an exact real value. Larger gives a stronger asymptotic saving because .
Each entry supplies its own exact numerical value and identifies the construction that motivates it. Historical and new entries use the same machine definition. A proposed value may be recorded while its complete proof is still open; it becomes a proved record only when the goal has a verified proof. Numerical certificates are supporting results with their own scope, and do not establish a complete machine time bound.
The value
is the conditional witness of S. Jain's integer-mult-kappa, round seven, at revision c05adfe, with the sharper moment certificate merged there (research/round7-moment-refinement/). The README's headline for the same construction is the slightly smaller ; the refinement keeps the frozen round-seven bit network, histogram, complex saving and assembly unchanged, and replaces the reciprocal bound in the moment certificate by a degree-eight Taylor enclosure, which certifies the bit saving .
The construction builds on the OpenAI manuscript and on Colkitt's integer-mult-bounds (it uses the PR #62 producer with interval strips and core-aware pair assembly). Its new ingredients are lifted frames with late copies, deferred readouts, and per-use leaves on the bit side; the complex side is round six's. The repository states that the claim is conditional on the OpenAI manuscript and Colkitt's framework, that stage two (the complement time-reversal of stage one) is assumed rather than machine-checked, and that its Lean files check only finite rational statements (moment certificates and parameter assembly), not the analytic tail inequalities or the multiplication theorem. It has not had independent review.
Earlier claims appear as milestones: Harvey–van der Hoeven (), OpenAI Theorem 1 (), Colkitt's checkpoint, Jain round six () and community PR #62 (). Each is implied by this goal because decreases in .
A proof for any positive value would give a strict asymptotic improvement over . Such an improvement would contradict the proposed lower bound, while remaining consistent with the known upper bound. The tracked value concerns asymptotic growth; it does not measure the runtime of a practical implementation. No claim about a currently fastest implementation follows from a larger saving.
Formalizing the full target connects exact finite calculations to a uniform algorithm. The community repository explicitly treats the original framework and remaining all-size interfaces as assumptions of its current evidence. In this mission those steps must be proved before the goal can be marked Proved. They are not added as hypotheses that would weaken the full target. Earlier published theorem statements and finite certificates may be reused with their original attribution and proof status.
A finite network certificate can establish a concrete role count or a rational margin, but does not itself supply a machine for every input length. A complete proof must establish correctness of the recursive construction, admissibility of its parameters, precision and error guarantees, and the cost of moving data on tapes. Counts of algebraic operations alone do not account for this last resource. The difficult connection is between these separate contracts and the single uniform machine quantified by the goal.
The goal imports the existing public Definitions.Def_IntMul_MultitapeModel bundle and uses IntMul.KappaBound directly. No alternative machine or cost model is introduced. Natural numbers describe input lengths, head positions, and step counts; real numbers describe the asymptotic constant and exponent. The real power has base at least one. Correctness is required even below the asymptotic threshold. Inputs of length zero and malformed inputs are outside the specified task.
The input and output conventions exclude a machine that merely decides a predicate about the product. The entire output tape must contain the required product and then blanks. Neither failure to halt nor correctness on a finite collection of test inputs meets the target. The work tapes and final head positions are unconstrained. Reusable contributions include machine composition with explicit costs, exact encodings, analytic estimates, and proofs that the finite certificates imply the contracts required by the recursive algorithm. Every such contribution should state its own assumptions and conclusion explicitly.
A strongly regular graph with parameters is a finite simple graph on vertices in which every vertex has exactly neighbours, every pair of adjacent vertices has exactly common neighbours, and every pair of non-adjacent vertices has exactly common neighbours. For most parameter tuples the elementary counting and integrality conditions already decide existence; the interesting cases are those that survive every known feasibility test and still resist construction. The tuple is the smallest such case in the family , , and its existence has been open for more than fifty years. John Horton Conway offered $1000 for a resolution, as one of five problems posed at the 2014 DIMACS conference on Challenges of Identifying Integer Sequences (Conway, Five $1,000 Problems (Update 2017)).
Timeline of the problem and of what is known about it:
No graph with these parameters has been found, and no non-existence proof is known.
Fix a finite vertex set and a simple graph on (irreflexive, symmetric adjacency ). For vertices write for the neighbourhood of and for the set of common neighbours. The graph is strongly regular with parameters , written , when
The case says that every edge lies in exactly one triangle — equivalently, the neighbourhood of each vertex induces a perfect matching, so such graphs are locally linear. The case says that every non-adjacent pair is the pair of opposite corners of exactly one -cycle. Conway's problem asks for with these two local conditions.
Counting paths of length two from a fixed vertex gives , which for , reduces to ; with this yields . Writing for the adjacency matrix, for the identity and for the all-ones matrix, strong regularity is equivalent to the matrix identity , which for reads ; the eigenvalues of other than are then and , and integrality of their multiplicities ( and ) is one of the feasibility conditions that passes.
The goal is Mathlib's own proof_wanted conway_99 in Mathlib/Combinatorics/SimpleGraph/StronglyRegular.lean, stated verbatim: existence of a finite type carrying a strongly regular graph with parameters . A resolution in either direction is welcome — a proof settles the existence half, and a proof of the negation settles the non-existence half; the platform records the two as proof and disproof of the same statement.
for every strongly regular graph with , : the counting identity, local linearity, and the integrality restriction that cuts the family down to five non-degenerate parameter tuples.
the two members of the family that are known to exist: the rook's graph (the Paley graph on vertices) and the Berlekamp–van Lint–Seidel graph.
structural consequences for a hypothetical -graph, the last one being Wilbrink's theorem.
A graph, if it exists, is a locally linear graph of maximal density in its parameter range and a partial linear space of girth with points and lines of size ; its existence would also produce new association schemes and new examples for the general classification of strongly regular graphs. A non-existence proof would be the first case in this family ruled out by anything other than the classical feasibility conditions, and would say something new about how far local conditions (, ) constrain global structure.
Nothing in this mission is presently formalized. Mathlib defines SimpleGraph.IsSRGWith, proves the counting identity IsSRGWith.param_eq, the complement rule IsSRGWith.compl, and the matrix identity IsSRGWith.matrix_eq, and records the -graph problem as a proof_wanted. The supporting targets are of three kinds: results that are proved in the literature and only need formalizing (existence at and ; Wilbrink's non-vertex-transitivity; the integrality restriction on ); routine consequences that supply reusable infrastructure (edge and triangle counts, the spectral identity, evenness of ); and the goal itself, which is open mathematics.
The obvious approaches fail for concrete reasons. Exhaustive search is out of range: the graph has edges among pairs, and no isomorph-free generation of locally linear graphs on vertices is feasible. Algebraic constructions are blocked by Wilbrink's theorem — the graph cannot be vertex-transitive, so it is not a Cayley graph and cannot be produced by the group-theoretic constructions that yield most known strongly regular graphs, including the two that work at and . On the non-existence side, every classical feasibility test (the counting identity, integrality of the eigenvalue multiplicities, the Krein conditions, the absolute bound) is passed by , so a proof of non-existence needs an argument that does not factor through the parameters alone.
All statements are phrased with Mathlib's SimpleGraph.IsSRGWith on a Fintype vertex type with DecidableRel adjacency, and use Fintype.card, SimpleGraph.edgeFinset, SimpleGraph.cliqueFinset 3 (triangles as -cliques), SimpleGraph.adjMatrix over , and graph isomorphisms g ≃g g for automorphisms. The goal quantifies over α : Type together with a Fintype α instance, so the vertex set is finite by construction and the empty type does not satisfy the cardinality clause; the statement is therefore not vacuously satisfiable. Note that Mathlib's definition constrains only through pairs that are actually adjacent and only through pairs that are actually distinct and non-adjacent, so degenerate small graphs (the one-vertex graph, ) do satisfy IsSRGWith with , ; the supporting statements carry the cardinality hypotheses (, ) that exclude them where needed, and the degenerate degree is listed explicitly in the classification of feasible degrees.
Infrastructure a complete development needs, and which is reusable beyond this mission: interface lemmas for counting common neighbours in a strongly regular graph; the spectral theory of the adjacency matrix (multiplicities of the two non-principal eigenvalues, and their integrality), which is the missing ingredient for the classification of feasible degrees; a Lean construction of the perfect ternary Golay code and its coset graph, for the case; and decision procedures for strong regularity of an explicitly given small graph, for the case. Contributions to any of these are welcome, as are partial non-existence results (for instance, restrictions on automorphisms of prime order) submitted as separate statements.
Discrepancy theory asks how evenly a collection of objects can be split into two parts. Its central open question is a conjecture of Komlós, first circulated in the 1980s: any finite family of vectors of Euclidean length at most one can be signed so that the signed sum is bounded in every coordinate by a universal constant — independent of how many vectors there are and of the dimension they live in.
Fix vectors with Euclidean norm . A sign vector is an : one sign per vector. Writing for the -th coordinate of the vector , the discrepancy of the family under is the largest coordinate, in absolute value, of the signed sum — that is, , the norm of the signed sum. The Komlós property at constant — KomlosBound K — says that every such family, in every and every , admits a sign vector with every coordinate of the signed sum at most in absolute value.
Set systems embed as the special case of -incidence matrices: if is an matrix of s and s in which every column has at most ones (every element lies in at most sets), the columns scaled by have norm at most one, so the Komlós property gives discrepancy — the Beck–Fiala conjecture.
The goal fixes no value of : any finite universal constant settles it, so the statement survives every improvement in the constant.
Eight results over the same definitions: Beck–Fiala's for degree- set systems; Spencer's for sets on points; Banaszczyk's for the Komlós setting; its corollary for set systems; the reduction "Komlós at implies Beck–Fiala at "; Kunisky's lower bound ; and the two 2025 Bansal–Jiang breakthroughs — for the Komlós setting, and the Beck–Fiala conjecture's bound in the regime .
The conjecture is the meeting point of the two main techniques of discrepancy theory — partial coloring and the Gaussian/convex-geometric method — and each further improvement has forced a new technique into existence. A proof would resolve the Beck–Fiala conjecture in full and sharpen the hereditary-discrepancy landscape; a disproof would break the widely-shared expectation that vector balancing is dimension-free. The problem is also a benchmark for algorithmic discrepancy: every known bound now has a polynomial-time counterpart, and the constructive tools built for it (random-walk roundings, spectral partial colorings) are used across approximation algorithms and ranging into differential privacy.
None of this literature is formalized anywhere; Mathlib has no discrepancy theory at all. The definitions here are elementary — finite sums, absolute values, one norm hypothesis — so the mission's entry cost is unusually low for an open-problem mission: the Beck–Fiala theorem and the scaling reduction are self-contained finite combinatorics, while Spencer and Banaszczyk each force a genuinely new proof technique (pigeonhole partial coloring; Gaussian measure on convex bodies) into Lean.
Random signs lose: they give , not a constant, so the naive probabilistic argument is ruled out from the start. The Beck–Fiala argument caps discrepancy by degree, not by norm, and provably cannot be pushed below by its own bookkeeping. Partial coloring alone loses a logarithm through its iteration, and Banaszczyk's method is blocked at by the Gaussian measure of the cube. The 2025 advance decouples the two methods but still pays iterated polylogarithmic factors. Nothing currently known contracts the remaining gap to a constant, and the lower bound says the constant, if it exists, is at least — so any proof must handle instances strictly harder than the set-system case.
The Lean model commits to: vectors as EuclideanSpace ℝ (Fin m), whose norm is the norm (the hypothesis reads ‖v i‖ ≤ 1); the conclusion written coordinatewise as ∀ j, |∑ i, ε i * v i j| ≤ K, avoiding any auxiliary sup-norm structure; sign vectors as real vectors with ε i = 1 ∨ ε i = -1; and set systems as matrices A : Fin m → Fin n → ℝ with an entrywise hypothesis and column-degree counted by Set.ncard. Quantifier order matters everywhere: in KomlosBound K the constant is fixed before and — a depending on would make the statement the trivial bound. In beck_fiala the hypothesis is required (the degree- system has discrepancy otherwise); the Banaszczyk-form bounds use so that the bound is positive already at . In the Bansal–Jiang milestones the asymptotic and are rendered by existential constants quantified before all instances: the hidden factor becomes for some fixed (the inner shift keeps the iterated logarithm positive), and the threshold becomes for some fixed .
Welcome contributions: any milestone in any order — beck_fiala and komlos_implies_beck_fiala are self-contained finite arguments and the natural entry points; spencer_six_deviations and banaszczyk_bound each import a major technique; komlos_lower_bound needs an explicit construction and a case analysis over all sign vectors. Reusable infrastructure — partial colorings, Gaussian measure bounds for convex bodies, hereditary discrepancy — is welcome as platform theorems. The matrix Spencer conjecture, prefix discrepancy, and the Steinitz problem are related but deliberately left to future missions.
Harmonic maps into singular nonpositively curved spaces arise in geometric analysis, rigidity theory, and the study of group actions on buildings. Near a point in the domain, their infinitesimal growth is measured by an order, obtained from an Almgren-type frequency quotient. For smooth targets that order is tied to familiar Taylor expansion data. Euclidean buildings are instead assembled from Euclidean apartments along reflection walls, so a map can branch through a singular link and a priori might exhibit a much less controlled spectrum of homogeneities. Breiner and Dees prove that, for maps from surfaces, this spectrum is discrete and is governed by the finite rotational Weyl group of the building. The mission formalizes their headline classification theorem, Theorem 1.1 of Breiner--Dees.
The discreteness matters because frequency information is a basic input to stratification and regularity arguments for singular harmonic maps. A finite list of possible denominators prevents homogeneities from accumulating arbitrarily and isolates rank-one behavior. The formal target makes explicit the nonconstant condition used by the source paper's tangent-map reduction. Without it, the usual numerator and denominator of the frequency quotient both vanish for a constant map, so its order is not defined.
A Euclidean Coxeter complex consists of Euclidean space together with an affine reflection group. Taking the linear parts of its affine isometries produces a finite rotational reflection group . A Euclidean building of type is a complete metric space covered by isometric Euclidean apartments whose overlaps are related by elements of the affine Weyl group; the atlas is required to contain the relevant geodesic segments, rays, and lines and to be maximal with these compatibility properties.
The domain is a connected open subset of a complex one-dimensional manifold, hence a Riemann surface domain. The formalization uses a concrete Korevaar--Schoen-style metric Sobolev energy built from normalized local difference quotients and Lebesgue area in charts. A map is harmonic when it has finite local energy and minimizes that energy against competitors with the same trace. For and small radii , the energy and boundary moment determine a frequency quotient. When its limit exists with positive denominator, that limit is the order .
For a nonconstant energy-minimizing harmonic map and any , prove that the order is defined and that there are positive integers such that
If the building has rank one, prove the sharper form
The same theorem also records the small-scale energy and positive-boundary-moment facts needed for the order to be meaningful; these are conclusions, not assumptions supplied by a solver.
The result identifies a purely algebraic constraint on an analytic singularity invariant: every denominator divides the order of the finite rotational Weyl group. In rank one, where the target is a tree or an -tree, it recovers the half-integer spectrum and its lower bound. This converts an apparently continuous local invariant into a discrete one determined by the building type.
Formalizing the theorem requires reusable infrastructure that is largely absent from current Mathlib: concrete Euclidean-building atlases, metric-valued Sobolev energy, trace and boundary-moment constructions, harmonic energy minimization, frequency quotients, and homogeneous tangent-map interfaces. The paper theorem is proved in ordinary mathematics; the open task is to replace the single sorry in the target with a machine-checked Lean proof. A completed development would provide components useful for other singular-target harmonic-map and CAT(0) formalizations.
The target is not a direct consequence of treating the building as a Euclidean vector space. A harmonic map can cross apartment walls, and a single chart need not contain the image of a punctured neighborhood. The local problem must respect both metric energy and Weyl-group compatibility. Moreover, the frequency quotient is defined through limiting analytic quantities, while the conclusion is an exact rational arithmetic classification. Bridging those levels requires controlling tangent maps and the geometry of directions in the building rather than merely proving monotonicity of the frequency.
The rank-one clause is not obtained by substituting into the general statement alone: it also asserts . The formal proof therefore must preserve the nonconstant hypothesis and the positivity information that rules out the degenerate zero-order case.
The Lean bundle fixes a complex one-dimensional manifold model for the source, a genuine complete metric target, a finite affine reflection group acting by Euclidean isometries, and an explicit building atlas. The rotational group is the image of the affine group under taking linear parts, so is not an arbitrary external number. The domain carries a point and is nonempty by construction. The map is required to be nonconstant on the domain; this is the necessary explicit repair of the printed headline, whose later reduction theorem uses the same condition.
Energy, trace, boundary moment, frequency, and order are transparent definitions tied to the supplied geometry. In particular, the caller cannot choose a zero measure or an unrelated predicate to make the target vacuous. The theorem must establish finite small-scale energy, positivity of the boundary moment, existence of the frequency limit, and its classification. Solvers may contribute supporting files for metric Sobolev estimates, tangent-map compactness, homogeneous harmonic-map classification, or finite-reflection-group lemmas, provided they preserve the exact conventions in the definition bundle.
Differentiation replaces a polynomial's zeros by a smaller set of critical points. Repeating it produces a sequence of finite root sets, ending at one point. The derivative-zero-chain problem asks whether a single path can visit an actual zero in every set without accumulating a length that grows with the degree. The question concerns the geometry of polynomial differentiation, rather than numerical root finding: every point of the path must satisfy the appropriate polynomial equation.
Ingo Althöfer posed the uniform-length question and the specific bound four in his derivative-chain problem announcement. Earlier work on assignments between roots and critical points is described in Konrad Kaffka's 2012 thesis. The established geometry includes the Gauss–Lucas theorem and the stochastic and convex-order refinements proved by S. M. Malamud. These results provide reusable inputs; they do not by themselves establish a degree-independent chain-length bound.
A root list is a finite list of complex numbers, with repeated entries recording multiplicity and with . It determines the monic polynomial
For , define its degree- row by , where is ordinary polynomial differentiation. A complete derivative-root chain chooses one complex number from every row, satisfying . Its cost is the Euclidean length
The order runs from the degree-one row to the original polynomial. The first point is therefore the centroid of the original root slots. Reversing the path gives the same cost. All source roots are normalized to the closed unit disk. Degree one has a single point and zero cost; no derivative row is omitted.
The mission's main goal is the weakest stable uniform assertion:
The same real constant must work for all degrees and all root lists. It cannot depend on the polynomial or its degree. This target remains unproved in this development.
The stronger unrestricted milestone is the four-bound, . The original announcement asks for total path length at most and specifically suggests , so this is the corresponding stated target. Additional open milestones concern real-coefficient polynomials with at most two, three or four nonreal conjugate pairs, counting multiplicity. Their proposed bounds are respectively , strictly less than , and . These are explicit statements to prove or refute, not accepted consequences of a scalar estimate. Their real-coefficient hypotheses must not be transferred to the unrestricted goal.
A uniform bound would control one compatible path through every nonconstant derivative row, even as the number of rows grows. It would give information beyond the containment of critical points in the convex hull of their parents. The stronger bound four specifies a quantitative target within the same problem.
The initial accepted development contained 52 proved theorem records and three definition bundles: derivative-chain foundations, root probability, and the finite Hermite model. All three bundles are now listed directly in this proposal. The six additional proved library references retain their original contributors and are separate from those initial 52 accepted proofs. They include standard mathematics, supporting lemmas, conditional constructions, overlapping formulations and restricted class results. This count is not a claim of 52 original discoveries. In particular the square-root baseline is already stated in the organizer-hosted report, while the explicit barycentric root weights and multiplicity-aware Rolle counting are available in Mathlib.
The accepted class results include the length bound for real-coefficient unit-disk polynomials with at most one nonreal conjugate pair, and the bound for real-compressed polynomials , where , , is real, and is its multiplicity-counted nonreal-root deficit. The compressed ray and pair-count bounds are corollaries within that family. The accepted cubic-cube theorem gives a complete chain for , for any monic complex cubic whose roots lie in a radius- disk, with length at most , a common monotone orthonormal coordinate frame and a repeated source-root tail. These are restricted results, not solutions of the main goal.
The proposal also references six existing public results: the real and multivariate martingale-coupling characterizations of convex order, the absolute-deviation and integrated-tail criteria, equality of means under multivariate convex order, and finite optimal-transport attainment and its triangle inequality. These are references to the original records, not duplicate submissions or claims of new proofs by this project. The five stochastic-order proofs are credited to Nickrobbins95 and the finite-transport proof to MKPynnic; theorem submitter and proof author can differ.
These results are supporting inputs, not proofs of the derivative-chain goal. Applying the coupling results still requires a proved convex-order statement for the actual polynomial root laws, with the correct multiplicity weights and uniform marginals. Repeated root slots yield a pseudometric, so the finite metric theorem needs distinct locations with multiplicity weights. The default norm on a real coordinate function space is not automatically the complex Euclidean norm. Neither coupling existence nor separate short edges supplies a complete uniform-length chain without a further compatible selection argument.
The fourth-power theorem and fifth-power theorem now have complete Lean proofs accepted by Prove2me. For every monic complex cubic whose roots lie in a disk of radius , they construct compatible chains through all twelve or fifteen ordinary derivative rows, respectively, with length at most .
Both theorems retain the cubic centroid, one common monotone orthonormal coordinate frame and a final source-root suffix of four or five entries. Repeated roots, zero radius and degenerate centered coefficients are included. Neither statement assumes a supplied prefix or continuation theorem. The accepted cubic-cube result remains a separate restricted-class theorem; these three class results do not settle either unrestricted goal or arbitrary larger powers.
The fourth-power research source, fifth-power research source and their checkpoint archive preserve the original analytic work. The linked theorem records carry the accepted formal proofs and their proved dependency chains.
The public Lean proof archive contains 193 Lean files (182 proof modules and 11 dependencies), reproduction instructions and SHA-256 manifests. This is the complete local-proof snapshot prepared before the final server submission packaging; the accepted submissions and their dependency chains on Prove2me are the authoritative server-verified artifacts. The archive README and formal-proof metadata record the accepted status of both theorems. The original research files are preserved unchanged; their earlier Open notices describe the historical research snapshot.
Convex containment does not control the sum of successive movements. Choosing a short edge separately at each row also need not produce a compatible path: the endpoint of one choice must be the start of the next. The known general square-root bound grows with degree, so it does not answer the uniform question. A variance bound controls squared increments and cannot simply be read as a constant bound on their unsquared sum.
Repeated roots and collisions are genuine cases, not numerical exceptions. The accepted Hermite obstruction rules out a particular local variance-increment estimate; it does not refute the unrestricted chain-length questions. Likewise, accepted scalar and conditional lemmas establish only their displayed conclusions under their stated hypotheses. A proposed polynomial application must prove those hypotheses for the same actual chain.
The Lean model uses Fin n → ℂ root slots, fromRoots for the product polynomial, row a m for the ordinary derivative row, IsChain for actual root membership and chainCost for the finite sum of complex norms. Positive degree, all nonconstant rows, source normalization and multiplicity counting are explicit. No root simplicity assumption or supplied short chain is permitted in the unrestricted goal. Real-coefficient and compressed-form restrictions belong only to their named class theorems.
The accepted proofs use Lean 4.33.1 and Mathlib revision 0df444a360eaa60ab8c11dca51a86af692955474. Existing declarations retain their identifiers and attribution. Generic convex-order and martingale-coupling results are reusable, but a citation to them does not prove the polynomial-specific uniform-root marginal property. Contributions are welcome on exact root-law adapters, compatible selection estimates and the listed open targets. Novelty and faithfulness to the stated problem should be assessed separately from successful Lean verification.
Ingo Althöfer, Math with AI — Diary, derivative-chain problem announcement, 15 August 2026. Announcement.
A Bound for Chains of Zeros of Successive Derivatives, organizer-hosted report. Report.
Konrad Kaffka, Zuordnungen zwischen Nullstellen und kritischen Punkten von Polynomen, Diplomarbeit, Friedrich-Schiller-Universität Jena, 2012. Thesis.
S. M. Malamud, Inverse spectral problem for normal matrices and a generalization of the Gauss–Lucas theorem, Transactions of the American Mathematical Society 357 (2005), 4043–4064. Preprint.
Rajesh Pereira, Differentiators and the geometry of polynomials, Journal of Mathematical Analysis and Applications 285 (2003), 336–348. Article.
Thorsten Theobald and Timo de Wolff, Norms of Roots of Trinomials, 2015 preprint version. Trinomial geometry.
Public formalization reference package: 60 numbered records, including the three definitions, five open targets and 52 accepted proof sources. Statements, proofs and source conventions.
Multiplying two binary integers is a basic task in computational complexity. The relevant resource here is the number of individual steps made by a machine whose tapes can only be accessed through moving heads. Harvey and van der Hoeven established an bound in this model. The OpenAI manuscript proposes a positive saving in the exponent of the logarithm. Subsequent constructions explore larger savings. The formalization target is the complete computation and its time bound, including the analytic and implementation arguments needed to connect a finite construction to every input length.
A deterministic multitape Turing machine has a fixed finite alphabet, a fixed finite state set, and a fixed finite number of tapes. Each tape extends in one direction and has one head. A step reads the symbols under the heads, changes state, writes at those positions, and moves each head by at most one cell. The alphabet contains distinct blank, start-marker, zero, one, and separator symbols. Tape zero is the read-only input tape; tape one is the output tape; further tapes are available for work. The halting state freezes the configuration.
An input consists of two bit strings of the same positive length , separated by . The strings are read most significant bit first, with leading zeros permitted. If denotes the represented natural number, the required output is exactly the -bit binary representation of , padded with leading zeros and followed by blanks. All tapes begin with a preserved start marker. Define .
The full target is
This asserts the existence of one machine that computes the exact product correctly for every positive input length, together with constants and such that every pair of -bit inputs, for and , halts within
steps. Constants, alphabet, states, and tape count are independent of the input length. The number is an exact real value. Larger gives a stronger asymptotic saving because .
This entry targets the reviewed PR #62 checkpoint, . The pinned repository attributes the selected construction to Avi Eisenberg’s interval strips and core-aware pair assembly, eumemic’s joint frame compiler, and Alejandro Zarzuelo Urdiales’s exact parameter refinement and scoped Lean certificates. Douglas Colkitt maintains the project and its integration. The checkpoint combines a bit network with 575-way branching and 137,151,806 physical roles with the retained complex construction. Its finite arithmetic checks do not prove the complete multiplication algorithm. The full theorem remains an open obligation.
A proof for any positive value would give a strict asymptotic improvement over . Such an improvement would contradict the proposed lower bound, while remaining consistent with the known upper bound. The tracked value concerns asymptotic growth; it does not measure the runtime of a practical implementation. No claim about a currently fastest implementation follows from a larger saving.
Formalizing the full target connects exact finite calculations to a uniform algorithm. The community repository explicitly treats the original framework and remaining all-size interfaces as assumptions of its current evidence. In this mission those steps must be proved before the goal can be marked Proved. They are not added as hypotheses that would weaken the full target. Earlier published theorem statements and finite certificates may be reused with their original attribution and proof status.
A finite network certificate can establish a concrete role count or a rational margin, but does not itself supply a machine for every input length. A complete proof must establish correctness of the recursive construction, admissibility of its parameters, precision and error guarantees, and the cost of moving data on tapes. Counts of algebraic operations alone do not account for this last resource. The difficult connection is between these separate contracts and the single uniform machine quantified by the goal.
The goal imports the existing public Definitions.Def_IntMul_MultitapeModel bundle and uses IntMul.KappaBound directly. No alternative machine or cost model is introduced. Natural numbers describe input lengths, head positions, and step counts; real numbers describe the asymptotic constant and exponent. The real power has base at least one. Correctness is required even below the asymptotic threshold. Inputs of length zero and malformed inputs are outside the specified task.
The input and output conventions exclude a machine that merely decides a predicate about the product. The entire output tape must contain the required product and then blanks. Neither failure to halt nor correctness on a finite collection of test inputs meets the target. The work tapes and final head positions are unconstrained. Reusable contributions include machine composition with explicit costs, exact encodings, analytic estimates, and proofs that the finite certificates imply the contracts required by the recursive algorithm. Every such contribution should state its own assumptions and conclusion explicitly.
An insurance company's surplus grows with premiums and falls with claims. In the Cramér–Lundberg model with a positive safety loading, the surplus drifts to with probability one. De Finetti (1957) objected that a company does not accumulate capital indefinitely: surplus above some level is paid out to shareholders. He proposed choosing the payout policy to maximize the expected discounted dividends paid before ruin. This is the optimal dividend problem. It is one of the basic stochastic control problems of actuarial mathematics and corporate finance, and it serves as a test case for singular control of processes with jumps.
The classical answer is a barrier strategy: pay out whatever lifts the surplus above a level and nothing else. Jeanblanc and Shiryaev (1995) proved this optimal when the surplus is a Brownian motion with drift, and Gerber and Shiu studied the same Brownian setting. Azcue and Muler (2005) showed that it can fail in the Cramér–Lundberg model, where the optimal policy may be a band strategy. Avram, Palmowski and Pistorius (Ann. Appl. Probab. 17 (2007) 156–180) treated a general spectrally negative Lévy process, a process with stationary independent increments and only downward jumps. They found the value of every barrier strategy in closed form through the scale function of the process and identified the best barrier level . They also gave a verification condition under which the barrier at is optimal among all strategies. Loeffen (2008) later showed that the condition holds whenever the Lévy measure has a completely monotone density.
Let be a spectrally negative Lévy process on a filtered probability space with and Lévy triplet . Its Laplace exponent is , finite for :
Increments after time are independent of . Initial capital is added to . The standing assumptions are the following: does not have monotone paths, , and either , , or has a density.
A dividend strategy is a nondecreasing, left-continuous, adapted process with . The risk process is and the ruin time is . The strategy is admissible () if no lump sum exceeds the current reserves. Its value is
with discount rate . For , consists of the admissible strategies that keep for .
The -scale function is the unique continuous nondecreasing function on with for large . It is extended by on . The barrier strategy reflects at the level , paying at time . The paper computes its value
and the optimal barrier level is , read as when this set is empty and for all . The generator is
Assume , or has bounded variation, or . Then and:
The goal fixes no constants: the barrier level and the value function are both given by the scale function of the given process.
The theorem gives an explicit solution to a singular control problem for a general Lévy model. The candidate value function and barrier level are expressed through one special function, , and optimality over all strategies reduces to one inequality on . It is the basis of the later literature on scale-function methods in dividend problems (Loeffen 2008, Kyprianou–Rivero–Song 2010, and the refracted and Parisian variants). Part (i) holds with no condition on the Lévy measure. Part (ii) shows exactly where barrier optimality can fail.
The paper's proofs use fluctuation identities (exit problems, excursion theory) and Itô's formula for semimartingales with jumps. None of these is in Mathlib. As far as is known, none of these results has been machine-checked. A formalization would produce a Lévy-process and scale-function layer, a formal model of singular control with jumps and lump-sum payments, and a checked verification argument. Each of these can be reused beyond this paper.
The analytic part is elementary once the value formula (5.1) is available: the choice of , Proposition 3(i) and Lemma 3(i) follow from the shape of . The difficulty lies in the two probabilistic steps. Proposition 1 identifies the value of a reflected process through exit identities for . Those identities rest on excursion theory, or on the martingale property of up to exit. The verification step, Proposition 4(i), needs Itô's formula for . Here is a jump process controlled by a left-continuous finite-variation process that may itself jump. The change-of-variables formula must also run under only regularity when has bounded variation. Just proving that and imply a supermartingale inequality does not settle the question: the lump-sum payments and the jumps of enter the Itô expansion separately and must each be bounded.
Time is (ℝ≥0). is a structure carrying the triplet and pathwise càdlàg paths with only downward jumps. It also carries independence of increments from the filtration and stationarity. Its law is fixed by the Laplace transform for . The standing assumptions of §2 and (3.3) are bundled as one predicate. The scale function is a hypothesis on a function argument (it is unique). is an extended real, since it is for unbounded variation without a Gaussian part.
Values of strategies and value functions lie in . The dividend integral is a Lebesgue–Stieltjes integral over : it counts the lump sum at time and excludes a payment at the ruin instant.
Several conventions are fixed, and each is disclosed in the item it affects:
A trivializing encoding is ruled out: the value is not a real supremum, the barrier strategy is constructed rather than assumed, and is a conclusion.
A complete development needs:
The Lévy and scale-function layer is shared with the companion mission on the bail-out problem. Contributions of general lemmas (Stieltjes integration by parts, optional stopping for càdlàg martingales) are welcome.
Euler's constant measures the gap between the harmonic numbers and the logarithm:
It appears wherever the harmonic series is compared against an integral, and it is the value at of the digamma function, , equivalently . Among the classical constants of analysis it is the conspicuous one whose arithmetic nature is unknown.
For and the arithmetic questions were settled long ago: both are irrational and transcendental. For , neither is known. It is not known whether is irrational, and a fortiori not whether it is transcendental, though it is universally expected to be both.
The goal theorem of this mission is transcendence,
with irrationality carried as a separate, weaker target — a proof of transcendence yields irrationality immediately, but not conversely, and irrationality alone would already be a landmark.
Progress has come in three forms, and the milestones below formalize each.
Conditional bounds on a putative denominator. If were rational, its denominator would have to be enormous. Brent and McMillan (1980), computing to places by an algorithm built on modified Bessel functions, showed any denominator exceeds ; a continued-fraction analysis by Papanikolaou (1997) pushed this past . These are not steps toward a proof so much as a measurement of how far brute computation can go.
Disjunctive results. The strongest unconditional statements pair with the Euler–Gompertz constant
Aptekarev, building on work of Mahler and Shidlovskii, observed that at least one of and is irrational. Rivoal later strengthened this to at least one of them is transcendental. Neither argument isolates which, and that is precisely the obstruction: the Padé-approximation machinery that controls the pair does not separate them.
Irrationality criteria. Sondow, adapting Beukers' treatment of Apéry's theorem for , gave criteria equivalent to the irrationality of in terms of the fractional parts of certain integer sequences. They reformulate the problem rather than resolve it.
Mathlib provides the constant as Real.eulerMascheroniConstant, defined as the limit of , together with the identifications and and the numeric bounds . Irrational and Transcendental ℚ are Mathlib's standard predicates. The Euler–Gompertz constant is not in Mathlib and is supplied here as a mission definition.
A polynomial is split if and for some and . Split polynomials are the simplest non-constant maps defined over that one can apply to an algebraic number: they are exactly the rational polynomials all of whose roots are rational. The question here is how much such a map can do — whether it can always push an algebraic number back down into .
Say is -collapsible if there are split with , collapsible if it is -collapsible, and eventually collapsible if it is -collapsible for some . Problem 3 of Griffin Macris's list of open problems asks whether every algebraic number is eventually collapsible. The two notions come apart at degree : Jordi Ribes settled the cubic case of eventual collapsibility using a composition of three split polynomials, and for eventual collapsibility the open frontier is . For the one-step notion the picture is different — degrees and are settled, and degree is open. That one-step cubic case is this mission's goal.
Let be an algebraic number with . After an affine change of variable over one may assume is a root of a depressed cubic
with discriminant . When the cubic is totally real (three real roots); when it has one real root and a complex-conjugate pair. In the latter case write the roots as
and set , the parameter that controls the archimedean obstruction below. Scaling sends , so the single rational invariant
determines the problem up to scaling: the search space is one rational parameter, not two.
This is the weakest statement that settles the case: it fixes no bound on , and asserts only that some split exists. A version with a degree bound would be strictly stronger and is not the goal, because no such bound is known — indeed the archimedean milestone below shows no uniform one can exist.
The milestone list runs from the reformulation and the invariance reductions, through the known sufficient conditions, to the two obstructions and the two genuinely open sub-targets. Ordered as they are stated there:
The mission also carries, as a plain theorem rather than a milestone, the single open instance — the smallest cubic within computational reach for which no collapsing is known. It is an instance of the goal rather than a step toward it, which is why it is not on the attack path.
A proof of the goal closes the one-step cubic case and, with Ribes's composition result, would give a complete picture at degree . A disproof would be at least as informative: a single cubic admitting no split with would separate -collapsibility from eventual collapsibility by an explicit example, showing that composition is genuinely necessary and not an artefact of the known proof.
The supporting targets have value independent of the goal. The product criterion is the statement everything else is phrased against. The archimedean bound is the only known mechanism forcing , and it is what rules out a uniform-degree approach.
Status, stated precisely. Six of the eight milestones have machine-checked Lean 4 + Mathlib proofs in the author's development, against a newer Mathlib revision than this mission's environment; restating and reproving them here is a port, not new mathematics, and they are included because the goal cannot be attacked without them. The two archimedean milestones are not proved in that form. For the cubic bound both halves exist — the convexity argument and the Möbius reduction — but the statement in terms of a collapsing polynomial has not been assembled. The extension beyond cubics has not been formalised at all; the argument is the same one, since nothing in it uses cubicness beyond the identification of a single circle parameter, but that observation is not a proof. The instance and the goal itself are open.
The obvious approach is to write down a split with rational roots and force by solving for the roots. This works when is a rational square, and more generally under the power-family condition, and produces the bulk of the known examples — but it cannot work in general, for a reason that is quantitative rather than technical.
Suppose and is split with . Irreducibility of forces to be divisible by , hence , hence . Each factor lies on a fixed circle through and determined by , and a convexity argument on then forces
As one has , so the required degree is unbounded: there is no uniform degree in which to search, and any construction must produce split polynomials of growing degree. This is the central difficulty. For the bound already gives , which is why that cubic resists the searches that settle its neighbours.
Only one step of this argument is special to cubics: the identification of the circle parameter as . For an algebraic number of any degree with a real conjugate and a non-real conjugate , irreducibility gives the same relation , the images again lie on a circle through and , and the parameter is , which specialises to in the depressed-cubic case. The obstruction therefore constrains the whole conjecture, not merely its cubic case, which is why the extension is carried as a milestone in its own right.
In the totally real case () the archimedean argument gives nothing at all — the relevant Möbius maps are real and surject onto — and the only known constraint is that each gap between consecutive conjugates contains an even number of roots of . Whether degrees stay bounded there is itself unsettled.
Representation. IsSplit f says and for a nonzero rational and a multiset of rationals; multiplicities are therefore allowed and the roots need not be distinct. Collapsible α is stated for in an arbitrary field carrying a -algebra structure, not only for , so the results apply verbatim to a root in , in , or in . The goal theorem is stated over , with "cubic" expressed as .
Ruling out a trivialisation. Collapsible places no lower bound on and does not require the value to be nonzero, so one must check that the goal is not satisfiable by degenerate means. It is not: would make , impossible for an irreducible cubic dividing a polynomial that splits over . Constant is excluded by . Nothing in the statement is vacuous — the hypotheses of the goal are satisfied by every cubic irrationality.
Conventions in the archimedean milestones. In the cubic bound the parameters enter as real numbers satisfying the factorisation identity, with the normalisation ; this is not a restriction, since is determined only up to sign and the sign may be chosen. Under it , and the conclusion is with the natural-number degree.
In the general bound the corresponding normalisation is . It forces , so is genuinely non-real and , hence and no division-by-zero value can arise in the conclusion. Passing to the complex conjugate of flips the sign of both factors, so the condition is a choice of conjugate rather than a restriction — except when , which the hypothesis excludes and which cannot occur for a depressed cubic with . No degree hypothesis on is needed: possessing both a real and a non-real root already forces .
Infrastructure. A complete development needs Polynomial, Multiset, minpoly, and for the archimedean bound Real.arctan, Complex.arg, and strict concavity of on . The convexity and Möbius lemmas are reusable well beyond this mission — they bound the number of factors in any product of complex numbers constrained to a circle through the origin. Contributions of any of the supporting targets are welcome independently of the goal; so is a disproof, and so is an explicit collapsing of of any degree.
The linear feasibility problem takes a matrix and a vector and asks whether the system of linear inequalities in real unknowns
has a solution. By linear programming duality, optimizing a linear objective over such a set reduces to feasibility, so this decision problem carries the whole complexity of linear programming.
What "polynomial time" means here depends on the machine. In the bit model the input is a list of rational numbers, its size counts the bits of all numerators and denominators, and an algorithm is polynomial if it runs in time . In the real-number model the input is a list of exact real numbers, each arithmetic operation (), comparison, or memory move costs one unit, and a running time may only depend on and . An algorithm polynomial in this second sense is what Smale asks for; the closely related bit-model notion — arithmetic operations and polynomially bounded intermediate bit sizes — is called strongly polynomial. This mission fixes the real-number model precisely as a Blum–Shub–Smale (BSS) machine (Blum–Shub–Smale 1989): a finite program of instructions acting on a bi-infinite tape of real registers — loads of arbitrary real machine constants, exact field arithmetic at fixed addresses, two-sided tape shifts, a sign-test branch, and accept/reject — with cost equal to the number of executed instructions. The convention that costs something: the program must be uniform, one finite instruction list serving every , , and every real instance. Uniformity is exactly what separates the question from point-location tricks available to non-uniform families of decision trees.
For optimization, the question is the last gap in the complexity of its central problem. Linear programs with combinatorial structure already admit strongly polynomial algorithms — Tardos (1986) solved every LP whose running time may depend on the entries of but not on or , covering network flows and all -constraint problems — and a positive answer for general LP would extend that unification to the whole class, while explaining why simplex-type methods behave so well in practice (Spielman–Teng 2004).
For the theory of computation over the reals, the problem is a benchmark for what unit-cost exact arithmetic can do: it is Problem 9 on Smale's list of mathematical problems for the twenty-first century (Smale 1998), posed in the BSS model as the real-number analogue of the P-versus-NP style questions of that program, and it interacts with polyhedral combinatorics through the polynomial Hirsch conjecture: a polynomial bound on polytope diameters is a necessary condition for any polynomial pivot rule. A problem that calibrates both the practice of optimization and the foundations of real computation is a subject, not a special case.
The timeline splits into a negative branch (lower bounds against algorithm classes) and a positive branch (polynomial algorithms in weaker senses).
Lower bounds. Klee–Minty (1972) constructed a deformed cube on which Dantzig's largest-coefficient simplex rule visits all vertices; analogous exponential examples were later found for essentially every deterministic pivot rule, and randomized rules were driven to subexponential lower bounds by Friedmann–Hansen–Zwick (2011) — against upper bounds of from Kalai (1992) and Matoušek–Sharir–Welzl (1996). On the interior-point side, Allamigeon–Benchimol–Gaubert–Joswig (2018) showed by tropical methods that log-barrier path following is not strongly polynomial, and Allamigeon–Gaubert–Vandame (2022) extended this to every self-concordant barrier: no interior-point method of that class can settle the question positively.
Polynomial algorithms in weaker senses. Khachiyan (1979/80) proved LP feasibility is polynomial in the bit model via the ellipsoid method; Karmarkar (1984) and then Renegar (1988) brought interior-point methods to iterations. Megiddo (1984) solved LP in linear time for every fixed dimension; Tardos (1986) gave the combinatorial strongly polynomial class; Vavasis–Ye (1996) and Dadush–Huiberts–Natura–Végh (2020) replaced the bit size by condition measures of alone; Ye (2011) proved policy iteration strongly polynomial for fixed-discount Markov decision processes.
The central difficulty is visible in every positive result: each known iteration count is controlled by a scale-dependent quantity — bit length, condition number, barrier curvature — that is unbounded over the real instances with fixed. The naive plan, "run the ellipsoid method and round", fails at its first step in the real model: the number of iterations needed to separate a feasible system from an infeasible one grows with the thinness of the feasible set, which is not a function of ; no data-independent perturbation exists when the data are arbitrary reals. All results above are proved on paper only; none has a machine-checked proof in the literature. What is already formalized, on this platform, is the substrate this mission builds on: the simplex iteration (mission Introduction to Linear Optimization IV), the ellipsoid method with its volume-halving correctness theorem (XI), interior-point path following (XII), and self-concordance with the barrier method (Convex Optimization VI).
The mission's milestone list realizes this hierarchy in order; each level states what it deliberately leaves open.
Level 0 — the model works. A uniform BSS program decides one-variable feasibility in linear time:
It fixes nothing about ; its role is to certify that the machine model and cost semantics of the goal are non-vacuous.
Level 1 — the classical method is exponential. On the Klee–Minty cube, Dantzig's rule admits a run of
from the all-slack basis to the optimum. It leaves open all other pivot rules — extensions to further rules are welcome as strengthenings.
Level 2 — the bit model succeeds. Through the Cramer–Hadamard solution bound and the perturbation estimates, Khachiyan's theorem: for integer data bounded by , every admissible ellipsoid run decides feasibility within
The generous constants are deliberate — only the polynomial order is load-bearing. This level leaves open exactly the dependence on .
Level 3 — the goal (open). A uniform program with data-independent polynomial cost:
The statement asserts only the shape of the truth — no hard-coded degree or constant — so it is stable under every future quantitative improvement. These levels do not exhaust the project: Tardos' combinatorial LP theorem, Ye's fixed-discount MDP result, and impossibility statements for restricted program classes in the style of Allamigeon–Gaubert–Vandame are natural later milestones.
Polyhedra, simplex states, pivots, and ellipsoid runs are the platform's existing LinearOptimization development over Matrix (Fin m) (Fin n) ℝ, with as polyhedron A b; algorithms with data-dependent iteration counts are formalized as run predicates, as in the parent missions. The new SmaleNinth definitions supply what the goal genuinely needs and the run-predicate style cannot express: a concrete inductive type of BSS programs with operational semantics and unit-cost accounting, the Klee–Minty data with Dantzig's rule, and the explicit Khachiyan constants. One convention closes the degenerate escape hatch: the goal quantifies over finite BSSProgram terms under the fixed encodeLP input convention — formalizing "algorithm" as an arbitrary function would make the statement trivially true and is not the theorem. Division is totalized as and the branch test is ; both are benign for the class of programs quantified over.
The machine module is infrastructure beyond this mission — any real-number complexity statement (other Smale problems, sums-of-square-roots, BSS-completeness) can reuse it, as can any pivot-rule lower bound reuse the Klee–Minty module. Formalization forces distinctions the literature leaves informal: which machine variant carries the unit-cost claim, how ties in Dantzig's rule are resolved, and which of the interchangeable Khachiyan constants each estimate actually needs. Welcome contributions include proofs of any milestone, alternative exponential instances for other pivot rules, sharper constants in the Khachiyan module, and ports of the known strongly polynomial special cases.
Moment-angle complexes are central objects in toric topology. They convert the combinatorics of a simplicial complex into a topological space assembled from disks and circles, allowing face structure to influence homotopy and homology. When the simplicial complex triangulates a sphere, the resulting space is a moment-angle manifold. Torsion in the integral homology of these manifolds is difficult to realize in low simplicial dimension, and torsion in the homology of their based loop spaces is even more constrained. Yang Han and Keke Li's Theorem 1.7 asserts that dimension four is already universal: every finitely generated abelian group can occur as a subgroup of both homology theories for one and the same simplicial -sphere.
This mission formalizes that headline existence statement. It is not restricted to a chosen finite list of groups or primes, and it requires a common simplicial sphere rather than permitting separate witnesses for ordinary and loop homology.
Let be an abstract simplicial complex on a finite vertex set . Its geometric realization is formed from probability vectors whose supports are faces of . The condition that is a simplicial -sphere means that this realization is homeomorphic to the unit sphere .
For each face , assign a copy of the closed disk at vertices in and the boundary circle at vertices outside . The associated moment-angle complex is
The all-ones point is a canonical basepoint. Write for the based loop space with the compact-open topology. For a space , the mission uses total integral singular homology
as an additive abelian group. Saying that an abelian group is a subgroup means that there is an injective additive homomorphism .
For every finitely generated abelian group , prove that there are an integer and a simplicial complex on Fin m such that and there are injective homomorphisms
The quantifier order matters: the same and the same must support both embeddings. The target concerns additive subgroups of total graded homology; it does not require the two embeddings to land in the same degree or to preserve multiplicative structures.
The theorem gives a universality statement for moment-angle manifolds over simplicial -spheres. It says that no classification by a bounded list of torsion primes or exponents can describe all such homology and loop-homology groups. Requiring both embeddings for a single connects the ordinary topology of the manifold to its based-loop topology rather than proving two unrelated existence results.
Formalizing the theorem requires reusable foundations in several areas: finite abstract simplicial complexes, geometric realization, polyhedral products, based loop spaces, integral singular homology, graded direct sums, and additive embeddings. The published article presents a human proof; this mission records its intended main theorem as an open Lean target. The definitions do not assume the existence of the required sphere or embeddings, so a solver must supply the mathematical construction and all homological consequences.
The assertion ranges over arbitrary finitely generated abelian groups, including free parts and prime-power torsion of unbounded exponent. A finite check of selected groups cannot establish the target. The same finite simplicial object must simultaneously control two different homology theories, one of which is applied to an infinite-dimensional function space. Standard library support is strongest for singular homology as a functor, while concrete calculations for moment-angle spaces and loop spaces require additional bridges.
There is also a substantial representation boundary between combinatorics and topology. The face data of , the union of disk-circle products, the homeomorphism , and the induced maps on homology must all refer to compatible spaces and basepoints. A formal solution cannot replace “simplicial sphere” by a mere Boolean flag or replace homology by an arbitrary group-valued field.
Lean represents using AbstractSimplicialComplex (Fin m). Because Mathlib's structure includes singleton faces automatically, the auxiliary face predicate explicitly restores the conventional empty face where the moment-angle union needs it. The geometric realization is the standard support-restricted probability simplex, and the sphere condition is an actual homeomorphism to the Euclidean unit -sphere.
The moment-angle space is a subtype of (Fin m → ℂ) defined by the literal disk/circle coordinate condition. The loop space consists of based continuous paths with matching endpoints and carries the compact-open topology inherited from Mathlib's path construction. Homology is singularHomologyFunctor with coefficients in , and total homology is a direct sum over all natural degrees.
The statement permits the two embeddings to occupy different degrees and makes no ring-embedding claim; these choices match the source phrase “contain as a subgroup.” It rules out vacuity by requiring an actual simplicial complex, an actual sphere homeomorphism, and injective additive maps. Contributions that isolate degree-specific refinements, compute homology of standard polyhedral products, or formalize reusable loop-space equivalences are welcome, provided they reconnect to the stated root theorem.
John Conway asked whether a graph on 99 vertices can have every edge in exactly one triangle and every nonedge in exactly one quadrilateral. He included this question among his five $1,000 problems and explicitly accepted either a construction or a proof of impossibility (Conway, 2017). This mission organizes structural constraints and graph reconstruction around the existing public formal statement, which remains open. It complements the existing Conway mission: both point to the same mathematical question, while this mission curates additional published intermediate theorems and the precise bridges still needed to use them.
The historical restriction most relevant here is Wilbrink's 1984 theorem that a hypothetical graph cannot be vertex-transitive (Wilbrink's paper). That result is already formalized on Prove2Me. The consolidated local Conway99 development also contains graph-owned point, finite-field, and rooted constraints. Its written and finite-check results have different verification levels; the platform-accepted lemmas cited below are the machine-checked part of that work.
A strongly regular graph with parameters is a finite simple graph on vertices in which each vertex has neighbours, adjacent vertices have exactly common neighbours, and distinct nonadjacent vertices have exactly common neighbours. Write for a candidate graph and for its integer adjacency matrix, whose entry is when and are adjacent and otherwise. Let be the identity matrix and the all-ones matrix. In this mission, the parameter tuple is .
The condition makes each edge part of a unique triangle. Each vertex's 14 neighbours split into seven paired edges. The condition makes each nonadjacent pair have exactly two common neighbours. These facts lead to triangles and the matrix equation , both already proved on the platform (triangle count, matrix identity). Choosing one vertex as a root splits the remaining vertices into its 14 neighbours and 84 nonneighbours; the graph's actual adjacency blocks then satisfy further identities (rooted theorem). The word actual matters: arbitrary matrices satisfying some of these identities have not thereby been shown to arise from one graph.
This is the already published Conway99.conway_99 theorem, reused as the goal. A graph satisfying it proves existence; a proof of the negation of this full existential settles nonexistence. Neither outcome has been established in the archive.
The first layer collects necessary facts about every hypothetical : rooted block equations, point-Gram identities, and finite-field identities. The accepted theorems are rooted blocks, point Gram, and finite fields. An independent binary cut-response rank theorem supplies reusable seven-vertex algebra; its statement does not assume a Conway graph. A selected twelve-owner contact theorem gives a further conclusion only when its chosen triangle, owner set, and regularity premises hold.
The reconstruction layer asks whether compatible local data can be obtained from, or assembled into, one graph satisfying all four strongly regular parameters. The public adjacency-matrix formulation and triangle line-system formulation are still open. A future coclique-completion equivalence concerns graphs with a specified independent 22-set; it cannot replace the unrestricted goal unless that set is shown to exist in every candidate. No unpublished or pending statement is presented as a completed milestone.
An accepted admitted-coclique spike theorem supplies a precise lattice membership identity when a 22-point set and its point-vector average are already admitted to one lattice. It does not produce that coclique, establish the needed lattice for every graph, or close the reconstruction gap. An accepted printed-census correction is retained as a reference to prevent the known erroneous expressions from being reused as graph counts; it is an audit of formulas, not a structural exclusion.
A construction would settle Conway's existence question with a checkable 99-vertex object. A nonexistence proof would explain why the local triangle and common-neighbour conditions cannot coexist globally, despite the standard parameter equations being consistent. Either result must address the whole graph, not one selected root, lattice, shell, or completion packet (Conway's question; formal goal).
The formalization already gives reusable graph-owned interfaces: block identities from an actual root, a point Gram representation, and modular restrictions. Those are machine-checked necessary conditions, while deeper rank, lattice, triangle-transport, and finite-support exclusions in the consolidated local development remain written or locally checked mathematics. This mission makes their status visible and provides a place to connect faithful formal versions as they are published. A conditional theorem remains useful, but its hypotheses must be derived from the candidate graph before it can narrow the unrestricted goal.
The adjacency equation and its eigenvalue multiplicities constrain every candidate but do not determine the binary off-diagonal entries of . Local equations can have feasible matrix or incidence data even when those data have not been embedded in a common simple graph. Conversely, excluding a fixed support, one lattice choice, or a branch with an ordinary point leaves other configurations untouched. The consolidated local frontier records those coverage gaps, including exceptional-only configurations and unexcluded incidence systems. The central task is to close a graph-wide bridge or exhibit a graph, while retaining every hypothesis on narrower results.
The goal uses Mathlib's SimpleGraph.IsSRGWith and quantifies over a finite vertex type, a graph, and decidable adjacency exactly as in the published statement. Supporting statements may use Fin 99 after an explicit relabelling, integer adjacency matrices, finite triangle sets, real Gram matrices, and finite-field reductions. They must derive data from one G, or mark any independent packet as an additional hypothesis. A theorem about selected owners, a prescribed coclique, a particular determinant or rank, or a saved finite support must keep that restriction visible; none may silently assert that every candidate supplies it.
Existing published definitions and theorems should be imported by their platform IDs. Contributions are welcome for exact bridges between graph, matrix, triangle, and coclique representations; proofs that a conditional packet follows from every candidate; faithful formalizations of written universal constraints; and a construction or unconditional contradiction. The mission's published milestones record actual theorem statements. Prospective bridge descriptions remain research targets until they have separately audited and published platform IDs.