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.
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?
Two closed subgroups and of a profinite group are locally conjugate if, for every prime , a Sylow -subgroup of is conjugate in to a Sylow -subgroup of . Conjugate subgroups are always locally conjugate. The converse, which lets conjugacy be tested one prime at a time, fails in general. Deciding when it holds is a classical question about supplements of nilpotent normal subgroups.
A profinite group is a compact Hausdorff totally disconnected topological group. Equivalently, it can be described through compatible finite quotient groups. A pronilpotent group has nilpotent finite continuous quotients. A prosupersolvable group has supersolvable finite continuous quotients; a finite group is supersolvable when it admits a normal series with cyclic factors. These properties concern all finite continuous quotients, with no uniform bound on their orders or nilpotency classes.
A subgroup supplements a normal subgroup when . It complements when, in addition, . Two closed subgroups are locally conjugate when, for each prime , a Sylow -subgroup of one is conjugate in to a Sylow -subgroup of the other. For profinite groups, Sylow subgroups are maximal closed pro- subgroups. The conjugating element may depend on the prime. All subgroup notation in the paper carries closedness, as stipulated in §1.2.
The cohomological statements concern a profinite group acting continuously by automorphisms on a discrete group . With a left action, a continuous cocycle satisfies . Two cocycles are equivalent when for one fixed . Their quotient is the pointed set , whose distinguished point is the identity cocycle. Stable classes on a subgroup compare a cocycle with its conjugates after restriction to the relevant intersections. This matters when the subgroup itself is not normal. The definitions follow §§1–1.2.
The central conjugacy assertion is Theorem 1.1. For a closed normal pronilpotent subgroup of a profinite group , assume that is prosupersolvable or is pronilpotent. Then closed supplements of satisfy
Lemma 1.2 asserts, for finite nilpotent coefficients and its stated structural alternatives, a pointed bijection induced by simultaneous restriction:
The other numbered targets are Corollaries 1.3–1.4 and Propositions 2.1–2.3, 3.1–3.2, and 4.1–4.2. They retain the paper's distinctions between finite coefficients, locally finite discrete coefficients, and arbitrary closed pronilpotent subgroups. They also retain the normal-intersection condition in the semidirect-product inclusion and fixed-point results. The abelian conclusions impose no solvability assumption on the ambient profinite group.
Both counterexamples in §1 are targets. The quaternion example realizes in , has exactly two global cohomology classes and trivial Sylow cohomology, and exhibits locally conjugate complements that are not conjugate. The Heisenberg example uses of order , with the Heisenberg group of order , , and . Local containment holds while containment of a conjugate of fails.
The combined goal asserts all eleven numbered results and both counterexamples. Each assertion remains a separate milestone with the source's numbering or, for the unnumbered counterexamples, its section and page.
The conjugacy and containment theorems make precise when separate prime-wise witnesses can be replaced by one global witness. The fixed-point results similarly turn prime-wise fixed points, which can be different points, into a point fixed by the full subgroup. The counterexamples record the limits of these conclusions under weakened hypotheses. These are proved mathematical results of the preprint, rather than new conjectures.
A completed development would also provide reusable formal interfaces for continuous nonabelian first cohomology, stable classes, profinite Sylow and Hall conditions, and local subgroup relations. An earlier local Lean development supplies definitions and substantial proof material. The present draft statements are aligned to the arXiv version; their target proofs remain open in this proposal. Reusing earlier proofs requires checking their types against these interfaces and the pinned environment.
Local conjugators can vary with the prime, and there need not be one conjugator that works for all primes simultaneously. The quaternion example demonstrates this obstruction even in finite groups. Nonabelian cohomology is a pointed set, so the usual additive primary-decomposition language does not itself provide the needed assertion. The transition from finite groups to profinite groups also requires tracking topology, closedness, and continuity. The counterexamples and the finite-versus-profinite distinctions are part of the mathematical scope, not optional simplifications. See §§1–3.
All declarations use the namespace LocalConjugacy. Profinite ambient groups use Mathlib's ProfiniteGrp; subgroups, quotient groups, normality, complements, actions, fixed points, finite Sylow subgroups, nilpotence, and solvability use Mathlib structures or predicates. Custom definitions cover the continuous nonabelian quotient and the profinite local conditions absent from the pinned library interface. Conjugation is written on the left. This changes the notation for the conjugating element, not the conjugacy or inclusion assertion.
The fixed-point targets quantify over nonempty sets with no added topology and require closed stabilizers. Propositions 2.1–2.2 allow infinite locally finite discrete coefficients. Theorem 1.1 allows arbitrary closed pronilpotent . Finite special cases cannot replace these targets. Both counterexamples include explicit isomorphisms to the concrete groups named in the paper. Contributions may reuse the existing proof development, improve the reusable interfaces, or prove the targets directly while preserving these statements.
Quantum mechanics predicts probabilities, but it is notoriously quiet about what a probability is. Categorical quantum mechanics answers that by rewriting the finite-dimensional formalism in the language of dagger categories: a state is a morphism , an effect is a morphism , and the probability of an outcome is a scalar — an endomorphism of the tensor unit. On that translation the Born rule stops being an axiom and becomes a theorem about a complete, disjoint family of effects.
This mission formalizes that theorem, together with the two lemmas it rests on, in Lean 4 over Mathlib. It covers the dagger and measurement material of Chapter 2 of Reutter and Vicary's Categorical Quantum Mechanics.
Fix a monoidal dagger category with zero morphisms. The unit object carries a commutative monoid structure — the scalars. For a state and an effect , the probability that occurs on is the scalar
A family of effects is complete when the induced map satisfies , and disjoint when for . Both conditions are stated for a dagger biproduct of the unit objects.
This is the mission's goal. It fixes nothing beyond completeness and disjointness; the statement is exactly the categorical Born rule for a finite outcome set.
The Born rule is the point where the categorical and the Hilbert-space pictures are reconciled: the abstract statement specialises, in , to the usual . Proving it categorically means the rule is a consequence of the dagger-biproduct structure rather than an extra assumption, which is what makes the framework usable for quantum protocols — measurement, teleportation and the like are all built on complete disjoint families.
The supporting lemmas are reusable well beyond this mission: dagger biproducts are the categorical home of matrix calculus, and the isometry/unitary characterisations of disjointness and completeness are the standard toolkit for any later argument about measurements.
Moderate. The mathematics is elementary once the definitions are in place — the work is in bookkeeping: biproduct universal properties, the interaction of the dagger with the biproduct structure, and careful handling of the scalar monoid. The main intellectual step is realising that completeness alone, not equalizers, gives the second unitary identity.
Formalized here: dagger categories and their morphism classes (§2.3), dagger biproducts
(§2.3.3), and the scalar/state/effect vocabulary with the Born rule (§2.4.3). Mathlib has
no dagger-category theory at all, so the definitions are supplied from scratch as Lean
Definitions and are importable independently of this mission.
Not formalized: the Hilbert-space and relational models, the graphical calculus of §2.2, and the measurement/post-processing material after §2.4.3.
Two corrections to the source are made and documented in the formalization. The printed statement of Proposition 2.55 assumes completeness only, which is false; disjointness is required, as the book's own proof (which invokes Lemma 2.52) already assumes. And the book attributes the identity on to Lemma 2.52, whereas Lemma 2.52 only gives the identity on ; the identity on is Lemma 2.53. Lemma 2.53 is proved here without the book's equalizer hypothesis, so it is strictly stronger than the printed version.
CategoryTheory.Limits.Biproducts and CategoryTheory.Monoidal.Category
API, on which the definitions are built.The 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. The question is how large a comparison constant is needed to make this inequality hold.
This mission establishes the best possible constant for complex diagonal matrices for every real . The result is proved in Lean. For each exponent, one constant works for every triple of diagonal matrices of the same size, across all finite sizes.
The constant comes from a simple family of three diagonal matrices, called the cyclic family. Varying one parameter determines the largest comparison constant these examples require. The theorem proves that this value also works for every other triple of diagonal matrices, however large. The goal theorem gives the exact formula and statement.
This is the foundation of the sharp diagonal Hlawka campaign. It supplies the shared definitions and supporting results for lowering the exponent cutoff while keeping the same formula. A later mission has now established the result in Lean for every real ; the campaign invites further improvements.
The broader question of optimal constants for Schatten norms appears in Audenaert and Kittaneh’s Problem 7. Extending the sharp diagonal constant to general matrices is a separate challenge.
79aa498bfcf7b22bd91d771fb32ec278e2d4704b. Source libraryA fine-tuned model can be stored as a pretrained model together with its parameter changes. Pruning these delta parameters reduces the amount of task-specific information to store. The DARE procedure independently deletes each change with probability and multiplies every surviving change by . This preserves the expected linear-layer output, but a single pruned model can still differ substantially from that expectation.
Deng and coauthors investigate this distinction in DARE the Extreme: Revisiting Delta-Parameter Pruning For Fine-Tuned Models, ICLR 2025. The paper motivates changes to the rescaling rule and to fine-tuning regularization. This mission focuses on its finite-sample mathematical analysis: the relation between random pruning, coefficient energy, and output concentration. Its goal is the Kearns–Saul bound in Appendix E.1, equation (8), PDF p. 30, expressed through the coefficient statistics used in Section 3.2.
The distinction between that appendix result and the printed Theorem 3.1 matters. The mission does not assert the latter's piecewise formula. Its low-pruning branch omits the square root present in equation (8), and its high-pruning branch applies a one-sided refinement to a two-sided event. The exact target below retains the appendix's valid bound across the entire interval .
Fix one output coordinate of a linear layer, an input vector , and a delta-weight row . There are input coordinates. Define the deterministic influence coefficients , their sum , and their energy . Equivalently, the formal statements quantify over every real coefficient vector ; choosing realizes every such vector in the layer model.
The only randomness is the pruning mask. Write for a dropped coordinate, with mutually independent . A mask has probability
Expectations and event probabilities are the finite weighted sums against . A surviving coordinate is rescaled by , where . The output error, original minus pruned, is
DARE uses ; denote its error by . This is the retention-mask formulation in Section 3.2, equation (2), PDF p. 5, with . The empirical coefficient mean and variance are and . These statistics describe a fixed vector, not another source of randomness.
Define the concentration coefficient with its removable singularity filled in:
For every and failure probability , the goal is
This is Appendix E.1, equation (8), PDF p. 30, followed by the unnumbered energy identity on PDF p. 31. Zero coefficients are included: no positive-energy assumption is attached to the goal.
Four supporting milestones state the following results.
The analytic input is Berend–Kontorovich, Section 3, Theorem 4, equation (6), PDF pp. 3–4. The bound on is also stated in the DAREx appendix on PDF p. 30. 4. Exponential output tail: for and ,
This is the unnumbered display immediately preceding equation (8), PDF p. 30.
The target quantifies the error of a randomly selected pruned layer in terms of its actual influence coefficients. It distinguishes preserving an expectation from controlling a realization. The moment identities also expose the bias introduced by choosing a rescaling denominator different from .
Formalization supplies a precise probability model and checks every coefficient, sign, and exceptional case. The finite mask model and its normalization already compile locally with proofs. The five milestone and goal statements have been elaborated, but their theorem proofs remain open. Completing this mission would formalize the selected appendix result; it would not establish the paper's experimental accuracy claims, a whole-network guarantee, or an optimal rescaling rule.
Signed coefficients require exponential-moment control for both positive and negative arguments. The sharper estimate in Berend–Kontorovich, Lemma 5, equation (9), PDF p. 4 has a nonnegative-argument restriction. Using it for an unrestricted absolute tail loses an essential hypothesis.
For example, with , , , and , the error is with probability and with probability . The printed Theorem 3.1 threshold is , so its failure probability exceeds . This concrete source audit is the reason for selecting equation (8), not a claim that the printed theorem has been formally disproved in Lean.
The Lean model uses real coefficients indexed by Fin n and Boolean functions for masks. Nonnegative masses and normalization are proved from the product formula; concentration is never assumed in a structure field. Fixed weights and inputs are external data. Random training, dependence between masks, nonlinear activations, structural pruning, and empirical validation are outside this mission.
The main goal requires for the empirical statistics, for DARE rescaling, and for the confidence level. The moments permit empty coefficient vectors and endpoint probabilities because they use a separate positive . The exponential-tail milestone requires to avoid division by zero; the main goal includes . The value is explicit. No theorem relies on Lean's total division or logarithm to supply a missing analytic hypothesis.
This mission formalizes §7 of J. W. Cannon, W. J. Floyd and W. R. Parry, Introductory notes on Richard Thompson's groups, L'Enseignement Mathématique (2) 42 (1996) 215–256, doi:10.5169/seals-87877: W. Thurston's interpretations of Thompson's groups and as groups of piecewise integral projective homeomorphisms of the interval and the circle.
The notes describe their last section as follows: "In §7 we give W. Thurston's interpretations of and in terms of piecewise integral projective homeomorphisms" (p. 216). Elements of and are piecewise linear, with dyadic breakpoints and slopes powers of . Thurston's models replace the linear pieces by linear fractional maps with integer matrices of determinant , and the dyadic intervals by the intervals of the Farey tree. The two descriptions give isomorphic groups because both are read off the same tree diagrams.
Earlier missions on this platform formalize (§1 and §4), its tree diagrams (§2), its presentations (§3) and the group (§5); this one states their projective models.
The simplex. (Simplex n) is the standard -simplex in , and (rho). A map on is integral projective (IsIntegralProjective) when it is for some with in the nonnegative orthant (p. 249). Subdivisions of are Mathlib's geometric simplicial complexes (Geometry.SimplicialComplex), finite and with underlying space ; a subdivision is rational or integral when each -simplex has rational vertices, or is the image of under an integral projective map. lift and ind are the primitive integer lift of a rational point and the index of a rational simplex (p. 250).
PIP maps. (PIPSet n) is the set of homeomorphisms of that are integral projective on each simplex of some integral subdivision. (PIPPlusSet n) consists of the orientation-preserving ones; in Lean orientation is read off the pieces, which are required to be with .
The interval and the circle. On p. 251 the notes move to and identify it with . There a map is integral projective (IsIntegralProjective01) when it is with , and . An interval is recorded by four natural numbers (FracInterval), with left part and right part , and fareyNode follows a path of left and right steps from down the tree of integral subsimplices. of (PIPPlus01Set) consists of the order isomorphisms of that are integral projective on each interval of an integral partition, and RepresentsPIP reads a §2 tree diagram on instead of on the dyadic tree. (PIPPlusCircleSet) consists of the permutations of UnitAddCircle with an order-preserving lift to commuting with that is integral projective, up to an integer, on each interval of an integral partition of , the way the published is defined through lifts.
The goal is Theorem 7.3 (p. 254),
together with the sentence that follows it, which names the three maps of corresponding to 's generators , , : the goal asks for an isomorphism sending them to exactly those maps (pipA, pipB, pipC).
The milestones follow the section. For : integral projective maps are homeomorphisms onto their images, is closed under inversion, two integral subdivisions have a common rational refinement (the notes cite Rourke and Sanderson), the index of a rational simplex, Theorem 7.1 (every rational subdivision refines to an integral one), is a group, and has index in it. For the interval: is isomorphic to its model on ; is an integral subsimplex exactly when ; left and right parts are integral; is an ordered rooted binary tree; integral projective maps between integral subsimplices are unique and given by an explicit formula; they restrict to, and are glued from, maps of the left and right parts; reduced tree diagrams correspond bijectively to of ; and Theorem 7.2, .
The result. Thurston's description identifies and with groups of piecewise maps of the interval and the circle, the dyadic tree becoming the Farey tree. The same substitution carries each element of or to its projective model; the conjugating map is Minkowski's question mark function.
Formalizing it. Nothing on this platform or in Mathlib concerns piecewise projective groups, the Farey tree of intervals or Minkowski's function. The mission reuses the published , and the tree diagrams of §2.
Theorem 7.1 is the one argument in the section that is not about the interval: a descent on the index, starring a rational subdivision at a well-chosen rational point. Mathlib has geometric simplicial complexes but no subdivisions, starring or common refinements, so both Theorem 7.1 and the cited results of Rourke and Sanderson need that apparatus built. The interval half is elementary number theory of integer matrices (the notes' proof of connectedness of is a Euclidean-algorithm descent), followed by the tree-diagram argument of §2 repeated on .
Simplex n ≃ₜ Simplex n. The milestones that they are groups assert a subgroup with exactly that carrier, and Theorem 7.2 asserts such a subgroup for together with an isomorphism from .Transfer learning starts with a representation learned on an earlier task and adapts it to a new one. Two common choices are linear probing, which changes only the final linear predictor, and fine-tuning, which changes the representation as well. These procedures optimize related training objectives, but their behavior away from the training data can differ. Kumar and coauthors study this distinction through two-layer linear networks, alongside experiments with nonlinear networks. This mission formalizes their perfect-feature LP-FT result, rather than the empirical claims or the general imperfect-feature comparison. See Section 3.4, Proposition 3.7, PDF p. 10.
LP-FT first learns a head by linear probing and then uses that head to initialize full fine-tuning. The perfect-feature setting isolates the effect of head initialization: the representation already contains exactly the features needed to predict the labels, but the head initially need not use them correctly. The mathematical question is whether joint training preserves or loses the representation's ability to predict outside the observed training subspace.
An input is a vector . A feature extractor is a matrix , and a head is a vector . Together they predict , with effective weight vector . The fixed matrix contains the training inputs as rows. Their span is , with dimension .
The ground truth has orthonormal-row features and a nonzero head . Write and . Perfect pretrained features mean for an orthogonal matrix . The corresponding aligned head is . The dimensions satisfy and .
The two geometric assumptions require the orthogonal projections from into and into to be injective. In this dimension regime these are exactly the positive largest-principal-angle cosine conditions used by the paper. They demand more than two subspaces having some nonorthogonal directions. The Lean definition spells out injectivity of for each . See Definition 3.2 and Appendix A.1, PDF pp. 7 and 22-23.
An out-of-distribution law is any probability measure on with a finite second moment and positive-definite uncentered second-moment matrix . Its mean need not be zero. Define
Both training methods use the unnormalized loss . Fine-tuning follows its gradient flow in both parameters; linear probing keeps . Time is real and nonnegative. These are the paper's equations (3.2)-(3.3), PDF p. 6.
The goal is Proposition 3.7 in an explicit nonzero-signal regime. For , initialize an FT head with independent Gaussian coordinates, . Establish
Linear probing, from any initial head, must converge to . Fine-tuning initialized at its limit must satisfy
The probability-one event applies to all times simultaneously. The goal also asserts existence of the relevant global flows; a conditional claim about a possibly nonexistent trajectory would not suffice. The statement does not assert a numerical error lower bound or a positive time-infimum.
Seven milestones supply the supporting results: global flow existence and FT uniqueness; unchanged features orthogonal to the training span; the balancedness invariant; the second-moment identity for OOD risk; almost-sure Gaussian head misalignment; exact LP recovery; and stationarity after LP initialization. The principal source is Appendices A.2 and A.7, PDF pp. 23-31 and 45-47.
The result distinguishes two initializations of the same joint-training procedure. In this idealized setting, a head obtained by linear probing gives zero OOD loss throughout subsequent fine-tuning, while a Gaussian head almost surely has positive OOD loss at every finite time. The conclusion concerns population squared prediction error, not classification accuracy or a finite test-set estimate.
The paper establishes the mathematical claim; this mission asks for a Lean proof of the stated model and result. The scope is deliberately limited to perfect pretrained features. It does not claim an LP-FT upper bound for imperfect features, which the authors identify as a further challenge in Section 3.4, PDF p. 10. A completed development would also provide reusable components for finite dimensional gradient flows, factorized linear models, and population risk.
The training loss alone does not select a unique effective predictor in an overparameterized problem. Knowing that a predictor fits the observed examples therefore does not determine its OOD loss. Formalization must track the head and feature extractor together, and it must distinguish parameter stationarity from a claim that a derivative happens to vanish at one time. The Gaussian conclusion also requires one event controlling an uncountable set of times; separate probability-one statements for individual times would be weaker.
Vectors use Mathlib's finite dimensional real Euclidean spaces. Matrices are represented as continuous linear maps, with Euclidean adjoints and operator norms. The feature update is written explicitly as the Frobenius-gradient equation; it is not a gradient with respect to the operator norm. Differentiability is imposed within , including the right derivative at zero.
The dimensions, nonzero target, positive Gaussian scale, finite second moments, and projection injectivity are explicit. The nonzero target restricts the formalization to the regime of the Gaussian alignment argument in Lemma A.12; makes the identifiability condition used in Proposition A.20 precise. The random-head law is the scaled standard Gaussian measure. No randomness of the fixed training matrix or independence from an additional data draw is assumed.
The model contains no assumed convergence, invariant, or desired risk bound. Each of those is a theorem obligation. The well-posedness milestone makes explicit an analytic prerequisite of the source's flow notation. The risk milestone uses the identity in (A.29)-(A.32), avoiding the reversed inequality printed in (A.28). The quantitative constant in Theorem 3.3 is outside this mission. Source-aligned proofs and the supporting analysis infrastructure are welcome; changing the learning rule or assuming a milestone inside the model would change the task.
Goldbach's problem asks whether every integer greater than can be written as a sum of a small number of primes. The first unconditional result of this kind was obtained by Schnirelmann around 1930: there is an absolute constant such that every integer is a sum of at most primes. His argument is elementary. It uses an upper-bound sieve and Chebyshev-type prime estimates, together with a notion of additive density, and it does not need the prime number theorem or complex analysis.
The constant has since been reduced by much deeper methods. A short timeline for odd :
This mission targets a much weaker constant than any of these, . It does so because the constant comes from Schnirelmann's elementary method with every estimate made explicit, and that proof is short enough to be a realistic target for a complete formalization.
A representation of as a sum of at most primes is a finite multiset of natural numbers such that every element of is prime, the elements of sum to , and has at most elements counted with multiplicity. Repetitions are allowed and order is irrelevant.
The number is not a sum of primes, so the question concerns odd . Even numbers are excluded from the campaign statement.
The Schnirelmann density of a set is
This notion is the additive tool behind the elementary approach. Mathlib provides it as schnirelmannDensity.
This is the campaign template of Odd numbers as sums of primes with the value filled in. A stronger explicit form in the source is that every odd is a sum of exactly primes; the at-most form for all odd follows from it immediately.
The result itself. The bound is far from the best known constants; five (Tao) and three (Helfgott) are both known on paper. Its value is that it rests on an elementary argument with every constant written out. There is no "sufficiently large" threshold and no appeal to the prime number theorem, zero-density estimates, or large-scale computation.
Formalizing it. No finite bound in this problem has a machine-checked proof on this platform yet. A proof of this goal would be the campaign's first proved value. The components are reusable beyond this mission:
The only substantial step is an upper bound for
that is sharp up to a constant factor, namely of order times an arithmetic factor depending on the prime divisors of , with an explicit constant. The trivial bound is weaker by a factor of . That loss makes the density of sums of two primes appear to be zero, so the additive argument cannot start. Everything after the sieve bound is short and explicit.
The Lean statement is the campaign template verbatim with in place of the value. It uses Multiset ℕ, Nat.Prime, and Odd n ∧ 1 < n. The statement is fixed by the campaign, and it has no vacuous hypotheses: every odd is covered.
Mathlib already contains schnirelmannDensity and the fact that with implies . It also contains the Λ² setup of the Selberg sieve (Mathlib/NumberTheory/SelbergSieve.lean) and central-binomial-coefficient bounds. Missing, and welcome as contributions:
This mission is pure mathematics about objects it defines itself: an octonion multiplication built from the Fano plane of the companion mission The role postulates force exactly seven points, and the matrix of the linear map
for two unit imaginary octonions . It is motivated by the two-generator D8 flow in the Shape Zero derivation (00_START_HERE/MODEL_SPEC.md §1b; 02_synthesis/D8_SYNTHESIS.md). The statements below do not depend on that motivation.
Result. For and with , the characteristic polynomial of is
With , , so the eigenvalues are and (each twice), and the ratio of the two nonzero frequencies is .
What this mission does NOT prove.
Write for the standard basis of . The imaginary unit () is labelled by the Fano point . For each line (mod ) of the companion mission's Fano plane RolesForceSeven.fanoLine, the product is oriented cyclically along the ordered triple :
(unit indices mod , shifted into ), with the reversed products negative, , and the identity. This defines OctonionD8.octTable and the bilinear product OctonionD8.omul on .
For , Rmat a is the matrix of and Lmat b the matrix of (column is the image of ). The flow matrix is
The Fano plane is imported from the companion mission, not restated. The reordering blockEquiv and the two blocks blockA c s, blockB c s are defined explicitly for the milestones.
This is OctonionD8.flow_charpoly. The hypothesis is the only one, and it is needed: without it the characteristic polynomial differs.
The proof goes through an invariant-subspace decomposition. Reorder the basis as (OctonionD8.blockEquiv).
OctonionD8.blockA, OctonionD8.blockB).The goal follows: the characteristic polynomial is unchanged by reordering the basis, and that of a block-diagonal matrix is the product of the blocks' characteristic polynomials.
For , with and , the roots over of the characteristic polynomial, with multiplicity, are exactly
and . So the two nonzero frequencies and are distinct, and their ratio is . Uses .
The result itself. It gives the spectrum of the two-generator flow for the canonical pair in closed form, for every angle, from an octonion table built on the formalized Fano plane.
Formalizing it. The spectrum had been checked numerically and symbolically only.
| check | result |
|---|---|
| table from the companion mission's Fano lines is a normed algebra (200 random pairs) | true |
| eigenvalue magnitudes at 5°, 30°, 60°, 76.3°, 90°, 120°, 150° | max error |
| symbolic characteristic polynomial (sympy, ) |
These agree with the repository's shape_zero_tests/d8_closed_form.py (frequencies to ), which uses a different octonion table.
Moderate. The goal needs the characteristic polynomial of an matrix with symbolic entries; a direct determinant expansion is expensive. The milestones take the invariant-subspace route: the block-diagonal form (M1) is an entrywise computation from the octonion table, and each block's characteristic polynomial (M2, M3) is a small determinant, reduced with . The further results are large but mechanical polynomial identities (the eight-square identity; the annihilating polynomial), where the risk is performance, not ideas.
Fin 8 → ℝ; matrices are Matrix (Fin 8) (Fin 8) ℝ, with column the image of the basis vector .Matrix.charpoly over ; the corollary maps it to and uses Polynomial.roots, a multiset, so multiplicities are part of the statement.This mission is a statement about ordinary differential equations and nothing else. It is motivated by the scaling analysis in the Shape Zero derivation (00_START_HERE/MODEL_SPEC.md §1b), which found that the golden ratio in an on-site quadratic well is a coordinate choice. The statements below do not depend on that motivation.
Result. For any and any two distinct real roots , the equation
becomes exactly
under one fixed shift and scaling of the value and one fixed rescaling of time. So every oscillator with a quadratic restoring force and two real roots is the same oscillator, described in different units. In particular, the golden-ratio well , whose roots are and , is the normal form in disguise: its is a choice of coordinates.
What this mission does NOT prove.
Solutions are functions that are twice continuously differentiable on all of (ContDiff ℝ 2 x), with written deriv (deriv x). The transformation is
a shift by , a scaling by of the value, and a rescaling of time with .
Let and . There are real numbers , , with and , chosen once, before any solution is considered, such that for every twice continuously differentiable :
This is QuadraticWell.quadratic_well_equiv. Explicitly , with the sign chosen so that , and .
The goal combines them: by M1 the equation reads with ; by M3 this becomes ; and , available by M2, gives . The converse uses .
For every twice continuously differentiable , everywhere if and only if
satisfies everywhere. This is the explicit instance with roots and : , .
The result itself. It shows that the only content of a quadratic restoring force with two real roots, for a single oscillator, is the normal form ; the roots and the stiffness are units.
Formalizing it. The equivalence had been checked numerically only.
| check | result |
|---|---|
| M1 identity, both signs of (sympy) | exact |
| golden-ratio well: , , | , , |
| against a direct solution of , 400 points | max difference |
| a case needing the sign flip (, roots and ) | , so gives |
These agree with the repository's shape_zero_tests/scale_invariance.py (runs at four unit choices agreeing to ).
Low–moderate. M1 and M2 are short. M3 is the only fiddly part: Mathlib's chain rule for a composition with , applied twice, needs the differentiability of and of that ContDiff ℝ 2 supplies. The goal and corollary then follow by rewriting.
deriv.A set of integers is sumfree when no two of its elements, equal or distinct, add up to an element of the set. The Schur number is the largest such that can be partitioned into sumfree sets; only are known. For the best theoretical upper bound that Eliahou and Revuelta could cite in 2021 was , where the Ramsey number is the least such that every -colouring of the edges of the complete graph has a monochromatic triangle. The Ramsey numbers satisfy for (Greenwood–Gleason 1955); for the paper knows no recursive upper bound.
Eliahou and Revuelta proposed a conjectural one. They defined a number through the Schur degree of block-sum sets, proved (Theorem 5.4) and (Proposition 5.3), and conjectured (Conjecture 5.6). This would give (Conjecture 5.7) and (Conjecture 5.8), against the range that they give. For they proved , conjectured , and left the value open.
Timeline.
ClassicalSchur formalizes both, with .All numbers are natural numbers, except in the group below.
Sumfree sets. A set is sumfree when the sum of two of its elements, equal or distinct, is never in . A set is covered by sumfree sets when it lies in the union of sumfree sets.
Schur degree. The Schur degree is the least such that sumfree sets cover . If there is no such , it is .
For example, holds for and fails for .
Block sums. Let be a finite sequence of length . Its block sums are the sums of runs of consecutive entries:
The set of these sums is . The average of is the rational number .
The number . A length has the ER property for when every sequence of positive integers with has .
For , the inequality holds when no sumfree sets cover . It fails when some sumfree sets cover .
The number is the least with the ER property for .
The pigeonhole bound. Let and . The first values are , , and .
For , is an upper bound for the Ramsey number: , with equality for .
The group . Let . A set is sumfree in when the sum in of two of its elements, equal or distinct, is never in .
The lifted sequence. Take and . Write the numbers , with and , in increasing order:
The lifted sequence is the sequence of the gaps between consecutive terms, . Lemma 4.1 below uses it to turn a cover of into a sequence in ℕ.
Lean names.
SumFree S: is sumfree.CoveredBySumFree X n: is covered by sumfree sets.sdeg X : ℕ∞: the Schur degree, with ⊤ for .blockSums A and average A, for A : List ℕ: and .ERProperty n L: the length has the ER property for .erL n: .ramseyBound k: .GroupSumFree C: is sumfree in . The Lean definition takes any type with an addition; the targets use it for ZMod m₁ × ZMod m₂.liftPrefix m₁ M L: , defined for all and by .liftSeq m₁ m₂ M: the lifted sequence, defined for all , and as the list of the differences .An exact value, so no later result changes the statement; it is the case Eliahou and Revuelta left open.
For , and sets , sumfree in , that cover , the sequence liftSeq m₁ m₂ M satisfies
For , and sets, sumfree in , that cover :
. At , Conjecture 5.6 predicts . So refutes the conjecture at . Here equals the upper bound of Proposition 5.3.
The two bounds of Proposition 5.3 coincide at , where the paper gives and . So is the first case in which the conjecture says more than Proposition 5.3.
. At , Conjecture 5.6 predicts . So refutes the conjecture at .
What remains open. Conjectures 5.7 and 5.8 remain open.
The paper derives Conjecture 5.7 at each from Conjecture 5.6 at the same , with Theorem 5.4. At that derivation is not available. But Conjecture 5.7 holds there by the known values: and .
Conjecture 5.8 follows from Conjecture 5.6 at (that is, ) with Theorem 5.4. Nothing here decides that case.
With , Theorem 5.4 gives only . This is weaker than .
Status. Every target is proved and formalized.
At launch, all 12 theorems of the tree, the goal included, are Proved in Lean over 4 definition bundles. Their only axioms are propext, Classical.choice and Quot.sound.
An independent verifier checked the definitions and the six headline statements against Eliahou–Revuelta and McKenna 2026. The six statements are the goal, Theorem 4.1, Proposition 5.3, Lemma 4.1, Corollary 4.2 and Theorem 1.2.
Literature. The literature search for McKenna 2026 found no result on , or Conjectures 5.6–5.8. One citing text, in Jungić 2023, was not read. This records the search; it is not a claim of priority.
Open work, not targets.
Two kinds of bound. The two sides of an exact value of are statements of different kinds.
An upper bound needs one length. It follows from for every sequence of positive integers of one length , with and average at most .
A lower bound needs every shorter length. For every with , it needs a sequence of positive integers, with average at most , whose block sums are covered by sumfree sets.
One counterexample at length is not enough. A sequence of length and average at most need not contain consecutive entries of average at most . So monotonicity in does not follow directly from the definition.
The average bound. The lower bound of Proposition 5.3 comes from the constant sequence , with . Conjecture 5.6 states that at length , no sequence of average at most has .
Without the bound on the average, this fails. The paper gives a sequence of length 14 with , found by semi-random search. Its average is 114, and the authors remark that such examples "are hard to come by".
The gap for . The gap from 49 to 61 is open. By McKenna 2026 (§5), the construction of Corollary 4.2 gives nothing above 49 at :
McKenna 2026 knows no sequence of length 49 with average at most 5 and ; such a sequence would give .
Set ℕ and sequences List ℕ. For the Schur degree is the same in ℕ and in ℤ. Theorem 4.1 is formalized for sequences in ℕ only.sdeg is sInf in ℕ∞, so it is ⊤ when no cover exists, and . Covers are Fin n → Set ℕ; the sets need not be disjoint or inside . Each lower bound on sdeg must exclude every cover.blockSums A uses B <:+: A with B ≠ []; average [] = 0 is never used, since erL requires .erL n is sInf {L | 0 < L ∧ ERProperty n L} in ℕ, defined for every (the paper: ). As sInf ∅ = 0, an upper bound on erL alone would hold if no length had the property; the Theorem 4.1 target excludes this, giving ERProperty (k+1) at length , and 0 satisfies neither the goal nor the lower bounds.TriangleRamsey k N says every colouring of the pairs of at least naturals with at most colours has a monochromatic triangle; the tree proves it for . As , the Lean upper bound for is 65, not 61.3 * m₁ - 2, m₁ * m₂ - 1, ramseyBound k - 1 and n - 1 in Fin (n - 1) () truncates, and the differences in liftSeq do not truncate when .decide; no native_decide, no external certificate.Bundles: ClassicalSchurBasic (the objects of the Setting), ClassicalSchurRamsey (TriangleRamsey, ramseyBound), ClassicalSchurLift (GroupSumFree, liftPrefix, liftSeq), ClassicalSchurValues (the finite data of the two value theorems). As a check, the definitions give the paper's values erL 2 = 2 and erL 3 = 5 (checked in Lean by an independent verifier in a scratch file; not in the tree). Reusable: the definitions of ClassicalSchurBasic (the interface lemmas are inlined in the proofs, not separate nodes), TriangleRamsey k (ramseyBound k), and the lift from group coverings. Welcome beyond the targets: a formal TriangleRamsey 4 62, which with not_coveredBySumFree_blockSums gives in Lean; the exact ; the case .
ClassicalSchur and the comparator check: https://github.com/mysticflounder/schur-degree-block-sums (tag v1.0.1).The representation function is one of the oldest objects in number theory. Fermat characterised the integers with — those in which every prime congruent to modulo occurs to an even power — and Euler's proof supplied the closed form , where counts divisors congruent to modulo (sum of two squares theorem).
That description counts representations but does not relate them to one another. The integers carrying several essentially different representations,
are exactly the integers that produce quadruples with
whose two sides are not identified by swapping the two entries or changing their signs. Three reasons make this relation worth a formal development rather than a passing remark.
takes two representations and produces a third. Known to Brahmagupta and stated by Fibonacci in Liber Quadratorum (1225), it is the multiplicativity of the norm in the Gaussian integers, and it is the engine behind every statement below.
The parametrisation targeted here is classical. Nothing in this mission claims new mathematics; the aim is a machine-checked development in which every hypothesis is explicit.
Fix integers. A solution is a quadruple with . It is trivial if the multisets and coincide, i.e. if equals or ; if entries are allowed to vanish, the least value carried by a non-trivial solution is , and requiring all four entries to be positive raises that value to . A solution is primitive when the four entries have greatest common divisor , and positive when all four entries are positive and pairwise distinct — the case in which nothing about the relation is explained by signs, zeros or coincidences.
Two constructions produce solutions. The four-parameter family associates to integers the quadruple
which solves the equation because both sides equal by the identity above. Substituting particular parameters is unrevealing, so a genuine supply comes instead from the elementary one-parameter family
whose four entries , , , are strictly increasing — hence positive and pairwise distinct — as soon as . The bound is sharp: at the two entries and are equal.
In the reverse direction, rewrite the equation as and set
The halves are integers exactly when and share a parity and so do and , and in that case the equation becomes
The development is organised in the namespace TwoSquares, with node names matching the roles above (four_param_identity, explicit_family_chain, sum_sq_eq_halves, four_factor_param, complete_parametrization).
For all integers with , there are integers with
possibly after interchanging and . The goal asserts only the existence of integral parameters and the necessity of at most one swap; it does not assert uniqueness of , which is false, and it says nothing about how many solutions lie in a given box.
The identity itself, over an arbitrary commutative ring, together with the two forms of the Brahmagupta–Fibonacci identity that imply it — so that the reason it holds, rather than the expansion, is what is recorded.
For every integer the displayed family is a positive pairwise distinct solution; the parametrisation is injective; the set of quadruples it produces is infinite; and no member is a nontrivial integer multiple of another, each member being primitive.
The equivalence of with ; the parity statement that matching entries share a parity after at most one swap; and the resulting existence of the half-sum variables satisfying .
For all integers with there are integers with , , , — the coordinate form of the statement that a rank-one matrix factors through the integers.
The result. Taken together, the reverse chain converts the Diophantine equation into four free integer parameters, at the cost of one possible swap. In that form every question about the solution set becomes a question about four independent variables, which is what makes energy estimates, density statements and searches for primitive solutions tractable. The chain also isolates where integrality enters: over a field the parametrisation of is formal, so the content is carried entirely by the parity step and by divisibility over .
Formalizing it. None of the mathematics is new, and that is the point: the value here is a development in which each link is a reusable statement with explicit hypotheses. Three conventions make the nodes reusable rather than bespoke. The algebraic identity is proved over a general commutative ring, not over . The positivity and distinctness of a family are packaged as one strict chain rather than as a list of inequalities, since later arguments use the ordering, not merely the disequalities. The parity issue is isolated into a single node stating a disjunction, instead of being discharged by case splits buried inside a later proof. Conversely, the shape of the final theorem records honestly what is not claimed: parameters are not unique, and no normal form is asserted.
As difficulty, the early nodes have short proofs, while completeness requires the full chain and is the substantial part of the mission.
The obvious first idea is to use the Gaussian integers: and have the same norm, so factor both and compare. It fails. Equal norm does not make two Gaussian integers associates or divisors of one another — and both have norm and are related by no divisibility — because uniqueness of factorisation regroups prime factors in ways that the norm alone cannot distinguish. The correct route recovers the four parameters from the product equation instead, and there the friction is entirely arithmetic:
Clearing halves. The substitution is not available for arbitrary solutions: forces only that the multiset of parities of matches that of , so may have different parities and no integer may exist. The example shows this is not vacuous, and it is why the goal carries a swap.
Factoring . Taking yields , with , and Euclid's lemma then forces and . The degenerate case — where the gcd vanishes and no cancellation is possible — must be handled separately, and because the variables range over rather than , every divisibility step must be tracked with signs. Working over a ring where division is available would delete both issues and with them the entire content of the statement.
Even.A trained neural network is used through its predictions, while its parameters are the coordinates in which training takes place. Distinct parameter vectors can describe exactly the same prediction function. A proposed explanation of generalization based on the shape of the parameter-space loss therefore needs to account for these equivalences. This mission concerns Hessian sharpness: the spectral norm of the matrix of second derivatives of the loss at a minimum. The question is whether that number is intrinsic to the predictor or can change without changing any prediction.
Dinh, Pascanu, Bengio, and Bengio establish that, for a one-hidden-layer rectified network, every sufficiently differentiable critical minimum with nonzero Hessian has equivalent parameterizations of arbitrarily large Hessian sharpness. The formalization target is their Section 4.2, Theorem 4, PDF pp. 5–6. The goal theorem and both supporting milestones now have accepted Lean proofs on Prove2Me. This public research-paper mission is complete.
The immediate historical sequence is:
Fix positive integers and , the input dimension and hidden width. Let and be the network's weights. For an input , define
This is a bias-free network with one hidden layer, rectified activation, and a scalar linear output. Its parameter vector has coordinates and the Euclidean norm. A function-based loss is a real-valued functional of the entire prediction function, giving . The Hessian targets assume is continuous. These conventions come from Sections 2–3, PDF pp. 2–4, Definition 3.
Two parameters are observationally equivalent if their predictions agree on every input. For a positive real number , the layer scaling is
The definition rescales the incoming and outgoing weights in opposite ways. It is the transformation in Section 3, Definition 5, PDF p. 4.
Write for the first Fréchet derivative and for the second derivative. The local differentiability condition requires to be differentiable throughout a neighborhood of , with differentiable at . This states the regularity needed for the paper's Hessian notation explicitly, without requiring global smoothness or continuous second derivatives. A critical local minimum satisfies and has no smaller loss in some neighborhood; it may belong to a continuum of minima.
The first milestone formalizes the scaling consequence of positive ReLU homogeneity in Theorem 1 and Definition 5, PDF p. 4:
and is a local minimum precisely when is. These statements hold for every parameter and every ; the milestone itself requires no loss regularity.
The second milestone is Theorem 3, Section 4.2, PDF p. 5. At every point satisfying the stated local differentiability condition,
for all parameter directions . The same regularity holds at the rescaled point. This is the coordinate-free form of the paper's gradient formula and Hessian congruence with .
The goal is Theorem 4. If is a critical local minimum with the stated differentiability and , then
For that same rescaling, predictions and loss agree with the original ones, and the transformed parameter remains a critical local minimum with the required differentiability. The subscript denotes the Euclidean spectral norm. The source statement and its interpretation are in Section 4.2, PDF pp. 5–6. The relevant displays in all three targets are unnumbered.
The result separates prediction behavior from this particular numerical measure of parameter-space curvature. Pointwise identical predictors have identical function-based evaluation losses wherever those are defined, even though their Hessian sharpness can be made arbitrarily large under the stated conditions. This is the scope of the obstruction: it concerns the unnormalized Euclidean Hessian norm and this rescaling symmetry. It does not assert that training reaches every point on a scaling orbit or supply a numerical bound on test error. Theorem 4 and following discussion, PDF p. 6.
The completed Lean development connects an explicitly computed ReLU prediction function to its actual first and second derivatives. It provides reusable results about invariant losses, transport of local minima, and curvature under linear changes of parameters. All three published theorem statements were proved unchanged and accepted on 26 September 2026. Both milestones are complete, and the goal has no remaining open leaves.
ReLU is not differentiable at every activation boundary. The loss-level local regularity must therefore be retained rather than inferred from the network's syntax. A nonzero symmetric matrix alone is also insufficient for the sharpness claim: local minimality supplies an additional sign constraint. Finally, the second derivative is an operator on the entire parameter space; bounds for a single arbitrarily chosen scalar model do not establish the quantified network result. These are obligations of the formal proof, not hypotheses assuming the desired transformation identities.
Parameters are represented by EuclideanSpace over the disjoint union of
first-layer matrix coordinates and output-weight coordinates. This retains the
sum-of-squares geometry rather than a product maximum norm. The Hessian is the
derivative of the actual Fréchet derivative, represented as a continuous bilinear
form. Its operator norm is the spectral norm under the Euclidean/Riesz
identification. The regularity condition excludes reliance on default derivative
values at nondifferentiable points.
The statement covers every positive input dimension and hidden width, arbitrary function-based losses with the specified regularity, and arbitrary qualifying minima. It imposes no separate nonzero-weight or active-neuron assumption. An input or output weight block may vanish when the loss hypotheses still hold. The nonzero-Hessian requirement is essential. Scaling by zero or a negative number is outside the claim. No probability model, random initialization, sampling measure, or training algorithm is assumed.
The mission focuses on the single-hidden-layer Hessian result. Volume flatness,
the multiple-eigenvalue deep-network theorem, and other reparameterizations
remain separate results in the paper. The local environment is Lean 4.30.0 with
supported Mathlib revision c5ea00351c28e24afc9f0f84379aa41082b1188f.
A neural network is nonlinear in its parameters, but a small change in those parameters changes its predictions through a Jacobian. The neural tangent kernel is the Gram kernel of that Jacobian: it records which changes in predictions can be produced by common parameter updates. An initialization limit identifies a deterministic object behind this random kernel. It supplies a mathematical starting point for studying wide networks through kernel methods, before addressing the additional question of how the kernel changes during training. Jacot, Gabriel, and Hongler establish this initialization limit in Section 4.1, Theorem 1, PDF p. 5.
The requested result is already a theorem of the paper. The open work here is its formal proof in Lean, including the probability model and the order of limits. The mission is classified as OpenProblem at the request of its proposer; that label does not assert that the underlying mathematical result remains an unsolved research question.
The source appeared in 2018 and was published at NeurIPS 2018; this formalization fixes arXiv version 4, dated February 10, 2020, so that page references and conventions remain stable. Its Appendix A explicitly distinguishes the sequential limit proved there from a possible stronger simultaneous-width limit.
Fix positive integers and , the input and output dimensions, a hidden-layer count , a bias scale , and a Lipschitz function . Write for the number of affine layers, with , , and positive hidden widths . The parameters are all entries of the weight matrices and bias vectors. Every parameter is sampled independently from .
For an input , let and define
At each hidden layer, coordinatewise. The output is , with no final activation. These are the conventions of Section 2, PDF pp. 2–3. Matrix storage order in Lean uses destination then source; the displayed operation is unchanged.
For output coordinates , set
The sum includes every weight and every bias, as in Section 4, PDF p. 5.
The covariance kernel starts with
Given a centered Gaussian pair with covariance matrix obtained by evaluating on , define
The deterministic limiting NTK is
These recurrences appear in Section 4.1, Proposition 1 and Theorem 1, PDF p. 5; their displays are unnumbered.
The goal is Theorem 1, on every fixed finite family of inputs and for every :
Here is one when the output coordinates coincide and zero otherwise. The limit takes first, then , through , precisely as specified in Appendix A, PDF p. 11, and Appendix A.1, PDF pp. 12–13.
Two supporting milestones expose the required mathematical content. First, the recursively defined has positive semidefinite Gram matrices on every finite input family and satisfies . This is a paper-derived well-definedness obligation for the covariance in Proposition 1. Second, Proposition 1 asserts joint convergence in distribution of to the centered Gaussian vector with covariance . This expresses the paper's independent output Gaussian processes through all their finite-dimensional distributions.
The result connects an explicitly parameterized random finite network to a deterministic kernel computed from its activation and depth. All output correlations, bias contributions, and layer normalizations remain visible in that connection. It would provide a checked foundation on which a separate training-stability development could build.
The formal contribution is the passage from finite random Jacobians to the limiting kernel. It does not assume that the empirical NTK already equals its limit. Nor does the goal claim convergence of a training trajectory, positive definiteness on a sphere, an early-stopping guarantee, or a generalization bound; those are separate results and questions in the source.
The parameter space changes with the widths. Outputs, hidden activations, and their parameter derivatives are dependent random quantities, so the limit of their products requires more than a scalar law of large numbers. The weak Gaussian limit alone also does not justify substituting an arbitrary discontinuous derivative into expectations. The Lipschitz-only hypothesis is part of the target and must be retained, including for nonsmooth activations. Remark 3, PDF p. 5 identifies almost-everywhere differentiation as the relevant convention.
Lean represents parameter coordinates by a finite dependent index carrying a layer, destination neuron, and optional source neuron; the missing source denotes a bias. Initialization is the finite product of Mathlib's standard Gaussian measures. Network outputs are obtained by the displayed recursion, and NTK entries use actual Fréchet derivatives in coordinate directions. Mathlib's derivative is zero where differentiation fails; the proof must establish that the exceptional parameters are null under the stated initialization law.
Centered Gaussian laws use Mathlib's multivariateGaussian, including singular covariance. The covariance-validity milestone must justify its covariance interpretation. No invertibility, distinct-input, smooth-activation, or positive-definite-kernel assumption is added. Positive actual hidden widths are indexed as for , a cofinal reindexing. Depth one, constant activations, repeated or zero inputs, and empty finite families are included. The empty family is harmless because the same theorem quantifies over every nonempty family as well.
The sequential filter puts the last hidden width outermost. For two hidden widths, a probability tolerance is met by first choosing a threshold for , then a threshold for that may depend on . There is no uniform limit over the entire input space and no simultaneous-width assertion. The development uses Lean 4.30.0 and supported Mathlib revision c5ea00351c28e24afc9f0f84379aa41082b1188f. The model and statements are locally checked; the three theorem proofs remain open. Contributions to Gaussian covariance consistency, finite-dimensional distribution limits, almost-everywhere network differentiation, and the NTK limit are in scope.
Training a machine-learning model often means choosing a vector of parameters to minimize an average loss. Evaluating the full gradient can require processing an entire dataset. A stochastic-gradient method instead updates the parameters using a random direction obtained from a smaller amount of information. Its computational appeal raises a mathematical question: which assumptions on those directions and the stepsizes guarantee progress, and what kind of convergence follows?
This mission formalizes the core convergence theory in Section 4 of Bottou, Curtis, and Nocedal, Optimization Methods for Large-Scale Machine Learning. The results distinguish strongly convex objectives, where expected objective error can be controlled, from general smooth objectives, where the guarantee concerns gradients. They also distinguish constant stepsizes, which leave a noise-dependent error bound, from diminishing stepsizes.
The mathematics targeted here is already proved in the literature; the task is its Lean formalization, not a claim that these convergence results are unresolved research conjectures.
Let be differentiable with an -Lipschitz gradient, where . On a probability space , let contain the history before step . Starting from a deterministic vector , the algorithm uses positive deterministic stepsizes and random directions to update
The state is measurable with respect to ; the direction is measurable with respect to and has a finite second moment. Conditional assertions hold almost surely. This uses the adapted-process formulation expressly permitted in footnote 4, PDF p. 22, rather than requiring independent sample seeds. The local index corresponds to the paper's . Algorithm 4.1 and footnote 4.
Write for conditioning on . The moment conditions use constants and :
Define . The iterates lie almost surely in an open region on which for a real lower bound . These are Assumptions 4.1 and 4.3, PDF pp. 23–24, equations (4.6)–(4.9). Source.
The goal is Theorem 4.10, Section 4.3, PDF p. 33, equations (4.30a)–(4.30b). Suppose
For , establish both
There is no convexity assumption and no restriction that the initial stepsizes already satisfy a small-step bound. Theorem 4.10.
Four milestones capture the surrounding theory. Lemma 4.4 gives the two successive conditional expected-descent inequalities (4.10a)–(4.10b), PDF pp. 24–25. It is a common input to the convergence results. Theorem 4.6 gives a geometric upper bound for strongly convex objectives with a constant stepsize. Theorem 4.7 gives the corresponding bound for . These are parallel strongly convex targets, not prerequisites for the nonconvex goal. Theorem 4.8 gives finite-horizon sum and average squared-gradient bounds for general objectives with a constant stepsize. Section 4.
For example, if is the strong-convexity constant, , and , Theorem 4.6 states, with and ,
The upper bound tends to ; this does not assert that the actual expected error tends to . Every milestone retains the paper's constants and all displayed conclusions. Equations (4.13)–(4.14), PDF p. 26.
The result explains precisely how noise and stepsize interact. The general-objective goal guarantees that the stepsize-weighted expected squared gradients average to zero even when . The strongly convex milestones quantify objective error and the effect of initialization. These results concern the stated quantities; they do not assert convergence of iterates, global optimality for a nonconvex objective, or almost-sure convergence. Sections 4.2–4.3.
A completed development would provide reusable Lean results for smooth objective functions, conditional moment bounds, stochastic updates, and expected convergence. The proposed statements are open proof obligations. Compilation establishes that the definitions and statements are well formed, not that their convergence claims have already been proved.
Finite conditional expectations must be connected to unconditional integrals without relying on total-function defaults. The infinite-horizon result also requires careful handling of a finite initial segment: square summability gives eventually small steps, not a bound at every step. Strong convexity must justify the objective-gap estimates and the properties of the optimum. Treating a descent recurrence as a hypothesis would omit the analytic content that this mission is intended to formalize.
The model uses real finite-dimensional Euclidean space, Mathlib gradients, filtrations, Bochner conditional expectations, and ordinary real integrals. The probability space is arbitrary; no finite-support or standard-Borel restriction is imposed. Directions have explicit finite second moments, making the finite-expectation convention in the paper visible. Square integrability of iterates and integrability of losses are consequences to establish, not extra model fields.
Strong convexity uses Mathlib's StrongConvexOn, equivalent here to Assumption 4.5's first-order inequality. The optimum is defined as the infimum of the range of , with its finiteness to be derived in the strongly convex branch. That branch requires : the paper's deduction implicitly uses a nontrivial space. The nonconvex statements allow . Zero noise is allowed. Finite-horizon averages require ; the value assigned at does not affect an asymptotic limit.
Contributions to the conditional-descent infrastructure and any of the four milestones are welcome. Variance reduction, Newton-type methods, and the remainder of the survey are outside this initial mission.
For every integer base , a finite-prime weighted summability witness on a positive-integer host makes the reciprocal Mersenne series irrational on every infinite subset of . A base-two witness gives that conclusion at every integer base. This is the source paper's proved Theorem 1; Erdős's unrestricted question for every infinite support remains outside its conclusion.
For an integer , write . Given a finite nonempty set of primes, let be the -part of , and set
All support elements are positive. The prime set specifies the weight, not which exponents may belong to the support; the weighted series must also converge.
Theorem 1 has two clauses for an infinite positive-integer host :
In each clause is finite and nonempty. In the second, one prime witness for is fixed before choosing and . Taking recovers the two direct assertions. The public formal main item states both hereditary clauses and has an accepted proof in the pinned Lean 4.30 environment.
Since , this criterion includes reciprocal-summable supports. The paper also gives an explicit with divergent reciprocal mass but finite weighted mass. The inherited conclusions let another formal result use one certified host for many infinite thinnings. The already proved Lean result makes the host criterion and its dependencies available for direct import; new applications can check the exact premise they need against the public statement.
Reciprocal summability cannot bound the tail for every weighted support. A faithful statement also has to preserve the different order of prime, subset and base quantifiers; dropping fixed-base inheritance changes Theorem 1.
The formal support is a Set ℕ, and 0 ∉ H enforces positive exponents. FinitePrimeWeighted contains one finite nonempty set of primes and summability of its weighted terms. The public main item joins two accepted Lean results: the fixed-base hereditary theorem and the binary-host all-base theorem. These statements and their public definitions can be reused in the same pinned environment. The later no-cover host is a separate result; it is not a clause of Theorem 1 or the paper's example. Will Cook is the named paper author; the paper discloses substantial AI-assisted research and drafting and does not claim independent human verification of every proof. Erdős’s earlier criterion and later platform contributions carry separate credit.
Solve a consistent system , with of full rank and . Kaczmarz's method (1937) projects the current iterate onto the solution hyperplane of one equation at a time. The cyclic version converges, but its rate depends on the order of the rows and has no clean bound in terms of a condition number.
Strohmer and Vershynin (2009) pick row at random with probability and prove
The rate does not depend on the number of equations .
A single projection can barely reduce the error, when the error is almost orthogonal to the chosen row. On average it always does. If is drawn with probability , then
Pythagoras for one projection then gives ; induct on .
EuclideanSpace ℂ (Fin n) and matrices in Matrix (Fin m) (Fin n) ℂ. Mathlib's inner product is conjugate-linear in its first argument, which is why is a conjugated row.expErrSq is an explicit finite sum, so no measure theory is needed. The tower identity is a milestone.A standard way to prove that a real number is irrational is to produce integer linear forms that are nonzero but arbitrarily small: if were rational, then would be a nonzero integer of absolute value below once the form is smaller than . This is the shape of every hypergeometric construction of linear forms in odd zeta values — Rivoal's proof that infinitely many are irrational and Zudilin's proof that at least one of is irrational both produce such forms and read off irrationality (of at least one member of a finite set) from a determinant condition.
The same reduction is useful in the other direction: it isolates exactly what a construction has to supply — small forms — from the arithmetic that consumes them. This mission formalizes that abstract layer: the criteria that turn small integer forms into irrationality, together with the positivity and quadrature lemmas used to certify that a form is nonzero.
The material is distilled from a research note on (Xu, 2026). That note does not prove the irrationality of , and nothing in this mission depends on whether it can be: every statement below is a statement about real numbers, integer linear forms, real polynomials, and finite sums, with and every other specific constant removed.
All objects live over .
Irrational x is Mathlib's predicate: as a real number.Fin 5.Polynomial.taylor u₀ p is the Taylor expansion of about ; its coefficients
are nonnegative when taylor u₀ p for every .Matrix.mulVec M v is the usual matrix–vector product over Fin 5; denotes
tsum over a Summable family.$$ \bigl(\forall \varepsilon>0,\ \exists, b,a\in\mathbb{Z}:\ b+ax\neq 0\ \wedge\ |b+ax|<\varepsilon\bigr)\ \Longrightarrow\ \text{ irrational.}
The goal is the weakest non-vacuous statement in the family: it assumes one form at a time and no rate. ### Stronger — the two-form criterion\bigl(\forall \varepsilon>0,\ \exists, b_1a_1b_2a_2\in\mathbb{Z}:\ b_1a_2\neq b_2a_1\ \wedge\ |b_1+a_1x|<\varepsilon\ \wedge\ |b_2+a_2x|<\varepsilon\bigr)\ \Longrightarrow\ \text{ irrational.} $$
Targets 1–6 correspond to the mission's milestones; the goal and the two-form criterion close the mission.
The results. The two criteria are the exact statements that a linear-form construction has to feed, and they are what turns "small forms exist" into irrationality without any analytic input. The supporting lemmas are the standard certificates used to show a form is nonzero — which is the other half of the argument, and the half that finite checks can actually settle.
Formalizing them. All eight statements are elementary and already have informal proofs;
each also has a locally compiled Lean proof (lake env lean, exit 0, no sorry) against
Lean 4.33.1 and Mathlib revision 0df444a3, held by the mission captain and published in
the companion repository. What this mission adds is platform verification plus reusable
infrastructure: the moment-matching quadrature lemma, the weighted-average and mediant
inequalities, and the positivity lemmas are stated in a form that transfers to any setting
where five-point data is certified by moments. Alternative proofs, generalizations to
-point quadrature, and sharper variants are welcome contributions.
The integrality step, not the estimate. In the one-form criterion the obvious move —
take — leaves the real inequality , which says nothing
until the form is rewritten as with ; only then does
force vanishing and contradict nonzeroness. Writing that rewrite in Lean
means carrying the cast from through field_simp and back through
exact_mod_cast, which is where naive attempts break.
Moment matching needs a degree bound, not interpolation. The quadrature lemma is not
"five values determine a degree- polynomial": the hypothesis is about the functional
on the five monomials, and the proof must expand an arbitrary in the monomial
basis (as_sum_range_C_mul_X_pow' with natDegree < 5) and commute two finite sums.
Sign conditions are load-bearing. In target 6, the shared-sign hypothesis is what turns a vanishing weighted sum into vanishing samples; the root-counting step then needs injective nodes and positive weights. Dropping either silently makes the statement false, and both are easy to forget.
Everything is over ; no complex numbers appear. The quadrature statements are
fixed at five nodes (Fin 5) and degree , as in the source note; the functional
is a Polynomial ℝ →ₗ[ℝ] ℝ, not a measure. natDegree (not degree) is the degree
notion. The infinite sum in target 5 is tsum with an explicit Summable hypothesis.
Matrices are Matrix (Fin 5) (Fin 5) ℝ with mulVec; irrationality is Mathlib's
Irrational.
Ruled out: a quadrature statement in which the weights are unconstrained by positivity but the conclusion is strengthened to a lower bound — target 1 assumes only moment matching, and any strengthening must add hypotheses rather than reinterpret the existing ones. A "criterion" whose hypothesis is vacuous for every real is likewise out of scope: both criteria are satisfiable hypotheses, not vacuous ones.
Infrastructure needed: the polynomial expansion and evaluation lemmas (as_sum_range,
eval_eq_sum_range'), Finset sum rearrangement, Matrix.mulVec, Summable.tsum_lt_tsum_of_nonneg,
and irrational_iff_ne_rational. The quadrature lemma, the mediant inequality, and the
positivity lemmas are reusable beyond this mission.
This mission formalizes A. Garrido, An introduction to amenable groups, lecture notes from four talks at the Oxford Advanced Class in Algebra, Michaelmas 2013 (archived PDF) — its Section 4, the (first) Grigorchuk group and its solution of half of the von Neumann–Day problem.
The first two Garrido missions, Amenable Groups I and Amenable Groups II (the Banach–Tarski paradox), established the inclusions between the elementary amenable groups, the amenable groups, and the groups with no free subgroup of rank two. "The von Neumann–Day problem asks whether these inclusions are strict" (p. 12). Ol'shanskii settled ; "The other part of the problem was solved in 1985 by Grigorchuk" (p. 12), with the theorem this mission targets.
Chou's theorem that every torsion group in is locally finite "traces a clear route for solving the Day problem. Namely, it suffices to find an amenable torsion group which is not locally finite" (p. 13). The Grigorchuk group is such a group: a finitely generated, infinite group of automorphisms of the binary tree in which every element has order a power of , and whose growth is subexponential, so that it is amenable.
The infinite rooted binary tree has as vertices the finite words in , and its automorphisms are the permutations of the vertices that preserve length and prefixes. The Grigorchuk group is generated by four of them: exchanges the two subtrees below the root, and , , fix the first level and are defined recursively by , , , meaning that acts on the subtree below as and on the subtree below as , and so on.
is the subgroup of fixing every vertex of level . An element acts on each of the subtrees below level as a tree automorphism, its section there. sends to the tuple of these sections, and for , is its section below the vertex . is the word length with respect to .
"The (first) Grigorchuk group is amenable but not elementary amenable" (p. 12). This is the goal because it is the theorem the section proves and the one that separates from .
Conjugation by exchanges the two sections of an element of ; is a Klein four-group and is generated by ; is infinite, since maps onto it; and the maps are monomorphisms.
Every element of has order a power of , so is an infinite finitely generated torsion group and, by Chou's Theorem 4.2, not in . The notes omit the proof of Proposition 4.7 and refer to de la Harpe's book; it is a milestone to be proved here.
The length contraction for , the index , and a general inequality comparing the balls of a group with those of a subgroup of finite index give subexponential growth (Theorem 4.9); Theorem 3.8 of the first Garrido mission then gives amenability.
The Grigorchuk group is one of the central examples of geometric group theory: the first group of intermediate growth, a finitely generated infinite torsion group, and the separation of amenable from elementary amenable groups. Neither Mathlib nor the platform has it, and a search of Lean Pool, Tau Ceti and the Palomar registry found no formalization; Mathlib's only mention is a bibliography entry in its Schreier-graph file. The tree-automorphism definitions here are reusable for other groups acting on the binary tree. Nothing here is a new mathematical result: all of it is classical, and the work is formalization.
Lemma 4.8 is the hard step: a careful count, over three levels of sections, of how a shortest word shrinks and how many cancellations occur. Proposition 4.7 has no proof in the notes; the standard argument is an induction on word length through the sections. The growth argument of Theorem 4.9 is an estimate on built from Lemma 4.8 and the ball inequality.
The tree is modelled by its vertices, List Bool, and is a subgroup of the group of
tree automorphisms, following the notes' "a group of automorphisms of ". The generators are
defined by Garrido's recursion, and the bundle proves that each is an involutive automorphism;
sections are defined for every automorphism and every vertex, with a proof that they are
automorphisms. The sections of and are shown to lie in as part of the
milestone rather than assumed.
One trivialising formalization is ruled out: is not taken to be an abstract group given by a presentation or by fiat, but the concrete group of tree automorphisms the notes define, so that the finiteness, torsion and growth statements are about that group.
Definition 4.4 and Lemma 4.5, the ordinal hierarchy , and Theorem 4.3 are covered by the Chou 1980 mission, which proved Theorem 4.3 with an inductive predicate in place of the ordinals; Theorem 4.2 enters as a reference. Ol'shanskii's is outside the notes' scope ("beyond the scope of these talks", p. 12) and is not formalized.
The Shape Zero model reaches the Fano plane — the seven-point, seven-line configuration behind the seven imaginary units of the octonions — by a combinatorial route: C1 Formal Proofs, §3, Theorem 3.6 ("Roles Force Fano") states that any Steiner triple system admitting a role colouring is the Fano plane. Its proof derives only that there are points, and takes the last step on trust: C1 §3 asserts "the unique STS(7) (the Fano plane PG(2, 2))" in Theorem 3.3 and justifies it with one sentence, "Uniqueness of STS(7) is classical."
The companion mission The role postulates force exactly seven points proved the point count and deliberately stopped there. This mission supplies the missing step and completes the chain:
The attack path is the standard textbook proof of the uniqueness of STS(7), supplying the step C1 §3 calls classical. The proof goes through three milestones: a normal form around one point, exactly two completions of it, and an explicit relabelling of each completion onto the Fano plane. The line count (seven lines, three through each point) and the meeting property (any two lines meet in exactly one point) then follow as corollaries of the goal. C1 gives no argument for this step; the milestones below are that classical argument, not C1's.
What this mission does NOT prove.
A Steiner triple system on the points is a family of -point subsets, called lines, such that every pair of distinct points lies on exactly one line. A role colouring gives each point of each line one of three roles so that the three points of a line get different roles and every point takes every role exactly once.
The Fano plane is the Steiner triple system on with lines modulo :
This is the companion mission's published definition RolesForceSeven.fano, labelled . (C1 §5 writes the same lines on ; this mission uses the companion mission's labelling.)
The definitions RolesForceSeven.STS, RolesForceSeven.RoleColouring and RolesForceSeven.fano are imported from the companion mission, not restated, so both missions refer to the same objects. The one new definition is FanoUnique.IsFano S: there is a bijection from the points of to with the Fano lines.
This is FanoUnique.sts7_is_fano.
The goal follows from M1, M2 and M3. (These are M3, M4 and M5 in the draft's original numbering.)
Both hold in the Fano plane and are preserved by relabelling, so they follow from the goal.
For , a Steiner triple system on points with a role colouring is the Fano plane up to relabelling (FanoUnique.roles_force_fano). The companion mission's goal gives ; the goal of this mission does the rest. The hypothesis is kept, following the erratum to C1 §3: the empty system satisfies every other condition and is not the Fano plane.
The result itself. Together with the companion mission, it makes C1 Theorem 3.6 fully machine-verified: the role postulates force not only seven points but the Fano plane itself, up to relabelling.
Formalizing it. C1 cites the uniqueness of STS(7) as classical. It was checked numerically — exhaustively over labelled systems — but never proved in the C1 package; this mission proves it.
| check | result |
|---|---|
| Steiner triple systems on 7 labelled points | 30 (classical count ) |
| of those, isomorphic to the Fano plane | 30 of 30 |
| any two distinct lines meet in exactly one point | true in all 30 |
| completions of | exactly 2 (A and B) |
| swapping points 1 and 2 carries A to B | true |
Moderate. M3 is a finite computation. The work is in M1 — building the relabelling bijection from the three lines through a point — and M2, the case analysis on the line through points and , which forces the remaining lines. Corollaries A and B follow from the goal by relabelling. Exhaustive search over all line families () is not feasible, so the structured proof is needed.
Fin n; lines are Finset (Fin n); the definitions are the companion mission's, imported unchanged.Fin n ≃ Fin 7; it forces and exactly lines.This mission formalizes A. Garrido, An introduction to amenable groups, lecture notes from four talks at the Oxford Advanced Class in Algebra, Michaelmas 2013 (archived PDF) — its Section 1.1, the Banach–Tarski paradox, together with the inclusion that the notes draw from it.
The notes open with the theorem that started the subject. In 1924, they recall, Banach and Tarski "proved a remarkable theorem which is nowadays stated as 'given a ball in 3-dimensional space, there is a way of decomposing it into finitely many disjoint pieces that can be rearranged to form two balls of the same size as the original one'" (p. 1). As the notes put it, "This counterintuitive result is essentially a statement about measure theory": no finitely additive, isometry-invariant measure defined on every subset of can give the unit ball a finite nonzero measure, so Lebesgue measure cannot be extended that way.
The reason is group-theoretic. The free group decomposes paradoxically under its own left multiplication, the rotation group contains a copy of , and a free action transports the decomposition to the sphere; Hausdorff's paradox and a countable correction give the sphere, and radial projection the ball. The same argument shows that a group containing cannot carry an invariant finitely additive probability measure — the inclusion of amenable groups into groups without free subgroups of rank two, whose converse was von Neumann's question.
This mission is the companion of the first Garrido mission, which formalized the measure-theoretic half of Section 1 (equidecomposability, the Banach–Schröder–Bernstein theorem, Tarski's theorem) and Sections 2 and 3.
A group acting on a set makes two subsets -equidecomposable, ,
when can be cut into finitely many pieces which, each moved by one element of ,
reassemble into ; a subset is -paradoxical when it contains two
disjoint proper subsets each equidecomposable with . Both are the published definitions from
the first Garrido mission, Equidecomposable and IsParadoxical, and paradoxicality is
defined for an arbitrary subset because the notes use it for and for
a ball.
The groups and spaces are the classical ones. is the unit sphere in
(Sphere n), with — Mathlib's
Matrix.specialOrthogonalGroup — acting by matrix-vector multiplication. is the group of
all isometries of (EuclideanGroup 3), acting by evaluation; it contains the
translations, the rotations and the reflections. A group acts freely (ActsFreely) when no
element other than the identity fixes a point. is FreeGroup (Fin 2), and "no free
subgroup of rank two" is the published Chou.NoFreeSubgroupOfRankTwo. The rotations and
of Proposition 1.6 are defined in the bundle with their matrices.
Every closed ball of positive radius in , and itself, is -paradoxical: "Any solid ball in is -paradoxical. Furthermore, is -paradoxical" (p. 3).
This is the goal because it is the theorem the section is named for and the one the notes build to.
is paradoxical, and so is every nonempty set on which it acts freely (Proposition 1.5); contains a free group of rank two (Proposition 1.6); the sphere minus a countable set is paradoxical (Theorem 1.7, Hausdorff's paradox); a countable set can be absorbed (Proposition 1.8); so the sphere is -paradoxical for (Corollary 1.9). The steps that the notes state inside proofs are milestones of their own: the two rotations and generate a free group, a nontrivial rotation fixes exactly two points of , and a countable subset of has a rotation whose positive powers move it off itself.
No rotation-invariant finitely additive probability measure lives on all subsets of for ; no isometry-invariant finitely additive measure on all subsets of gives the unit ball a finite nonzero value; and an amenable group has no free subgroup of rank two.
The Banach–Tarski paradox is one of the best-known theorems of twentieth-century mathematics,
and it is the reason finitely additive measure theory and amenability exist as subjects.
Neither Mathlib nor the platform has it. It has been formalized in Lean outside both:
aetilley/banach-tarski, following Tomkowicz and Wagon,
proves that the closed unit ball in is paradoxical under its isometry group, and is a
candidate for inclusion in
Lean Pool. This mission follows Garrido's statements instead,
and publishes each step as a theorem other work can import. Mathlib has the equidecomposition machinery in
Equidecomp.lean
and the ping-pong lemma, which is the natural tool for Proposition 1.6, but no paradoxical
decomposition of anything.
The inclusion completes, with the first Garrido mission's , the display on p. 11 of the notes. Nothing here is a new mathematical result: all of it is classical, and the work is formalization.
Three steps carry the weight. The freeness of and is a computation the notes defer to Wagon's book: a nonempty reduced word is shown to move a suitable vector, by tracking coordinates of the form with integers reduced modulo . The absorption of a countable set needs a rotation whose powers move the set off itself, which is a countability argument about angles. And the passage to for is only sketched in the notes ("by the same arguments as in Proposition 1.8"): the induction lifts a paradoxical decomposition of to minus two poles, and the poles must then be absorbed by a rotation of .
Transferring the sphere to the ball needs radial projection and the absorption of the center, again by a rotation of infinite order, this time about an axis that misses the center.
Rotations are matrices: is Matrix.specialOrthogonalGroup (Fin (n + 1)) ℝ,
acting on the sphere by mulVec; the bundle proves that an orthogonal matrix preserves the
Euclidean norm, so the action is well defined. is the full group of isometries
EuclideanSpace ℝ (Fin 3) ≃ᵢ EuclideanSpace ℝ (Fin 3), as in the first Garrido mission's
Corollary 2.5, with an action by evaluation defined in the bundle.
Committed conventions. "Solid ball" is read as a closed ball Metric.closedBall c r with
, for every center . "Countable" is Set.Countable, which includes finite sets.
Proposition 1.5's second part assumes the set nonempty, since the empty set carries a free
action and is not paradoxical. The p. 1 consequence asks for a finite nonzero value on the
unit ball: the notes say only "non-zero", and the measure that is on every nonempty set
satisfies that. Both departures are named in the statements' descriptions.
One trivialising formalization is ruled out: equidecomposability with the whole group allowed to
act on each piece by an arbitrary bijection would make every two sets of the same cardinality
equidecomposable. Here each piece is moved by a single group element, through Mathlib's
Equidecomp, and paradoxicality needs two disjoint proper subsets.
A complete development needs the sphere and its rotation action, the isometry group of , and the combinatorics of paradoxical decompositions; the definitions are reusable for any later work on the paradox. Contributions are welcome on any milestone. Proposition 1.5 and the step on fixed points of rotations are the most self-contained entry points.
The locally compact and measurable versions of the paradox, and the questions of how few pieces suffice, are not in the notes and are not formalized. Tarski's theorem, the converse that a non-paradoxical set carries an invariant measure, is proved in the first Garrido mission and is not restated here.
The Shape Zero model (Shape Zero LLC, unpublished) predicts a propagation asymmetry: with a gyroscopic coupling of strength , a wave travelling one way oscillates at a slightly different frequency from the same wave travelling the other way, and the difference, , does not depend on the on-site stiffness . The companion mission The propagation asymmetry does not depend on the on-site stiffness proves this on a one-dimensional uniform lattice. The model's base is three-dimensional, where a wave also carries transverse wavenumbers. This mission extends the result to a uniform lattice with any number q ≥ 1 of axes, and shows that the asymmetry is independent of both the stiffness and every transverse wavenumber.
What this mission does NOT prove.
Fix real numbers (on-site stiffness), (neighbour coupling) and (gyroscopic strength), and a wavevector . The upper-branch frequency is
with the sum over all axes. Reversing the wave along axis 0 gives . In Lean these are PinnedAsymmetryQ.omega q K c β k (with Real.sqrt) and flip0 q k. The formula has been checked against the eigenvalues of the actual q = 3 lattice generator to across 216 wavevectors and three parameter sets.
This is PinnedAsymmetryQ.asymmetry. Neither nor any transverse wavenumber appears on the right.
The result itself. The goal isolates the part of the frequency that is exactly independent of the stiffness and of the transverse wavenumbers on a lattice of any dimension. At q = 3 it is the statement relevant to the model's actual base; at q = 1 it reduces to the companion mission.
Formalizing it. The q-dimensional statement had been checked numerically only (3,000 random parameter sets at q = 3: goal to ). A proof covers every , every wavevector and all real parameters.
Low. The asymmetry is a difference of two expressions whose square-root parts depend on and on every ; the point is that reversing axis 0 leaves the radicand unchanged, so the square roots cancel. M1 needs the radicand non-negative in order to square the square root.
[NeZero q]), so axis 0 exists. All parameters are arbitrary reals, with no sign conditions in the goal.Real.sqrt returns on negative inputs. The goal still holds there, because the two radicands are equal, so the two square roots are equal whatever value they take.Mathlib.Analysis.Real.Sqrt (Real.sqrt, returning on negative inputs). https://leanprover-community.github.io/mathlib4_docs/Mathlib/Analysis/Real/Sqrt.htmlThe Shape Zero model (Shape Zero LLC, unpublished) couples neighbouring nodes through a velocity-dependent force, one coupling matrix per link. The companion mission Zero net power forces every link coupling to be symmetric (rings of ≥ 3 sites) proves that a coupling doing no net work (a passive coupling) must have every link matrix symmetric — but only on a one-dimensional ring. The model's base is three-dimensional. This mission extends the result to a periodic cubic lattice with any number q of spatial axes, so it covers q = 3 directly and reduces exactly to the ring result at q = 1.
What this mission does NOT prove. As with the companion missions, commuting with the complex structure is not derived here; it remains a modelling premise. This mission shows only that passivity forces symmetry on every link in every direction.
Fix natural numbers (number of axes), (sites along each axis) and . A site is a point of the periodic cubic lattice; is the site one step forward or back along axis , wrapping around. Each link — a site together with an axis — carries its own real matrix , and each site carries a velocity . The force on site is
where the second term uses the matrix of the link behind . The total power is
In Lean, sites are Site q L = Fin q → Fin L, the step is shift x a s (update coordinate by in Fin L), and the power is PassivityTorus.power q L d W v. The coupling is passive when for every .
This is PassivityTorus.passive_iff_symm, for every and .
The result itself. It is the dimension-independent form of the passivity theorem: whatever the number of spatial axes, a per-link coupling does no net work for every motion exactly when every link matrix is symmetric. It removes the one-dimensional restriction from the step that justifies restricting the model's coupling class to symmetric matrices.
Formalizing it. The ring result has been machine-checked; the lattice extension had been checked numerically only (identity error at ). A proof covers every , and .
The algebra is the ring argument; the difficulty is bookkeeping. The incoming term must be reindexed by the one-step shift, which is a bijection of the torus, and the converse needs a test motion supported on two neighbouring sites and together with a proof that no other link joins them.
The hypothesis is necessary. At the step forward and the step back along an axis reach the same site. This is proved (in Lean, locally): for every , putting the same non-symmetric matrix on every link of the lattice gives exactly zero power for every velocity field, so passivity does not force symmetry there. Weakening the hypothesis makes the goal false.
[NeZero L] is needed for the literal in Fin L and is implied by in the goal.Mathlib.Data.Matrix.Mul (dot product ⬝ᵥ, matrix–vector product *ᵥ). https://leanprover-community.github.io/mathlib4_docs/Mathlib/Data/Matrix/Mul.htmlThe Shape Zero model (Shape Zero LLC, unpublished) makes one experimentally testable prediction: a propagation asymmetry. In a ring of oscillators with a gyroscopic coupling of strength , a wave travelling one way oscillates at a slightly different frequency from the same wave travelling the other way. The predicted difference is
where is the neighbour coupling and the wavenumber. The claim is that this difference is pinned: it does not depend on the on-site stiffness , even though each of the two frequencies does. Simulations of the model measured the linear asymmetry at , and times the predicted value at stiffness , and , i.e. protected to about . This mission proves the exact statement for a uniform lattice.
What this mission does NOT prove.
Fix real numbers (on-site stiffness), (neighbour coupling), (gyroscopic strength) and a wavenumber . Write
The upper-branch frequency on a uniform ring is
In the Lean development this is PinnedAsymmetry.omega K c β q, with Real.sqrt for the square root. When , is a root of the dispersion relation
This is PinnedAsymmetry.asymmetry. The right-hand side contains no . As an immediate consequence, for any two stiffnesses and the asymmetry is identical.
The result itself. The goal isolates the one quantity in the model's prediction that is exactly independent of the on-site stiffness: the direction-dependent part of the frequency. Each branch frequency depends on through the square root, but the difference between the two directions does not. M1 is what makes this a statement about the physical frequency rather than about an arbitrary expression, by showing the formula solves the model's dispersion relation.
Formalizing it. The algebra is elementary; the content is that the stiffness provably drops out, for every value of the parameters rather than at the sampled stiffnesses of a simulation. The formal statement also records precisely what is covered (the linear asymmetry on a uniform lattice) and what is not (the nonlinear coefficient and non-uniform stiffness).
The difficulty is low. The asymmetry is a difference of two expressions that each contain a square root depending on ; the point to establish is that the two square roots coincide, so that no stiffness dependence survives the subtraction. M1 requires squaring the square root, which is valid only when the radicand is non-negative.
Real.sqrt returns on negative inputs. The goal still holds in that regime, because the two radicands and are equal, so the two square roots are equal whatever value they take. For physical parameters (, ) the radicand is always non-negative.The development needs only Mathlib's real trigonometric functions and Real.sqrt.
Mathlib.Analysis.Real.Sqrt (Real.sqrt, returning on negative inputs; Real.sq_sqrt). https://leanprover-community.github.io/mathlib4_docs/Mathlib/Analysis/Real/Sqrt.htmlThe Shape Zero model (Shape Zero LLC, unpublished) couples neighbouring nodes on a ring through a velocity-dependent force, with one coupling matrix per link. A companion mission, The passivity-admissible couplings have dimension n² = dim u(n), shows that real matrices which are symmetric and commute with a complex structure form a space of dimension . That mission deliberately takes symmetry as given. This mission supplies the reason for it: a coupling that never does net work (a passive coupling) must have every link matrix symmetric, provided the ring has at least three sites.
Together the two missions give the chain
What these two missions do NOT prove. Commuting with is not derived here. It is the requirement that the coupling respect each node's complex structure, and in the model it is imposed, not forced by passivity. After both missions the proved content is: passivity forces symmetry, and symmetric -compatible couplings have the dimension of . The -compatibility step remains a modelling premise. In addition, the coupling space consists of the Hermitian matrices, which match in dimension; the Lie algebra itself appears only after multiplying by (Unitary group).
Let and be natural numbers with . A ring has sites labelled by , so site is next to site ; indices and are taken modulo . Each site carries a velocity vector , and each link carries a real link matrix . The force on site is
where the second term uses the previous link's matrix . The total power delivered by the coupling is
In the Lean development this is PassivityRing.power N d W v, with sites indexed by Fin N (whose addition and subtraction wrap around modulo ), vectors in Fin d → ℝ, and the dot product ⬝ᵥ. The coupling is passive when for every choice of velocities .
This is PassivityRing.passive_iff_symm. It holds for every and every family of link matrices, with no assumption relating different links.
The result itself. The goal turns a physical requirement — no net work for any motion — into an exact algebraic condition on each link separately. It is the step that justifies restricting the companion mission's coupling class to symmetric matrices, so that the dimension count applies to the passive couplings of the model rather than to an assumed class.
Formalizing it. The model's claim has so far been checked numerically at ring sizes . A machine-checked proof covers every and every , makes the role of the hypothesis explicit, and separates what is proved (passivity forces symmetry) from what remains a modelling premise (-compatibility).
The forward direction and the power identity are finite-sum bookkeeping. The central difficulty is the converse: the hypothesis constrains a single scalar quantity summed around the ring, and it must be shown to constrain each link matrix individually. On small rings this fails because distinct terms of the sum coincide, so the argument depends on the ring being large enough that neighbouring sites are genuinely distinct, and in Lean that is modular arithmetic on Fin N.
The hypothesis is necessary, not a convenience:
Weakening the hypothesis to , or dropping it, makes the goal false.
Fin N with its wrap-around arithmetic, so and go around the ring; [NeZero N] is required for the literal in Fin N and is implied by in the goal.W : Fin N → Matrix (Fin d) (Fin d) ℝ, not a single shared matrix, and no relation between different links is assumed.v : Fin N → (Fin d → ℝ).ℝ); symmetry is (W i)ᵀ = W i.M1 and M2 hold for every and carry no ring-size hypothesis; M3 and the goal require . The development needs only Mathlib's finite sums, dot products, matrix–vector products and Fin arithmetic.
Mathlib.Data.Matrix.Mul (dot product ⬝ᵥ, matrix–vector product *ᵥ). https://leanprover-community.github.io/mathlib4_docs/Mathlib/Data/Matrix/Mul.htmlThis mission formalizes A. Garrido, An introduction to amenable groups, lecture notes from four talks at the Oxford Advanced Class in Algebra, Michaelmas 2013 (archived PDF) — its Section 1.2, Section 2 and Section 3.
A group is amenable when its subsets can be measured in a way that translation does not disturb. Von Neumann isolated the notion in 1929 to explain the Banach–Tarski paradox: a solid ball in can be cut into finitely many pieces and reassembled into two balls of the original size, and the reason is group-theoretic rather than geometric — the rotation group contains a free group of rank two, while the isometry groups of and do not. No paradox is possible for a group carrying a translation-invariant finitely additive probability measure.
Mahlon Day proved in the 1950s that von Neumann's definition agrees with the existence of an invariant mean on bounded functions, moving the theory into functional analysis, and coined the word "amenable" as a pun on "mean"; the problem below was first stated in print, with von Neumann's name attached, in Day's 1957 paper. Følner gave a combinatorial criterion — a group is amenable exactly when it has finite subsets almost invariant under translation — now usually taken as the definition, and the link to growth.
The organizing question of the classical theory was the von Neumann–Day problem: writing for the elementary amenable groups, for the amenable groups and for the groups with no free subgroup of rank two, one has , and both inclusions were asked to be equalities. Both are strict. Ol'shanskii (1980) showed , and Grigorchuk (1985) showed with a group of intermediate growth. Chou (1980) supplied the structural facts about that the separation rests on.
Amenability is now basic vocabulary in geometric group theory, ergodic theory and operator algebras.
Let be a discrete group. A measure on , in von Neumann's sense, is a function assigning a value to every subset of — not merely to a distinguished -algebra — such that
for all and all disjoint . Only finite additivity is required; countable additivity together with invariance is impossible for a countably infinite group. is amenable if such a exists.
Two reformulations matter. A left-invariant mean is a positive linear functional on the bounded real functions with and , where . And satisfies the Følner condition if for every finite and every there is a finite nonempty with
where is symmetric difference. In the Cayley graph this says has small boundary relative to its size.
Against amenability stands paradoxicality. Two subsets of a -set are -equidecomposable, written , if can be cut into finitely many pieces which, after each is moved by a single element of , reassemble to ; and is -paradoxical if it has two disjoint proper subsets each equidecomposable with itself. A group that is paradoxical under left translation admits no invariant measure.
This is the goal because it bridges the combinatorial and measure-theoretic sides of the subject, and every later application of amenability to growth uses it in one direction or the other.
For a group , these four are equivalent: is amenable; there is a left-invariant mean on ; is not paradoxical; and has the invariant extension property.
Amenability passes to subgroups and quotients, is closed under extensions, and is closed under directed unions; hence all abelian and all virtually solvable groups are amenable, and .
Each of the three equivalent pictures serves a different purpose: the measure gives non-paradoxicality, the mean gives access to functional analysis and fixed-point arguments, and the Følner condition is what one can verify for a concrete group. Theorem 3.8 is the typical consequence — a group of subexponential growth is amenable — proved by exhibiting the balls of the word metric as a Følner sequence, which only the equivalence licenses.
Mathlib has very little of this. It names no definition of amenability:
FoelnerFilter.lean
says one "has not yet been given" for want of "a general consensus" on the right generality, and
writes the property out inline in the conclusion of IsFoelner.amenable, which is one direction
of the goal. Equidecomp.lean
has the equidecomposition machinery, with a TODO asking for the Schröder–Bernstein theorem for
equidecomposability that is Theorem 1.2 here.
This mission supplies the missing definitions, that Schröder–Bernstein theorem, the closure properties, and the direction of the Følner equivalence that is genuinely open. Nothing here is a new mathematical result: all of it is classical, and the work is formalization.
The Følner-implies-amenable direction is the easier one, and the natural construction almost works: given a Følner sequence , set . That limit need not exist. It must be replaced by a limit along a non-principal ultrafilter, or the measure obtained by compactness in .
The converse — amenable implies Følner — is where the content is, and no averaging argument reaches it. One has to produce, from a mean, finite sets that are almost invariant; the passage runs through a separation theorem in , the only step here needing a genuinely infinite-dimensional tool. The classical arguments provide no combinatorial route.
Two smaller obstructions are worth naming. Tarski's theorem — an invariant measure giving a set measure one exists precisely when that set is not paradoxical — is quoted without proof in the source and is the hardest single statement in the mission. And Theorem 2.6 rests on a finitely additive extension theorem for measures on a Boolean algebra, which is not the Carathéodory construction in Mathlib; Mathlib's is about outer measures and -additivity.
Amenability is IsAmenable G: the existence of with
, finitely additive on disjoint pairs, and invariant under left translation. The
codomain is the extended nonnegative reals rather than , to match the conclusion of
Mathlib's IsFoelner.amenable — which at with every set measurable is exactly
IsAmenable — so that theorem is directly usable; finite additivity and
force anyway, so nothing is added or lost.
Committed conventions. Means live on , realised as lp (fun _ : G => ℝ) ∞ —
not on all of , where invariance and normalisation are already
contradictory (proved for ),
so every statement about means would be vacuously unprovable. Normalisation is phrased via constantly- functions, to avoid depending
on the ring structure of . Cardinalities use Set.ncard, so no DecidableEq
instance propagates into the statements.
Paradoxicality is defined for an arbitrary subset, recovering the source's whole-space notion as
a special case, because the source states it for the whole space but uses it for subsets
throughout. Equidecomposability builds on Mathlib's Equidecomp, and growth on the published
Chou_Growth bundle, rather than either being redefined.
One trivialising formalization is ruled out: amenability requiring only and
additivity, without invariance, is satisfied by any normalised counting density and would make
the mission vacuous. Left-invariance is part of every definition here, and IsAmenable is
exhibited non-vacuously for finite groups.
A complete development needs finitely additive measures on a power set, invariant means on , the Følner condition and sequences, paradoxical decompositions, and a finitely additive extension theorem on a Boolean algebra; the definitions and the last of these are reusable beyond this mission. Contributions are welcome on any milestone. Proposition 2.2's closure properties are the most self-contained entry points, and Theorem 1.2 is the one Mathlib has explicitly asked for.
Two bodies of material from the source are deliberately out of scope, left for later missions in this series.
The geometric construction of the Banach–Tarski paradox — that contains a free group of rank two, the Hausdorff paradox, and the paradoxical decompositions of the sphere and the ball. This mission takes the measure-theoretic half of Section 1 and leaves the half about the -sphere. Tarski's theorem and the Banach–Schröder–Bernstein theorem are in scope despite being printed alongside that material, because both are equidecomposability combinatorics and both are needed by results that are in scope.
The Grigorchuk group — its construction on the binary rooted tree, the proof that it is amenable but not elementary amenable, and its subexponential growth. Theorem 4.2 and Theorem 4.3 are the exceptions, and they enter as references rather than targets.
Also out of scope: the locally compact case. The source gives most definitions for both discrete and locally compact groups, then says it will "mostly focus on discrete groups"; only the discrete case is formalized. Følner nets for uncountable groups are likewise omitted, as is the extension of Example 3.5 to finitely generated abelian groups, which the source leaves as an exercise.