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.
Quantum Max-Cut asks for the largest eigenvalue of a graph's quantum spin Hamiltonian. For a graph with nonnegative rational edge weights, write
This campaign tracks expected approximation ratios for classical polynomial-time energy estimation. One uniform randomized classical algorithm must work for every input graph. For each fixed , let be the algorithm's internal fair random bits, and let be its nonnegative rational output. A ratio requires
The expectation averages the algorithm's internal randomness on a fixed graph. Its running time is bounded by a polynomial on every run. Higher ratios are better.
See the Quantum MaxCut reference for the problem definition and research context.
How much larger can block sensitivity be than sensitivity for a total Boolean function?
For a total Boolean function , a block of coordinates is sensitive at if flipping every bit in that block changes . Let count sensitive singletons and be the maximum number of pairwise disjoint sensitive blocks. Define and .
This campaign seeks larger exponents for which there exists an infinite family of total Boolean functions , indexed by , satisfying
Here denotes a quantity tending to zero as . Higher is better. The classical exponent is , and Huang's bound gives a ceiling of .
OpenAI's construction achieves an exponent strictly greater than .
One sufficient way to establish an exponent is to find a single total Boolean function with and . Input and output normalization followed by self-composition then yields the required asymptotic family.
Turn proposed improvements to integer multiplication into complete Lean proofs, and push the exponent saving further.
Harvey and van der Hoeven established an algorithm in 2021. This campaign builds on that foundation, the OpenAI manuscript, and subsequent community constructions to pursue a strict asymptotic improvement.
For two -bit integers, the target is
A positive beats asymptotically; larger is better. Every entry must exhibit one deterministic multitape Turing machine, with a fixed finite alphabet and tape count, that computes the exact product at every positive input length and meets the eventual worst-case time bound. The tracked number measures an asymptotic exponent saving.
Classical algorithms solve 3SUM in time. In a 2026 breakthrough, Alman and Vassilevska Williams gave a deterministic algorithm, refuting the integer 3SUM hypothesis. How low can the exponent go?
Building on existing Lean formalizations, this campaign tracks upper bounds for 3SUM on polynomially bounded integers, using a word RAM with -bit words, and pursues smaller exponents.
Classical algorithms solve all-pairs shortest paths in time. In a 2026 breakthrough, Alman and Vassilevska Williams refuted the APSP conjecture with a deterministic algorithm. How low can the exponent go?
Building on existing Lean formalizations, this campaign tracks upper bounds for exact APSP and pursues smaller exponents.
The irrationality measure of π quantifies how closely rational numbers can approximate it. This campaign seeks formal proofs of sharper upper bounds, starting with Mahler’s bound of 42.
The sharp Hlawka inequality for Schatten -norms is a cousin of the triangle inequality: it relates the norms of three matrices to the norms of their pairwise sums and their total sum. For complex diagonal matrices, an exact formula for the best possible comparison constant has been proved in Lean for every real . We conjecture that the same formula holds for all .
What is the smallest cutoff for which this formula holds for every real ?
References:
Is every odd number a sum of primes? This campaign tracks formalized proofs of the smallest that suffices.
Schnirelmann (1930) showed some finite works. Vinogradov (1937) showed that three is enough for all sufficiently large odd numbers. Tao (2012) proved unconditionally. Helfgott (2013) proved that every odd number greater than is a sum of three primes, though the proof is still unrefereed. Ideally, we can formalize this statement here. Note that three is optimal: is neither prime nor + prime.
Schoolbook matrix multiplication takes operations. The exponent is the infimum of all such that two matrices can be multiplied in arithmetic operations; trivially , and is conjectured but open.
Strassen gave the first nontrivial bound, , in 1969, and introduced the laser method in 1986 to reach . Coppersmith and Winograd's 1990 bound of stood for two decades. Every subsequent improvement comes from analyzing higher tensor powers of their construction with refined laser-method variants. That line reached in 2025, and the current record is , from August 2026. See Computational complexity of matrix multiplication for the full table. Can we formalize these results and even improve on them?
An additive question about the primes asks how many of them are needed to represent every integer. Shnirelman's constant is the least such that every natural number greater than is a sum of at most primes; that such a exists at all is Shnirelman's theorem (1930). The even Goldbach conjecture would give , and is close to equivalent to that claim, but Goldbach is open, so every bound on has come from the circle method together with explicit numerical input.
The history is a sequence of shrinking bounds, each one effective and each one resting on a numerical verification available at the time:
For a real number write . The von Mangoldt
function equals when is a prime power and
otherwise; it is Mathlib's ArithmeticFunction.vonMangoldt.
The paper does not work with the sharp-cutoff exponential sum but with a smoothed variant. For a piecewise smooth and a modulus , set
The modulus is a technical device: taking restricts the sum to odd and saves a factor of two in the explicit constants. Because of that restriction it is , not , that gets approximated by a rational .
Two explicit cutoffs are fixed. The Lipschitz cutoff
has unit mass and is supported on ; it is chosen because it factorises the Type II sums. The -normalised cutoff
is supported on and symmetric, .
Throughout, denotes a quantity of magnitude at most — an explicit bound, not an asymptotic one. Two numerical constants are fixed once and for all: and .
The goal fixes no constants and no thresholds, so no later improvement can invalidate it.
The milestone list is the paper's own attack path, in its numbering: the two numerical verifications (Theorems 1.5, 1.6) and the short-interval prime bound (Theorem 8.1) that together settle ; the apparatus (Lemma 4.4, Proposition 4.10) and Vaughan-type identity (Lemma 4.11) feeding the minor-arc bound (Theorem 5.1) and hence the main exponential sum estimate (Theorem 1.3); the major-arc analysis (Proposition 7.2); and the circle-method core (Theorem 8.2).
The result itself. Theorem 1.4 lowers Shnirelman's constant from to and removes the Riemann hypothesis from Kaniecki's conditional "five primes". Its durable content, however, is not the headline but the explicit exponential sum estimate of Theorem 1.3: a bound on with constants small enough to be useful for between and , a range where the asymptotically superior estimates of Vinogradov, Chen–Daboussi and Ramaré carry constants too large or too ineffective to apply. That estimate is the reusable object; it has been improved since (Helfgott–Platt) but not superseded in method.
Formalizing it. Status honesty matters here. Theorem 1.4 is closed mathematics, and as a statement it was superseded within a year by Helfgott's ternary Goldbach theorem, which gives three primes for every odd and hence five a fortiori. Neither Tao's theorem nor Helfgott's is formalized anywhere, and this mission does not claim to be attacking an open problem: the work is formalizing a known, fully explicit proof. That proof happens to be an unusually good formalization target, because every constant in it is written down.
The platform already hosts the surrounding infrastructure. The CircleMethod namespace
carries a large verified development of Hardy–Littlewood apparatus following Vaughan, and
the ThreePrimes namespace carries a machine-checked proof of Vinogradov's three primes
theorem conditional on Siegel–Walfisz. This mission sits directly downstream of both and
should import from them rather than rebuild.
The obvious route — deduce five primes from three primes — fails on the range where it is needed. Vinogradov's theorem is asymptotic, and the best effective threshold is ; below it the theorem says nothing, and is far beyond any possible exhaustive check. So the entire difficulty lives in the window , which must be handled by a circle-method argument carrying explicit constants at every step.
Within that window the specific obstruction is the minor arc . A direct Plancherel bound on the side costs a factor of , which is more than the argument can afford; Montgomery's uncertainty principle cuts the loss to roughly , and only a large-sieve estimate on prime pairs brings it down to a bounded factor of . On the side, Theorem 1.3 must be non-trivial across the whole window, which is why the refinements (1.10)–(1.12) for near and near exist at all. Neither bound alone suffices; the proof closes only because both are pushed to explicit constants simultaneously.
The goal is stated over as a Multiset ℕ of cardinality at most whose
members are all Nat.Prime and whose sum is . A multiset, not a list or a finset:
repetition is essential () and order is not. "At most five" is not "exactly
five" — is a sum of one prime and cannot be a sum of five, since the least sum of
five primes is . A formalization asserting exactly five primes is false, not merely
weaker.
The goal admits no trivializing reading: the empty multiset has sum , and the cardinality bound is on the multiset itself, so no prime can be counted with multiplicity zero to evade it.
Everything else in the mission is stated with explicit constants and bounds
rather than asymptotic notation, matching the paper: becomes
outright. Sums over are unrestricted sums against a compactly supported cutoff, not
sums over Finset.range. Real powers are Real.rpow. The two cutoffs and
the sum are published as mission definitions; solvers should use them
verbatim rather than re-deriving equivalent forms.
Three of the milestones are honest dead weight for a solver to attempt directly, and are listed so the dependency graph is truthful rather than because they are tractable. Theorem 1.5 (all zeroes of up to height lie on the critical line) and Theorem 1.6 (every even number up to is a sum of two primes) are finite, decidable statements that Lean can express and that are true, but each represents a verified computation of a scale no current proof assistant can replay — Theorem 1.6 alone is cases. Theorem 8.1 is quoted from Ramaré–Saouter and itself depends on Theorem 1.5. They are leaves that will stay open; a solver's effort is far better spent on the analytic milestones, and the circle-method core (Theorem 8.2) can be closed independently of them.
A complete development additionally needs the smoothed Vaughan identity bookkeeping, the large sieve in Siebert's form, the von Mangoldt explicit formula with a zero sum (Proposition 7.1), and Bourgain's trick of taking one of the three summands of size . The exponential sum machinery is reusable well beyond this mission — it is the standard input to every explicit Goldbach-type result. Contributions to any milestone are welcome independently, and a formalization of Helfgott's theorem that closes the goal by a different route would be an entirely acceptable solution.
This mission seeks a Lean proof that every odd natural number greater than 1 is the sum of at most three primes. It follows from Helfgott's ternary Goldbach theorem for odd numbers greater than 5, together with the small cases 3 and 5, each of which is itself prime.
For every natural number n with Odd n and 1 < n, construct a multiset of at most three prime natural numbers whose sum is n. Repetition is allowed and order is irrelevant. Examples include 3 = 3, 5 = 5, 7 = 2 + 2 + 3, and 9 = 3 + 3 + 3. The primes need not all be odd.
The goal uses the same Multiset ℕ representation and the same hypothesis 1 < n as Every Odd Number Greater Than 1 is the Sum of at Most Five Primes. The cardinality bound changes from s.card ≤ 5 to s.card ≤ 3. No custom definitions are needed.
The target is unconditional and covers every odd natural number greater than 1. At most three is essential: 3 and 5 cannot be sums of exactly three primes. All summands must satisfy Nat.Prime, and multiplicities count toward the cardinality bound. The initial proposal contains the goal with an open proof, ready for formalization.
A proof may combine a formalization of Helfgott's theorem, which supplies exactly three primes for odd n > 5, with singleton multisets for n = 3 and n = 5. Establishing Helfgott's result requires verified proofs of the analytic and computational ingredients of the chosen argument.
H. A. Helfgott, The ternary Goldbach conjecture is true, 2013, revised 2014. The mission's at-most-three formulation also includes the elementary cases n = 3 and n = 5.
Wikipedia's pages on open problems are, for many mathematicians, the first contact with a conjecture: a one-paragraph statement, a short history, a list of partial results. The Formal Conjectures library (Google DeepMind, Apache-2.0) turned a large part of that material into Lean 4 statements, so that the conjectures can be attacked — and, just as importantly, stated unambiguously — by machine.
This mission ports a coherent slice of that material to Prove2Me. It is deliberately a portfolio mission: the goal theorem is the Bateman–Horn conjecture, the strongest single statement in the collection, and the milestone list gathers the other conjectures and the landmark theorems that surround them. Some milestones are genuine steps toward the goal (the Bunyakovsky conjecture is literally the one-polynomial case); most are independent open problems from other fields, grouped here because they share a source, a level of difficulty, and a need for faithful formal statements. A reader should not assume that proving a milestone advances the goal theorem. The mission's value is that every statement in it has been written against the same Mathlib revision, checked to compile, and documented well enough to be attacked.
A rough timeline of the collection's landmarks:
The goal theorem concerns prime values of polynomials. Fix a finite set of distinct polynomials. Say that satisfies the Bunyakovsky condition if its leading coefficient is positive, , and is irreducible over ; say that satisfies the Schinzel condition if for every prime there is an integer with — i.e. no fixed prime divides the product at every argument.
For a prime let be the number of residue classes at which some vanishes, let , and let
The Bateman–Horn constant is the (conditionally convergent) Euler product
The other groups use their own vocabulary, each fixed in a definition item of this mission: Kakeya sets in and over ; Mills' property ; Wagstaff primes and Catalan–Mersenne numbers; polynomial self-maps and their Jacobian matrix; nontrivial closed invariant subspaces; linear extensions of a finite poset; Catalan's constant; and an explicit two-symbol Turing machine model with its maximum-shifts function .
The goal theorem is the Bateman–Horn asymptotic: under the Bunyakovsky and Schinzel hypotheses, exists and is positive and
Weaker statements in the same direction appear as milestones, first of all Bunyakovsky's conjecture: under the same hypotheses with , takes prime values infinitely often. The remaining milestones are listed in the milestone panel and are grouped by subject: Diophantine equations (Brocard, Pillai, Lebesgue–Nagell, Catalan/Mihăilescu), Mersenne-type primality (New Mersenne, infinitude of Mersenne primes, Catalan–Mersenne), prime-representing constants (Mills), geometric measure theory (Kakeya in , Kakeya over , Falconer), operator theory (invariant subspace problem and Read's counterexample), group algebras (Kaplansky's zero-divisor and idempotent conjectures), affine algebraic geometry (the two-variable Jacobian conjecture), irrationality and transcendence (, all odd zeta values, Zudilin's theorem, , , , Catalan's constant), order theory (the – conjecture), and computability (Radó's theorem).
The results themselves. Bateman–Horn is the quantitative form of Schinzel's hypothesis H: it contains the twin prime conjecture, the infinitude of primes of the form , and Bunyakovsky as special cases, and it is the standard heuristic behind prime-counting predictions. The other targets are each the headline question of their area: whether every bounded Hilbert-space operator has an invariant subspace; whether group algebras of torsion-free groups are domains; whether Kakeya sets must have full dimension. The solved milestones (Mihăilescu, Davies, Dvir, Zudilin, Read, Saito, Radó) are landmarks whose formal proofs would be significant library contributions in their own right.
Formalizing them. None of the open statements is expected to fall here; the concrete deliverable is a set of faithful, compiling, reusable statements plus formal proofs of the solved milestones, most of which are not in Mathlib today. Several are realistically in reach: the finite-field Kakeya bound (Dvir's polynomial method is short), the elementary fact that and cannot both be algebraic, and Radó's diagonal argument.
For Bateman–Horn, the obstruction is visible already for , : sieve methods bound from above by a constant times the conjectured main term and produce almost-primes, but the parity problem blocks every known sieve from producing a single prime value of an irreducible quadratic. The conditional convergence of the Euler product is a second, smaller trap: the product over must be taken in order, so any reformulation as an unordered infinite product changes the statement.
Each other group has its own obstruction, and they do not transfer: the parity problem says nothing about Kakeya, where the difficulty is that dimension is not stable under the natural compactness arguments, nor about the invariant subspace problem, where the known counterexamples on show that no soft argument can work.
Conventions this mission commits to, all fixed in the definition items:
ℤ[X]; primality of a polynomial value is primality of its
absolute value, and the counting function ranges over natural numbers .IsMulTorsionFree).Contributions welcome: proofs of the solved milestones; sharper variants; and additional faithful statements from the same source library, which contains far more than fits in one mission.
Provenance note. The Lean statements in this mission are adaptations of the Formal Conjectures library (Apache-2.0), rewritten to depend only on Mathlib and on this mission's own definition items, and checked to compile against the platform's Mathlib revision. Each draft item carries a read-back; those read-backs are non-blind — they were written by the same agent that drafted the statements, and each says so in its first line. They are documentation, not independent testimony.
The 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.
Recommendation platforms and online retailers choose which products to show a customer, and customers often buy more than one of them in a single visit. Classical choice models such as the multinomial logit (MNL) assume a customer buys at most one product, and under MNL the revenue-maximizing set of products to display is easy to find: it is one of the revenue-ordered sets, so it can be found in linear time. Tulabandhula, Sinha, Karra and Patidar (arXiv:2006.08055, Manufacturing & Service Operations Management, 2023) introduce the BundleMVL-K model, a multivariate logit model in which a customer buys a bundle of up to products, with pairwise interaction terms that capture complementarity and substitution. They estimate it on retail data and design algorithms for choosing the recommendation set.
The first question for any such model is whether the revenue problem stays tractable once purchases of two products are allowed. Theorem 1 of the paper answers it negatively: already for the unconstrained revenue problem is NP-complete. This mission formalizes that theorem and its proof, a reduction from Max-Cut.
The products are . Product has a revenue . A BundleMVL-2 instance assigns a nonnegative weight to every product and to every unordered pair of products, together with a no-purchase weight . (In the paper , and , so , is allowed.) A customer shown the recommendation set buys the nonempty bundle , , with probability , and buys nothing with probability . The expected revenue of is eq. (4),
With the indicator of , the weights , () and the revenues , (), both numerator and denominator are quadratic forms in .
The revenue problem (5) is ; its decision version asks, for a threshold , whether some has . SIMPLE MAX CUT asks, for a simple graph and an integer , whether the nodes of split into two parts with at least edges between them.
NP-completeness is in the sense of Cook's Definition 4: membership in NP and a polynomial-time many-one reduction from every NP language.
The result. Theorem 1 separates the multi-purchase model from its single-purchase counterpart: the revenue-ordered structure that makes MNL assortment optimization linear-time fails once pairs can be bought, and no polynomial-time exact algorithm exists unless P = NP. This is what justifies the paper's design of exact algorithms without running-time guarantees (a noisy binary search over the Compare-Step) and of polynomial-time heuristics, and it places BundleMVL-2 next to other hard assortment problems such as the mixture of two multinomial logits (Rusmevichientong et al. 2010, as cited by the paper) and the MMC model of Benson, Kumar and Tomkins (2018), whose hardness is the paper's Theorem 2.
Formalizing it. The theorem is proved in the paper; no machine-checked proof exists. The paper's argument constructs the instance and asserts the equivalence; it does not argue NP membership or the polynomial running time of the reduction, and it leaves the revenues and threshold free subject to inequalities. A formal proof must fix concrete rational parameters, show that the instance code has polynomial size, and handle malformed inputs. The Compare-Step identity (milestone 2) is also the correctness lemma for the paper's binary-search algorithm.
The mathematics of the reduction is short; the obstacles are the two halves that the paper treats as evident. First, the reduction must be a polynomial-time computable map on strings, in Cook's one-tape Turing-machine model, that sends codes of Max-Cut instances to codes of BundleMVL-2 instances and every other string to a non-member; the rational entries must be computed and written in reduced form. Second, NP membership needs a polynomial-time verifier that evaluates exactly in rational arithmetic, with a bound on the bit size of the sums. An approach that states the reduction as "for every graph there is an instance with the same answer" proves nothing: a fixed yes- or no-instance does that.
The development is in MultiPurchase.Hardness. Conventions committed to:
Fin n, 0-based; in the reduction the hub is 0 : Fin (m+1) and graph node i : Fin m is product i.succ.ℚ). Weights may be zero (), as the paper's own reduction requires (); revenues are positive and . These well-formedness conditions are part of the yes-predicate.BSym, rationals as reduced numerator and denominator.The complexity layer is the published CookPvsNP_defs (Cook's , , , NP-completeness) and ProjSchedTW_Complexity_Encoding (binary codes, cutSize, maxCutLang), with the proved CookPvsNP.polyReducible_trans. Contributions welcome: Turing-machine programs for rational arithmetic and list manipulation (reusable for every NP-membership proof over rational data), the polynomial-time reduction, and a proof of Karp's theorem for SIMPLE MAX CUT, which would discharge the hypothesis.
A graph records pairs of objects that cannot be chosen together. An independent set is a choice with no conflicting pair. When each vertex has a nonnegative weight, maximum weighted independent set asks for a conflict-free set with the greatest total weight. This model occurs when choices have values and pairwise incompatibilities. On general graphs the optimization problem is difficult; the planar restriction gives a concrete geometric promise under which approximation is possible. Williamson and Shmoys state a polynomial-time approximation scheme for planar maximum independent set as Theorem 10.11 of The Design of Approximation Algorithms, in the author electronic manuscript at PDF/manuscript page 271.
The instance has vertices labeled by Fin n, an adjacency table edge : Fin n → Fin n → Bool, and a real weight weight i for each vertex. SimpleGraph.fromRel turns the table into an undirected simple graph G. The theorem requires every weight to be nonnegative. A finite set S is feasible when G.IsIndepSet (S : Set (Fin n)) holds. Its value is ∑ i ∈ S, weight i.
Planarity is expressed by HasPlanarDrawing G: vertices are placed at distinct points of the real plane, and every edge is represented by a continuous simple arc. An arc has no vertex in its interior, and distinct edges can meet only at endpoints. This is a concrete local drawing convention for the planar graph promise. The drawing witnesses the hypothesis; it is not passed as part of the algorithm's input.
The computational model is a fixed finite unit-cost RAM program. Its input includes the vertex count, an integer accuracy parameter, a complete adjacency table, and the real weights in named memory cells. Its instructions include natural-number and real addition and subtraction, exact comparisons, random-access loads and stores, branches, jumps, and halt. The machine starts with the instance preloaded and produces a bitmap after the adjacency table. This precise instruction set is a formalization convention: the book states an arithmetic-operation running time but does not specify a machine language.
For every real , let . The goal asserts that a single finite program and fixed positive natural constants work for every planar instance and every vector of nonnegative real weights. The program must halt after a number of operations satisfying
Its bitmap must represent an independent set , and for every independent set ,
Comparison with every feasible includes an optimal solution. The same program and constants precede all accuracy and instance quantifiers. The form includes the empty graph without imposing zero running time. The result corresponds to the bound in Theorem 10.11; the formal statement makes the constants and accuracy parameter explicit.
The result supplies an accuracy-time tradeoff for planar weighted independent set: any fixed positive accuracy has a quadratic dependence on graph size in this operation model, while the accuracy dependence is exponential. It separates the planar setting from the general graph problem. The finite instruction set and input layout make the computational claim inspectable, including what information the program receives and what counts as an operation.
The cited result is known in the textbook. This mission asks for a Lean proof of the packaged statement; the theorem currently has sorry, and no machine construction or correctness proof is claimed. The original local statement was compiled and source reviewed before packaging. That prior result establishes statement validity in its source workspace, while the upload payload is checked separately.
A high-quality independent set in each planar region does not immediately give a high-quality global set: edges across regions can create conflicts, and discarding boundary vertices can lose weight. A proof must coordinate the approximation inequality with a uniform operation bound for one program across all graph sizes, accuracies, and real weight vectors. It must also show the computed bitmap is always independent and that execution reaches an explicit halt instruction within the bound. These requirements rule out treating an optimizer, an embedding, or a best solution as preloaded input.
The goal uses finite labeled graphs, nonnegative arbitrary real weights, exact real arithmetic, and the concrete drawing predicate above. It does not claim a bit-complexity bound for encoded reals. The RAM starts from a complete adjacency table and weight vector, with no supplied drawing or optimum. Its step function is deterministic; an invalid program counter is stuck, so the theorem explicitly requires a halt instruction. Outputs are bits in designated natural memory cells and are checked for validity before their weighted value is compared.
The packaged definitions are the drawing predicate, instruction type, state, transition, iteration, input layout, and output decoder. They contain no proof axioms or optimization oracle. The rational-input polynomial bit-time fragment in the source workspace is a separate statement and is outside this goal. A complete contribution would construct the finite program and prove its running time and approximation guarantee in the specified model.
A positive integer is perfect when it equals the sum of its proper divisors: , , then , , and so on. Every perfect number anyone has ever exhibited is even. Whether an odd one exists is one of the oldest unsettled questions in mathematics, and it is unsettled in a strong sense: there is no heuristic consensus that odd perfect numbers should be absent for a structural reason, only an accumulating list of conditions any example would have to meet.
The even side of the question is completely resolved. Euclid (Elements IX.36) showed that if is prime then is perfect; Euler proved the converse, so even perfect numbers correspond exactly to Mersenne primes. Nothing comparable is known on the odd side, and the literature instead consists of increasingly severe necessary conditions.
A timeline of what is actually proved about a hypothetical odd perfect number :
None of these results, alone or together, rules out an odd perfect number.
For write for the sum of all positive divisors of . Then is perfect exactly when
equivalently when the divisors of other than itself sum to . The function is multiplicative: whenever , and for a prime power. The quantity is the abundancy index of , so a perfect number is one of abundancy index exactly .
Write for the number of distinct prime divisors of . In Lean, is n.primeFactors.card, and perfection is Mathlib's Nat.Perfect n, which unfolds to ∑ i ∈ n.properDivisors, i = n ∧ 0 < n — the positivity clause is part of the definition, so is not perfect.
Every perfect number is even; equivalently, no odd perfect number exists. This is the weakest statement that settles the question, and it fixes no constants, so no future numerical improvement can invalidate it.
The milestones are the unconditional theorems of the literature listed above, each stated for a hypothetical odd perfect number :
The result itself. A proof of the goal would complete the classification of perfect numbers begun by Euclid: together with the Euclid–Euler theorem, every perfect number would be for a Mersenne prime . A disproof — an explicit odd perfect number — would be an object with at least ten distinct prime factors and more than decimal digits, and would immediately settle a long list of dependent questions about the abundancy index, about the distribution of the values of , and about the multiperfect numbers.
Formalizing it. Only the even half of the theory is currently formalized: the Euclid–Euler theorem is available in Mathlib's Archive (Archive/Wiedijk100Theorems/PerfectNumbers.lean, as Nat.eq_two_pow_mul_prime_mersenne_of_even_perfect and Theorems.perfect_iff_even_and_mersenne), and the main library carries the divisor-sum API around Nat.Perfect in Mathlib/NumberTheory/Divisors.lean, but nothing about the odd case. None of the milestones above is in Mathlib; formalizing them builds the missing -arithmetic infrastructure — factor chains, abundancy estimates, and the parity analysis of on odd numbers — that any attack on the goal, or any future formalization of the computational bounds, will need.
The obvious approach — take Euler's form and push the congruence conditions until they conflict — does not terminate. There is no known local obstruction: the equation has no contradiction modulo any fixed integer, so no congruence argument can close the problem. The known results are all of a different type: they exclude configurations of the prime factorization by finite case analysis on factor chains, and each analysis leaves infinitely many admissible configurations. Increasing weakens the constraints rather than strengthening them, which is why the lower bounds on have advanced by one prime factor per decade at very high computational cost. The upper bound makes the search space finite for each fixed , but astronomically so.
The development is stated over ℕ with Mathlib's Nat.Perfect, so positivity is built into the hypothesis and no separate 0 < n assumption appears. Oddness is Odd n, the number of distinct prime divisors is n.primeFactors.card, and Euler's form is stated with explicit residues p % 4 = 1, k % 4 = 1, together with ¬ p ∣ m and n = p ^ k * m ^ 2. No custom definitions are introduced; everything rests on Mathlib's Nat.sigma / Nat.Perfect API.
One caution on the shape of the milestones. Each is stated conditionally, for an assumed both perfect and odd, so each would follow trivially from the goal theorem. The point of the milestones is precisely that they are proved unconditionally in the literature: a submission is expected to reproduce (or improve on) the published argument, not to derive the statement from an unproved conjecture. Since the goal is itself open on the platform, no admissible proof can take that shortcut.
Contributions welcome: any of the milestones, the supporting multiplicativity and abundancy lemmas needed for them, and reusable infrastructure for on odd numbers. Sharper published bounds — larger values of , the improved Nielsen bound , the Ochem–Rao size bound — are also in scope and are strictly stronger than the milestones listed.
In 1915, George D. Birkhoff proved the existence of a retrograde periodic orbit in each bounded component of the planar circular restricted three-body problem and asked whether its double cover bounds a disk-like global surface of section. Such a surface turns a three-dimensional flow into a two-dimensional return map and was intended as a route to a direct periodic orbit (Birkhoff 1915; Liu--Salomão, Section 1.4). McGehee obtained the corresponding section in the small-mass perturbative regime in 1969, while modern contact and symplectic methods recast the question in terms of regularized energy hypersurfaces and Reeb dynamics (Joung--van Koert, Introduction).
In 2012, Hryniewicz established the global-section criterion later quoted by Joung and van Koert: on a dynamically convex star-shaped hypersurface, the proposed binding orbit must be unknotted with self-linking number −1 (Joung--van Koert, Theorem 1.3; Hryniewicz). In 2025, Joung and van Koert combined that criterion with validated orbit and convexity computations for and (Theorems 1.2 and 1.5). In May 2026, Liu and Salomão proved the conjecture at every subcritical energy for mass ratios sufficiently close to , in fact obtaining rational open books bound by every retrograde orbit in that regime (Theorem 1.16). Their June 2026 Hill result covers every subcritical energy in Hill's lunar problem, which is a limiting model rather than a finite-mass instance of the circular restricted problem (Liu--Salomão 2026). These results leave the universal finite-mass, all-subcritical statement below as the open target.
Two primaries of masses and , with , are fixed in rotating coordinates at and . For a massless particle with phase coordinates , the Hamiltonian is
This is equation (1.1) of Joung--van Koert. Let be the smallest collision-free critical value, where lies between the primaries. The subcritical range is ; there are then two bounded physical components, one around each primary (Liu--Salomão, Section 4).
The mission labels the primary at . With complex Levi-Civita variables and , the inverse position map is , and the regularized Hamiltonian is
On the collision-free domain, , and its zero level regularizes collision with the labeled primary (Joung--van Koert, equation (2.2)). The selected component is anchored at . Below , it is a star-shaped three-sphere, invariant under the free antipodal deck map , and it double-covers the corresponding Moser-regularized component (Joung--van Koert, Proposition 2.4).
For every , every , and every complete flow on generated by and commuting with the antipodal map, prove
Here consists of and a quotient period with , with no earlier positive time reaching either or . Its physical projection is required to be a -symmetric, simple, collision-free loop of winding around the labeled primary. Traversing it twice gives a least-period closed orbit upstairs. This records the geometric retrograde orbit used in the Birkhoff-conjecture formulation; it does not impose the stronger pointwise astronomical monotonicity test distinguished in Joung--van Koert, Definition 2.1, Proposition 2.2, and Remark 2.3.
The rational page is encoded by a smooth immersive disk lift . Its lift is embedded, its interior is transverse to , and its boundary is the closed double lift. After passing to the antipodal quotient, the interior remains embedded and the only nontrivial fibers are antipodal boundary pairs; hence the boundary maps exactly two-to-one onto the prime quotient orbit. Every nonbinding quotient trajectory must meet the page interior at arbitrarily large positive and negative times, matching the recurrence clause in the standard definition of a global surface of section (Hryniewicz, Definition 1.1).
A global surface of section replaces the continuous three-dimensional regularized flow, away from its binding, by the iterates of a two-dimensional first-return map. Periodic points, invariant sets, and recurrence of that map encode periodic and recurrent trajectories of the original system. This is why Birkhoff connected the conjecture to the existence of a direct orbit, and why later work uses such sections to obtain global dynamical consequences (Birkhoff 1915; Joung--van Koert, Introduction). A proof across all finite mass ratios and all subcritical energies would close the gap between the known perturbative, near-equal-mass, and narrow validated regimes.
Existence of a -symmetric geometric retrograde orbit is not the unresolved step: Birkhoff's shooting argument supplies one in each bounded component for every and every energy below (Liu--Salomão, Theorem 5.1). The difficult assertion is global. One must produce a disk with the correct two-fold boundary behavior, prove transversality at every interior point, and prove that every other trajectory returns to it indefinitely in both time directions. Known proofs obtain these conclusions from convexity, dynamical convexity, and pseudo-holomorphic-curve machinery only in restricted parameter ranges (Joung--van Koert, Theorem 1.5; Liu--Salomão, Theorem 1.16).
The Lean model uses total real-valued extensions of the displayed Hamiltonians, but every physical assertion carries explicit collision-free or denominator guards. The first critical value is initially an infimum; a separate theorem row proves nonemptiness, boundedness below, and attainment at an inner Lagrange point. The energy component is selected by a concrete regularized collision point, the physical mass range is strict, and the headline theorem assumes an actual Flow together with its Hamiltonian-generator and antipodal-equivariance properties. These choices prevent singular derivatives, an unintended component, an empty critical set, or an arbitrary dynamics from satisfying the goal vacuously.
The antipodal quotient in Lean is presently the topological quotient by the explicit deck relation. The formal rational-page predicate is therefore a cover-lift encoding: continuity, the real-action laws, exact quotient fibers, primeness, and global returns are stated downstairs, while smoothness, immersion, and transversality are stated on the Levi-Civita lift. It does not install a smooth atlas or explicit Moser coordinates on the quotient, and it asks for one rational page rather than a full open-book fibration. The theorem concerns one labeled primary; it does not simultaneously assert the analogous result on the other bounded component. The Hill limiting problem and the pointwise astronomical sign condition are not part of the headline conclusion.
All theorem rows are Lean declarations ending in by sorry. Successful elaboration verifies that the statements are syntactically and type-theoretically coherent; it is not evidence that the open theorem has been proved. Supporting rows isolate analytic facts, regularization identities, component geometry, quotient descent, the known retrograde-orbit theorem, and the parameter ranges already covered in the cited literature.
The quantum relative entropy is frequently used as a distance, or distinguishability measure between two quantum states. In this paper we study the relation between this measure and a number of other measures used for that purpose, including the trace norm distance. More precisely, we derive lower and upper bounds on the relative entropy in terms of various distance measures for the difference of the states based on unitarily invariant norms. The upper bounds can be considered as statements of continuity of the relative entropy distance in the sense of Fannes. We employ methods from optimisation theory to obtain bounds that are as sharp as possible.
This mission is the statement-level formalization of Continuity bounds on the quantum relative entropy (arXiv:quant-ph/0503218v3). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.
25 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is §VI, Theorem 4: sharp lower bound for every UI norm (seed headline) (§VI, Theorem 4: sharp lower bound for every UI norm (seed headline), PDF p. 1). The milestones are the other numbered results, in the paper's order, each quoting the paper.
The paper's own objects are the definition item of this mission. Objects shared across papers come from the prove2quantum library and from earlier papers' missions, listed as references.
Provenance: prove2quantum's pipeline drafted each statement (gpt-6.1-sol on Stanford's Sherlock cluster). A blind read-back, written without seeing the paper, is attached to every item. An independent moderator compared each statement against the paper and passed the whole paper without edits.
4 results of the paper are not stated yet, because the library lacks an interface they need:
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.
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.
An election is run by someone — a chair, a committee, an organiser — who can shape it without touching a single ballot: by deciding which candidates appear, which voters are registered, or how the electorate is split into bodies that pre-select nominees. Bartholdi, Tovey and Trick (1992) proposed to measure how well a voting rule protects itself against such manipulation by the computational difficulty of finding a successful manipulation: a rule for which the chair's problem is NP-complete is resistant, one for which it is solvable in polynomial time is vulnerable. They studied constructive control, where the chair wants a given candidate to become the unique winner.
Hemaspaandra, Hemaspaandra and Rothe (arXiv:cs/0507027, Artificial Intelligence 171, 2007) introduced destructive control: the chair wants a despised candidate not to be the unique winner ("anyone but him"). They classified plurality, Condorcet and approval voting under seven control types in both settings. This mission formalizes the last of their main results, Theorem 3.6, on control by partition of voters.
Timeline:
An election has candidates and voters , each casting a ballot. For plurality and Condorcet voting a ballot is a strict ranking of ; for approval voting it is the set of candidates the voter approves of. The election , with candidates and voters , reads each ballot through the preferences it induces on . Its winner set is:
In control by partition of voters the chair splits into two subcommittees and (either may be empty). Each subcommittee holds the subelection and nominates candidates. Under Ties-Promote (TP) it nominates all its winners; under Ties-Eliminate (TE) it nominates its winner if there is exactly one and nobody otherwise. The two-stage election then is
the nominees running against each other before all voters. Given , the constructive problem asks whether some partition gives , the destructive problem whether some partition gives .
Definition 3.1 of the paper: a rule is susceptible to a control type if in some election the chair can change from not being the unique winner to being it (constructive), or from being the unique winner to not being it (destructive). It is vulnerable if it is susceptible and the problem's language is in P; certifiably-vulnerable if it is susceptible and a successful partition can be computed in polynomial time; resistant if it is susceptible and the language is NP-complete.
With Hitting Set and Exact Cover by Three-Sets NP-complete (the two facts the paper takes from Garey and Johnson),
Nine clauses, each including its susceptibility part.
Theorem 3.6 is where the tie-handling model changes the classification: plurality is vulnerable under TE and resistant under TP, for both constructive and destructive control. Under TE at most one candidate leaves each subcommittee; under TP any set of tied candidates may advance. The theorem also shows that approval and Condorcet, which resist constructive control by partition of voters, are vulnerable to its destructive form. Results of this kind underlie the comparison tables of the later control literature (Faliszewski, Hemaspaandra and Hemaspaandra, Control and bribery in voting, 2016).
The paper's proofs are combinatorial algorithms and many-one reductions, stated informally. No part of the paper has been machine-checked. A formal development produces:
The algorithmic clauses need more than correctness of a decision procedure: membership in P and polynomial-time computability are statements about a one-tape Turing machine reading binary codes. An algorithm described by "for each candidate d, check …" has to be compiled to that model, and its running time bounded, which no existing library on the platform does for elections.
The plurality TE algorithms are case analyses: who can be nominated by each part, and how many first-place votes each candidate must surrender. The cases where has no first-place vote, or where a subcommittee is empty, are exactly where the printed algorithms slip. The approval TP destructive algorithm was wrong as first published.
For the hardness clauses the reductions must be shown correct for every instance. Claim 4.41 needs an arithmetic padding condition, which is why the paper first proves Restricted Hitting Set NP-complete (Theorem 4.39) and then reduces from it. NP membership, which the paper calls obvious, still has to be proved in the checking-relation form of NP.
Fin m and voters Fin n, both possibly empty. A profile is Fin n → Ballot m, so the multiset of ballots is a list (one ballot per voter, as the paper assumes on p. 4).Equiv.Perm (Fin m), read as the position of each candidate. An approval ballot is a Finset.V₁ : Finset (Fin n) and its complement.{c}; an empty winner set is a destructive success.CookPvsNP notions. Instance codes are lists of binary numbers over the published alphabet BSym: , then the ballots.encNats [0]) on every no-instance.None of these is a trivializing reading. "In P" is a Turing-machine statement, not a Decidable instance. Every vulnerable or resistant clause carries its susceptibility part. A certifiable-vulnerability witness must output a successful partition, which is more than deciding the language.
Welcome contributions: proofs of the examples (finite computations), of Claims 4.29–4.41 (counting arguments), of NP membership of the control languages, and Turing-machine implementations of election-scoring primitives, which later missions can reuse.
The n-Queens problem, placing mutually non-attacking queens on an chessboard, is a standard benchmark in constraint programming and artificial intelligence. As a decision problem it is trivial: a solution exists for every other than and and can be written down in closed form, and the input has only bits. This has repeatedly led to criticism of its use as a benchmark.
The variant n-Queens Completion, posed in 1850, asks whether a board on which some queens are already placed can be completed to a full solution. Gent, Jefferson and Nightingale (JAIR 2017) show that this variant is genuinely hard: deciding it is NP-complete and counting its completions is #P-complete. This gives benchmark designers a version of the puzzle with a provable hardness guarantee, and it makes the n-Queens literature (Pólya's modular construction, Rivin–Zabih exchanges) a source of reduction gadgets.
Timeline:
A queen is a pair of non-negative integers, its column and row. Its sum-diagonal is and its difference-diagonal is the integer . It fits on board size if . Two distinct queens attack each other if they share a column, a row, a sum-diagonal or a difference-diagonal. A solution to the -Queens problem () is a set of queens that fit on board size , no two attacking.
An instance of n-Queens Completion (Problem 2) is a pair : a board size and a set of queens that fit on board size , no two in the same row or column. may contain two queens on a common diagonal; such an instance simply has no solution. A completion is an -Queens solution with .
The proof passes through four intermediate problems. In Problem 3 the extra queens must use prescribed columns and rows . In Problem 4 (Excluded Diagonals) sets , of difference- and sum-diagonals are forbidden. Problem 5 is a family of Problem 4 instances that interact only through their sum-diagonals. Problem 6 is Restricted 1-in-3-SAT: clauses of three distinct positive variables, every variable in at most three clauses, and an assignment must make exactly one variable of every clause true.
Complexity is measured on the published CookLevin machine model: a language is a set of binary strings, CookLevin.NPComplete is NP-completeness under polynomial-time many-one reductions, and a function from strings to is in #P if it counts the accepted certificates of an NP verifier. Every instance is coded with its board size in unary, as the paper assumes (p. 820). is the language of codes of instances that have a completion, and is the number of completions of the instance coded by .
Here #P-completeness means membership in #P together with hardness under parsimonious reductions: polynomial-time maps with for every string . The statement is unconditional.
Each reduction theorem states both halves of "parsimonious": the paper's construction preserves the number of solutions instance by instance, and a polynomial-time map on codes implements it.
The result. Theorem 37 shows that the hardness of n-Queens Completion is not an artefact of a particular solver. The same chain shows that Excluded Diagonals and Blocked n-Queens are NP- and #P-complete (Corollary 38), and Corollary 15 (from Lemma 12) shows that every non-attacking set of queens occurs inside some full solution of a larger board. Because the reductions are parsimonious, they also transfer counting hardness: counting completions exactly is as hard as #SAT.
Formalizing it. The result is proved on paper; no part of it is machine-checked. The mission adds the platform's first #P layer (#P, parsimonious reductions, #P-completeness) on top of the published CookLevin NP framework, and the first chessboard objects. Four printed slips are corrected, each with a counterexample: Lemma 8 needs ; Problem 3 needs (Theorem 13 fails otherwise); Definition 20's overshoots ; Definition 20 is undefined for the empty family.
The obvious argument fails in two places.
First, each reduction is a bijection between solution sets whose correctness depends on exhaustive diagonal bookkeeping: that the 19-queens frame and the embedded modular solutions leave exactly the intended squares free, that the blockers of Definition 16 rule out exactly the chosen diagonals, and that gadgets on a long diagonal interact only through sum-diagonals. Each is a case analysis over many families of squares, with integer arithmetic on both diagonals.
Second, Theorem 4 is cited, not proved, for its hard part. A proof from scratch needs #P-hardness of a 1-in-3-SAT variant, i.e. a parsimonious version of the Cook–Levin theorem. The published CookLevin.sat_npComplete gives the decision half only, and many standard reductions from SAT are not parsimonious. In addition, every map must be shown polynomial-time on the CookLevin machine model, which the paper asserts "by inspection".
Lean conventions:
ℕ × ℕ (column, row), the difference-diagonal is computed in ℤ, and sets of queens are Finset (ℕ × ℕ);List of Problem 4 instances, and its sum-diagonal condition applies to distinct indices;Set.ncard of solution sets, which are finite.The constructions (Definitions 10, 16, 20, 24, 26–28, 31) are transcribed as defs, never chosen by Classical.choice. Each reduction theorem fixes its output to the code of the paper's construction.
Trivializing formalizations are ruled out explicitly:
List Bool languages, not Prop-valued predicates;ncard of an infinite set is ;CookLevin.IsPolyTimeComputable;Infrastructure that is reusable beyond this mission: the #P definitions and their closure under composition of parsimonious reductions, and polynomial-time computability of list and arithmetic manipulations on unary codes, for which the published WordRAM simulation (CookLevin.ramPolyTime_to_tm_poly, CookLevin.polyTimeComputable_comp) is the intended route. A parsimonious Cook–Levin theorem would serve every future #P-completeness result. Contributions are welcome on any milestone; the gadget lemmas (33–35) and the arithmetic facts (Lemma 9, Observations 6 and 29, Lemma 30) are self-contained and decidable on finite data.
Multiplying two binary integers is a basic task in computational complexity. The relevant resource here is the number of individual steps made by a machine whose tapes can only be accessed through moving heads. Harvey and van der Hoeven established an bound in this model. The OpenAI manuscript proposes a positive saving in the exponent of the logarithm. Subsequent constructions explore larger savings. The formalization target is the complete computation and its time bound, including the analytic and implementation arguments needed to connect a finite construction to every input length.
A deterministic multitape Turing machine has a fixed finite alphabet, a fixed finite state set, and a fixed finite number of tapes. Each tape extends in one direction and has one head. A step reads the symbols under the heads, changes state, writes at those positions, and moves each head by at most one cell. The alphabet contains distinct blank, start-marker, zero, one, and separator symbols. Tape zero is the read-only input tape; tape one is the output tape; further tapes are available for work. The halting state freezes the configuration.
An input consists of two bit strings of the same positive length , separated by . The strings are read most significant bit first, with leading zeros permitted. If denotes the represented natural number, the required output is exactly the -bit binary representation of , padded with leading zeros and followed by blanks. All tapes begin with a preserved start marker. Define .
The full target is
This asserts the existence of one machine that computes the exact product correctly for every positive input length, together with constants and such that every pair of -bit inputs, for and , halts within
steps. Constants, alphabet, states, and tape count are independent of the input length. The number is an exact real value. Larger gives a stronger asymptotic saving because .
Each entry supplies its own exact numerical value and identifies the construction that motivates it. Historical and new entries use the same machine definition. A proposed value may be recorded while its complete proof is still open; it becomes a proved record only when the goal has a verified proof. Numerical certificates are supporting results with their own scope, and do not establish a complete machine time bound.
The value
is the headline conditional witness of S. Jain's integer-mult-kappa, round eight, at revision 5868dc7. It is bound by the complex side ().
The repository states that the claim is conditional: it assumes the full upstream multiplication theorem (the OpenAI manuscript and Colkitt's framework) and that stage two is the complement time-reversal of stage one, and it rests on three further interfaces that are stated but not machine-checked there — IceKylin's normal form for alternating residuals, the cost of binary address adapters for the exterior fix-up children, and the row stock of the stopped bit interchange. Its Lean files check only finite rational statements (moment certificates, the stopped mix and the parameter assembly), not the analytic inequalities or the multiplication theorem. It has not had independent review.
Earlier claims appear as milestones: Harvey–van der Hoeven (), OpenAI Theorem 1 (), Colkitt's checkpoint, Jain rounds six and seven, and community PR #62. Each is implied by this goal because decreases in .
A proof for any positive value would give a strict asymptotic improvement over . Such an improvement would contradict the proposed lower bound, while remaining consistent with the known upper bound. The tracked value concerns asymptotic growth; it does not measure the runtime of a practical implementation. No claim about a currently fastest implementation follows from a larger saving.
Formalizing the full target connects exact finite calculations to a uniform algorithm. The community repository explicitly treats the original framework and remaining all-size interfaces as assumptions of its current evidence. In this mission those steps must be proved before the goal can be marked Proved. They are not added as hypotheses that would weaken the full target. Earlier published theorem statements and finite certificates may be reused with their original attribution and proof status.
A finite network certificate can establish a concrete role count or a rational margin, but does not itself supply a machine for every input length. A complete proof must establish correctness of the recursive construction, admissibility of its parameters, precision and error guarantees, and the cost of moving data on tapes. Counts of algebraic operations alone do not account for this last resource. The difficult connection is between these separate contracts and the single uniform machine quantified by the goal.
The goal imports the existing public Definitions.Def_IntMul_MultitapeModel bundle and uses IntMul.KappaBound directly. No alternative machine or cost model is introduced. Natural numbers describe input lengths, head positions, and step counts; real numbers describe the asymptotic constant and exponent. The real power has base at least one. Correctness is required even below the asymptotic threshold. Inputs of length zero and malformed inputs are outside the specified task.
The input and output conventions exclude a machine that merely decides a predicate about the product. The entire output tape must contain the required product and then blanks. Neither failure to halt nor correctness on a finite collection of test inputs meets the target. The work tapes and final head positions are unconstrained. Reusable contributions include machine composition with explicit costs, exact encodings, analytic estimates, and proofs that the finite certificates imply the contracts required by the recursive algorithm. Every such contribution should state its own assumptions and conclusion explicitly.
Multiplying two binary integers is a basic task in computational complexity. The relevant resource here is the number of individual steps made by a machine whose tapes can only be accessed through moving heads. Harvey and van der Hoeven established an bound in this model. The OpenAI manuscript proposes a positive saving in the exponent of the logarithm. Subsequent constructions explore larger savings. The formalization target is the complete computation and its time bound, including the analytic and implementation arguments needed to connect a finite construction to every input length.
A deterministic multitape Turing machine has a fixed finite alphabet, a fixed finite state set, and a fixed finite number of tapes. Each tape extends in one direction and has one head. A step reads the symbols under the heads, changes state, writes at those positions, and moves each head by at most one cell. The alphabet contains distinct blank, start-marker, zero, one, and separator symbols. Tape zero is the read-only input tape; tape one is the output tape; further tapes are available for work. The halting state freezes the configuration.
An input consists of two bit strings of the same positive length , separated by . The strings are read most significant bit first, with leading zeros permitted. If denotes the represented natural number, the required output is exactly the -bit binary representation of , padded with leading zeros and followed by blanks. All tapes begin with a preserved start marker. Define .
The full target is
This asserts the existence of one machine that computes the exact product correctly for every positive input length, together with constants and such that every pair of -bit inputs, for and , halts within
steps. Constants, alphabet, states, and tape count are independent of the input length. The number is an exact real value. Larger gives a stronger asymptotic saving because .
Each entry supplies its own exact numerical value and identifies the construction that motivates it. Historical and new entries use the same machine definition. A proposed value may be recorded while its complete proof is still open; it becomes a proved record only when the goal has a verified proof. Numerical certificates are supporting results with their own scope, and do not establish a complete machine time bound.
The value
is the conditional witness of S. Jain's integer-mult-kappa, round seven, at revision c05adfe, with the sharper moment certificate merged there (research/round7-moment-refinement/). The README's headline for the same construction is the slightly smaller ; the refinement keeps the frozen round-seven bit network, histogram, complex saving and assembly unchanged, and replaces the reciprocal bound in the moment certificate by a degree-eight Taylor enclosure, which certifies the bit saving .
The construction builds on the OpenAI manuscript and on Colkitt's integer-mult-bounds (it uses the PR #62 producer with interval strips and core-aware pair assembly). Its new ingredients are lifted frames with late copies, deferred readouts, and per-use leaves on the bit side; the complex side is round six's. The repository states that the claim is conditional on the OpenAI manuscript and Colkitt's framework, that stage two (the complement time-reversal of stage one) is assumed rather than machine-checked, and that its Lean files check only finite rational statements (moment certificates and parameter assembly), not the analytic tail inequalities or the multiplication theorem. It has not had independent review.
Earlier claims appear as milestones: Harvey–van der Hoeven (), OpenAI Theorem 1 (), Colkitt's checkpoint, Jain round six () and community PR #62 (). Each is implied by this goal because decreases in .
A proof for any positive value would give a strict asymptotic improvement over . Such an improvement would contradict the proposed lower bound, while remaining consistent with the known upper bound. The tracked value concerns asymptotic growth; it does not measure the runtime of a practical implementation. No claim about a currently fastest implementation follows from a larger saving.
Formalizing the full target connects exact finite calculations to a uniform algorithm. The community repository explicitly treats the original framework and remaining all-size interfaces as assumptions of its current evidence. In this mission those steps must be proved before the goal can be marked Proved. They are not added as hypotheses that would weaken the full target. Earlier published theorem statements and finite certificates may be reused with their original attribution and proof status.
A finite network certificate can establish a concrete role count or a rational margin, but does not itself supply a machine for every input length. A complete proof must establish correctness of the recursive construction, admissibility of its parameters, precision and error guarantees, and the cost of moving data on tapes. Counts of algebraic operations alone do not account for this last resource. The difficult connection is between these separate contracts and the single uniform machine quantified by the goal.
The goal imports the existing public Definitions.Def_IntMul_MultitapeModel bundle and uses IntMul.KappaBound directly. No alternative machine or cost model is introduced. Natural numbers describe input lengths, head positions, and step counts; real numbers describe the asymptotic constant and exponent. The real power has base at least one. Correctness is required even below the asymptotic threshold. Inputs of length zero and malformed inputs are outside the specified task.
The input and output conventions exclude a machine that merely decides a predicate about the product. The entire output tape must contain the required product and then blanks. Neither failure to halt nor correctness on a finite collection of test inputs meets the target. The work tapes and final head positions are unconstrained. Reusable contributions include machine composition with explicit costs, exact encodings, analytic estimates, and proofs that the finite certificates imply the contracts required by the recursive algorithm. Every such contribution should state its own assumptions and conclusion explicitly.
Scheduling with earliness and tardiness penalties asks for schedules in which a job finishing early is as undesirable as a job finishing late. The model fits production planned for just-in-time delivery, where finished goods held before their due date cost money, and sequences of experiments tied to fixed external events. It departs from classical scheduling, in which finishing early is never penalized.
Garey, Tarjan and Wilfong (Math. Oper. Res. 13 (1988) 330–348) study the symmetric version on one processor: each task has a preferred starting time, and the penalty is the absolute deviation from it. Their §2.1 settles the complexity of the most natural objective, the sum of these deviations, by proving it NP-complete. The result explains why the rest of their paper, and much of the later literature, turns to special cases that can be solved efficiently: a fixed task order, equal task lengths, or the maximum deviation instead of the sum.
A short history of the model:
There are tasks . Task has a length and a preferred midtime . A schedule assigns every task a starting time such that no two tasks overlap on the single processor: for , either or . Idle time is allowed. The actual midtime of is , and the total discrepancy of is
The paper works with midtimes because the special case below is then symmetric. Preferred midtimes and preferred starting times are interchangeable through .
Total discrepancy (the decision problem). Given and , is there a schedule with ?
Even-odd partition. Given positive integers , can they be split into two sets of equal sum so that each set contains exactly one of for every ?
The special case. For tasks with and one common preferred midtime , write and . A schedule is ordered if, on each side of , shorter tasks lie nearer to . The bracket is the schedule that puts at midtime and packs the listed tasks against it in the listed order.
The hypothesis is the one result the paper imports (Garey and Johnson, 1979). The conclusion includes membership in NP and polynomial-time many-one reductions from every NP language, with Turing machines as the model of computation.
THEOREM 1 is the hardness boundary for one-processor scheduling with symmetric earliness–tardiness penalties and arbitrary preferred times. It is the reason exact algorithms for this objective are enumerative, and the reason polynomial results are sought under extra structure, such as the fixed-order algorithm of the same paper. The special-case lemmas characterize every optimal schedule for a common, unrestrictive midtime, not just one of them: shortest task centered at , the -th pair of lengths in the -th positions on either side, either member on either side. This characterization holds independently of the reduction.
The result has been proved since 1988, and no machine-checked version of it is known to us. A formalization adds three things. First, the parts the paper calls "straightforward" or "a simple exercise", membership of both problems in NP. Second, the two places where the published argument is imprecise. The instance D has half-integer midtimes and threshold although the decision problem asks for integers, so a correct reduction must rescale. And the special-case lemmas are proved for a large midtime but applied with , so they must be restated for every . Third, a reusable formal treatment of absolute-deviation scheduling objectives and of reductions between number problems written in binary.
The obvious argument fails at the step from the special case to the instance D. The lemmas on pp. 333–336 assume the common midtime is large, so that the constraint never binds. In D the midtime is , exactly half the total length, and the reduction works because the constraint binds. The tasks before must fit in , and the extra task must sit at . Together these force the two sides to have equal total length. A proof that only cites the large- lemmas proves nothing about D. Conversely, dropping makes the reduction false: put the shorter element of every pair after .
The other obstacle is the complexity bookkeeping. NP-completeness here means Turing machines, binary codes, and polynomial bounds, and a full proof must compute D from the code of , double the times to clear the half-integers, and certify membership in NP for a problem whose schedules have real starting times. The certificate cannot be the real starting times themselves.
Fin N from . In the special case is index , and the paper's () are the indices for .CookPvsNP_defs (Cook's one-tape Turing machines, NP, NPComplete) and the published ProjSchedTW.Complexity.Encoding (four-letter alphabet and binary codes). This mission defines positivePartitionLang by restricting the imported equal-sum predicate to nonempty lists of positive integers, as on p. 333. Only codes of well-formed instances belong to the even-odd and total discrepancy languages.NPComplete evenOddLang as the hypothesis instead would drop LEMMA 1 and is not what is asked.Contributions welcome: proofs of any milestone, and reusable lemmas on Turing-machine computability of arithmetic on binary codes, which the two membership results and both reductions need.
An insurance company's surplus grows with premiums and falls with claims. In the Cramér–Lundberg model with a positive safety loading, the surplus drifts to with probability one. De Finetti (1957) objected that a company does not accumulate capital indefinitely: surplus above some level is paid out to shareholders. He proposed choosing the payout policy to maximize the expected discounted dividends paid before ruin. This is the optimal dividend problem. It is one of the basic stochastic control problems of actuarial mathematics and corporate finance, and it serves as a test case for singular control of processes with jumps.
The classical answer is a barrier strategy: pay out whatever lifts the surplus above a level and nothing else. Jeanblanc and Shiryaev (1995) proved this optimal when the surplus is a Brownian motion with drift, and Gerber and Shiu studied the same Brownian setting. Azcue and Muler (2005) showed that it can fail in the Cramér–Lundberg model, where the optimal policy may be a band strategy. Avram, Palmowski and Pistorius (Ann. Appl. Probab. 17 (2007) 156–180) treated a general spectrally negative Lévy process, a process with stationary independent increments and only downward jumps. They found the value of every barrier strategy in closed form through the scale function of the process and identified the best barrier level . They also gave a verification condition under which the barrier at is optimal among all strategies. Loeffen (2008) later showed that the condition holds whenever the Lévy measure has a completely monotone density.
Let be a spectrally negative Lévy process on a filtered probability space with and Lévy triplet . Its Laplace exponent is , finite for :
Increments after time are independent of . Initial capital is added to . The standing assumptions are the following: does not have monotone paths, , and either , , or has a density.
A dividend strategy is a nondecreasing, left-continuous, adapted process with . The risk process is and the ruin time is . The strategy is admissible () if no lump sum exceeds the current reserves. Its value is
with discount rate . For , consists of the admissible strategies that keep for .
The -scale function is the unique continuous nondecreasing function on with for large . It is extended by on . The barrier strategy reflects at the level , paying at time . The paper computes its value
and the optimal barrier level is , read as when this set is empty and for all . The generator is
Assume , or has bounded variation, or . Then and:
The goal fixes no constants: the barrier level and the value function are both given by the scale function of the given process.
The theorem gives an explicit solution to a singular control problem for a general Lévy model. The candidate value function and barrier level are expressed through one special function, , and optimality over all strategies reduces to one inequality on . It is the basis of the later literature on scale-function methods in dividend problems (Loeffen 2008, Kyprianou–Rivero–Song 2010, and the refracted and Parisian variants). Part (i) holds with no condition on the Lévy measure. Part (ii) shows exactly where barrier optimality can fail.
The paper's proofs use fluctuation identities (exit problems, excursion theory) and Itô's formula for semimartingales with jumps. None of these is in Mathlib. As far as is known, none of these results has been machine-checked. A formalization would produce a Lévy-process and scale-function layer, a formal model of singular control with jumps and lump-sum payments, and a checked verification argument. Each of these can be reused beyond this paper.
The analytic part is elementary once the value formula (5.1) is available: the choice of , Proposition 3(i) and Lemma 3(i) follow from the shape of . The difficulty lies in the two probabilistic steps. Proposition 1 identifies the value of a reflected process through exit identities for . Those identities rest on excursion theory, or on the martingale property of up to exit. The verification step, Proposition 4(i), needs Itô's formula for . Here is a jump process controlled by a left-continuous finite-variation process that may itself jump. The change-of-variables formula must also run under only regularity when has bounded variation. Just proving that and imply a supermartingale inequality does not settle the question: the lump-sum payments and the jumps of enter the Itô expansion separately and must each be bounded.
Time is (ℝ≥0). is a structure carrying the triplet and pathwise càdlàg paths with only downward jumps. It also carries independence of increments from the filtration and stationarity. Its law is fixed by the Laplace transform for . The standing assumptions of §2 and (3.3) are bundled as one predicate. The scale function is a hypothesis on a function argument (it is unique). is an extended real, since it is for unbounded variation without a Gaussian part.
Values of strategies and value functions lie in . The dividend integral is a Lebesgue–Stieltjes integral over : it counts the lump sum at time and excludes a payment at the ruin instant.
Several conventions are fixed, and each is disclosed in the item it affects:
A trivializing encoding is ruled out: the value is not a real supremum, the barrier strategy is constructed rather than assumed, and is a conclusion.
A complete development needs:
The Lévy and scale-function layer is shared with the companion mission on the bail-out problem. Contributions of general lemmas (Stieltjes integration by parts, optional stopping for càdlàg martingales) are welcome.
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.
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.
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.
Kall and Mayer's Stochastic Linear Programming: Models, Theory, and Computation (Kluwer/Springer, 2005) reduces most stochastic models to deterministic optimization problems. Chance-constrained problems become nonlinear programs with convex constraint functions, and the regularized decomposition methods for recourse problems solve a quadratic master program at every iteration. Chapter 1, §3 therefore collects what the rest of the book needs from nonlinear programming: subgradients of convex functions, the regularity conditions under which local information certifies global optimality, the Karush–Kuhn–Tucker (KKT) conditions, and the saddle point theorem for the Lagrange function.
This is the first mission of a series that formalizes the book chapter by chapter. It formalizes Chapter 1, §3–§3.1 (printed pp.60–66), together with the Farkas lemma of §2 (p.21) on which the KKT proof rests.
The results are classical: Karush (1939) and Kuhn and Tucker (1951) for the multiplier conditions, Slater (1950) for the interior-point regularity condition, Farkas (1902) for the theorem of the alternative. The book cites Luenberger for the saddle point theorem and Rockafellar's Convex Analysis for subdifferentials.
The object is the convex program
where are convex and, from p.62 on, continuously differentiable. Its feasible set is , and a point solves (3.1) if and for all . The active set at is .
Two regularity conditions are compared. RC 0 requires that at every optimum , every direction with for all has . RC 1, the Slater condition, requires a point with for all .
The KKT conditions (3.3) for a pair are
The Lagrange function is . A saddle point is a pair with for all and all (3.6). The dual function is and the primal function is .
For a convex , a subgradient at is a with for all , and the subdifferential is the set of all subgradients (Definition 3.2).
If is a saddle point of the Lagrange function of (3.1), then
and solves each of the two problems: attains the maximum and the minimum.
Proposition 3.4 is what makes the convex reformulations of later chapters checkable. A point satisfying a finite system of equations and inequalities is certified globally optimal. Under the Slater condition, every optimum carries such a certificate. The saddle point theorem recasts the same multipliers as an optimal solution of a dual problem with equal optimal value. Its milestone (3.6) connects it back to the KKT conditions. Proposition 3.2 supplies the calculus that Chapter 3 applies to the nonsmooth expected recourse function.
The status is mixed. The KKT characterization (Proposition 3.4) is already formalized on the platform as a more general statement with additional linear equality constraints, and so are the gradient inequality (Proposition 3.3), the continuity of finite convex functions (Proposition 3.1) and the Farkas lemma. These enter as references. The rest has no machine-checked proof on the platform: the subdifferential facts of Proposition 3.2 (the chain rule in particular), the regularity conditions RC 0 and RC 1 with Remark 3.1, the sign-constrained KKT system (3.5), and the saddle point theorem in its min–max form with values in the extended reals.
The saddle point theorem itself is short once the extended-real bookkeeping is right. The inner infimum can be and the inner supremum , so "max" and "min" in (3.7) assert attainment as well as equality. A version that compares only finite values, or proves only weak duality , is a different theorem.
The milestones carry most of the mathematical weight. "RC 1 implies RC 0" is stated in the book without proof. The obvious approach fails at a direction with for an active , where first-order information says nothing about whether stays feasible. The refined version, with strictness only for the nonlinear constraints, can no longer push linear constraints into the interior. The chain rule of Proposition 3.2 needs the inclusion , which fails for general convex functions with restricted domains, and not only the easy reverse inclusion. "Differentiable iff the subdifferential is a singleton" asks for Fréchet differentiability from a unique subgradient, which is false without convexity and finite dimension.
is EuclideanSpace ℝ (Fin n). Constraints are indexed by Fin m. is the inner product and is Mathlib's gradient. Convexity is ConvexOn ℝ Set.univ, continuous differentiability is ContDiff ℝ 1, and every theorem states both standing assumptions for and every . Multipliers are Fin m → ℝ with the componentwise order. The dual and primal functions take values in EReal. "Solves (3.1)" is global optimality over . The definitions use gradient, which returns at a point of non-differentiability, so RC 0 and the KKT predicate carry their meaning only under the differentiability hypotheses that every theorem includes. A theorem about them without those hypotheses would be a different statement.
The definitions (feasible set, optimality, active set, RC 0, RC 1, KKT conditions, subdifferential, Lagrange function, saddle point, dual and primal functions) are written for reuse by later missions of the series. Chapter 2's chance-constrained programs and Chapter 3's recourse functions use the same convex program and subdifferential. Contributions are welcome on any milestone. The regularity milestones (RC 1 implies RC 0 and its refinement) and the chain rule of Proposition 3.2 are the substantial ones.
An allocation decision does not always produce a reward. An advertisement may receive no click, or a recommended product may not be purchased. In online matching with stochastic rewards, a failed offer uses the customer's opportunity but leaves the resource available for a later customer. This distinction changes both the algorithm and the benchmark against which it should be compared. Goyal and Udwani study this issue with arbitrary vertex rewards and establish the competitiveness of a randomized greedy rule when success probabilities factor across the two endpoints (supplied artifact, §§1–3).
The relevant offline comparison also faces uncertainty. Knowing tomorrow's arrivals is different from knowing which future offers will succeed. The mission concerns the former advantage: offline algorithms know the graph and probabilities, but learn an outcome only after making its offer. Its central target is the exact constant claimed by Theorem 1, including the assertion that no randomized online policy has a better uniform guarantee.
A source instance consists of a finite set of resources, an ordered finite sequence of arrivals, and a bipartite graph of available offers. Resource i has unit capacity and a nonnegative real reward r_i. A present edge (i,t) has success probability p_it in [0,1]. The graph and arrival sequence are fixed independently of the algorithm's random choices. At time t, the algorithm learns the incident edges and their probabilities, then offers at most one remaining neighbor or skips. Success earns r_i and consumes i. Failure earns zero and leaves i available. Either outcome consumes the arrival. Unused edge outcomes remain hidden (§§1–2, pp. 2–3 and 8–9).
Probabilities are decomposable if p_it=a_i b_t for nonnegative endpoint factors on every present edge. The products, rather than the individual factors, must be at most one. Algorithm 1 does not require the factors: it uses the revealed probabilities. It draws independent real uniform seeds y_i in [0,1] once, sets g(x)=exp(x-1), and at each arrival offers an available neighbor maximizing p_it r_i(1-g(y_i)). Seeds persist after failures. Ties use increasing resource index, consistently across the full and resource-deleted executions (Algorithm 1, p. 9).
The clairvoyant benchmark processes arrivals in the original order. The fully offline benchmark may adaptively choose any unprocessed arrival next. Both know the complete fixed instance, may randomize, may discard an arrival, and observe only the outcomes of their own offers. Their values are suprema of expected rewards over these operational policy classes. They are not the values of an expectation relaxation.
Write ALG(D) for Algorithm 1's expected reward, C(D) and F(D) for the two benchmark values, and c=1-exp(-1). The goal is the full conjunction
and
Here A ranges over general randomized online algorithm families, before the hard instance D is chosen. The goal retains the exact constant, both benchmarks, and optimality from Theorem 1, p. 5.
The six milestones are Lemmas 1, 2, 3, 5, 6, and 4 in that order. They concern deterministic DP attainment of both benchmarks; both conclusions of path-based weak duality; equality of the actual reward and the constructed dual total; both arrival-side conditional bounds; the resource-side conditional bound; and the averaging implication for the other seeds. Each keeps its source statement and scope. The seven theorem declarations are open proof targets.
The claimed result compares an implementable online rule with an adaptive fully offline competitor for arbitrary finite input sizes, arbitrary nonnegative resource weights, and nonvanishing probabilities. An expectation LP is a different, potentially stronger numerical comparison, and substituting it would change the target (§3.1, pp. 10–11).
The formalization provides separate interfaces for observable histories, randomized policies, independent edge experiments, continuous seed perturbations, finite dynamic programming, and the path-based program. It reuses the published bare probing-policy recursion and a general finite linear-program definition. The classical randomized b-matching lower bound is already proved on Prove2Me; its unit-capacity specialization is reference support for optimality. The bridge to this stochastic model remains mathematical work, rather than an assumption supplied to the goal.
Adaptive decisions depend on previous observations. Treating all potential successful offers as independent after selection loses that dependence. Likewise, fully offline's ability to choose the next arrival depends on previous outcomes; a maximum over fixed arrival permutations would not automatically describe the same benchmark.
The supplied artifact also contains two specific problems in its supporting claims. With two unit-reward resources, one arrival, probabilities one half, the other seed one half, and the other edge fixed to failure, Lemma 5's conditional bound fails. Separately, the critical-threshold display omits the competing resource reward; rewards 1 and 10 with unit probabilities contradict Lemma 6 under that literal definition (pp. 9 and 14–16). These printed claims are preserved as targets and documented with numerical evidence. Neither finding is a counterexample to Theorem 1 itself.
Resources and arrivals use Fin n and Fin m for arbitrary natural sizes, including empty cases. Present edges form a subtype; absent edges are unavailable. Edge expectations are finite product-Bernoulli sums. Seed expectations are integrals over the continuous unit cube. Single-edge conditioning is the explicitly defined two-point resampling operator, including outside configurations of probability zero. Histories include offers, discards, and observed outcomes. Randomized policies use conditional distributions on finite actions, which represent arbitrary private randomness with full observable-history recall.
The path-based program is built on the published finite-LP object. Its constraints enforce realized resource capacity, arrival capacity, bounds on each variable, and invariance under flipping the variable's own edge bit. Equality uses two directed inequalities. Its optimum is a supremum over a nonempty compact feasible set. Benchmark reward sets contain zero and are bounded by the total resource reward. All integral uses in the targets involve bounded Borel functions of finitely many real seeds. No correctness or competitiveness field, assumed certificate, or equality between LP and benchmark trivializes the goal.
For the printed critical threshold, an empty competing set gives 1 and an unsolvable equation gives 0. Where zero coefficients make the root nonunique, the largest root is selected. The printed missing reward factor remains missing. Lemma 5's shorthand lambda_i denotes the arrival variable lambda_t, as its preceding display states. Independent Algorithm 2 and large-inventory results are outside this mission's scope.