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?
This mission formalizes A. Connes, J. Feldman and B. Weiss, An amenable equivalence relation is generated by a single transformation, Ergodic Theory Dynam. Systems 1 (1981) 431–450 (doi:10.1017/S014338570000136X).
A countable group acting on a measure space partitions it into countable orbits, and much of ergodic theory studies actions only through this orbit equivalence relation. The simplest relations are those of a single transformation, the orbits of an action of . Connes, Feldman and Weiss characterize exactly which relations are of this kind, up to null sets: the amenable ones, those carrying an invariant mean. Since the orbit relation of any action of a countable amenable group is amenable, every such action is orbit equivalent to an action of . The same theorem gives the uniqueness of Cartan subalgebras in hyperfinite von Neumann algebras.
On this platform it is the missing link in the Lodha–Moore mission, which passes between Lodha and Moore's definition of a -amenable relation (an orbit relation of off a null set) and the invariant-mean definition of the Monod bundle: one direction is proved, the other (LodhaMoore.isMuAmenable_of_isAmenableRel) is this mission's goal in Lodha and Moore's language.
Timeline.
is a standard Borel space with a -finite measure . A discrete measured equivalence relation (IsDiscreteMeasured μ R) is a Borel equivalence relation whose classes are countable and for which is quasi-invariant: the saturation of a null Borel set is null.
carries the measure , the counting measure on the class of (relMeasure), and the module , the density of against its image under (module). A partial transformation of is a Borel bijection between Borel subsets of whose graph lies in (Monod.PartialTransformation).
is amenable (Monod.IsAmenableRel) when it has a left invariant mean: a positive normalized map from bounded functions on to bounded functions on with for every partial transformation (Definitions 5–6). is of type I (IsTypeI) when, off a null saturated set, its quotient is a standard Borel space, and hyperfinite (IsHyperfinite) when, off a null set, it is a countable increasing union of type I equivalence relations (Definition 1). A finite subequivalence relation (IsFiniteSubrelation) is a Borel that is an equivalence relation with finite classes on .
For amenable there are a non-singular Borel automorphism of and a null set with
The result. Theorem 10 turns amenability, which is usually easy to check, into hyperfiniteness, which is the structure one wants: for instance, the action of on the projective line, or of any discrete group on with amenable, is generated by a single transformation. On this platform it closes the open direction, LodhaMoore.isMuAmenable_of_isAmenableRel, and with it Lodha and Moore's Theorem 2.1.
Formalizing it. No machine-checked proof of the theorem exists, in Mathlib or elsewhere as far as a search finds; Mathlib has no theory of countable Borel equivalence relations. A complete development builds that theory from the descriptive set theory Mathlib has.
The theorem is about relations without a group. The obvious route, through a countable group generating and an amenability of that group, is unavailable: the orbit relation of a nonamenable group, such as acting on the projective line, can be amenable, and there is no group whose Følner sets one could use. The Følner sets of Lemma 8 have to be produced from the invariant mean on the relation itself, which needs duality between and and convexity arguments. Underneath, even the basic facts used in §§1–3 (that is a countable union of graphs of Borel automorphisms, that is a measure, that saturations of Borel sets are Borel) rest on the Lusin–Novikov uniformization theorem, which is not in Mathlib. It is published here as standalone theorems: a Borel set with countable sections is a countable union of Borel graphs, and a countable-to-one Borel map is injective on countably many Borel pieces covering its domain.
All statements carry the hypotheses of §1: standard Borel (StandardBorelSpace), -finite, a Borel equivalence relation with countable classes and quasi-invariant. Lemmas 8 and 9 take a probability measure, as the paper's proof of Lemma 9 does. “Up to a null set” is read as “off a -null Borel set of points”, which by quasi-invariance agrees with the paper's -null sets. Amenability is the published Monod definition, an invariant mean on bounded measurable functions modulo null sets; it is not trivial (the relation of for a countable dense subring of is not amenable, Monod.not_isAmenableRel_mob).
The definitions are in the definition bundle ConnesFeldmanWeiss. Reusable beyond this mission: the Feldman–Moore theorem and the basic theory of countable Borel equivalence relations, both welcome as standalone theorems.
What is left out. Proposition 7 and Corollary 11 need the von Neumann algebra of a relation and its Cartan subalgebras, which Mathlib does not have. The final part of the paper (Lemma 15 to Corollary 21) treats relations with uncountable classes through transverse functions, including foliations; it is a different setting with its own definitions.
Gustafson, Meinert and Melcher construct axisymmetric saddle points of the micromagnetic energy of a spherical shell in two ways (a heat flow, and continuation from an explicit solution at ). Their Remark 3.18 conjectures that a single uniqueness statement identifies the two; it is problem 241 of the AIM open problem list.
Timeline. 2016: Kravchuk et al. propose the model. 2025: Gustafson–Meinert–Melcher construct the saddle points and state the conjecture.
For anisotropy the energy of is . An axisymmetric field with profile is critical exactly when
The hemispheric class adds , , .
For every there is exactly one smooth profile in that solves (2.6) and induces a smooth map . The statement may be proved or disproved.
Uniqueness would identify the two constructions as one saddle branch; a counterexample would give further degree-zero critical points of .
(2.6) is singular at both poles and is a two-point boundary condition, so standard ODE uniqueness does not apply, and the paper's comparison arguments only control solutions in the wedge . Numerical evidence (shooting) finds at , besides , a second solution in the class with (similarly at ), which leaves the wedge.
Profiles are functions ; all conditions, and the uniqueness, are imposed on only (values outside are unconstrained, so uniqueness on would be trivially false). Smoothness is ContDiffOn ℝ ∞ on . "Induces a smooth map" means the field extended to as a function of is there; this excludes profiles with a cone singularity at a pole. The paper's uses piecewise profiles; by its Corollary 2.7 it has the same solutions.
A Costas array is a permutation matrix in which the difference vectors between distinct dots are pairwise distinct; such arrays are frequency-hopping patterns for sonar and radar (Costas, 1984). Rubio and Torres ask whether their -dimensional version can stay Costas in every window of its periodic extension, and conjecture that this happens only in the smallest order.
Timeline. 1984: Taylor proves that 2D periodic Costas arrays have order . 2023: Rubio–Torres prove the odd-order and 3D cases, give examples, and state Conjecture 1.
Let , , with all sides , and a bijection; the dots are . The array is Costas if the difference vectors between distinct dots are distinct, and periodic Costas if moreover, after repeating the dots periodically over , the dots inside every translate have distinct difference vectors.
Conjecture 1: if and defines a periodic Costas array, then
equivalently every . The condition is a normalization ( swaps the boxes).
A proof would give the multidimensional analogue of Taylor's theorem; a counterexample would give periodic distinct-difference patterns of non-power-of-two order.
The Rubio–Torres counting argument needs a bound that is available only when is one-dimensional, which is why it stops at . Computational evidence: an exhaustive window check reports that the array with dots is periodic Costas, which would disprove the conjecture.
A point of is a pair ; boxes are 1-based; is a total function whose values off are unused. Differences are plain integer vectors (not reduced modulo the sides), windows range over all , and and sides are part of the definition, so no degenerate case holds vacuously.
The Schur number is the largest such that can be partitioned into sumfree sets, sets with no such that ( allowed). Schur's argument gives , where the triangle Ramsey number is the least such that every colouring of the edges of with colours has a monochromatic triangle (Fredricksen–Sweet 2000, inequality (2)). Only are known (Heule 2018). For six colours the published range is ; the upper bound is with (DS1, rev. 18).
Timeline.
The first target is a centred-interval bound: if , then . With the recursive bound gives , and the centred bound gives ; with it gives only . The mission formalizes what a Schur colouring of with six colours would have to look like under .
All numbers are natural numbers, , and .
Schur colourings and covers. A colouring with colours is a map . It is a Schur colouring of (SchurColoring N c) if there are no with and , the case included. The cover form uses SumFree S and CoveredBySumFree X n ( lies in the union of sumfree sets); for the two bridge theorems pass between the two forms in both directions.
Triangle Ramsey property. (TriangleRamsey k r): every colouring with at most colours of the pairs of a finite set of at least naturals has a monochromatic triangle. For it is the inequality .
Neighbourhoods. The difference colouring gives a pair the colour . For a Schur colouring of it has no monochromatic triangle on , since . Write
colorNbhd c V v i);centralNbhd c m), which contains ;endpointNbhd c m i).The frontier. The frontier hypotheses are , , , and a Schur colouring of with colours. From the first two, holds, and the centred bound excludes Schur colourings of with colours; is the frontier interval. Six colours: , , , , .
Example. For , , , (and ), the classes , , form a Schur colouring of , with and endpoint neighbourhoods and , both closed under .
where , and :
The goal is a structure theorem under the hypothesis . It does not prove , and it does not assert that a Schur colouring of with six colours exists; whether such a colouring, or the structure it would force, exists is open. The goal is the six-colour instance of the general theorems below.
For a colouring of ordered pairs, a finite set , a point and a map with , on and on :
The result itself. Under , , and the goal constrains a six-colour Schur colouring of as listed above. In particular, each of its five endpoint neighbourhoods is a set of pairs whose difference colouring uses at most four colours, is invariant under and, like that of every subset of , has no monochromatic triangle. So such a colouring yields five colourings of with at most four colours, no monochromatic triangle and a fixed-point-free colour-preserving involution. A proof that this configuration cannot occur would give under the same hypothesis. Whether it can occur, and whether , are open.
Formalizing it. All 12 theorems of the tree, the goal included, are proved in Lean 4 with Mathlib over the bundles ClassicalSchurBasic, ClassicalSchurRamsey and ClassicalSchurColoring, with the axioms propext, Classical.choice and Quot.sound only. Independent Claude agents checked the Lean: one rebuilt the frontier theorems, re-ran their axiom audit and checked their statements against the argument; another checked every statement of the tree against the mathematics. The mathematics is in the paper if : a centred Schur bound and the structure at the frontier (A. McKenna, Zenodo, 2026, doi:10.5281/zenodo.23156099), and the Lean code is in its repository; the paper has not been refereed. is not formalized in the mission.
The centred bound counts, for one colour class, the points around the centre of the interval. At the frontier every such count is tight: each colour has elements in , and inside each colour other than has degree , the largest value that allows. So no single counting step gives a contradiction, and the theorems describe the tight case instead of excluding it. The first exclusion that the structure gives, parity, works only for odd ; at six colours .
The reflection is not a property of Schur colourings in general: the colouring , , of has but . At the frontier the theorem asserts it only for the with , so an argument that assumes a fully symmetric colouring proves a different statement. A direct search is no substitute: already needed a large certified SAT computation (Heule 2018), and with six colours is a much larger instance.
ℕ → Fin n on all of ; SchurColoring N c constrains only , with allowed. Distances are Nat.dist.Finsets. lies in range (2 * m + 2) , so the point is a candidate member; the centre never is.TriangleRamsey k r takes colours from any Finset of at most naturals; the pair colouring ℕ → ℕ → ℕ is constrained only on the pairs of the vertex set, which is any finite set of naturals. TriangleRamsey k 0 and TriangleRamsey k 1 are false.CoveredBySumFree X n uses Fin n → Set ℕ; the sets need not be disjoint or lie in .Bundles: ClassicalSchurBasic (SumFree, CoveredBySumFree) and ClassicalSchurRamsey (TriangleRamsey) are already public; ClassicalSchurColoring holds SchurColoring, colorNbhd, centralNbhd and endpointNbhd. Reusable: the colouring–cover bridges, the pigeonhole step, the centred bound for every , and the automorphism-extension lemma (arbitrary types). Welcome beyond the targets: a formal proof of TriangleRamsey 4 61, and results on whether the configuration of five paired -point sets exists.
Provenance: the centred-interval argument was first written by an AI agent based on ChatGPT (OpenAI) in a project discussion on 2026-09-27, and a Claude (Anthropic) agent audited it. The balance, saturation and reflection argument was proposed by an AI agent based on ChatGPT (OpenAI) in a project discussion; Claude checked each step and restated it with explicit hypotheses. Claude wrote the Lean proofs of both parts; the independent checks are described under Formalizing it.
Schnirelmann showed around 1930, by elementary means, that some absolute constant makes every integer a sum of at most primes. For odd :
The campaign's first proved value, , came from Schnirelmann's method with every constant written out. This entry records a sharper value, , from the same elementary circle of ideas.
A representation of as a sum of at most primes is a finite multiset of primes summing to with at most elements counted with multiplicity. The Schnirelmann density of is (Mathlib: schnirelmannDensity).
This is the campaign template with the value filled in. The source proves the stronger statement that every odd is a sum of exactly primes; the at-most form for all odd follows.
It keeps the explicit Selberg sieve, Cauchy–Schwarz and Schnirelmann's original sumset inequality from the entry, and improves the first moment:
The bound is far weaker than Tao's or Helfgott's , but it rests on an elementary argument with no "sufficiently large" threshold and no prime number theorem, so it is a realistic target for a complete formalization and a large step down from . Reusable components:
The Lean statement is the campaign template verbatim with in place of the value. Mathlib already has schnirelmannDensity, the Λ² Selberg sieve setup (Mathlib/NumberTheory/SelbergSieve.lean) and central-binomial bounds.
Schnirelmann showed around 1930, by elementary means, that some absolute constant makes every integer a sum of at most primes. For odd :
The campaign's first proved value, , came from Schnirelmann's method with every constant written out. This entry records a sharper value, , from the same elementary circle of ideas.
A representation of as a sum of at most primes is a finite multiset of primes summing to with at most elements counted with multiplicity. The Schnirelmann density of is (Mathlib: schnirelmannDensity).
This is the campaign template with the value filled in. The source proves the stronger statement that every odd is a sum of exactly primes; the at-most form for all odd follows.
It is the argument behind the entry, unchanged up to the last step: the explicit Selberg sieve and Cauchy–Schwarz give for , . The only change is to take the smallest admissible in Schnirelmann's inequality: first holds at (rather than the rounded ), so and .
The bound is far weaker than Tao's or Helfgott's , but it rests on an elementary argument with no "sufficiently large" threshold and no prime number theorem, so it is a realistic target for a complete formalization and a large step down from . Reusable components:
The Lean statement is the campaign template verbatim with in place of the value. Mathlib already has schnirelmannDensity, the Λ² Selberg sieve setup (Mathlib/NumberTheory/SelbergSieve.lean) and central-binomial bounds.
This mission formalizes J. T. Moore, Fast growth in the Følner function for Thompson's group F, Groups Geom. Dyn. 7 (2013) 633–651 (doi:10.4171/GGD/201; arXiv:0905.1118v7, whose page numbers are used): if Thompson's group has Følner sets at all, they are larger than any tower of exponentials.
Whether Thompson's group is amenable is a long-standing open problem, the goal of the F-amenability mission on this platform. By Følner's criterion a finitely generated group is amenable exactly when it has Følner sets, finite sets almost invariant under translation by the generators, of every precision. Moore's theorem is unconditional: for every finite symmetric generating set there is a constant such that every -Følner set has at least elements, a tower of exponentials. If is amenable, its Følner function therefore outgrows every tower, and would answer negatively Gromov's question whether some primitive recursive function dominates the Følner functions of all amenable finitely presented groups (Moore's Question 1.2, from Gromov 2008, p. 578).
Timeline.
Thompson's group (CannonFloydParry.F, published) is the group of order-preserving homeomorphisms of that are piecewise linear with finitely many breakpoints, all dyadic rationals, and all slopes powers of . Moore multiplies elements as " followed by "; that group, the opposite of the group of maps under composition, is MooreF, and it acts on the right.
A finite set is -Følner with respect to a finite (IsFolnerSet Γ A ε) when , where . The tower function is , (ThompsonAmenability.towerExp, published). The Følner function (folnerFunction) is the least size of a -Følner set, and if there is none.
The proof works with finite rooted binary trees, recorded as the sets of addresses of their leaves (IsTree), on which acts partially by acting on the addresses (treeAct), and with weighted Følner sets and marginal sets for partial actions of a group (IsWeightedFolner, IsMarginal). These are defined in the two definitions items.
For every finite symmetric generating set of there is such that, for every ,
The goal is the published F-amenability milestone ThompsonAmenability.exists_const_forall_isFolner_le_card, for the product of maps by composition and left translates; a milestone states the same theorem in Moore's conventions, and another states its second sentence, that is not eventually dominated by any .
Every numbered result of §§3–5 (Lemmas 3.4, 3.5, 3.9–3.12, 3.14, 3.15, 4.1, 4.2, 5.2, 5.4, 5.5, 5.7, 5.9, 5.10, 5.12, 5.13, Remark 3.8 and Claim 5.14), the unnumbered facts about trees and tree diagrams stated in §2, and the word-length bound Moore cites from Burillo, Cleary and Stein.
The result. The theorem constrains any proof that is amenable: Følner sets of , if they exist, cannot be found by any search whose size is bounded by a tower of fixed height. If is amenable, it answers Gromov's question negatively. If is not amenable, the bound is vacuous but its method, controlling how Følner sets distribute over tree diagrams, is one of the few quantitative tools on the problem.
Formalizing it. None of the paper is formalized. The general theory of §3 (partial actions, weighted Følner sets, marginal sets) applies to any group acting partially on a set and is reusable; the partial action of on binary trees is the natural model for combinatorial arguments about .
The difficulty is quantitative. A Følner set is defined only by an inequality between counts, and nothing in that inequality forces its elements to be large; yet the bound must hold for every Følner set, with a single constant for all , while the height of the tower grows with . Any argument can therefore afford to lose only a constant factor in the Følner constant for each level of the tower.
Lean representation and conventions.
(CannonFloydParry.F)ᵐᵒᵖ, so products and right translates match the paper; the goal is stated for CannonFloydParry.F with left translates.List Bool). Tree diagrams, their maps on sequences, equivalence and reducedness follow Moore's §2; a tree diagram describes an element of the published through the dyadic intervals of its leaves, and Moore's sentence defining as the reduced tree diagrams is a milestone.Option-valued function, and the action of is defined on all finite sets of sequences; on trees it is Moore's action.What is left out, and deviations.
What a development needs. Tree diagrams, normal forms and generation of are published and proved on this platform (the Cannon–Floyd–Parry missions on tree diagrams and the normal form and the two presentations of ); Følner's criterion is published by Garrido's first mission. New are the combinatorics of binary trees as leaf sets, the bridge between them and the published tree diagrams, and the theory of §3. Proofs of any milestone are welcome.
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.