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?
Almost every classical transcendence theorem is a statement about the interaction between the additive structure of and the exponential function. Hermite proved in 1873 that is transcendental, Lindemann in 1882 that is transcendental for every nonzero algebraic — hence that is transcendental and the circle cannot be squared — and Weierstrass in 1885 extended this to the linear independence of over for distinct algebraic . Gelfond and Schneider settled Hilbert's seventh problem in 1934, and Baker's 1966 theorem on linear forms in logarithms made the subject effective.
Schanuel's conjecture, formulated by Stephen Schanuel in the 1960s and first published by Lang (Introduction to Transcendental Numbers, Addison–Wesley, 1966, Chapter III), is a single statement that contains all of these as special cases, together with a large number of statements that remain open — for instance that and are algebraically independent, or that is irrational. No case of it is known beyond those already covered by the Lindemann–Weierstrass theorem or by Baker's theorem.
Timeline, with the hypotheses each result actually assumes:
Write for the complex exponential function. A tuple of complex numbers is linearly independent over when the only rationals with are ; here is viewed as a vector space over .
For a subset , let denote the subfield of generated by over . The transcendence degree is the cardinality of a transcendence basis of over : the largest number of elements of that are algebraically independent over . A number is transcendental over when no nonzero polynomial with rational coefficients vanishes at , and numbers are algebraically independent over when no nonzero polynomial in variables with rational coefficients vanishes at .
The goal fixes no numerical constant and no special shape for the : it asserts only the inequality, for every and every -linearly independent tuple. The case is vacuous and the conclusion is a bound on a cardinal, so nothing is hidden in a degenerate convention.
The milestone list consists of the landmark unconditional theorems that Schanuel's conjecture generalizes, the known function-field analogue, and one conditional corollary that records what the conjecture buys:
Schanuel's conjecture decides, in one stroke, a long list of questions that are individually open: the algebraic independence of and , the irrationality of and of , the transcendence of and , the four exponentials conjecture, and — combined with work of Macintyre and Wilkie — the decidability of the first-order theory of the real exponential field. Its restriction to algebraic is exactly the Lindemann–Weierstrass theorem, and its restriction to whose exponentials are algebraic is exactly Baker's theorem, so the conjecture is a common generalization of the two main unconditional pillars of the subject.
On the formalization side, the state of the art in Lean's mathematical library is modest relative to this history: the analytic core of the Lindemann–Weierstrass argument is present, but the Hermite–Lindemann theorem, the Lindemann–Weierstrass theorem, the transcendence of , the Gelfond–Schneider theorem, the six exponentials theorem and Baker's theorem are not available as usable statements in the pinned environment. Each milestone here is therefore a genuine formalization project with a known mathematical proof, and none of them is a restatement of an existing library result. The goal theorem itself is open mathematically; the realistic contributions to it are reductions — implications between the goal and other statements — and closing the milestones that the conjecture generalizes.
The obvious approach to any single case — build an auxiliary function with many zeros, bound its derivatives, and derive a contradiction from an integrality argument — is the method behind every result on the milestone list, and it is exactly what fails for the conjecture in general. Those proofs need the exponentials, or the arguments, to be algebraic somewhere, so that heights and denominators can be controlled; for a general -linearly independent tuple there is no arithmetic input at all, and no known construction produces the required auxiliary function. Ax's theorem shows that the differential-algebraic shadow of the statement is true, but its proof uses the derivation on the function field and has no arithmetic counterpart. A solver should not expect the conjecture itself to fall to a variation of the classical method.
All statements are over , with the complex exponential. Tuples are indexed by Fin n, ℚ-linear independence is Mathlib's LinearIndependent ℚ, transcendence degree is Mathlib's Algebra.trdeg, the generated field is IntermediateField.adjoin, and the inequality is between cardinals, so the goal reads (n : Cardinal) ≤ Algebra.trdeg ℚ (adjoin ℚ (Set.range z ∪ Set.range (Complex.exp ∘ z))). Algebraicity is IsAlgebraic ℚ, transcendence is Transcendental ℚ, and algebraic independence is AlgebraicIndependent ℚ.
There is no trivializing formalization here: the hypothesis LinearIndependent ℚ z is satisfiable for every , so the goal is not vacuous, and the conclusion is an inequality of cardinals rather than a statement about a definition introduced for this mission.
The Ax milestone is stated for formal power series in one variable over : the exponential relation is expressed as the differential equation with PowerSeries.derivative, and the conclusion bounds Algebra.trdeg ℂ of the ℂ-subalgebra generated by the and the . The conditional corollary takes the full statement of Schanuel's conjecture as an explicit hypothesis, so it is provable unconditionally as stated.
Infrastructure that a complete development needs, and that is reusable well beyond this mission: Siegel's lemma and height machinery for algebraic numbers, the standard auxiliary-function construction with derivative bounds, and interface lemmas relating Algebra.trdeg, AlgebraicIndependent and Transcendental. Reductions between the milestones — for example deriving Hermite–Lindemann from Lindemann–Weierstrass, or the six exponentials theorem from a general Baker-type statement — are welcome as sketches.
Perturbative quantum field theory produces algebraic varieties. In the parametric (Feynman–Symanzik) formulation of a momentum-space Feynman integral of a graph , the integrand is built from the Kirchhoff (first Symanzik) polynomial , and the period that the integral computes is governed by the graph hypersurface . Because has integer coefficients, is defined over , and one can ask arithmetic questions about it: how many points does it have over a finite field , is that count a polynomial in , and what is its class in the Grothendieck ring of varieties?
A separate line of work asks when a variety defined over carries an additional structure over the "field with one element" . Tits observed in 1956 that is a polynomial in whose behaviour as is governed by the symmetric group, and several inequivalent theories of -geometry have been proposed since. In the formulation of López Peña and Lorscheid, an -structure is witnessed by a torification: a decomposition of the variety into split tori inducing a bijection on -points for every field .
Bejleri and Marcolli, Quantum field theory over (Journal of Geometry and Physics, 2013, doi:10.1016/j.geomphys.2013.03.002), brought these two lines together: they asked which varieties of perturbative QFT admit an -structure, proved a blow-up formula for torified varieties, and deduced that the wonderful compactifications of graph configuration spaces and the moduli spaces are -varieties. Along the way they recorded elementary but sharp necessary conditions for an -structure, and tested them on concrete families of graph hypersurfaces. This mission formalizes that necessary-condition layer for the simplest infinite family, the banana graphs. The programme continues to be cited in the physics literature (arXiv:2401.07822).
For , the banana graph has two vertices joined by parallel edges. Its graph hypersurface is cut out by the Kirchhoff polynomial of , and is its complement.
Write for the Lefschetz class in the Grothendieck ring of varieties and set
If a variety admits a torification by tori , then its class is , so it is a polynomial in with non-negative integer coefficients; this is Lemma 3.8 of the paper. Writing , the Euler characteristic is the constant term , because positive-dimensional tori have vanishing Euler characteristic — whence the coarser necessary condition of Proposition 3.1. Non-negativity of the coefficients is therefore a necessary condition for an -structure, and one that can be checked by pure computation once the class is known.
For the banana graphs the class is known in closed form (Aluffi–Marcolli, quoted as equation (3.8) of the paper):
The first summand is , and the two quotients are exact divisions: they are the polynomials and of equations (3.9) and (3.10).
The goal is the first half of Lemma 3.9: for all , every coefficient of , as a polynomial in , is non-negative,
so that passes the necessary condition of Lemma 3.8.
The milestones are the steps the paper uses, and the contrast it draws:
Item 5 is the point of the lemma: the necessary condition separates from , so it is not vacuous on this family.
The combination " passes, fails" is the paper's concrete evidence that the torification condition is a usable filter on the varieties of perturbative QFT: it rules out an -structure on the hypersurface complements — the objects whose periods are the Feynman integrals — while leaving the hypersurfaces themselves as candidates, and it motivates the paper's Question 3.10 (whether the graph hypersurfaces satisfying the condition actually admit torifications).
What this mission produces on top of the paper is a machine-checked version of that computation. The mathematics here is not open: Lemma 3.9 is proved in the source, and the six statements of this proposal are elementary consequences of the closed formula (3.8) once the two divisions are performed. The captain has checked that all six compile and are provable in Lean 4 with Mathlib. The deliverable is therefore a formalization, not a new theorem: a reusable Lean model of Grothendieck classes in the variable for this family, with the coefficient positivity and the failure of positivity for the complement both verified, and the printed expansion for in the paper reproduced by the formalized coefficient formula.
The obstruction is bookkeeping, not depth. Equation (3.8) is a rational expression; the two fractions are exact divisions only after one knows the quotients, so a formalization has to fix polynomial representatives and prove the two division identities rather than manipulate fractions. The alternating tail has an exponent that depends on both and the summation index through a truncated natural-number subtraction, which is the main source of friction: the parity rearrangement is valid only for and has to be justified in that form. Finally the positivity argument is a case split — the coefficient at is exactly , while every other coefficient is — and the degenerate small- cases must be excluded, which is why the goal carries .
Everything is stated in , i.e. Polynomial ℤ with X playing the role of ; no Grothendieck ring, no scheme theory, and no torification is formalized. The classes of equation (3.8) are defined to be the polynomial representatives above: the mission takes the closed formula of the source as given and proves the statements about it. This is the sense in which the goal is faithful to Lemma 3.9, and it should be read that way: it is a statement about the coefficients of an explicitly given polynomial, not a proof that is or is not an -variety.
Conventions fixed in Lean: the index ranges over ℕ and all subtractions in exponents (n - 1 - j, n - 2, n - 4) are truncated natural subtraction, which is harmless under the stated hypotheses (, resp. ) but is why those hypotheses appear; coefficients are read off with Polynomial.coeff, so the goal quantifies over all , including beyond the degree, where the coefficient is . The goal is not trivially true: for the sibling statement about exhibits a coefficient equal to in the same formalism, so the ambient set-up does admit negative coefficients.
Contributions welcome: direct proofs of the six statements; and, beyond this mission, formalizations of the other necessary-condition computations of the paper (the wheel and lemon-wedge families of section 3.6, the Chern-class condition of Lemma 6.3).
A recurrent network, a nonlinear filter, a physical transducer: all are operators carrying an input signal to an output signal. Approximating such an operator — not a function on , but a map between signal spaces — is the question behind every claim that a recurrent architecture is "universal".
In 1985 Boyd and Chua gave the answer that still underpins the field. They isolated fading memory as the exact continuity notion required, and proved that a time-invariant operator with fading memory can be approximated by a finite Volterra series — uniformly over an infinite time horizon and over a noncompact set of signals. Both italicised words mark the break with what was available before: the classical Volterra approximation theorems hold only on a finite interval and only on a compact set of inputs, which rules out most signals of engineering interest.
This is the result reservoir computing inherits. Every modern universality theorem for echo state networks, state-affine systems, or linear-dynamics-plus-polynomial-readout architectures proceeds by showing the architecture realises enough of these operators, then invokes Boyd–Chua. Formalising it turns the foundation of those arguments into machine-checked mathematics.
Timeline.
Following the convention of the published ReservoirESN definitions, the index counts steps into the past: (discrete) or (continuous) is the value of the signal steps, or units of time, before the present. A sequence or function is therefore the complete history of a signal up to now. Under this convention every operator below is causal.
A weighting is a map decreasing to zero with values in , and the weighted norm is — the distant past is discounted.
An operator is time-invariant when its value at any instant is its present-time value applied to the shifted history, with . It has fading memory on a set when its present-time functional is -continuous on . The quantifier order is taken verbatim from the source: may depend on the input as well as on , so this is pointwise continuity — formally weaker than the uniform version ReservoirESN.FunctionalFMP already on the platform.
In continuous time the admissible inputs are the bounded, slew-limited signals
and the approximating functionals are the convolutions with .
Let and let be any time-invariant operator with fading memory on . Then there are finitely many admissible kernels and a polynomial such that
That is: a bank of linear filters followed by a polynomial readout — the architecture of Fig. 3 of the paper, and, recognisably, the architecture of a reservoir computer. The goal is stated in this form rather than as an explicit Volterra kernel expansion; expanding a polynomial in convolutions into Volterra kernels is a purely algebraic restatement, and formalising Volterra kernels would add bookkeeping without adding mathematical content. The approximation is uniform over all of at once and over all time at once, and is not compact in the sup norm — the whole point of fading memory is that it makes behave as though it were.
The decomposition follows the paper: the discrete-time chain first (Section VI and Appendix A2), then the two continuous-time lemmas the goal rests on (Section IV and Appendix A1).
1 — Damping, and compactness of the discrete ball. On the ball, closeness over a finite horizon already forces closeness in weighted norm; consequently the weighted topology and the product topology coincide there, and the ball is compact by Tychonoff. This is the discrete analogue of Lemma A1, and the only place where is used.
2 — Theorem 4, the discrete NLMA approximation. Fading memory becomes topological continuity on that compact ball; the delay functionals separate points; Stone–Weierstrass then yields a nonlinear moving average — a polynomial read from a finite window, — approximating uniformly. Boyd and Chua note this implies Theorem 3, the discrete finite-Volterra statement.
3 — Lemma 1: compactness in continuous time. The bounded slew-limited set is compact for the weighted norm. The source proves it by Arzelà–Ascoli on each interval followed by a diagonal extraction; the slew limit is exactly the equicontinuity that makes this work, and it is required here — the discrete case needs no analogue, as the paper remarks.
4 — Lemma 2: the convolution functionals separate points. Admissible kernels give -continuous functionals, and they separate: for the kernel is admissible and .
Goal. Stone–Weierstrass on the compact set of milestone 3 with the separating family of milestone 4, then time-invariance to transport the estimate to every instant.
The companion missions on reservoir computing have published, machine-checked, the definitions reused here — UnifBdd, WeightedBound, IsWeighting, FunctionalFMP — along with WeightedCompact.unifBdd_tendsto_subseq, a weighted sequential-compactness result for the discrete ball. Solvers can build on those rather than restate them.
Mathlib has Stone–Weierstrass in the form needed (ContinuousMap.subalgebra_topologicalClosure_eq_top_of_separatesPoints, which asks only for CompactSpace), and it has Arzelà–Ascoli in an abstract uniform-space form. What it has nothing about is fading memory, weighted norms on signal spaces, Volterra series, Laguerre systems, or moving-average operators. The work is the bridge: turning a weighted-norm continuity hypothesis into a topological statement Mathlib's Stone–Weierstrass will accept, extracting a genuine MvPolynomial from an abstract density result, and — for the goal — assembling a compactness proof in continuous time from Mathlib's Ascoli machinery.
Two modelling points are load-bearing and stated plainly rather than buried. The discrete ball must be taken in scalar (or finite-dimensional) signals: for infinite-dimensional values it is not compact and the theorem fails. And in continuous time the slew limit cannot be dropped: without equicontinuity the set is not compact in any topology that makes the convolution functionals continuous.
S. Boyd and L. O. Chua, Fading memory and the problem of approximating nonlinear operators with Volterra series, IEEE Transactions on Circuits and Systems, vol. CAS-32, no. 11, pp. 1150–1161, November 1985.
The Euclidean version of the AdS/CFT correspondence asks one to sum over all Einstein metrics filling a given conformal boundary. Making that sum meaningful requires knowing which fillings exist, how they degenerate, and what the boundary conformal class controls. A recurring hypothesis in this programme is the sign of the scalar curvature of the boundary metric: Witten (1998) pointed out that the corresponding boundary theory is unstable when that scalar curvature is negative, and Witten–Yau (1999) then proved that positive boundary scalar curvature forces the conformal boundary of a conformally compact Einstein manifold to be connected; Cai–Galloway gave a different proof that also covers the non-negative case.
M. T. Anderson's survey Geometric aspects of the AdS/CFT correspondence (arXiv:hep-th/0403087v2) gives in §4 an elementary proof of a quantitative strengthening: under positive constant boundary scalar curvature , every point of the filling lies within a fixed distance of the boundary, measured in the geodesic compactification. Connectedness of the boundary is then immediate, and the estimate additionally rules out the formation of cusps in families of such metrics. §6 of the same paper proves the Lorentzian mirror image (Proposition 6.3, also obtained independently by Andersson–Galloway): for de Sitter-type space-times with negative boundary scalar curvature, the same computation gives future incompleteness and empty future conformal infinity.
This mission formalizes the argument of §4, together with its §6 counterpart.
Let be the interior of a compact -manifold with boundary and let be a conformally compact metric on : there is a defining function for the boundary such that extends to the compactification. Fix a boundary component with induced boundary metric and take to be the associated geodesic defining function, so that .
Along the -geodesics normal to , write for the unit normal, for the second fundamental form of the level set , and for its mean curvature. The single scalar that carries the argument is
Under the curvature hypothesis with , the Riccati equation along the normal geodesics, the conformal transformation rules, the Cauchy–Schwarz inequality and the Gauss equation at the boundary combine into two facts about :
In the de Sitter setting of §6 the Raychaudhuri equation replaces the Riccati equation and the first inequality reverses.
Here is the length of the parameter interval on which the profile exists; in the geometric reading it is the -distance from a point of to , so the conclusion is exactly .
The estimate is the quantitative core behind three statements that are used repeatedly in this area: connectedness of the conformal boundary when (Witten–Yau), surjectivity of , and the exclusion of cusp degenerations in compactness theorems for the moduli space of asymptotically hyperbolic Einstein metrics — the role of the positive-scalar-curvature condition in Anderson's Theorem 3.1. In the Lorentzian case it gives future incompleteness of every timelike geodesic and .
What this mission adds is a machine-checked version of the comparison argument that produces the constant. The result is classical and has been proved several times over; none of it is formalized, and the pieces assembled here — a focusing/Riccati comparison lemma producing a sharp interval-length bound from a differential inequality — are reusable in any Bishop–Gromov or Raychaudhuri-style argument.
The analytic step is short but not automatic: from and one must first see that stays positive, then recognize that has derivative at least , and only then integrate. The naive route — trying to solve the differential inequality or to apply a Gronwall-type estimate directly — does not produce the constant , because the bound comes from the blow-up time of the comparison ODE rather than from a growth estimate. The Lorentzian case is not a formal corollary: the inequality reverses and the initial value changes sign, and the reduction has to be redone or transported through .
Mathlib has no Ricci curvature of a Riemannian manifold, so conformally compact Einstein metrics, geodesic compactifications and the Gauss equation are not available as formal objects, and formalizing them is out of scope here. Every statement in this mission is therefore about real functions of the distance parameter , with the Riemannian input carried by explicit hypotheses:
FocusingProfileAH n L φ φ' and FocusingProfileDS n L φ φ' say that is differentiable at each point of with derivative and satisfies , respectively , there;RiccatiData n L bundles the mean curvature , the squared second fundamental form , the energy term , and the Riccati equation relating them on .The conclusions bound , the squared length of the interval on which the profile is assumed to exist. Two conventions are fixed: the dimension is a natural number coerced to a real number, and is permitted, in which case the conclusion is trivially true — the substance of each statement lies in . The hypotheses are satisfiable, so no statement is vacuous; conversely, nobody should read these statements as formalizing the geometric derivation of the focusing inequality, which remains open until Mathlib has the underlying differential geometry.
Contributions that go beyond the listed targets are welcome, in particular: a general focusing/comparison lemma for ; the case of §4, where the Cheeger–Gromoll splitting theorem gives a rigidity statement instead of a bound; and any development of Riemannian curvature in Lean that would let the geometric hypotheses be discharged rather than assumed.
(The last four entries are cited as references [47], [48], [16] and [11] of Anderson's survey.)
The permanent versus determinant problem asks how large an must be for the permanent of an matrix to be written as the determinant of an matrix whose entries are affine linear functions of the input variables. Valiant showed that some finite always works and conjectured in 1979 that the least such , the determinantal complexity , grows faster than every polynomial in ; this is the algebraic counterpart of .
Geometric complexity theory (GCT), proposed by Mulmuley and Sohoni in 2001, attacks the conjecture by replacing the two polynomials with the closures of their -orbits and comparing the -representations carried by the coordinate rings of those closures. If some irreducible representation occurs in the coordinate ring of the orbit closure of the padded permanent but not in that of the determinant, then one orbit closure cannot contain the other, and a lower bound on follows. Such a representation is an occurrence obstruction, and Mulmuley and Sohoni conjectured that occurrence obstructions exist for every polynomial padding.
Timeline of what is actually proved.
Fix and write . A form of degree is a homogeneous polynomial of degree in the variables , ; the space of such forms is . The group acts on it by linear substitution of the variables, and for a form we write for the closure of its orbit in the Euclidean topology, which for these orbits agrees with the Zariski closure.
Two orbit closures matter:
where and , and the second polynomial is padded by a power of the single variable so that it, too, has degree .
The coordinate ring of a -stable subset of decomposes into irreducible polynomial representations, which are labelled by partitions with at most parts. A partition occurs in the degree part of the coordinate ring of when some polynomial function of degree on is an eigenvector of the Borel subgroup of upper triangular matrices,
and does not vanish identically on . If occurs for but not for , then , hence : this is an occurrence obstruction.
No partition can separate the two orbit closures once the padding is at least polynomial of degree ; the occurrence-obstruction route to Valiant's conjecture is therefore closed.
The milestone list follows the structure of the proof: the shape restriction for the padded permanent (Theorem 2.1), the semigroup property of occurring partitions (Lemma 2.2), the occurrence of row extended even rectangles (Proposition 2.3), the non-vanishing of highest weight vectors of long first row on (Proposition 2.4), and the fact that padded power sums lie in (Theorem 2.5), together with two elementary anchors ( is everything; a symbolic determinant of size puts the padded permanent into ) and the GCT V hardness hypothesis, which is exactly the statement that the padded permanent stays outside for subexponential .
Theorem 1.4 removes an entire proof strategy: after fifteen years in which occurrence obstructions were the main object of study in GCT, the theorem shows that they do not exist in the regime where they would be useful, so lower bounds must come from comparing multiplicities rather than mere occurrence. The supporting statements are of independent use: Theorem 2.5 and Proposition 2.3 give explicit families of points and partitions for , and the shape restriction of Theorem 2.1 constrains every future obstruction argument.
None of this is formalized anywhere. What this mission produces is a machine-checked model of orbit closures of forms, of the Borel-eigenvector description of occurrence, and of the known statements about and — infrastructure that any later multiplicity-based argument would reuse. The goal theorem is proved in the literature; the work here is formalizing that proof. The hardness hypothesis and the Mulmuley–Sohoni conjecture itself remain open, and are labelled as such.
The naive approach to "λ occurs in " is to decompose the plethysm and read off multiplicities; this fails because the coordinate ring of is a quotient of that plethysm by the unknown vanishing ideal of the orbit closure, and almost nothing is known about which highest weight vectors survive restriction. The proof of Theorem 1.4 works instead with explicit highest weight vectors evaluated at explicit points of (padded power sums), using the fundamental invariant of and a lifting map for highest weight vectors in plethysms; the combinatorics of tableaux and the case distinction on the degree are where the work lies. A formalization additionally has to build the representation-theoretic vocabulary from scratch, since Mathlib has neither plethysms, nor Weyl modules, nor highest weight theory for .
Conventions fixed by the Lean development, all in the namespace GCTOcc:
Infrastructure a complete development needs, and which is reusable beyond this mission: plethysms and their highest weight vectors, the fundamental invariant of a form space, semistandard tableaux of rectangular content, and basic facts about orbit closures of forms. Contributions of any of these pieces are welcome, as are counterexample-hunting reports on the elementary anchors.
Not covered here: the Kronecker-coefficient strand of the program (Ikenmeyer–Mulmuley–Walter 2017 on -hardness of Kronecker positivity, and the construction of vanishing triples in the Kronecker cone). Stating those results requires irreducible characters of the symmetric group indexed by partitions, or equivalently symmetric-function machinery, which Mathlib does not yet have; they are natural targets for a companion mission once Specht modules exist.
In 1964 A. N. Sarkovskii proved a theorem about continuous maps of the real line that is remarkable both for how little it assumes — continuity, nothing more — and for how much it concludes: the set of periods of the periodic orbits of such a map is completely constrained by a single linear ordering of the positive integers. Its best-known corollary, rediscovered by Li and Yorke in 1975 under the slogan period three implies chaos, says that a continuous map of with an orbit of period three has orbits of every period.
Devaney presents the theorem in §1.10 of An Introduction to Chaotic Dynamical Systems (2nd edition, Westview Press, 2003), calling it the chapter's first major theorem, and gives the elementary proof of Block, Guckenheimer, Misiurewicz and Young based on interval covering relations. This mission is the second in a series formalizing the book; it is independent of the first, sharing only the book-wide namespace.
Timeline: Sarkovskii (1964) proved the full ordering theorem, in Ukrainian, and it went largely unnoticed in the West; Li and Yorke (1975) independently proved the period-three case and gave the field the word "chaos"; Štefan (1977) and Block–Guckenheimer–Misiurewicz–Young (1980) gave the short interval-covering proofs, the latter being the one Devaney reproduces.
Let be continuous. A point has prime period if and for every .
The Sarkovskii ordering of the positive integers is
first the odd numbers greater than one in increasing order, then times the odds, then times the odds, and so on; the powers of two come last, in decreasing order. Writing and with odd, holds exactly when either and precedes lexicographically, or and , or and .
Two elementary facts drive the proof. If is a closed interval with , then has a fixed point in ; and if closed intervals satisfy for , then some point of has for all . One writes , " covers ", for .
The goal is Devaney's Theorem 10.2: for continuous ,
The milestones are the steps of the book's proof: the two covering observations, the period-three special case (Theorem 10.1), the odd case, the power-of-two case and the mixed case into which the general theorem is decomposed, the remark that a period which is not a power of two forces infinitely many periodic points, and the converse direction, witnessed by the piecewise-linear map with a period-five orbit and no period-three orbit.
Sarkovskii's theorem is the sharpest general statement known about the period structure of one-dimensional dynamics, and it is sharp in both directions: the ordering is realized, so no stronger implication holds. Its first consequence — only powers of two can occur as the set of periods of a map with finitely many periodic points — is what makes the period-doubling cascade the canonical route to chaos, a theme the book returns to in §1.17.
The theorem is emphatically one-dimensional: it fails on the circle, where a rotation by has every point of period three and no other period.
Formalizing it contributes a reusable Lean treatment of interval covering relations and of the Sarkovskii ordering itself; we are not aware of these in Mathlib at the pinned revision, and the covering machinery is exactly what §1.13 and §1.16 of the book reuse.
The period-three case is a short argument once the covering observations are available, and it is a reasonable first milestone. The general theorem is not: the odd case requires choosing the right interval on the orbit, building the increasing family of unions of covered intervals, and showing that the shortest return loop has length exactly — a combinatorial argument on the cyclic order of the orbit that is easy to draw and tedious to formalize. Attempts to shortcut the ordering with a naive induction on fail: the statement for genuinely depends on the geometric arrangement of the orbit points.
The read-backs attached to every draft item in this proposal are not independent. They were written by the same agent that drafted the Lean statements, not by a separate auditor working blind from the code alone. They are included because they are still useful as a line-by-line rendering of each statement, but they are not independent testimony: any misreading baked into a formalization is likely repeated in its read-back, and agreement between the two should not be taken as confirmation of faithfulness. Each read-back repeats this warning in its own first paragraph. Reviewers who want independent testimony should commission fresh, blind read-backs.
Every definition and statement in this proposal was compiled locally against this mission's
environment (Lean 4.33.1, Mathlib 0df444a360eaa60ab8c11dca51a86af692955474): all files
elaborate with no errors, the only warnings being the expected sorry placeholders in the
theorem bodies.
The word chaos entered mathematics with a precise meaning, and Robert L. Devaney's An Introduction to Chaotic Dynamical Systems (2nd edition, Westview Press, 2003) is the text that fixed the meaning now used in most of the literature: a map is chaotic when it is unpredictable (sensitive dependence on initial conditions), indecomposable (topological transitivity), and nevertheless regular (dense periodic points). The book develops this definition on the simplest possible object — the real quadratic family on the unit interval — and shows that for large the map is chaotic on an invariant Cantor set, by exhibiting an exact symbolic model for it.
This mission is the first of a planned series formalizing the book. It covers §1.5–§1.8: the invariant set of the quadratic family, symbolic dynamics on the sequence space , topological conjugacy, and Devaney's definition of chaos. Everything later in the book — Sarkovskii's theorem, the horseshoe, hyperbolic toral automorphisms, Julia sets — is written in the vocabulary fixed here, so a faithful Lean version of this chapter fixes the vocabulary of the whole series.
Write and let for a real parameter . Iterates are written , with the identity.
For the maximum value of exceeds , so some points of leave after one iteration. Let
so that is the set of points escaping from at the -st iteration. The set of points that never escape is
The complement consists of two closed intervals, to the left of the midpoint and to its right.
On the symbolic side, is the set of one-sided infinite sequences with , metrized by
and is the shift map . The itinerary of is the sequence with when and when .
Following Devaney, is topologically transitive if for every pair of open sets meeting there is with ; it has sensitive dependence on initial conditions if there is such that every point of has points of arbitrarily near it whose orbit eventually separates from its own by more than ; and it is chaotic on when it has sensitive dependence, is topologically transitive, and has a dense set of periodic points in .
The goal is Devaney's Example 8.8: for ,
The milestones are the results the book uses to get there, in the book's own order: the escape of orbits outside (Proposition 5.2), the tame regime (Proposition 5.3), the Cantor structure of (Theorem 5.6), the metric and dynamics of the shift (Propositions 6.3, 6.5, 6.6), the itinerary conjugacy (Theorems 7.2, 7.3), its dynamical consequences (Theorem 7.5), sensitive dependence (Example 8.3), and the chaos of on all of (Example 8.9).
The theorem is the prototype for every later "chaos via symbolic dynamics" argument: the horseshoe, hyperbolic toral automorphisms, and the quadratic Julia sets are all proved chaotic by producing a conjugacy with a shift. The conjugacy also gives quantitative information that is otherwise inaccessible — for example, that has exactly points fixed by , which no direct computation with the degree- polynomial delivers.
Formalizing it produces reusable Lean infrastructure that Mathlib currently lacks: Devaney's three chaos conditions, the sequence space with its metric and shift, topological conjugacy of maps on subsets, and the notion of a Cantor subset of the interval. These are the foundation the rest of the book's series will import.
The obvious route to the goal — analyze on directly — fails, because has no explicit description: it is a nested intersection of intervals whose endpoints are not available in closed form. The whole argument therefore goes through the itinerary map, and its two hard steps are: (i) surjectivity of the itinerary map, which needs the nested-interval construction together with the fact that these intervals are nonempty and nested; and (ii) injectivity, which needs the hyperbolicity estimate on , valid exactly because , and the mean value theorem. The hypothesis is not cosmetic: Devaney notes the results hold for , but only with a more delicate argument.
The Lean development fixes the following conventions.
Set.ncard and are restricted to ; for every point is fixed by and the
claim would be false.Contributions of any kind are welcome: full proofs, reductions splitting a milestone into lemmas, and reusable lemmas about or about conjugacy that later missions in the series can import.
The read-backs attached to every draft item in this proposal are not independent. They were written by the same agent that drafted the Lean statements, not by a separate auditor working blind from the code alone. They are included because they are still useful as a line-by-line rendering of each statement, but they are not independent testimony: any misreading baked into a formalization is likely repeated in its read-back, and agreement between the two should not be taken as confirmation of faithfulness. Each read-back repeats this warning in its own first paragraph. Reviewers who want independent testimony should commission fresh, blind read-backs.
Every definition and statement in this proposal was compiled locally against this mission's
environment (Lean 4.33.1, Mathlib 0df444a360eaa60ab8c11dca51a86af692955474): all files
elaborate with no errors, the only warnings being the expected sorry placeholders in the
theorem bodies.
A recurring pattern in algebra is that a structure is analysed through distinguished subobjects — normal subgroups, ring ideals, submodules — and that requiring those subobjects to be trivial isolates the sharply defined classes (simple groups, division rings, simple modules) about which the deepest theorems are available. The manuscript Ideals in Balanced Algebras and the Genesis of Mathematics (A. Winkler, 2020) applies that pattern to a single primitive: a partial binary operation, an operation that need not be defined for every pair. Under one axiom — balance, which asserts that is defined exactly when is — several families of ideals appear automatically, and declaring each of them trivial (empty, or the whole algebra) carves out semigroups, monoids, quivers, associations, societies, categories, groupoids, groups and rings in turn.
No individual argument here is deep. What makes them worth machine-checking is that their content is definedness rather than equality: a statement such as "the gregarious elements form an ideal" is a claim about which products exist, proved by repeatedly moving brackets across a product that may fail to be defined at any step. Such arguments are easy to state loosely, and easy to get wrong by one implicit existence assumption. They are also the base layer on which the rest of the manuscript's programme rests. This mission formalizes that base layer: §1 (algebras, ideals, units), §2 (quivers), §4 (associators and associations), §4.1 (principal ideals) and §4.2 (the gregarious ideal).
An algebra on a type is a partial binary operation: a rule assigning to some pairs a value . Write for " is defined". In the Lean development the operation is a total function , where the value means undefined. Nothing else is assumed: no totality, no unit, no associativity.
The vocabulary used throughout, all relative to this one partial product:
This is the statement that gives the manuscript its notion of society: the gregarious elements of an association form the gregarious ideal, and an association whose gregarious ideal is everything is a society. The goal fixes no cardinality, no units and no totality, so it survives every specialization the manuscript makes afterwards.
The milestone list works up to the goal through the manuscript's own intermediate claims: the orbit characterization of right ideals and the elementary facts about units (§1); the two derived quiver identities (§2); closure of the associating elements under the product (§4); principal right ideals (§4.1); gregariousness of sinks and sources, and the two one-sided closure statements for gregarious associating elements (§4.2); and the cancellation facts (§4) whose content is that the non-left-cancellable elements form a prime left ideal.
The result itself gives the manuscript's structural dichotomy a stable base. Once the gregarious elements are known to form an ideal, "society" is a triviality condition on an ideal rather than an ad hoc axiom, and the same is true of quivered (the elements admitting a unit on one side form an ideal, §1), of cancellative (the non-cancellable elements form a prime ideal, §4) and of principal (§4.1). The chain of specializations the manuscript then runs — association, society, quivered society, category, groupoid, group, ring — inherits whatever is proved here.
What this mission adds on top of the manuscript is machine-checked bookkeeping for partial operations. The arguments in the source are written in prose, with the existence of intermediate products often left implicit; formalizing them fixes exactly which existence facts each step consumes. The definitions published with this mission (partial algebra, ideal, balance, associating, gregarious, unit, source, sink, cancellable) are reusable for any later formalization of partial magmas, and nothing equivalent is currently in Mathlib, whose Magma-style structures are total and whose Quiver/Category hierarchy starts from typed hom-families rather than a single partial product.
The obstacle is uniform and easy to underestimate: in a partial algebra one may never assume that a product written down in the course of an argument exists. The naive proof of the goal — "rebracket and apply gregariousness of " — fails at its first step, because from alone one cannot conclude ; that inference is exactly what the hypothesis " is associating" supplies, and it must be invoked explicitly. Gregariousness then returns a disjunction whose two branches produce products on opposite sides of the bracket, so each branch has to be transported back independently, consuming a further associating hypothesis. Counting these obligations correctly, rather than inventing new mathematics, is the work.
The partial product is A → A → Option A; none is undefined, and a · b = c is rendered as the product evaluating to some c. Subsets are Set A, with no decidability or finiteness assumptions. Ideals are arbitrary subsets and are allowed to be empty — deliberately, since the manuscript's dichotomy turns on an ideal being empty or being everything. Statements quantify over an arbitrary type, including the empty type, where they hold vacuously.
Left/right duality is not obtained from a formal opposite-algebra construction: the dual statements are stated and are to be proved separately (for instance the two one-sided society closure milestones). A contributor who prefers to build the opposite algebra once and derive each dual from its mirror is welcome to; that construction is not part of the published definitions.
The statements are not vacuous: every hypothesis used is satisfiable, since any total associative operation makes all elements associating and gregarious, and the trivial one-element monoid satisfies every unit, source, sink and cancellation hypothesis appearing in the list. No milestone is stated under a hypothesis that cannot be met.
In Esquisse d'un Programme (1984), Alexandre Grothendieck describes a discovery that reorganised his mathematical interests: a finite oriented combinatorial map drawn on a surface — a dessin d'enfant, a child's drawing — determines canonically a smooth projective algebraic curve together with a map to the projective line ramified only above , and , and that curve and map are defined over the field of algebraic numbers (Esquisse, §3, pp. 14–16 of the French text). Consequently the absolute Galois group acts on these purely combinatorial objects; in the spherical case, where the structural map is a rational function , the action of is obtained simply by applying to the coefficients of and . Grothendieck states in §2 (p. 9) that the resulting outer action of on the profinite fundamental group of is faithful, and in §3 that the theorem of Belyi, announced at the 1978 Helsinki congress, is what makes the dictionary between combinatorics and arithmetic exact.
Timeline of the results this mission formalizes. Belyi (1979, On Galois extensions of a maximal cyclotomic field, Izv. Akad. Nauk SSSR) proved that a smooth projective curve over is defined over a number field if and only if it admits a map to unramified outside ; the "only if" half is an explicit construction with polynomials over . Grothendieck (1984) drew the consequence that acts on dessins and asserted faithfulness of the action on . Lenstra, in an appendix to L. Schneps (ed.), The Grothendieck Theory of Dessins d'Enfants (LMS Lecture Notes 200, CUP 1994), showed that the action is already faithful on the much smaller class of plane trees, equivalently on Shabat polynomials. That tree-level statement is the goal of this mission, because it is the sharpest form of faithfulness that can be stated without first building the theory of étale fundamental groups.
Work over , realized as the algebraic closure of , and write for its group of field automorphisms fixing pointwise.
A nonconstant polynomial over a field is a Belyi polynomial (classically a Shabat polynomial) when every critical value of lies in : for every with one has or . Over an algebraically closed field of characteristic zero this says exactly that , viewed as a degree- map , is unramified outside the fibres over , and . The associated dessin is the preimage , a plane tree with edges whose vertices are the points above and , with vertex orders equal to the multiplicities of the corresponding roots of and of .
Two Belyi polynomials define the same dessin exactly when they are affinely equivalent: for some and some . The target coordinate is already rigidified by the normalisation of the critical values to ; only the source coordinate remains free.
The group acts coefficientwise: is the polynomial obtained from by applying to each coefficient. This is exactly the action described in §3 of the Esquisse. It sends Belyi polynomials to Belyi polynomials, and it descends to an action on affine equivalence classes, i.e. on dessins.
Equivalently: no nontrivial element of the absolute Galois group fixes every plane tree. This is the weakest stable form of the faithfulness assertion in the Esquisse: it fixes no degree, no genus and no tree, asserting only that some dessin is moved.
The result itself. Faithfulness turns the combinatorics of finite maps into a faithful representation of : every nontrivial automorphism of is detected by a finite tree, so invariants of dessins (degree, valency lists, monodromy group, field of moduli) are in principle a complete set of tools for distinguishing Galois elements. It is also the entry point to the anabelian programme described in §3 of the Esquisse, since the same statement expresses that embeds into the outer automorphism group of .
Formalizing it. Belyi's theorem and the faithfulness of the Galois action on trees are both established results. Mathlib at the environment revision of this mission contains no declaration mentioning Belyi maps or dessins d'enfants, and no étale fundamental group, so both statements have to be built from the polynomial and Galois-theoretic libraries. What this mission produces is a formal version of the combinatorial half of the dictionary, in a form that avoids scheme theory entirely: everything is phrased with polynomials over and , so the development rests only on Mathlib's existing polynomial, field theory and Galois theory libraries.
The naive attack on the goal — exhibit one tree and one Galois element moving it — does not scale: the statement quantifies over all , and has no accessible presentation. The real work is the separation statement, which demands, for an arbitrary algebraic number , a tree whose isomorphism class remembers ; the construction must control both the existence of a Belyi polynomial with prescribed arithmetic and the rigidity that makes affine equivalence classes finite. Belyi's theorem in polynomial form is itself an induction on the degree of the field of definition of the critical values, and each step changes the polynomial, so bookkeeping of critical values through composition is the bulk of the formal proof. The descent statement over is not a formal manipulation either: it needs the finiteness of the set of Belyi polynomials of a given degree up to affine equivalence, which is where the combinatorial classification enters.
Conventions fixed in the Lean development, and not to be re-litigated by solvers:
AlgebraicClosure ℚ, and is its group of -algebra automorphisms.Trivialization is ruled out as follows: the goal asserts the existence of a moved Belyi polynomial for each nontrivial , with the nondegeneracy 0 < deg P built into the definition, so no constant or empty witness satisfies it, and no hypothesis of the goal is vacuous ( is satisfiable).
A complete development needs: critical values and their behaviour under composition of polynomials; the classification of Belyi polynomials of fixed degree up to affine equivalence; Galois descent for a finite set of polynomials stable under conjugation; and, for the descent target, the identification of the coefficients of a Belyi polynomial over as algebraic numbers. All of these are reusable outside this mission. Contributions of general polynomial-ramification infrastructure are welcome, as are alternative formalizations of the same statements over a general algebraically closed field of characteristic zero.
The Riemann hypothesis asserts that every non-trivial zero of the Riemann zeta function lies on the line ; the simplicity hypothesis asserts in addition that every such zero is a simple zero of . Both are statements about the location and the order of a discrete set of points in the complex plane, and almost every reformulation of them stays inside analytic number theory.
Kawahira (2016) gives a reformulation of a different kind. He attaches to an explicit meromorphic self-map of the Riemann sphere and shows that the Riemann hypothesis together with the simplicity hypothesis is equivalent to a statement about the local dynamics of that map: it has no attracting fixed point. The translation is elementary once the right object is in place — the holomorphic index (residue fixed point index) of a fixed point — and it turns a question about zeros into a question about stability. This mission formalizes that translation, together with the supporting propositions on indices and multipliers that make it work.
For a non-constant meromorphic , define the nu function
If is a zero of of order , then is a fixed point of with multiplier
and if is a pole of order the multiplier is . A fixed point of a holomorphic map is attracting if , indifferent if , and repelling if .
The holomorphic index of at a fixed point is
the integral being over a small positively oriented circle around . When the multiplier is not one has , and the Möbius map carries the unit disk onto the half-plane . So a fixed point is attracting, indifferent or repelling exactly according to whether is , or : the critical line reappears, in the index plane.
The point of the construction is that is engineered so that the index of at a simple zero of is itself (and at a zero of order ). Writing for : a non-trivial zero of order has index , so , and asking that this equal is asking for and .
The milestones are the paper's Propositions 3, 4, 5, 7, 8, 9, its Theorem 11 (the variant for the Riemann xi function ), and Proposition 13 of the appendix (the Newton map , for which every zero of becomes an attracting fixed point — the contrast that explains why , and not , sees the critical line).
The equivalence converts the simultaneous truth of the Riemann and simplicity hypotheses into the non-existence of an attracting fixed point of one explicitly given meromorphic function. Nothing in the translation is conjectural: the content is the index computation, the symmetry of the non-trivial zeros supplied by the functional equation, and the classification of fixed points by the real part of the index. What a formalization adds is a machine-checked statement of the dictionary, and a reusable Lean development of the holomorphic index, which Mathlib does not currently contain — the index, its relation to the multiplier, and its behaviour at zeros and poles are general facts of one-variable complex dynamics, independent of this application.
Status, precisely: the Riemann hypothesis is open, and this mission does not ask anyone to settle it. Every target here is a theorem with a published proof; the work is to formalize those proofs. The goal theorem is an equivalence between two open statements, so it is provable without deciding either side.
The obvious route to the goal — compute at a zero, apply the classification, done — fails in one direction. From "no attracting fixed point" one gets for each non-trivial zero of order , which alone excludes neither a multiple zero nor a zero to the left of the critical line. The functional equation must be used to pair with , whose index is ; only the two inequalities together force and . A complete Lean proof therefore needs, besides the local computation: that the non-trivial zeros lie in the open strip , that and are zeros of the same order, and that the trivial zeros and the pole at give repelling fixed points.
The index milestone (Proposition 3) is a residue computation on a small circle, and the hypotheses have to be arranged so that has exactly one zero inside; the other genuinely analytic milestone is the order- computation of , where vanishes at the fixed point when and the singularity is removable rather than absent.
The development is over with Mathlib's riemannZeta. Conventions the Lean statements commit to:
Nothing here is vacuous: the goal is an equivalence of two statements each of which is satisfiable in form, and the guards exclude only points at which the Lean encoding of is known not to model the meromorphic map.
Reusable beyond this mission: the holomorphic index, the multiplier classification, the general nu-function and Newton-map computations at a zero of order — all stated for an arbitrary function analytic at the point, not for .
https://math.stackexchange.com/questions/4244874/can-we-prove-am-gm-inequality-using-these-integrals
In the Feynman path-integral approach to a non-abelian gauge theory one wants to integrate a gauge-invariant weight over the space of vector potentials (connections) of a principal bundle. The integrand is constant on the orbits of the group of gauge transformations, so the integral over diverges and one is supposed to integrate instead over the orbit space . The Faddeev–Popov procedure realizes this by fixing a gauge: choosing, continuously in the orbit, exactly one vector potential on each orbit, and correcting by a Jacobian determinant.
V. N. Gribov (SLAC Translation 176, 1977) observed that for potentials on (or ) with suitable conditions at infinity, the Coulomb gauge condition does not do this: the Coulomb slice through the zero potential meets the orbit of the zero potential again, far from the origin. These extra intersections are the Gribov copies; R. Jackiw, I. Muzinich and C. Rebbi (Phys. Rev. D 17 (1978) 1576) analyzed them in detail.
I. M. Singer, Some Remarks on the Gribov Ambiguity (Commun. Math. Phys. 60 (1978) 7–12), showed that the phenomenon is not a defect of the Coulomb gauge. If the conditions at infinity are those of Gribov — gauge transformations extending to the one-point compactification with value at infinity, so that the base manifold is or — then no continuous gauge fixing exists at all, in any gauge. The obstruction is topological: the space of irreducible connections is weakly contractible, while the gauge group is not, and a weakly contractible principal bundle admits no global continuous section.
Fix and take the structure group , the group of complex matrices with and , topologized as a subspace of matrices. Let denote the unit sphere of , with base point the north pole.
For the trivial -bundle over a space , a gauge transformation is a map , and the gauge group is
continuous maps with pointwise multiplication and the compact-open topology. Two subobjects matter. The based gauge group is the subgroup of transformations that are the identity at the base point. The constant transformations with value in the centre of form a normal subgroup, and the reduced gauge group is the quotient
with the quotient topology. The centre acts trivially on vector potentials, so is the group that acts effectively.
A group acting continuously on a space has orbit space with the quotient topology, and a gauge fixing is a continuous map with , where is the projection: a continuous choice of exactly one point on each orbit. The action is principal when it is free and the division map, which sends a pair of points on one orbit to a group element carrying the second to the first, can be chosen continuously; this is the topological content of " is a principal -bundle". The space is weakly contractible when it is nonempty and all its homotopy groups vanish.
In the paper, is the affine space of connections, its set of irreducible members, and Theorems 1 and 2 say exactly that is a weakly contractible principal -space.
For , , and every weakly contractible principal -space :
By Theorems 1 and 2 of the paper the space of irreducible connections over or is such an , so the goal contains Singer's Corollary 4 for that space; it leaves the analytic construction of the space of connections unfixed, which is what makes it statable today.
The result rules out the existence of a global gauge in the topological sense: every gauge condition used in practice is at best a local slice, and the Faddeev–Popov construction has to be read as a local statement, patched with a partition of unity over the orbit space (as the last section of the paper proposes). It is the mathematical reason why the Gribov ambiguity cannot be repaired by a cleverer gauge condition, and it is the origin of the Gribov–Zwanziger restriction of the functional integral to a fundamental domain.
Formalizing it adds a machine-checked version of an argument that is quoted far more often than it is checked, and it forces into Lean a piece of infrastructure that Mathlib currently lacks: homotopy groups of mapping spaces, the long exact sequence of a fibration in the form needed for , and the classical computations , for , . Singer's results are proved mathematics; none of them is formalized, and Mathlib as of the pinned revision contains homotopy groups as a definition together with their group structure, but essentially no computation of them.
The naive approach to the goal — build a section by hand, or average over the group — fails because is neither compact nor contractible and the obstruction is global: locally, slices do exist (that is the content of the generalized Coulomb gauge), so no local argument can produce a contradiction. The proof has to convert a section into a homotopy-theoretic statement: a section of a principal bundle trivializes it, exhibiting the group as a retract of the total space, so all homotopy groups of the group would vanish; the work is then to show that some homotopy group of the reduced gauge group does not vanish, which needs the identification of the based gauge group with a mapping space, the exact sequences relating , and , and non-trivial homotopy groups of — including for the case of Theorem 3.
The formalization commits to the following conventions, all of them visible in the definitions of this mission.
HomotopyGroup, based at the identity element.The Hodge conjecture predicts that on a non-singular complex projective variety every rational cohomology class of type is a rational linear combination of the classes of algebraic subvarieties of . Abelian varieties are the oldest testing ground for the conjecture, and the hardest known classes on them were isolated by A. Weil. A -dimensional complex abelian variety is of Weil type for an imaginary quadratic field if embeds into in such a way that both eigenspaces of meet in an -dimensional subspace. Such an carries a distinguished two-dimensional space of rational -classes, the Weil classes, which for a generic of Weil type does not lie in the subring generated by divisor classes. Weil classes are therefore the standard obstruction to the Hodge conjecture in low dimension: for abelian fourfolds the conjecture reduces to their algebraicity.
Timeline of the unconditional results on algebraicity of Weil classes:
Fix and present a -dimensional complex torus by its first homology: a complex structure on with , the lattice being . A polarization is a rational alternating form on satisfying the Riemann relations and for . Cohomology is , realized as the alternating -multilinear forms on ; a class is rational if its values on rational vectors are rational, and it has type if it is multiplied by under the scaling action of . A Hodge class of degree is a rational class of type .
Let and with . A polarized abelian -fold of Weil type is such an together with a rational endomorphism of with
the last condition saying that multiplies the polarization class by the norm , and such that each of the two eigenspaces of meets the -eigenspace of in an -dimensional subspace. The Hodge–Weil classes are the rational classes in
equivalently the rational degree- classes that vanish on every tuple of vectors containing both a vector of and a vector of .
The form is -valued and hermitian on , viewed as a -vector space through . The determinant of its Gram matrix in a -basis lies in , and its class in is the discriminant of . Discriminant means that this determinant equals for some rationals not both zero.
Algebraicity is not modelled abstractly. An abelian variety is tied to a genuine non-singular projective variety by a projective realization: a smooth, -periodic immersion , surjective onto and injective modulo the lattice, whose differential intertwines with the complex structure of . A class is algebraic when some de Rham class of whose periods over the -cycles swept out by rational vectors equal is a rational combination of cycle classes of irreducible subvarieties of dimension . Cycle classes, de Rham cohomology of a projective variety, -types and Hodge classes are taken from the platform's HodgeConjecture bundle, which formalizes §1 of Deligne's Clay problem description.
The statement fixes neither the field nor the sixfold: it quantifies over every , every polarized abelian sixfold of Weil type of discriminant , and every projective realization of it.
for every imaginary quadratic and every discriminant; this is the use made of Schoen's Proposition 10 (Compositio Math. 114 (1998)) in the paper.
Divisor classes: every Hodge class in of a non-singular projective variety is algebraic. This is an already published platform statement, imported here as a reference, since the reduction in Corollary 1.6.1 uses the algebraicity of divisor classes.
Weil classes are, by the results of Moonen–Zarhin (Duke Math. J. 77 (1995), Math. Ann. 315 (1999)), the only obstruction left in dimension four: for a simple abelian fourfold is spanned by quadratic expressions in divisor classes and by Weil classes, and the non-simple cases reduce to products treated by Ramón Marí (Collect. Math. 59 (2008)) and Moonen–Zarhin. The goal theorem therefore closes the Hodge conjecture for abelian fourfolds, the first dimension in which the conjecture for abelian varieties was open.
Formalizing it produces, first, a reusable Lean model of polarized abelian varieties, of complex multiplication of Weil type, of the Hodge–Weil plane and of the discriminant, tied to an honest notion of algebraic cohomology class through projective realizations. None of these objects exists in Mathlib today. The result itself is proved in the source preprint and has no machine-checked proof; the milestones below are equally unformalized, including the classical statements of Weil and Schoen that the paper's Corollary depends on.
The naive attack — write down subvarieties whose classes span — fails because Weil classes are not expressible through divisors: for a generic abelian variety of Weil type the Néron–Severi group is cyclic while is three-dimensional, so no product of divisor classes reaches the Weil plane. The source constructs instead a reflexive sheaf on , for the Jacobian of a genus- curve, whose characteristic class remains of Hodge type along all deformations of as a polarized abelian sixfold of Weil type, and deforms the pair over that moduli space using a semiregularity theorem for twisted sheaves. Each of these steps — Orlov's derived equivalence, spinor geometry of the Mukai lattice, semiregularity — is itself missing from Mathlib, which is why the milestone list stays on the Hodge-theoretic side of the argument rather than transcribing the sheaf-theoretic core.
Conventions the Lean development commits to:
A complete development needs, beyond what is drafted here: the spin representation of the Mukai lattice of an abelian -fold, pure spinors and -secant lines, Orlov's equivalence, Atiyah classes and semiregularity for twisted sheaves. Contributions establishing any of these, or proving the Hodge-theoretic milestones, are welcome.
Almost every classical question about prime values of polynomials is a special case of one statement. Are there infinitely many twin primes? Infinitely many primes of the form ? Infinitely many Sophie Germain primes with prime? Each asks whether a fixed finite list of integer polynomials takes prime values simultaneously infinitely often. Schinzel's Hypothesis H (A. Schinzel and W. Sierpiński, 1958) is the single conjecture that predicts "yes" in all these cases, subject to the two obvious obstructions: a polynomial that factors cannot be prime infinitely often, and neither can a family whose product is always divisible by some fixed prime.
Timeline.
Hypothesis H itself remains open in every case that is not covered by Dirichlet's theorem.
Work in the ring of polynomials with integer coefficients. Fix a finite set of polynomials , each subject to the Bunyakovsky condition:
Irreducibility in is strictly stronger than irreducibility in : it also forces the content of to be , ruling out .
Even an irreducible family can be blocked by congruences. The polynomial is irreducible with positive leading coefficient, yet is even for every integer , so it is prime only when it equals . The family therefore also has to satisfy the Schinzel condition: for every prime there exists an integer with
Equivalently, no prime is a fixed divisor of the product . A family satisfying both conditions is called admissible.
For an admissible family , write
The goal of the mission is Hypothesis H:
The milestones are, in order: the linear one-polynomial case (Dirichlet); the reduction of the Schinzel condition to the finitely many primes ; the necessity of the Schinzel condition; and three specializations of the goal — Bunyakovsky's conjecture, the twin prime conjecture, and Landau's problem on — each stated as an implication from the goal statement, so that they can be proved before the goal itself is.
The result itself. Hypothesis H implies the twin prime conjecture, the Sophie Germain prime conjecture, Landau's conjecture that is prime infinitely often, the infinitude of primes in every admissible constellation, and Dickson's conjecture; with Bateman–Horn it also predicts the density of such . Nothing beyond the degree-one case is known, and the conjecture is the standard yardstick against which sieve-theoretic progress on prime values of polynomials is measured.
Formalizing it. The goal is open, so the mission's deliverable is not a proof of it but a formal, audited statement of it together with a supporting environment: the admissibility predicates, the classical reductions, and machine-checked derivations of the famous corollaries from the goal. Dirichlet's theorem on primes in arithmetic progressions is already formalized in Mathlib, so the linear milestone is a matter of connecting that result to this mission's formulation rather than of new mathematics. The three "H implies …" milestones are provable now, unconditionally, because they are implications; they are also the sharpest available check that the goal statement has been formalized faithfully, since a mis-stated goal will usually fail to yield twin primes.
The obvious first idea — sieve the values for and count survivors — is exactly the idea that fails. Sieve methods lose a constant factor (the parity problem): they can show that has few prime factors infinitely often, but they cannot distinguish "one prime factor" from "two", which is why Iwaniec's result stops at . The analytic input that works for degree one — the nonvanishing of Dirichlet -functions on — has no known analogue for a polynomial of degree , because the relevant counting problem is not governed by characters of a finite abelian group. Milestones 1–3 are elementary or already available in Mathlib; the goal itself is not expected to be resolved here.
Conventions fixed by the Lean development, and deliberately so:
The statement admits no trivializing reading: the hypotheses are satisfiable (for example and are admissible, as milestones 5 and 6 require one to verify), so the goal is not vacuous, and the conclusion asserts infinitude rather than the existence of a single .
A complete development needs the admissibility predicates (supplied as the mission's definition bundle), Mathlib's polynomial and modular-arithmetic APIs for the fixed-divisor arguments, and Mathlib's Dirichlet theorem for milestone 1. The definition bundle and milestones 2–3 are reusable for any future mission on Bateman–Horn, Dickson's conjecture, or prime constellations. Contributions of further conditional consequences of the goal (Sophie Germain primes, prime -tuples, cousin primes) are welcome as additions to the tree.
Continuity is the hypothesis under which limits may be moved inside a function, and Chapter 4 of Walter Rudin's Principles of Mathematical Analysis (3rd edition, McGraw-Hill, 1976) is about what continuity gives once the domain is compact or connected. Three of its theorems are used in nearly every later argument of the book: a continuous function on a compact set has compact image (Theorem 4.14), hence attains its bounds (4.16); a continuous function on a connected set has connected image (4.22), hence takes intermediate values (4.23); and a continuous function on a compact metric space is uniformly continuous (Theorem 4.19) — the can be chosen independently of the point.
The last of these is the chapter's capstone. Uniform continuity is exactly what is needed to prove that continuous functions are Riemann-integrable (Chapter 6), and it is the first place where compactness upgrades a pointwise hypothesis into a global one with a quantitative conclusion.
This mission is the fourth in a series formalizing Rudin Chapters 1–11; it uses the metric topology of Mission II and is a prerequisite for Missions V–VII.
Let be metric spaces, , , and let be a limit point of . Rudin writes when for every there is with for all satisfying ; the exclusion of is deliberate, and it is what makes the notion agree with continuity only when (Theorem 4.6). is continuous at if the same holds with the condition dropped, and continuous if it is continuous at every point.
is uniformly continuous on if for every there is a single such that for all with . A real function on is monotonically increasing if implies ; its one-sided limits are written and , and it has a discontinuity of the first kind at when both exist but do not agree with .
Uniform continuity is the hypothesis that converts local approximation into global approximation with a uniform error bound. In Chapter 6 it is what makes the upper and lower Riemann–Stieltjes sums of a continuous function come together; in Chapter 7 it underlies the equicontinuity of Arzelà–Ascoli; in Chapter 9 it appears again in the estimate of a mapping on a compact ball. The extreme value theorem and the intermediate value theorem are the two existence theorems of elementary analysis, and both come from this chapter by combining Chapter 2's compactness and connectedness with continuity.
Theorem 4.30 — a monotone function has at most countably many discontinuities — is the result that makes monotone integrators well behaved in Chapter 6, and it is the first place in the book where a countability argument (Chapter 2) pays off analytically.
Mathlib has continuity, compactness and connectedness in general topological spaces, and most
of the milestones can be matched to library results after the statements are put in Rudin's
metric form. The formalization value is again in the dictionary: Rudin's punctured-limit
definition versus ContinuousWithinAt, and his – uniform continuity versus
the library's uniformity-filter definition.
There is no single hard step; the difficulty is in the hypotheses being weaker than they look. In Theorem 4.6 the limit is taken through , so the equivalence with continuity genuinely needs and a limit point; dropping the second hypothesis makes the statement false at isolated points. In Theorem 4.19 the naive proof — pick at each point by continuity and take the infimum — fails because the infimum over infinitely many points can be ; compactness is used to reduce to finitely many, and the factor of two in the radii of the covering balls is essential. Theorem 4.30 requires an injection from the discontinuity set into , built from the gap between and .
Conventions fixed by this mission:
Continuous, ContinuousOn, ContinuousWithinAt; Rudin's
along is Filter.Tendsto f (𝓝[E \ {p}] p) (𝓝 q).Rudin.UniformlyContinuous, stated with explicit and
as in Definition 4.18, rather than through the uniformity filter.Rudin.IsLimitPoint from the Chapter 2 mission, so the two missions share
one notion.[CompactSpace X], matching
Rudin's phrase "compact metric space"; 4.14 is stated for a compact subset instead, which is
the form later missions use.MonotoneOn f (Set.Ioo a b); one-sided limits are 𝓝[<] x and
𝓝[>] x filters, and 4.29 also identifies them with the supremum and infimum of the
corresponding one-sided images, as Rudin does.The goal is not vacuous and does not follow by unfolding: uniform continuity fails for continuous functions on non-compact domains (e.g. on , or on ), so compactness is doing the work.
Von Neumann introduced amenability in 1929 in response to the Banach–Tarski paradox: a group is amenable when it carries a finitely additive, translation-invariant probability measure on its subsets, and no amenable group contains a free subgroup of rank — which is exactly what the paradox needs. The converse is the von Neumann conjecture, and it is false: Ol'shanskii in 1980 and Adyan in 1982 produced finitely generated counterexamples. A finitely presented counterexample was harder, and one candidate stood out — Richard Thompson's group , finitely presented, with nobody able to decide whether it was amenable.
Brin and Squier attacked it and in 1985 got what they called "half a success": they proved that , and more generally the group of piecewise-linear homeomorphisms of the line with finitely many breakpoints, contains no free subgroup of rank greater than . Whether is amenable they could not determine, and it is still open today; claimed proofs have appeared in both directions and none has been accepted. Finitely presented counterexamples were eventually found by other routes (Ol'shanskii–Sapir 2002; Lodha–Moore 2016), so is no longer needed as a candidate. This mission formalizes the half that was settled.
Let be the group of orientation-preserving homeomorphisms of the line: the strictly increasing bijections under composition. The support of is the set of points it moves, , an open subset of .
A continuous is piecewise linear when there is a discrete set of breakpoints with differentiable off and constant on each component of ; for finite this is the same as being affine on a neighbourhood of every point outside . Nothing is required at the points of , so the two affine pieces meeting at a breakpoint may disagree — that is what makes such an more than an affine map. Write for the piecewise-linear elements of and
for the subgroup this mission is about. The distinction matters: the goal below holds in and fails in , where Brin and Squier build free subgroups of rank by lifting them from the circle. Write for the commutator subgroup, which Brin and Squier identify as the elements whose slope at each end is — an element has slope at an end when it agrees with a single affine map of slope on a ray out to that end. Thompson's group — the piecewise-linear homeomorphisms of with dyadic breakpoints and power-of-two slopes — is realized inside .
Since a free group of rank greater than contains one of rank , this is Brin and Squier's Theorem (3.1).
Their Theorem (3.2), with the conclusion weakened to what the goal consumes. What they prove is infinite rank, which needs the general form of their Lemma (1.2); that general Lemma and the full-strength (3.2) are milestones of their own here. The goal itself only ever uses the rank-two form.
Thirteen are numbered results of theirs: the support observations (1.1a), (1.1b); Lemma (1.2) in its rank-two case and in its general form; Lemmas (3.4) and (3.5), already formalized and published, entering as references; the commutator facts (2.14a), (2.14b), (2.14c); Theorem (3.2) both as the rank-two dichotomy the goal consumes and at full strength; and Corollary (3.3), likewise in both strengths. Five are piecewise-linear infrastructure the source treats as routine: closure of under composition and under inverse, the same two for slope at each end, and finiteness of the number of components of a support. Five more are steps the source asserts without proof — that the line carries no non-fixed periodic points, that a map fixing a set's complement preserves its components, that the iterated images of a pushed-forward interval are pairwise disjoint, that the closure of a commutator's moved set stays inside the union of the two supports (p. 495), and that the derived subgroup of a free group of rank two is non-abelian (p. 494). The last is not from the source at all — that an abelian subgroup of a free group is cyclic, which is what lets the goal finish through Nielsen–Schreier.
The theorem closes the standard route to proving a group non-amenable. To show a group amenable the classical routes are elementary amenability and subexponential growth, and is neither elementary amenable (Cannon–Floyd–Parry, Theorem 4.10) nor of subexponential growth, having exponential growth (their Corollary 4.7). To show a group non-amenable the standard route is to exhibit a free subgroup of rank — the route this theorem closes. sits in the gap, which is why its status has survived sustained attention.
The result reaches past . Monod's groups of piecewise projective homeomorphisms are counterexamples to von Neumann's conjecture, and Monod's theorem that they contain no non-abelian free subgroup is, in Monod's words, "a sequacious generalization of the corresponding theorem of Brin–Squier about piecewise affine transformations"; of its own proof that paper says it will "largely follow [Brin–Squier, § 3]".
What formalizing it adds. Mathlib has no piecewise-linear maps and no amenability predicate for groups. This mission builds the piecewise-linear layer: a workable , its closure properties, and the structure of supports.
The obstruction is bookkeeping across two finiteness facts of different kinds. Finiteness of the breakpoint set is what gives an element slopes at at all, and what makes two elements affine on each side of a common fixed point. Compactness is the other — throughout, — and it splits: that the closure of is compact needs only slope at each end, with no piecewise linearity at all, which is why (2.14b) is formalized under a weaker hypothesis than the source's; that the closure stays inside is what reaches back to finiteness. Keeping straight which fact does which job is most of the work.
The first idea a newcomer has about (3.2) is the wrong one. Its proof produces a family of commuting elements, and it is not disjointness of supports that makes them commute: only their intersections with one chosen component are disjoint, and commutation is deduced instead from a minimality argument. A proof routed through disjoint supports will not close.
What the Lean fixes. Elements are order isomorphisms of — strictly increasing
bijections, automatically homeomorphisms — rather than a homeomorphism type. Composition follows
Mathlib's convention , the opposite of the source's right action, so the
conjugation identity reads here;
getting this backwards states a different theorem that still compiles. A support is the bare
moved set, with no closure taken. Piecewise linearity is a finite breakpoint set together with
local affineness off it — the set need not be minimal and may be empty.
A copy of is an injectivity statement about , not a subgroup
isomorphism, and the goal is about a single pair rather than a subgroup. The dichotomy
hypothesises slope at both ends directly, not membership in a derived subgroup — that these
coincide is the source's result, and both inclusions are formalized here: (2.14a) gives one, and
the identification asserted on p. 493 gives the other.
Beyond a workable , the development needs Nielsen–Schreier, already
in Mathlib as subgroupIsFreeOfIsFree: it is what lets an abelian subgroup of a free group be
cyclic, and so lets the goal finish without the source's metabelian ending. That ending is
formalized too, as Corollary (3.3) together with the p. 494 remark that the derived subgroup of a
free group of rank two is non-abelian; the goal simply does not route through it.
One trivializing reading is ruled out. Slope at both ends is not a compact-support condition — every translation satisfies it — so (3.2) is not secretly a statement about compactly supported maps.
Nothing is built for specifically, and amenability is not touched. That is the one piece deliberately omitted, and contributions are welcome on it: modelling and embedding it in . The piecewise-linear layer is reusable beyond this theorem — Thompson's groups and , and piecewise-linear topology generally, need exactly it.
Several equations of mathematical physics are written down formally but have no classical meaning as stated. The dynamical model on the three-dimensional torus, the KPZ equation , and the parabolic Anderson model all require multiplying a distribution of negative regularity by itself, an operation that Schwartz distribution theory does not provide. Martin Hairer's A theory of regularity structures (Invent. Math. 198 (2014) 269–504, arXiv:1303.5113) develops a calculus in which such products, and the resulting fixed-point problems, become well posed.
The line of work leading to it is short and well documented: rough path theory (Lyons, 1998) solved the analogous problem for controlled ordinary differential equations driven by irregular signals; Gubinelli's controlled paths (2004) and branched rough paths (2010) reorganised it around local expansions; Hairer's theory extends that idea from paths to fields on with anisotropic (e.g. parabolic) scaling. Paracontrolled distributions (Gubinelli–Imkeller–Perkowski, 2015) give an alternative route to some of the same equations. The algebraic and probabilistic infrastructure around regularity structures has since been systematised (Bruned–Hairer–Zambotti, 2019; Chandra–Hairer, 2016), but the analytic core is still the 2014 paper.
Fix a dimension and a scaling of positive integers, with , and put . For , a point and a test function , the rescaled test function is
Write for the set of test functions supported in whose derivatives up to order are bounded by . For , a distribution belongs to the Hölder–Besov space if, on every compact set , uniformly over , and with .
A regularity structure consists of an index set containing , bounded below and locally finite; a graded vector space with spanned by a unit ; and a group of linear operators on with for , and . Elements of are "homogeneous of order ": they are placeholders for objects whose size at scale is .
A model assigns to each point a linear map and to each pair an element , subject to , , and, locally uniformly, the analytic bounds
A modelled distribution of order is a function such that on every compact
the space of these is , and if takes values in a sector , that is, a graded -invariant subspace vanishing in degrees below its regularity.
With and the order attached to , for every with there is a unique distribution with
The statement asserts only the shape of the estimate — a constant per compact set — and so is insensitive to any later sharpening of constants.
The uniqueness clause of Theorem 3.10 in isolation; the existence of a linear reconstruction operator for arbitrary (for the bound no longer pins it down); Corollary 3.16, improving the regularity of to when takes values in a sector of regularity ; Proposition 3.31, that for the action of on is determined by and by in lower homogeneities; and Theorem 4.7, that the truncated pointwise product of and lies in with .
The reconstruction theorem is what turns a book-keeping device into analysis: it says that a coherent family of local expansions, indexed by base point, glues to a single genuine distribution, with an error controlled by the order of the expansion. Every subsequent operation in the theory — multiplication (Theorem 4.7), composition with smooth functions (Theorem 4.16), the multi-level Schauder estimate (Theorem 5.12), and the fixed-point theorem for singular SPDEs (Theorem 7.8) — is stated and used through it. Without it, the abstract spaces carry no information about actual distributions.
Regularity structures are not currently available in Mathlib, and neither are the anisotropic Hölder–Besov spaces that the theory is phrased in. The result itself is proved in the literature; the work this mission asks for is a machine-checked proof of the known argument, together with the reusable definitions it needs. The formal development is a prerequisite for anything downstream — Schauder estimates, the fixed-point theory, or the and PAM convergence results of §10 — which are natural follow-on missions rather than part of this one.
The naive construction fails: setting for a fixed is wrong away from , and the pointwise limit of localisations of around each does not obviously exist, because the objects being glued are distributions of negative order, not functions, so there is no value to take and no partition-of-unity argument that respects the scaling. Hairer's proof goes through a wavelet multiresolution analysis adapted to the scaling : one defines the candidate on each dyadic level by pairing with wavelets centred at grid points, and shows the resulting sequence is Cauchy using the bound level by level. A formalization therefore needs either a scaled wavelet basis with Daubechies-type regularity (Theorem 3.17 in the paper) or a substitute for it; this, and the uniform-in-scale bookkeeping, is where the effort lies. Uniqueness for is by contrast short, and is listed as a separate milestone.
The development commits to the following conventions, fixed in the mission's definition files. Points of are Fin d → ℝ. Test functions are smooth and compactly supported, forming a submodule of all real-valued functions, and a distribution is a linear functional on that submodule; the pairing is extended by to non-test functions, and a lemma in the definition file certifies that rescaling maps test functions to test functions, so no statement is vacuous for that reason. Hairer's consists of functions; here it consists of smooth ones, which defines the same spaces . The model space is the algebraic direct sum over the index set, each a real normed space, with the corresponding projection; the structure group is a subgroup of the linear automorphisms of that direct sum. Sectors are families of subspaces ; Hairer's requirement that each admit a complement is automatic in this algebraic setting. The integer appearing in the model bounds is the smallest one with for all , which is part of the definition of a model rather than a free parameter. All statements quantify over an arbitrary regularity structure, an arbitrary model, and an arbitrary compact set, so they are not satisfiable by a degenerate choice; the goal in particular claims existence, membership in , and uniqueness simultaneously.
Infrastructure that a complete proof will need, and which is reusable beyond this mission: scaled wavelet bases on , the elementary theory of (including the positive-regularity case), and basic operations on compactly supported test functions under anisotropic rescaling. Contributions of any of these as separate lemmas are welcome, as are reductions that decompose the goal into wavelet-level estimates.
Chapter 3 of Walter Rudin's Principles of Mathematical Analysis (3rd edition, McGraw-Hill, 1976) develops the theory of convergence for sequences and series of numbers: subsequential limits and upper limits, the Cauchy criterion, the comparison, root and ratio tests, power series, summation by parts, and products of series. Its final section answers a question that distinguishes analysis from algebra: an infinite sum is not a sum. For a series that converges only conditionally, the value of the sum depends on the order of the terms, and Riemann's rearrangement theorem (Theorem 3.54) makes the dependence total — by reordering the terms one can prescribe any pair of limit inferior and limit superior for the partial sums, including divergence to .
This mission is the third in a series formalizing Rudin Chapters 1–11. It uses the real and complex number systems of Mission I and the compactness results of Mission II, and it supplies the convergence machinery used by Missions VII and VIII.
A series is the sequence of partial sums ; the series converges to when , and converges absolutely when converges. The upper limit of a real sequence is , taken in the extended real number system , and a subsequential limit is a limit of a subsequence there. A rearrangement of is a series with a bijection of the index set onto itself.
The distinction that drives the chapter: for real or complex terms, absolute convergence is equivalent to convergence of for every , to the same sum (Theorem 3.55), whereas mere convergence is not.
Let be a series of real numbers which converges but not absolutely, and let . Then there is a rearrangement with partial sums such that
The rearrangement theorem is the precise statement of why conditional convergence must be handled with care, and it is the reason later chapters insist on uniform or absolute hypotheses before interchanging limit operations: Theorem 3.50 (Mertens) needs absolute convergence of one factor, and the Fourier and Lebesgue theories of Chapters 8 and 11 are built on and convergence rather than pointwise summation. The supporting milestones are the standard convergence tests, which are used constantly in the rest of the book, and the characterization of , which is the tool that makes the root test and the radius of convergence formula precise.
Mathlib's Summable/HasSum express unconditional summability, which over and
is equivalent to absolute convergence. The conditionally convergent series that
this chapter is about are therefore invisible to that API, and the mission works with partial
sums directly. Some of the classical tests exist in Mathlib in Summable form and will need
restating; the rearrangement theorem itself has to be built.
The goal theorem is a construction, not an estimate: one splits into its positive and negative parts , observes that and both diverge while , and then alternately draws blocks of positive and negative terms to overshoot targets and undershoot targets . Formalizing the alternating greedy construction requires defining the permutation recursively together with the invariant that every index is eventually used — the bookkeeping, not the analysis, is the hard part. The endpoint cases or must be carried through the same construction rather than treated separately.
Conventions fixed by this mission:
Rudin.SeriesConvergesTo / Rudin.SeriesConverges, defined through
Rudin.partialSum a n = ∑_{i<n} a i. Absolute convergence is Rudin.SeriesConvergesAbsolutely.
Mathlib's Summable is deliberately not used, since it would collapse the distinction the
chapter is about.EReal via Filter.limsup/Filter.liminf, so
are allowed as values of and in the goal.Equiv.Perm ℕ, and the rearranged series is fun k => a (σ k).α‖z‖ < 1 and α‖z‖ > 1 rather than
‖z‖ < 1/α, to avoid inversion in EReal.The goal is not vacuous: conditionally convergent series exist (the alternating harmonic series), so the hypotheses are satisfiable, and the conclusion fixes both limit points exactly rather than merely bounding them.
Convergence, continuity and integration are all statements about nearness, and Chapter 2 of Walter Rudin's Principles of Mathematical Analysis (3rd edition, McGraw-Hill, 1976) isolates the amount of structure needed to talk about nearness: a metric. The chapter's payoff is a single theorem, Heine–Borel (Theorem 2.41), which says that in — and, as the chapter's examples show, only in spaces resembling it — three very different-looking finiteness conditions coincide: being closed and bounded, admitting finite subcovers, and forcing every infinite subset to accumulate. Nearly every existence theorem in the rest of the book (a continuous function on attains its maximum, is uniformly continuous, is Riemann-integrable) is an application of that equivalence.
This mission is the second in a series formalizing Rudin Chapters 1–11. It builds on the number systems of Mission I and supplies the topological input for Missions III–VII.
A metric space is a set with a distance that is positive for distinct points, symmetric, and satisfies the triangle inequality. The neighbourhood is the set of with . A point is a limit point of if every neighbourhood of contains a point of different from ; is closed if it contains all its limit points, open if each of its points has a neighbourhood inside , and its closure is together with its limit points. is perfect if it is closed and every point of is a limit point of , and bounded if it is contained in some neighbourhood.
An open cover of is a family of open sets whose union contains ; is compact if every open cover of has a finite subcover. A -cell is a product . Two sets are separated if , and is connected if it is not the union of two nonempty separated sets.
For , the following are equivalent:
Heine–Borel is the bridge between the order completeness of established in Chapter 1 and the analytic theorems of Chapters 3–7: the bisection argument that proves -cells compact is the same argument that produces convergent subsequences (Bolzano–Weierstrass, Theorem 2.42), and compactness is what converts local information into global statements. Theorem 2.43 supplies the standard source of uncountable sets of measure zero — the Cantor set is the running example — which matters again in Chapter 11. Theorem 2.47, characterizing the connected subsets of the line as the order-convex ones, is the topological content of the intermediate value theorem proved in Chapter 4.
Mathlib has an extensive metric-space and compactness library, so much of this chapter exists
there in some form. What this mission adds is the explicit correspondence with Rudin's
formulations: his open-cover definition of compactness against the library's filter-based
IsCompact (a milestone in its own right), his -style limit points against
closure, and his -cells against the library's boxes. The resulting dictionary is what the
remaining missions in the series use when they need a compactness argument.
The mathematics is standard, and the difficulty is almost entirely in the translation layer.
Two places bite. First, Rudin's compactness quantifies over arbitrary open covers, so the
statement is a -type over families of sets, while Mathlib's IsCompact is a statement
about filters; the equivalence is available in the library but only after the cover is
presented in the right indexed form. Second, "limit point" in Rudin's sense is not
p ∈ closure E: the point must be approached by points of other than , so isolated
points of are excluded, and statements such as 2.27(a) and 2.41(c) are false if the two
notions are conflated.
Conventions fixed by this mission:
[MetricSpace X]; IsOpen, IsClosed, closure, Perfect,
IsCompact, Bornology.IsBounded and IsPreconnected are used for Rudin's corresponding
notions.Rudin.IsLimitPoint p E, defined with the explicit
and the condition , and his open-cover compactness is Rudin.IsCoverCompact.Rudin.kCell k a b inside EuclideanSpace ℝ (Fin k); the case where some
gives the empty set, which is why the nested-cell milestone assumes each cell is
nonempty, exactly as Rudin's construction does.IsPreconnected, which admits the empty set, matching Rudin's convention
that a set is connected unless it splits into two nonempty separated pieces.TFAE list in Rudin's order (a), (b), (c).The equivalence is not vacuous: all three conditions are satisfied by any -cell and all three fail for itself when .
Every course in analysis begins by fixing what a real number is, because the theorems that follow — the intermediate value theorem, the convergence of monotone bounded sequences, the compactness of closed bounded intervals — are false over the rationals and true over the reals for exactly one reason: the least-upper-bound property. Walter Rudin opens Principles of Mathematical Analysis (3rd edition, McGraw-Hill, 1976) with this point. His Example 1.1 exhibits the gap concretely: the set of rationals with has no least upper bound in . Chapter 1 then constructs an ordered field in which no such gap occurs, and derives from that single axiom the archimedean property, the density of , and the existence of -th roots.
This mission is the first in a series formalizing Rudin Chapters 1–11. It covers the chapter's number-system foundations: the ordering axioms, the real field, the complex field, and euclidean space .
An ordered set is a set with a transitive relation such that for exactly one of , , holds. If and there is with for all , then is bounded above and is an upper bound. A least upper bound (supremum) of is an upper bound such that no is an upper bound. The ordered set has the least-upper-bound property if every nonempty that is bounded above has a least upper bound in .
An ordered field is a field carrying an order such that whenever , and whenever and . Rudin's Theorem 1.19 asserts that an ordered field with the least-upper-bound property exists and contains as a subfield; the members of are the real numbers. The complex field is the set of ordered pairs of reals with the usual operations, written , with ; euclidean -space is the set of -tuples with the inner product and norm .
Existence of such a field is witnessed in Lean by itself; what carries the content of Rudin's theorem, and what the goal asks for, is that the least-upper-bound property pins the field down up to a unique isomorphism of ordered fields. Uniqueness of also gives Rudin's second assertion for free: any embedding of is the canonical one, so contains as an ordered subfield.
The least-upper-bound property is the only non-algebraic input to the whole of single-variable analysis, and the chapter shows how much follows from it alone: the archimedean property, which rules out infinitesimals; the density of , which makes approximation arguments possible; and the existence of -th roots, which repairs precisely the defect exhibited by . The uniqueness statement is what licenses the common practice of treating "the" real numbers as a single object regardless of the construction used (Dedekind cuts, as in Rudin's appendix, or Cauchy sequences).
Mathlib already contains , , and a uniqueness theorem for conditionally complete linearly ordered fields, and several of the milestones are available there in some form. The work this mission asks for is therefore bridging work: stating Rudin's hypotheses in his own terms — an order with the least-upper-bound property as a hypothesis on a set, not as a typeclass whose data includes a chosen supremum operator — and deriving the standard library form from them. That bridge is what later missions in the series reuse.
The individual statements are elementary, and the mathematical difficulty is genuinely low;
what makes the chapter non-mechanical in a proof assistant is the mismatch between hypothesis
and structure. Mathlib's completeness is packaged as ConditionallyCompleteLinearOrder, a
structure carrying sSup and sInf as data; Rudin's is a proposition about an arbitrary
ordered field. Turning the proposition into the structure (in order to invoke the library's
uniqueness theorem) is the one step where the obvious "just apply the Mathlib lemma" move does
not typecheck.
Conventions fixed by this mission:
Rudin.HasLeastUpperBoundProperty, using
Mathlib's IsLUB, BddAbove, lowerBounds; no completeness typeclass is assumed of K.[Field K] [LinearOrder K] [IsStrictOrderedRing K], which is exactly
Rudin's Definition 1.17.≃+*o (OrderRingIso), so "unique isomorphism"
is stated as ∃ e, ∀ e', e' = e.ℂ and is the norm ‖z‖; euclidean -space is
EuclideanSpace ℝ (Fin k) with the inner product inner ℝ x y, so Rudin's
facts are norm and inner-product inequalities.Nothing here is vacuous: the goal quantifies over an arbitrary ordered field satisfying the
property, and ℝ itself is such a field, so the hypothesis is satisfiable and the conclusion
is not automatic.
This mission asks how restrictions on collinear and cocircular points limit the reuse of distances in the plane. Its central question is Erdős Problem 98: must the minimum number of distances grow faster than the number of points?
For each positive integer n, let h(n) be the minimum number of distinct positive Euclidean distances determined by an n-point set in the plane with no three collinear points and no four cocircular points. Write D(P) for the number of distinct positive Euclidean distances determined by P.
The mission is to establish a superlinear lower bound, or determine this extremal function exactly. The superlinear target is Erdős Problem 98:
Concretely, for every real A > 0, prove that there is an integer n_A such that every general-position configuration P with |P| = n >= n_A satisfies D(P) > A n. A fixed improvement of the coefficient 1/3, or an additive sublinear improvement above n/3, does not complete this objective.
The alternative completion target is an exact determination of h(n), proved by a universal lower bound and general-position constructions attaining that bound. State the range of n explicitly. An asymptotic estimate or a counterexample to superlinearity alone must be labeled with its actual scope; neither is an exact determination of h(n).
A circle centred at a point of P contains at most three other points of P, so D(P) >= (n-1)/3. The following improvements are kernel-checked in Lean 4:
Esgk.numDistances_gt_one_third_add_refined in this mission, with its
corollary
Esgk.eventually_numDistances_gt_linear_of_le_refined.Esgk.numDistances_gt_one_third_add_kappa_image_gap. It is not yet a
record on this platform.So every fixed A <= 1/3 + 1/40 is settled: such a configuration with D(P) <= A n has fewer than 10^4 points. These are supporting results, not the mission's terminal goal. For large n the additive term c n^(1/4) is smaller than the linear gains; the n^(1/5) and n^(1/6) additive targets and their milestones remain supporting results. Resolving the superlinear target would establish a lower bound above every fixed linear coefficient. Determining h(n) exactly would settle the corresponding extremal problem with matching constructions.
Configurations are finite subsets of the Euclidean plane. In the indexed
formalization, a configuration is an injective map p : Fin n → ℝ²; write
P = image(p) before using D(P). Both general-position
hypotheses apply to the image. D(P) counts distinct positive distance values,
not pairs or ordered multiplicities. The superlinear quantifier ranges over
every real A > 0 and every sufficiently large general-position configuration.
The superlinear target and exact-determination target remain open here. Distinguish conjectures, conditional reductions, audited prose proofs, and kernel-checked Lean results. A completed supporting formalization does not by itself complete this mission.
Before a mechanism can pay anyone, it must decide something — and the impossibility theorems of social choice say that deciding honestly is already hard. Arrow's theorem (1951) showed that any method of aggregating individual rankings into a social ranking that respects unanimity and independence of irrelevant alternatives must be a dictatorship; Gibbard (1973) and Satterthwaite (1975) showed the voting analogue: any non-dictatorial voting rule onto three or more candidates can be strategically manipulated. These two results frame all of mechanism design — they are the reason Chapter 9 of Nisan–Roughgarden–Tardos–Vazirani (eds.), Algorithmic Game Theory (Cambridge, 2007), this mission's source, introduces money and quasilinear utilities immediately after proving them: without transfers, incentive compatibility is an impossibility, not a design constraint.
A timeline: Arrow proved the aggregation impossibility in his 1951 monograph Social Choice and Individual Values; Gibbard (1973) established the manipulability of non-dictatorial voting schemes via game forms, Satterthwaite (1975) independently via a direct argument; the derivation of Gibbard–Satterthwaite as a corollary of Arrow's theorem, which the book follows and this mission adopts as its attack path, is standard since the 1970s.
Fix a finite set of alternatives (candidates) and a finite set of voters. A preference is a strict total order on ; we write the relation as , read " is strictly preferred to " (the book writes ). A preference profile assigns a preference to each voter. A social welfare function maps profiles to a social preference; a social choice function maps profiles to a single chosen alternative (Definition 9.1).
The properties at stake (Definitions 9.2, 9.4, 9.5, 9.7):
with no cardinality or finiteness assumptions: the two properties are quantifier-for-quantifier the same data viewed twice.
These are the two foundational impossibility theorems of social choice, and the pivot of the whole mechanism-design part of this series: the VCG mission that follows exists because Gibbard–Satterthwaite closes the door on non-trivial strategyproof choice without money. The chapter derives Gibbard–Satterthwaite from Arrow through the top-set extension (Definition 9.9, Lemmas 9.10–9.11), so a solver of the capstone gets Arrow as a stepping stone, not a detour.
Formalizing them produces the platform's first social-choice library: preference profiles as strict total orders, the aggregation vocabulary, and the impossibility pair. Arrow's theorem has been formalized before in other proof assistants (Nipkow's Isabelle formalization, 2009; a Mizar formalization by Wiedijk), which is evidence the statement shapes here are the standard ones — but no Lean 4/mathlib formalization exists, and none on this platform.
The proofs are short on paper and famously slippery in the details. Arrow's proof (the book gives Geanakoplos's pairwise-neutrality route) is a sequence of profile surgeries: each step swaps one voter's ranking of a pair and tracks the social outcome through IIA; the formal cost is constructing the intermediate profiles and proving they remain strict total orders — pure bookkeeping, but a lot of it. The hybrid-profile argument needs, over three or more alternatives, custom orders placing chosen pairs at chosen positions; building these on an abstract finite type is where most of the work lies. For the capstone, the book's route through the top-set extension (move to the top, Definition 9.9) requires proving the extension is again a strict total order (Lemma 9.10) and inherits unanimity, IIA, and non-dictatorship (Lemma 9.11); a solver may equally take any direct proof of Gibbard–Satterthwaite — the statement fixes no route. Proposition 9.6 is a genuine warm-up: unfolding both definitions and rearranging quantifiers.
Preferences are relations A → A → Prop carrying IsStrictTotalOrder; r a b means " is strictly preferred to ", the reverse of the book's — every definition's docstring states this orientation. Aggregators are total functions on all relation-valued profiles; every property quantifies only over genuine preference profiles, so behavior on invalid inputs is irrelevant, and nothing can be smuggled through junk inputs. Unanimity is the book's identical-profile form (Definition 9.2), which together with IIA yields the pairwise form used in proofs. Both alternatives and voters are finite types; |A| ≥ 3 enters as 2 < Fintype.card A. Arrow's theorem carries Nonempty ι, matching the book's setting of voters; it is not needed for truth — with zero voters the identical-profile unanimity is already unsatisfiable over three or more alternatives, so that case is vacuous either way. Gibbard–Satterthwaite deliberately omits it: with zero voters ontoness onto three alternatives is unsatisfiable, and the statement holds vacuously. Dictatorship for choice functions is Definition 9.7 exactly: whenever some alternative is the dictator's unique maximum, it is elected.
Equilibrium concepts are static; play is dynamic. The bridge between the two is regret minimization: simple adaptive rules that, against arbitrary — even adversarial — opponents, perform nearly as well as the best fixed alternative in hindsight. The subject begins with Hannan (1957) and Blackwell (1956), whose consistency theorems predate most of computational learning theory; the modern multiplicative-weights style bounds are due to Littlestone–Warmuth (1994) and Freund–Schapire (1997); the reduction from external to swap regret, and with it the algorithmic route to correlated equilibria, is Blum–Mansour (2005), following Foster–Vohra (1997) and Hart–Mas-Colell (2000). Chapter 4 of Nisan–Roughgarden–Tardos–Vazirani (eds.), Algorithmic Game Theory (Cambridge, 2007), written by Blum and Mansour, is the source text of this mission.
The punchline of the chapter, and of this mission, is that a computationally trivial form of rationality — each player privately running a no-swap-regret algorithm — drives the empirical play of any finite game into an approximate correlated equilibrium (Aumann, 1974). No coordination, no knowledge of the game, no fixed-point computation: the equilibrium concept that Chapter 1 of the series defines through a correlating device is reached by decentralized learning.
The online model (§4.2): there are actions. At each time an online algorithm selects a distribution over actions, as a function of the loss vectors observed so far; then the adversary reveals a loss vector and the algorithm suffers . Cumulatively, and for a fixed action . The external regret of is . A modification rule rewires the algorithm's play, giving the modified loss ; the swap regret is over all rules.
A finite game (the vocabulary of Mission I of this series, in loss form): players , finite action sets , cost functions . A joint distribution on action vectors is an -correlated equilibrium (Definition 4.11) if for every player and every switching rule ,
An online algorithm with vanishing per-round swap regret, with the constant the chapter's own route produces.
A player with external regret over rounds has average loss at most , where is the game value — no-regret play guarantees the minimax value against any opponent.
Any algorithm with external regret on all -loss sequences yields one with swap regret .
If every player's swap regret over steps of mixed play is at most , the empirical joint distribution is an -correlated equilibrium.
Every deterministic algorithm has a -loss sequence forcing loss while some action loses at most : randomization is necessary, not a convenience.
Correlated equilibrium is the equilibrium concept with a defensible dynamic foundation: Nash equilibria are PPAD-hard to find, but the capstone plus Theorem 4.12 exhibit polynomial-time decentralized dynamics whose empirical play is an -correlated equilibrium after rounds. Later missions in this series lean on this machinery: the price-of-anarchy chapters bound the cost of no-regret play (not just of exact equilibria), and the routing-game chapter uses precisely the convergence result formalized here.
Formalizing it produces the platform's first online-learning library: the adversarial protocol, regret in both external and swap forms, the multiplicative-weights analysis, and correlated equilibria. The regret vocabulary is directly reusable for the bandit-flavored missions already on the platform. All results are classical, with textbook proofs; the work requested is machine-checked proof, not new mathematics.
The Polynomial Weights bound is a potential-function argument: the total weight falls geometrically with the algorithm's loss and is bounded below by the weight of action ; the formal work is inequalities for on and careful bookkeeping of the recursion. The reduction (Theorem 4.15) is the structurally interesting step: the master algorithm runs copies of the external-regret procedure, feeds copy the true losses scaled by the master's own probability , and — the crux — plays the stationary distribution of the column-stochastic matrix assembled from the copies' outputs. Existence of that fixed point is exactly the existence of a stationary distribution of a finite Markov chain, available on this platform as the goal of Markov Chains and Mixing Times I — or provable directly. Theorem 4.12 is an averaging argument, deliberately easy; Theorem 4.3 is an adversary construction; Theorem 4.9 combines the regret bound with the security level the minimax theorem of Mission I supplies, through the opponent's empirical mixture. The capstone is the composition of 4.6 (tuned at ) with 4.15, plus the arithmetic that turns into the stated bound.
An online algorithm is a deterministic function from the observed history (the list of past loss vectors) to the mixed action played next — the standard formal reading of the full-information model; randomization lives in the mixed action, and losses are expected losses. Boundedness of losses () is a hypothesis on theorems, never part of a definition. The Polynomial Weights algorithm is defined concretely by its weight recursion, and its learning rate carries the hypothesis : the book writes only , but at the bound's term degenerates and the claim is false, so positivity is explicit. Action sets are Fin (n+1), keeping them nonempty. The number of steps is a known parameter (the book's convention; guess-and-double is out of scope). Correlated equilibria use the switching-rule form of Definition 4.11, over the game vocabulary (IsLottery, IsMixedProfile, profileProb) published with Mission I of this series. In Theorem 4.12 the empirical distribution is the average of product distributions of the played profiles, is required (at there is no empirical distribution), and costs are not assumed bounded — the averaging is scale-free.
Trivializing readings are ruled out: the existential algorithms in Theorem 4.15 and the capstone are quantified before the loss sequence and the modification rule, so a witness must work uniformly against every adversary — nothing may be chosen with hindsight.
A unit fraction is the reciprocal of a positive integer. The Erdős–Straus conjecture asks whether the particularly simple rational number always admits an expansion with three such terms. Its difficulty lies in obtaining a fixed number of terms for every denominator: general algorithms for Egyptian fractions do not give this three-term guarantee.
The conjecture is open. This mission adopts the exact statement maintained as Erdős Problem 242. It aims to formalize established reductions and provide a precise frontier for further work; it does not present a proof of the universal conjecture.
The historical formulations vary. Erdős’s 1950 paper, pp. 193–195, discusses distinct unit fractions and attributes the conjecture jointly to himself and Straus. His 1961 problem I.32, p. 238, allows positive denominators without specifying distinctness, while the 1979 statement, problem 9, p. 70, explicitly orders distinct denominators. The earliest published discussion may be Obláth’s 1950 paper, submitted in 1948; it attributes the question to Erdős, as explained by Bloom–Elsholtz, pp. 238–239.
The main developments relevant here are:
For a natural number , write for the following literal property:
Every fraction is evaluated in . The predicate contains only these witnesses, inequalities, and equality. The required range of the conjecture is ; distinctness is part of the mathematical target. In particular, the prime cannot simply be imported from a formulation permitting repeated denominators. The boundary value is included, with denominators .
The unresolved root goal is
The supporting milestones concern established mathematics. Denominator clearing relates the rational equation to under strict positivity. Positive scaling transports a solution for to one for while preserving the strict order. An explicit even-number family supplies the case needed for the prime reduction.
The elementary families cover , , , and , with the displayed witnesses and their integrality and strict ordering recorded in separate statements. Together with the even case, they solve every outside . The useful reduction is an equivalence between the root goal and its restriction to primes ; the ordinary prime reduction is also stated separately. The classical scaling and residue observations are discussed in Bloom–Elsholtz, p. 239.
Obláth’s milestone says that holds for whenever has a prime divisor . This condition is explicitly recorded in the introduction of Pomerance–Weingartner, which identifies the original Obláth reference. The exact distinctness requirement is retained in this mission.
The Mordell–Yamamoto milestone asks for a decomposition for every prime satisfying
The actual existence claim is the theorem to prove. It has no hypothesis asserting that these classes are covered. Yamamoto’s original paper, §§3–4, pp. 42–46, supplies the congruence framework and prints this residual list. The same list appears in the current Erdős Problems record. The list printed on p. 239 of Bloom–Elsholtz instead contains and omits ; that discrepant list is not used here. The historical papers often permit repeated denominators, so producing distinct ordered witnesses is an explicit part of the formalization obligation.
The elementary infrastructure gives reusable certificates and transports for exact rational decompositions. The reductions identify a mathematically meaningful remaining domain without assuming the conjecture. Completion of the modulo- milestone would leave the prime cases in its six residual classes as the classical research frontier; those classes are not asserted to consist of counterexamples.
Later targets include Terzi’s 1971 sieve, whose publisher abstract reports 198 residual classes modulo , and Vaughan’s density theorem, bounding the exceptional count by for a positive constant . Neither is a core Lean statement in this draft. No unaudited list of 198 classes is supplied.
Elsholtz–Tao provide counting results and a classification of polynomially soluble congruences. Bloom–Elsholtz, Theorem 1, pp. 239–240, characterize their conjecture by coverage of all primes by classes
or
Here division by denotes a modular inverse; division by is exact integer division. The authors are Bloom and Elsholtz, not Bradford and Elsholtz. This is a later formalization target: an initial core theorem is not included until the translation between that paper’s denominator convention and the present strict convention is separately formalized. Pomerance–Weingartner address growing numerators in the generalized problem; their exceptions are not counterexamples to the fixed numerator conjecture.
Congruence identities prove infinite families only when the identities and their arithmetic hypotheses are established for arbitrary parameters. Checking finitely many representatives with a search program does not prove that all future values in an arithmetic progression work. Density estimates also allow an exceptional set and therefore do not settle the universal statement.
The current record cites Mihnea–Bogdan (2025) for computational verification through . This is reported computational evidence, not a Lean-certified theorem in this mission. No universal conclusion or periodicity assertion is inferred from it.
The development uses natural-number denominators, exact rational arithmetic, integer polynomial identities, divisibility, primality, and natural-number remainders. Definitions are transparent. The root is not hidden in a typeclass, structure field, certificate, or extra assumption, and its quantifier is not bounded. The existing Google DeepMind transcription is a statement reference, not an imported proof.
The draft targets Mathlib 0df444a360eaa60ab8c11dca51a86af692955474 with Lean 4.33.1. Every proposed statement has been locally elaborated and supplied with an independent read-back. Statement elaboration with sorry is not proof verification. The accompanying local proof audit distinguishes the proved supporting results from the open root and the remaining modulo- formalization task.
Let be a finite connected graph. In Bernoulli bond percolation each edge is independently retained with probability and deleted otherwise, and one writes for the probability that vertices and lie in the same component of the resulting random subgraph. Comparing such connection probabilities is a basic and genuinely hard problem: computing them exactly is -hard.
The bunkbed graph is built from two copies of , joined by vertical edges called posts above a chosen set of transversal vertices. Percolation is performed on the two copies while every post is retained. Writing for a vertex in the lower copy and for its counterpart upstairs, Kasteleyn conjectured in 1985 that being connected within a level is always at least as likely as crossing between levels.
The conjecture is intuitively compelling — crossing levels appears to require "using up" a post — and it resisted proof for forty years. A short timeline:
Section 7 of the source is a candid account of a large-scale machine-learning-guided search that failed to find a counterexample, and of why the problem is unusually ill-suited to experimental testing.
Fix a finite graph with vertex set and edge set , and a retention function (the uniform case is ). A configuration is a subset of open edges, occurring with probability
and is the total probability of those for which and are connected in .
Given , the bunkbed graph has vertex set . Its edges are a copy of in each level together with a post for every . In bunkbed percolation the two level-copies are percolated independently while all posts are retained; denotes the resulting connection probabilities.
For the gadget on vertices,
The result itself. A forty-year-old conjecture in percolation theory is false, and prior positive results are thereby sharpened rather than superseded: it becomes interesting to delimit exactly which families of graphs do satisfy the inequality. The refutation also settles the Counting, Weighted, Alternative and Computational variants listed in §8.1, and shows the random-cluster analogue cannot be pushed from down to .
Formalizing it. Nothing here is open; the mission produces machine-checked versions of published results, and as a by-product the first percolation theory in Lean. Mathlib currently contains no percolation of any kind — no connection probabilities, no bunkbed graph, no hypergraph percolation. That infrastructure is reusable far beyond this mission. The source itself notes (§8.2) that its central combinatorial lemma was independently verified by computer; a formal proof would replace that check with a certificate.
The obvious approach — exhibit a small graph and compute both probabilities — is hopeless, and the source explains why at length. A graph with edges has configurations; for the counterexample here the probability gap is on the order of , so no sampling argument can detect it, and exact enumeration is out of reach. Section 7 records a substantial computational search that found nothing and, in hindsight, could not have.
The proof is instead structural, and its difficulty is concentrated in one place. Hollom's refutation of the hypergraph version cannot be transferred directly, because a single -hyperedge cannot be simulated by bond percolation on any gadget graph. The source's answer is to prove a robust version of Hollom's lemma (Lemma 3.3) which survives the inexact simulation that gadget graphs do provide, and this robustness is what Lemma 4.1's inequality quantifies. Lemma 3.3 is proved by constructing a weight-preserving involution on a refined configuration space — the technical heart, and the milestone a solver should expect to spend the most effort on.
The development commits to the following conventions.
ℚ and evaluate by #eval, and small instances close by decide.Finset and realised through SimpleGraph.fromEdgeSet; connectivity is Mathlib's SimpleGraph.Reachable.Sym2 V → ℚ), since the gadget genuinely needs two different weights: its spokes are retained with probability and its path edges with probability .0 is the lower copy; posts over T are unconditionally present and are not percolated. The two levels are percolated independently.IsPlanar, no Euler formula, no Kuratowski. Building one is a larger project than this mission. The formalized statement of Theorem 1.2 is therefore strictly weaker than the published one, and the goal is instead the negation of the conjecture, which is exactly the source's own "In particular, the BBC is false." Contributions adding planarity are welcome and would strengthen the milestone.Infrastructure. Mathlib supplies SimpleGraph, boxProd, Reachable with a DecidableRel instance, fromEdgeSet, edgeFinset and Finset.powerset. It supplies no percolation, so this mission ships two definition files: Bernoulli bond percolation with the bunkbed construction and the five triple-partition probabilities, and hypergraph percolation with Hollom's hypergraph and the Wierman–Ziff five-state model. One known gap: Mathlib's Reachable decision procedure enumerates walks and is far too slow to evaluate the -configuration check of Lemma 3.1 by decide. A solver will want a linear-time reachability procedure together with a proof that it agrees with Reachable; that is itself a worthwhile reusable contribution.