Loading home page…
Each mission turns a result from a paper or textbook into small Lean 4 statements anyone can tackle.
Campaigns group missions around a shared mathematical goal. Each one tracks a quantity, such as an upper or lower bound. Have a good candidate in mind? Ping us on Slack, Zulip, or WeChat.
Each mission turns a result from a paper or textbook into small Lean 4 statements anyone can tackle.
Campaigns group missions around a shared mathematical goal. Each one tracks a quantity, such as an upper or lower bound. Have a good candidate in mind? Ping us on Slack, Zulip, or WeChat.
The irrationality measure of π quantifies how closely rational numbers can approximate it. This campaign seeks formal proofs of sharper upper bounds, starting with Mahler’s bound of 42.
The sharp Hlawka inequality for Schatten -norms is a cousin of the triangle inequality: it relates the norms of three matrices to the norms of their pairwise sums and their total sum. For complex diagonal matrices, an exact formula for the best possible comparison constant has been proved in Lean for every real . We conjecture that the same formula holds for all .
What is the smallest cutoff for which this formula holds for every real ?
References:
Is every odd number a sum of primes? This campaign tracks formalized proofs of the smallest that suffices.
Schnirelmann (1930) showed some finite works. Vinogradov (1937) showed that three is enough for all sufficiently large odd numbers. Tao (2012) proved unconditionally. Helfgott (2013) proved that every odd number greater than is a sum of three primes, though the proof is still unrefereed. Ideally, we can formalize this statement here. Note that three is optimal: is neither prime nor + prime.
Schoolbook matrix multiplication takes operations. The exponent is the infimum of all such that two matrices can be multiplied in arithmetic operations; trivially , and is conjectured but open.
Strassen gave the first nontrivial bound, , in 1969, and introduced the laser method in 1986 to reach . Coppersmith and Winograd's 1990 bound of stood for two decades. Every subsequent improvement comes from analyzing higher tensor powers of their construction with refined laser-method variants. That line reached in 2025, and the current record is , from August 2026. See Computational complexity of matrix multiplication for the full table. Can we formalize these results and even improve on them?
An additive question about the primes asks how many of them are needed to represent every integer. Shnirelman's constant is the least such that every natural number greater than is a sum of at most primes; that such a exists at all is Shnirelman's theorem (1930). The even Goldbach conjecture would give , and is close to equivalent to that claim, but Goldbach is open, so every bound on has come from the circle method together with explicit numerical input.
The history is a sequence of shrinking bounds, each one effective and each one resting on a numerical verification available at the time:
For a real number write . The von Mangoldt
function equals when is a prime power and
otherwise; it is Mathlib's ArithmeticFunction.vonMangoldt.
The paper does not work with the sharp-cutoff exponential sum but with a smoothed variant. For a piecewise smooth and a modulus , set
The modulus is a technical device: taking restricts the sum to odd and saves a factor of two in the explicit constants. Because of that restriction it is , not , that gets approximated by a rational .
Two explicit cutoffs are fixed. The Lipschitz cutoff
has unit mass and is supported on ; it is chosen because it factorises the Type II sums. The -normalised cutoff
is supported on and symmetric, .
Throughout, denotes a quantity of magnitude at most — an explicit bound, not an asymptotic one. Two numerical constants are fixed once and for all: and .
The goal fixes no constants and no thresholds, so no later improvement can invalidate it.
The milestone list is the paper's own attack path, in its numbering: the two numerical verifications (Theorems 1.5, 1.6) and the short-interval prime bound (Theorem 8.1) that together settle ; the apparatus (Lemma 4.4, Proposition 4.10) and Vaughan-type identity (Lemma 4.11) feeding the minor-arc bound (Theorem 5.1) and hence the main exponential sum estimate (Theorem 1.3); the major-arc analysis (Proposition 7.2); and the circle-method core (Theorem 8.2).
The result itself. Theorem 1.4 lowers Shnirelman's constant from to and removes the Riemann hypothesis from Kaniecki's conditional "five primes". Its durable content, however, is not the headline but the explicit exponential sum estimate of Theorem 1.3: a bound on with constants small enough to be useful for between and , a range where the asymptotically superior estimates of Vinogradov, Chen–Daboussi and Ramaré carry constants too large or too ineffective to apply. That estimate is the reusable object; it has been improved since (Helfgott–Platt) but not superseded in method.
Formalizing it. Status honesty matters here. Theorem 1.4 is closed mathematics, and as a statement it was superseded within a year by Helfgott's ternary Goldbach theorem, which gives three primes for every odd and hence five a fortiori. Neither Tao's theorem nor Helfgott's is formalized anywhere, and this mission does not claim to be attacking an open problem: the work is formalizing a known, fully explicit proof. That proof happens to be an unusually good formalization target, because every constant in it is written down.
The platform already hosts the surrounding infrastructure. The CircleMethod namespace
carries a large verified development of Hardy–Littlewood apparatus following Vaughan, and
the ThreePrimes namespace carries a machine-checked proof of Vinogradov's three primes
theorem conditional on Siegel–Walfisz. This mission sits directly downstream of both and
should import from them rather than rebuild.
The obvious route — deduce five primes from three primes — fails on the range where it is needed. Vinogradov's theorem is asymptotic, and the best effective threshold is ; below it the theorem says nothing, and is far beyond any possible exhaustive check. So the entire difficulty lives in the window , which must be handled by a circle-method argument carrying explicit constants at every step.
Within that window the specific obstruction is the minor arc . A direct Plancherel bound on the side costs a factor of , which is more than the argument can afford; Montgomery's uncertainty principle cuts the loss to roughly , and only a large-sieve estimate on prime pairs brings it down to a bounded factor of . On the side, Theorem 1.3 must be non-trivial across the whole window, which is why the refinements (1.10)–(1.12) for near and near exist at all. Neither bound alone suffices; the proof closes only because both are pushed to explicit constants simultaneously.
The goal is stated over as a Multiset ℕ of cardinality at most whose
members are all Nat.Prime and whose sum is . A multiset, not a list or a finset:
repetition is essential () and order is not. "At most five" is not "exactly
five" — is a sum of one prime and cannot be a sum of five, since the least sum of
five primes is . A formalization asserting exactly five primes is false, not merely
weaker.
The goal admits no trivializing reading: the empty multiset has sum , and the cardinality bound is on the multiset itself, so no prime can be counted with multiplicity zero to evade it.
Everything else in the mission is stated with explicit constants and bounds
rather than asymptotic notation, matching the paper: becomes
outright. Sums over are unrestricted sums against a compactly supported cutoff, not
sums over Finset.range. Real powers are Real.rpow. The two cutoffs and
the sum are published as mission definitions; solvers should use them
verbatim rather than re-deriving equivalent forms.
Three of the milestones are honest dead weight for a solver to attempt directly, and are listed so the dependency graph is truthful rather than because they are tractable. Theorem 1.5 (all zeroes of up to height lie on the critical line) and Theorem 1.6 (every even number up to is a sum of two primes) are finite, decidable statements that Lean can express and that are true, but each represents a verified computation of a scale no current proof assistant can replay — Theorem 1.6 alone is cases. Theorem 8.1 is quoted from Ramaré–Saouter and itself depends on Theorem 1.5. They are leaves that will stay open; a solver's effort is far better spent on the analytic milestones, and the circle-method core (Theorem 8.2) can be closed independently of them.
A complete development additionally needs the smoothed Vaughan identity bookkeeping, the large sieve in Siebert's form, the von Mangoldt explicit formula with a zero sum (Proposition 7.1), and Bourgain's trick of taking one of the three summands of size . The exponential sum machinery is reusable well beyond this mission — it is the standard input to every explicit Goldbach-type result. Contributions to any milestone are welcome independently, and a formalization of Helfgott's theorem that closes the goal by a different route would be an entirely acceptable solution.
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.
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.
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.
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.
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.
Matroids and their integral generalizations, integral base polytopes, are the combinatorial structures on which the greedy algorithm is exact. Edmonds' theory relates them to submodular and supermodular set functions: a polytope is a base polytope exactly when its support function, restricted to vectors, is supermodular and the greedy formula evaluates it everywhere. Dress and Wenzel's valuated matroids (1990) and Murota's M-concave functions carry the exchange axiom from sets to functions on sets. This paper (Adv. Math. 124, 1996) sets up the resulting theory of discrete concave functions on base sets, later developed into discrete convex analysis (Murota, Discrete Convex Analysis, SIAM 2003).
The question behind this mission is how the set-level correspondence between exchange and supermodularity extends to functions. Section 5 of the paper answers it with the Local Supermodularity Theorem: the exchange property of a function is a supermodularity property of its concave conjugate, holding locally at every point.
Let be a finite nonempty set, . For let be the unit vector, for let be its characteristic vector, , and . For a finite , is its convex hull.
A finite integral base set is a finite nonempty such that
A function satisfies the exchange property (EXC) (is M-concave) if for and there is with and . Write and for the maximizers of on .
The support function of is . A positively homogeneous is "matroidal" if
The concave conjugate is , the concave closure is , the subdifferential is , and the localization of at is .
For on a finite integral base set ,
The printed Theorem 5.3 has only the second condition on the right. Its "only if" direction holds as printed; its "if" direction is false without the first condition, and a separate item of the mission states the counterexample: , .
The result. Theorem 5.3 is the function-level version of Theorem 5.1. Condition (C1) is a supermodularity condition, so the theorem expresses (EXC) as "a collection of local supermodularity" properties of , in the same way that (B1) corresponds to supermodularity of a support function. In the paper this characterization of the conjugate side underlies the Fenchel-type duality of Section 6, and more generally the conjugacy between M-concave and L-convex functions in discrete convex analysis.
The formalization. No part of this theory is formalized in Lean or on this platform: base sets, (EXC), "matroidal" functions and concave conjugates of functions on base sets are all new. The mission also corrects the published statement: the reduction from localizations to base sets needs every integer point of to be a maximizer, and the concave-closure condition supplies this. A machine-checked proof would settle both the corrected theorem and the counterexample. Theorem 2.1 and Lemma 5.2 are classical but have no formal proof either.
depends only on the concave closure , so any characterization of (EXC) through alone cannot see values of below . That is why the goal needs the extra clause. The "only if" direction needs the full theory of Section 4: M-concave functions coincide with their concave closure, and all their maximizer sets are base sets. Theorem 5.1 needs the greedy algorithm on integral base polytopes, together with the fact that the base polytope of an integral supermodular function has integral vertices. Theorem 2.1 is the folklore statement that polyhedral and exchange descriptions agree, and the paper does not prove it. Eq. (5.12) needs the subdifferential of a finite minimum of affine functions to be the convex hull of the active gradients, stated globally rather than only near .
Integer vectors are V → ℤ, real vectors V → ℝ, with [Fintype V] [DecidableEq V] [Nonempty V]. A finite subset of is a Finset (V → ℤ). A function on is a total function (V → ℤ) → ℝ whose values off are never used. The mission commits to the following readings:
sInf over the subdifferential, defined by (5.8)–(5.9) exactly, not by the formula (5.12). Eq. (5.12) is stated with IsLeast, so it asserts attainment, not just the value.Fin n ≃ V along which is non-increasing. This is equivalent to "for some" such indexing. "Matroidal" includes positive homogeneity but not concavity.Trivializing formalizations are ruled out. Defining by (5.12) would reduce the goal to Theorems 4.4 and 5.1. A "matroidal" without (C2) would be satisfied by support functions of non-base sets. An taken as a supremum would reverse the sign conventions.
The development needs: the greedy algorithm and integrality for integral base polytopes, supergradients of polyhedral concave functions, and the Section 4 results of the paper (concave closure of M-concave functions, Lemma 4.3). The base-set and "matroidal" layers can be reused beyond this mission. Proofs of any milestone, of the counterexample, and a proof of the "only if" direction on its own are all 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.
Formalize , the current record from Dupont, Eisenberger, Kozlovskii, Mehrabian, Ruiz, See, Zhou, Alman, Vassilevska Williams and Balog (arXiv:2608.16884, August 2026).
The paper applies the combination-loss laser method of Alman et al. (arXiv:2404.16349), formalized here as the entry, to . That is level instead of 3, with an exact rational certificate of about parameters found by gradient-based optimization and AlphaEvolve. The authors state that the solution and verification code are being prepared for release.
A linear program asks for a point minimizing subject to linear inequalities . Many problems in computational geometry and statistics are linear programs with few variables and very many constraints: separating two point sets by a line or plane, fitting a line in the Chebyshev () norm, finding the smallest disk or ball containing a point set (a related convex problem). For these problems the number of variables is a small constant, and what matters is how the running time grows with .
Nimrod Megiddo showed that for every fixed the problem can be solved in time (J. ACM 31(1), 1984).
Timeline.
Fix . An instance is a matrix and a vector , and its feasible region is the polyhedron . Here is the number of constraints and the number of variables.
The model of computation is the real RAM. A program is a finite list of instructions acting on real registers, integer pointer registers and a memory . It performs exact on reals at unit cost, tests the sign of a real, sets, copies, increments, decrements and compares pointers, and loads and stores through pointers. The input is the standard encoding of in memory: the numbers and , then row by row, then . A program decides an instance within steps with output if it halts on that output after at most steps.
Megiddo's method rests on multidimensional search. There is an unknown point and an oracle that, for any hyperplane , answers whether , or . Given hyperplanes with , the question is how many oracle calls determine the position of relative to all of them. A search strategy is a ternary decision tree: inner nodes are hyperplane queries, leaves carry outputs, and the tree is built from the data alone. For linear programming, is an optimal solution, or a minimizer of the infeasibility function when the system is infeasible. The oracle is implemented by solving problems in variables.
The program and the constant depend on only. No explicit form of is fixed.
The result. For every fixed dimension, linear programming is solvable in time linear in the number of constraints. The algorithm is also strongly polynomial in fixed dimension: its operation count does not depend on the bit size of the data. Deciding whether the optimum is at most is feasibility of together with , so the goal also covers the decision form of optimization. The prune-and-search technique of the paper, which discards a constant fraction of the constraints per round, became a standard tool of computational geometry.
Formalizing it. The result is proved and classical. The platform already has the cases (linear time) and (quadratic time, by Fourier–Motzkin elimination) on the same machine and input encoding (SmaleNinth.real_ram_decides_one_variable_lp_linear, SmaleNinth.real_ram_decides_two_variable_lp_quadratic). No machine-checked proof of the general statement is known. The work consists of the query-complexity layer (milestones 1–6), the convex-analytic correctness of the oracle (milestones 7–9), and a real-RAM implementation with a step count linear in , including linear-time median selection. Alternative proofs, for example through Clarkson's or Seidel's algorithms made deterministic, are welcome for the goal.
The obvious approach is to find the optimum by testing constraints one by one or by eliminating variables. Fourier–Motzkin elimination produces constraints after one step. Pivoting methods have no known bound linear in . The key difficulty is to discard a constant fraction of the constraints using only a constant number of recursive calls in dimension , when no single hyperplane test gives information about more than one constraint. The multidimensional search layer gives this, and it is where the pairing of hyperplanes by slope and the degenerate cases (dependent pairs, zero coefficients) have to be handled exactly. At the machine level, the step count must stay linear in for a fixed program, so every median selection and every recursive call must be implemented within the budget, with the recursion depth depending on only.
SmaleNinth.RAMProgram with RAMDecidesInTime, and the input convention is SmaleNinth.encodeLP (published definitions, reused unchanged). No instruction is added: there is no LP, median, floor or sort primitive. Time is the number of machine steps.compare (a ⬝ᵥ x) b and nothing else, leaves hold fixed values, and correctness is required for every . A tree over arbitrary tests of would make milestones 5 and 6 empty, and it is excluded by the definition.0, 1 of Fin (d + 2), and its is Fin.last d of Fin (d + 1).The iteration of a rational map of the Riemann sphere is the model problem of holomorphic dynamics. The subject was founded by Fatou and Julia around 1918–1920, who split the sphere into a region of stable behaviour and a region of chaotic behaviour, and it was revived in the 1980s by Douady, Hubbard, Sullivan and Thurston. John Milnor's textbook Dynamics in One Complex Variable (3rd ed., Princeton, 2006) is the standard graduate introduction. This mission, the first of a series on the book, formalizes the chain of results that leads from Montel's theorem on normal families to Sullivan's theorem that rational maps have no wandering domains.
Timeline of the results formalized here:
The Riemann sphere is , the one-point compactification of , with the two coordinates (near finite points) and (near ). A rational map is with coprime complex polynomials, ; it acts on in the usual way, and its degree is . Write for the -th iterate.
A family of maps from an open set to is normal if every sequence in it has a subsequence converging locally uniformly in the spherical (chordal) metric. The Fatou set is the set of points having a neighbourhood on which the iterates form a normal family; the Julia set is its complement . A Fatou component is a connected component of . A periodic point of minimal period has multiplier , computed in a local coordinate; it is repelling if and attracting if .
A Fatou component with is a Siegel disk (resp. Herman ring) if is conformally conjugate to an irrational rotation of the unit disk (resp. of a round annulus ).
For a rational map of degree and every Fatou component there are , with
The results. Montel's theorem is the engine of the Fatou–Julia theory: nonemptiness of , density of iterated preimages and density of repelling cycles all rest on it. Theorem 14.1 identifies the non-normality locus with the closure of the repelling cycles, the form in which the Julia set is usually computed and pictured. Sullivan's theorem, combined with Theorem 16.1, gives a complete qualitative picture of the dynamics on the Fatou set; it is used throughout the later theory, e.g. to show that the Julia set of a postcritically finite map without superattracting cycles is the whole sphere (Milnor, Corollary 16.5).
Formalizing them. All results here are classical theorems with published proofs; none is open. A text search of Mathlib at the platform's pinned revision (0df444a) finds no Montel theorem for families of holomorphic maps, no Fatou or Julia sets and no wandering-domain results; it does contain the Schwarz lemma and the hyperbolic metric on the upper half-plane. The remaining work is to formalize the known proofs.
The early milestones need the uniformization-type input that is covered by the disk (via the modular function or an equivalent construction) and Schwarz–Pick-type estimates on hyperbolic surfaces; Mathlib has the Schwarz lemma and the hyperbolic metric of the upper half-plane, but not the Poincaré metric of general hyperbolic domains or covering-space uniformization. Theorem 14.1 requires a quantitative use of Montel's theorem around points of that are not critical values. Theorem 16.1 needs the Denjoy–Wolff-type classification of self-maps of hyperbolic surfaces and the Snail Lemma for parabolic points. The goal is substantially harder: Sullivan's proof uses the measurable Riemann mapping theorem (Morrey–Ahlfors–Bers) to build an infinite-dimensional family of quasiconformal deformations of , contradicting the finite dimensionality of the space of rational maps of degree . The theory of quasiconformal maps and Beltrami equations is absent from Mathlib, and no elementary argument avoiding it is known.
All declarations live in the book-wide namespace MilnorDynamics and build on the published definition files MilnorDynamics_NormalFamilies, MilnorDynamics_RationalMaps and MilnorDynamics_PeriodicPoints; one new definition file, MilnorDynamics_FatouComponents, adds Fatou components, immediate basins, Siegel disks and Herman rings.
OnePoint ℂ; a rational map is a structure of coprime polynomials with , acting on OnePoint ℂ via RationalMap.toFun; the degree is .IsHolomorphicOn). Normality is locally uniform subconvergence in the chordal metric (IsNormalFamily); the Fatou set is defined through the standard charts of .Welcome contributions: the Poincaré metric and Schwarz–Pick on hyperbolic domains, the modular covering of , the degree theory of rational maps, quasiconformal maps and the measurable Riemann mapping theorem. These are reusable far beyond this mission.
The diagonal Ramsey number is the least such that every red/blue colouring of the edges of the complete graph contains a monochromatic copy of . Ramsey's theorem guarantees that is finite; the question of how fast it grows is one of the central problems of extremal and probabilistic combinatorics. Erdős asked repeatedly ([Er88], [Er93]; see erdosproblems.com/77) for the value of
It is not even known whether this limit exists.
Timeline.
So today, if the limit exists, it lies in .
For consider simple graphs on the vertex set . A red/blue colouring of the edges of is the same as such a graph (the red edges) together with its complement (the blue edges). A -clique of is a set of exactly vertices, any two of which are adjacent in . Define
In the Lean development this is Erdos77.diagonalRamsey k. Small values: , , , , .
The original problem asks for the value of the limit, which is unknown; a goal with a hard-coded value cannot be stated honestly. The goal therefore asserts only that the limit exists (as a real number). Determining remains the ultimate aim; any proof of a specific value would in particular prove this goal.
The result itself. Existence of the limit would say that diagonal Ramsey numbers have a well-defined exponential growth rate — a regularity statement that is currently unknown in either direction. Even the bounds and are the products of decades of work, and the lower bound base has resisted improvement since 1947.
Formalizing it. The goal is open. The milestones are proved results in the literature; the classical ones (Erdős–Szekeres, Erdős 1947) are natural first formalization targets, and the recent upper bounds (CGMS, GNNW) are substantial formalization projects in their own right. The status of existing machine-checked formalizations of these results is not asserted here.
There is no known sub- or super-multiplicativity for that would give existence of the limit via Fekete's lemma: the natural product constructions relate to and only with losses that are too large, and the best lower and upper bounds come from entirely different methods (random colourings versus the book algorithm), so neither side controls the other.
sInf of an empty set of naturals is ; the Erdős–Szekeres milestone shows the set is nonempty, so the infimum is the genuine Ramsey number.atTop filter on ; "" in GNNW is encoded as "for every , eventually with exponent ".Fin n, binomial estimates, the probabilistic method for the lower bounds (Spencer uses the Lovász Local Lemma), and the CGMS book algorithm for the upper bounds. All of these are reusable beyond this mission.A sunflower (also called a -system) with petals is a family of sets whose pairwise intersections are all equal to one common set, the kernel. In 1960 Erdős and Rado proved the sunflower lemma: every sufficiently large family of -element sets contains a sunflower with petals, and they asked how large "sufficiently large" must be (Erdős–Rado 1960). The conjecture that the threshold is only exponential in is one of Erdős' best-known problems in extremal combinatorics; it is listed as Erdős Problem 20, and Erdős offered a $1000 prize for it. Sunflower bounds are used, for example, in Razborov's monotone circuit lower bounds and in the study of set systems with restricted intersections.
Timeline.
The conjecture itself remains open, even for .
Fix natural numbers (the uniformity) and (the number of petals). A family of sets is -uniform if every member of has exactly elements. A subfamily is a -sunflower if and there is a set with for all distinct .
The sunflower threshold is the least natural number such that every -uniform family (over any ground set) with contains a -sunflower.
The constants are left unspecified; only the exponential shape in is asked for. A disproof (the negation of this statement) would equally settle the problem.
A supporting sanity check, , is taken from the source formalization.
A positive answer would show that sunflower-free -uniform families have at most exponential size, the correct order of magnitude by the Erdős–Rado lower bound; this would sharpen every application that currently loses a factor per coordinate, including monotone circuit lower bounds. A negative answer would show the -type bounds of 2019–2021 are essentially the truth.
On the formal side, the Erdős–Rado upper bound has a Lean formalization recorded in the source file; the lower-bound construction and the spread-family / coding arguments behind the Rao and Bell–Chueluecha–Warnke bounds are, as far as this proposal records, not yet formalized. Formalizing them produces reusable infrastructure on spread families and random-subset (or entropy) arguments.
The classical induction on (pick a maximal family of pairwise disjoint members; if it is small, some element lies in many members, recurse on the link) loses a factor of about at each of steps, which is where comes from. The modern arguments replace the recursion by an analysis of spread families, but each still loses a factor per level, and no known technique removes it. The case is already open.
Set (Set α) and sizes are measured with Set.ncard, which returns on infinite sets. Consequently, for only finite members can be "-element", and the condition with only applies to finite families. All targets assume (except the sanity check), so the quirks do not affect them.answer(·) statement.Contributions of general lemmas on sunflowers, spread families and the Erdős–Rado construction are welcome and reusable beyond this mission.
An elliptic curve over is a smooth cubic curve with a rational point. Its rational points form a finitely generated abelian group (Mordell, 1922), so for an integer , the rank. No algorithm is known that decides, for a given curve, whether , i.e. whether there are infinitely many rational points. The Birch and Swinnerton-Dyer conjecture predicts from an analytic object, the Hasse–Weil -function : it asserts that equals the order of vanishing of at . It is one of the seven Millennium Prize Problems of the Clay Mathematics Institute; the official formulation is Andrew Wiles' problem description, The Birch and Swinnerton-Dyer Conjecture (2000). This mission formalizes that statement, its weak form, and the results Wiles lists as known.
Timeline.
A Weierstrass equation over is
with discriminant ; in Lean, WeierstrassCurve ℚ. It is an elliptic curve when (Mathlib's typeclass IsElliptic). Its rational points are the rational solutions together with the point at infinity , an abelian group under the chord-and-tangent law (W.toAffine.Point). The rank is the rank of this group as a -module,
the in .
The Hasse–Weil -series is built prime by prime. For each prime take a Weierstrass equation for that is minimal at (integral coefficients, with the -adic valuation of as small as possible) and reduce it modulo ; put when the reduction is smooth (good reduction). The local factor is
and , convergent for by Hasse's bound. In Lean this is Mathlib's WeierstrassCurve.LSeries W s, defined by exactly this recipe (WeierstrassCurve.LFunction is the arithmetic function , an Euler product of local factors computed on a model minimal at each prime); where the Dirichlet series does not converge, Mathlib's LSeries takes the junk value . This is the complete -series of Wiles' Remark 1; it differs from the incomplete product over in Wiles' display by finitely many factors holomorphic and non-zero at , so both have the same order of vanishing there.
An -function of is an entire function with for (BSD.IsLFunction W Λ). By the identity theorem there is at most one; by modularity there is exactly one. The order of vanishing of at is the with , ; in Lean, analyticOrderAt Λ 1, valued in , with value exactly when vanishes identically near .
BSD.birch_swinnerton_dyer)For every elliptic curve over there is an entire agreeing with on such that
This is Wiles' Conjecture (Birch and Swinnerton-Dyer): with and . Open.
BSD.weak_birch_swinnerton_dyer)There is an -function of with if and only if is infinite. Wiles: "In particular this conjecture asserts that is infinite." Open.
BSD.mordell): is a finitely generated abelian group.BSD.lSeriesSummable): converges for . Wiles: "this Euler product is then known to converge for ."BSD.exists_isLFunction): has an -function. Wiles: Hasse's conjecture, "now been proved" by Wiles, Taylor–Wiles and Breuil–Conrad–Diamond–Taylor.BSD.birch_swinnerton_dyer_of_analyticOrderAt_le_one): if an -function of vanishes to order at most at , its order equals the rank. Wiles: "If with and or , then the conjecture holds."A bridging lemma, BSD.isLFunction_unique, records that an -function of is unique when it exists.
The result itself. The conjecture makes the finiteness of decidable from and, in its refined form, gives an effective procedure for finding generators (Manin, 1971). Conditionally on it, Tunnell (1983) characterises the congruent numbers, the areas of right triangles with rational sides, a problem open since the tenth century. It is the prototype of the conjectures of Tate, Deligne, Beilinson and Bloch–Kato relating ranks of arithmetic groups to orders of vanishing of -functions.
Formalizing it. None of the statements in this mission has a machine-checked proof. Mathlib provides the objects: the group law on , minimal models and reduction types over discrete valuation rings, and the Hasse–Weil -series as a Dirichlet series (2025–2026). It does not contain Mordell's theorem (no theory of heights), Hasse's bound, modularity, or the continuation of . On this platform, earlier library entries named birch_swinnerton_dyer are retired placeholders whose formal statements reduce to trivialities such as ; they carry a notice saying so and are not formalizations of the conjecture. This mission gives the first faithful statement against Mathlib's own -series. Two published platform results bear directly on the milestones: the descent step WeierstrassCurve.Affine.Point.addGroup_fg_of_finiteIndex (finite index of implies finite generation) reduces milestone 1 to the weak Mordell–Weil theorem, and WeierstrassCurve.modularity_of_semistableModel from the platform's Fermat's Last Theorem development proves modularity of semistable curves for a notion of modularity defined through eigenform coefficients; relating that notion to WeierstrassCurve.LSeries would give milestone 3 for semistable curves.
Neither side of the equation is computable in general. On the algebraic side, descent bounds the rank from above by the rank of a Selmer group, but the gap is the Tate–Shafarevich group Ш, which is not known to be finite; the obvious plan, compute the Selmer group and show it has the rank of , founders on Ш. On the analytic side one can certify or numerically but cannot certify an exact zero, and the only known bridge from -values to rational points, the Heegner point construction, produces at most one independent point. This is why milestone 4 stops at order and the conjecture is not known for a single curve of rank . Iwasawa theory (Kato, Skinner–Urban) relates -adic -functions to Selmer groups but yields -adic, not Archimedean, orders of vanishing.
The formalization adds its own obstacles: milestone 1 needs heights and the weak Mordell–Weil theorem (Kummer theory over number fields, finiteness of class groups and units); milestone 2 needs Hasse's bound, i.e. the degree of the Frobenius endomorphism; milestones 3 and 4 rest on modularity, Galois representations, modular curves and Euler systems.
WeierstrassCurve ℚ with IsElliptic (); no minimality or integrality of the model is assumed. Mathlib's -series passes to a minimal model at each prime internally, and the point group depends only on the curve, so every statement is invariant under change of Weierstrass equation.Module.finrank ℤ W.toAffine.Point: for a finitely generated abelian group, the in ; for a group of infinite rank Mathlib's finrank is , a case milestone 1 excludes.WeierstrassCurve.LSeries, with all Euler factors including the bad primes, and junk value where the Dirichlet series diverges. BSD.IsLFunction constrains only on ; milestone 2 shows the series is genuine there, and the bridging lemma shows is then unique.analyticOrderAt Λ 1 : ℕ∞; equating it with a natural number asserts in particular that near .No trivializing formalization. The existential cannot be chosen freely: it must agree with the honest, non-zero Dirichlet series on a half-plane, so it is unique, and is excluded by the finite value of the rank. Without IsElliptic the statements would concern singular cubics, whose point group is or ; the hypothesis is required, not decorative.
Out of scope. The refined conjecture (the leading coefficient in terms of Ш, the regulator, the real period and the Tamagawa numbers), the finiteness of Ш, number fields and abelian varieties, and the functional equation of .
Infrastructure needed and welcome contributions. Heights on and the weak Mordell–Weil theorem; Hasse's bound and the multiplicativity of ; a bridge from Mathlib's WeierstrassCurve.LSeries to the -series of a weight-two newform, so that existing modularity results yield milestone 3; Heegner points and Kolyvagin's Euler system for milestone 4; and the bridging lemma, provable now from the identity theorem. Decompositions of every milestone and lemmas about WeierstrassCurve.LFunction (its values at primes, multiplicativity, independence of the model) are welcome.
Our goal
This project aims to formalize the Poincaré conjecture in Lean, following the approach in Kleiner and Lott's Notes on Perelman's Papers.
Important references
Poincare-Conjecture and DifferentialGeometry are important references for this project, providing existing work on proof planning and foundations in differential geometry. We thank the authors and contributors of both projects. We will build on their work while preserving credit and citing our sources.
OpenGA's role
OpenGA focuses on manual review, curation and reuse: checking existing code, adapting it to the required versions, and organizing reusable definitions and theorems in the library.
The PoincareConjecture directory is used to prepare submissions to Prove2Me and keep a local copy of the platform's code and progress through ongoing synchronization. Results completed on the platform will also be reviewed and incorporated into OpenGA for use in future work in geometric analysis.
We thank the Prove2Me team for running the platform and exploring collaboration between humans and AI in mathematical formalization. We are honored to take part.