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.
How much larger can block sensitivity be than sensitivity for a total Boolean function?
For a total Boolean function , a block of coordinates is sensitive at if flipping every bit in that block changes . Let count sensitive singletons and be the maximum number of pairwise disjoint sensitive blocks. Define and .
This campaign seeks larger exponents for which there exists an infinite family of total Boolean functions , indexed by , satisfying
Here denotes a quantity tending to zero as . Higher is better. The classical exponent is , and Huang's bound gives a ceiling of .
OpenAI's construction achieves an exponent strictly greater than .
One sufficient way to establish an exponent is to find a single total Boolean function with and . Input and output normalization followed by self-composition then yields the required asymptotic family.
Turn proposed improvements to integer multiplication into complete Lean proofs, and push the exponent saving further.
Harvey and van der Hoeven established an algorithm in 2021. This campaign builds on that foundation, the OpenAI manuscript, and subsequent community constructions to pursue a strict asymptotic improvement.
For two -bit integers, the target is
A positive beats asymptotically; larger is better. Every entry must exhibit one deterministic multitape Turing machine, with a fixed finite alphabet and tape count, that computes the exact product at every positive input length and meets the eventual worst-case time bound. The tracked number measures an asymptotic exponent saving.
Classical algorithms solve 3SUM in time. In a 2026 breakthrough, Alman and Vassilevska Williams gave a deterministic algorithm, refuting the integer 3SUM hypothesis. How low can the exponent go?
Building on existing Lean formalizations, this campaign tracks upper bounds for 3SUM on polynomially bounded integers, using a word RAM with -bit words, and pursues smaller exponents.
Classical algorithms solve all-pairs shortest paths in time. In a 2026 breakthrough, Alman and Vassilevska Williams refuted the APSP conjecture with a deterministic algorithm. How low can the exponent go?
Building on existing Lean formalizations, this campaign tracks upper bounds for exact APSP and pursues smaller exponents.
The irrationality measure of π quantifies how closely rational numbers can approximate it. This campaign seeks formal proofs of sharper upper bounds, starting with Mahler’s bound of 42.
The sharp Hlawka inequality for Schatten -norms is a cousin of the triangle inequality: it relates the norms of three matrices to the norms of their pairwise sums and their total sum. For complex diagonal matrices, an exact formula for the best possible comparison constant has been proved in Lean for every real . We conjecture that the same formula holds for all .
What is the smallest cutoff for which this formula holds for every real ?
References:
Is every odd number a sum of primes? This campaign tracks formalized proofs of the smallest that suffices.
Schnirelmann (1930) showed some finite works. Vinogradov (1937) showed that three is enough for all sufficiently large odd numbers. Tao (2012) proved unconditionally. Helfgott (2013) proved that every odd number greater than is a sum of three primes, though the proof is still unrefereed. Ideally, we can formalize this statement here. Note that three is optimal: is neither prime nor + prime.
Schoolbook matrix multiplication takes operations. The exponent is the infimum of all such that two matrices can be multiplied in arithmetic operations; trivially , and is conjectured but open.
Strassen gave the first nontrivial bound, , in 1969, and introduced the laser method in 1986 to reach . Coppersmith and Winograd's 1990 bound of stood for two decades. Every subsequent improvement comes from analyzing higher tensor powers of their construction with refined laser-method variants. That line reached in 2025, and the current record is , from August 2026. See Computational complexity of matrix multiplication for the full table. Can we formalize these results and even improve on them?
Multiplying matrices is a basic operation whose asymptotic cost is measured by the number of scalar arithmetic operations needed as the matrix dimensions increase. The familiar entry-by-entry algorithm has cubic cost. The question addressed here is how small an exponent can describe exact multiplication of square matrices when algorithms may use more elaborate finite computations. OpenAI's October 2, 2026 paper establishes the bound for matrices over the complex numbers. Its Theorem 1.1 concerns asymptotic arithmetic complexity, with arbitrarily small positive slack in the exponent.
An arithmetic program is a finite sequence of register computations. A step can load a field constant, read an input entry, or add, subtract, or multiply two values from preceding registers. Constant loads and input reads have zero cost. Each addition, subtraction, and multiplication has cost one. There is no division operation in this program model. Outputs are selected registers, and a program is correct only when these outputs equal the matrix product for every pair of input matrices.
For a field , a real number is an admissible exponent if, for every real , there exists a real constant such that every integer size admits a correct program with cost at most . The constant must work uniformly for all sizes and all input entries. The chosen program may depend on and . The definition does not charge for a separate procedure that constructs these programs. The arithmetic matrix multiplication exponent is the real infimum of the set of admissible exponents.
The goal is exactly the complex-field exponent conclusion of OpenAI's Theorem 1.1:
In the Lean source, the quantity on the left is OAI.MatrixMultiplication.Arithmetic.omega ℂ. The bound on the right is the exact real rational (9 : ℝ) / 4, equal to . The inequality is non-strict. The theorem does not assert a strict inequality below , and it is not quantified over arbitrary fields.
The paper also states the corresponding algorithmic conclusion with every positive exponent slack. The goal here retains the exact infimum formulation used by its released comparator challenge. In particular, the bound should not be read as asserting that one fixed family has cost without any slack, or that an algorithm is efficient at a specified finite matrix size.
The result places above the asymptotic arithmetic exponent in a model with explicitly defined programs, outputs, correctness, and operation counts. It gives a statement that other formal developments can use without leaving those conventions implicit. The dependence on the complex field is part of that statement, so results using another field or another computational model require their own justified connection.
This is a port and verification of an existing proof, not a claim that the source theorem remains unproved. The released Lean development contains the proof entry point. Keeping the original definitions and conclusion allows compatibility changes to be reviewed independently of the mathematical claim.
An asymptotic exponent bound requires one uniform cost constant for every positive matrix size, while correctness quantifies over all pairs of matrices at each size. A computation for selected dimensions or selected inputs cannot satisfy those requirements. Arguments about tensors must also support the stated arithmetic program cost, including the operations needed for the relevant linear combinations. The infimum formulation makes its defining set and the interpretation of its bounds part of the supporting mathematics, rather than assumptions to insert into the target theorem.
The environment is Lean 4.33.1 with Mathlib revision 0df444a360eaa60ab8c11dca51a86af692955474. Matrices are functions on finite index sets. Program evaluation and output selection give exact field values. The main theorem fixes the field to , excludes size zero from admissibility, and uses real powers for its cost estimates. Constants may be arbitrary complex numbers; no bit-cost interpretation is asserted.
The definition item preserves the original source block, including its rectangular matrix multiplication definitions and complex dual exponent. Those additional definitions support the shared source development but are not additional mission goals. A complete proof must establish the displayed bound without an admitted lemma, a new axiom, or an assumption equivalent to that bound. Reusable components include the arithmetic program model, finite tensor constructions, asymptotic bounds, and the bridge from tensor rank to arithmetic operations.
This entry records a completed elementary result in the campaign on odd numbers as sums of primes: every odd natural number greater than 1 is a sum of at most 4401 primes. It illustrates how an additive density estimate can reduce the number of prime summands in a Schnirelmann argument.
For every natural number , if is odd and , there is a multiset of primes with and . Repeated primes are allowed. The bound applies to every such , not only sufficiently large integers.
The goal references the existing proved 4401 theorem. Its statement is the campaign template instantiated with 4401.
The two supporting references are the density bound and Mann's theorem, both already proved.
Let and . The density estimate gives . Mann's theorem gives , so yields density at least . The sumset cover argument then produces 4400 odd prime summands, with one additional 3 to obtain the required parity. Explicit sums of 2s and 3s handle the remaining small and medium ranges. These steps are included in the accepted goal proof; they are not unfinished milestones.
All three referenced theorems have ACCEPTED proof submissions under the account moona3k, are marked Proved, and use Mathlib revision 0df444a360eaa60ab8c11dca51a86af692955474. No new Lean statement or duplicate theorem is introduced by this proposal.
The density theorem's published source credits an extraction from the accepted 6101 proof. Mann's theorem is the classical additive density theorem of H. B. Mann; the accepted formalization follows the Dyson transform presentation cited in its theorem record. This entry assembles those existing results into the 4401 bound.
The 4401 bound was an intermediate improvement on 6101. It is not the current campaign frontier: the campaign now includes a proved bound of 27. This proposal preserves the earlier result and its proof route without claiming a new literature result or a new record.
Status: complete. This mission records a finished formalization rather than an open call for work. Every statement below, including the goal, was uploaded together with a proof that the platform has verified, so there is nothing left to prove.
The Lovász Local Lemma (LLL) is a basic tool of the probabilistic method. It shows that a collection of rare "bad" events can all be avoided simultaneously, even when the events are not independent, provided each event depends on only a few others. Its best-known application is to satisfiability: a -CNF formula in which every variable appears in few clauses has a satisfying assignment.
Quantum satisfiability (-QSAT) is the quantum analogue of -SAT. Clauses are replaced by projectors acting on qubits, and the question is whether some nonzero state is annihilated by all of them, equivalently whether the corresponding local Hamiltonian is frustration-free. Bravyi showed that -QSAT is -complete for , so sufficient conditions for satisfiability are of interest in quantum complexity theory and in many-body physics. Ambainis, Kempe and Sattath (arXiv:0911.1696, J. ACM 2012) proved a quantum version of the LLL in which probability is replaced by relative dimension, and derived a sufficient condition for -QSAT instances to be satisfiable.
Let be a nonzero finite-dimensional vector space. For a subspace , the relative dimension is
It plays the role of probability: subspaces replace events, intersection replaces conjunction, and replaces conditional probability.
Subspaces have dependency sets when, for every and every set of indices with and ,
In words, is independent, for relative dimension, of every intersection of subspaces outside its dependency set.
A -QSAT instance on qubits is a family of projectors , each acting on a set of qubits and extended by the identity on the others. It is satisfiable if a nonzero state lies in the kernel of every .
The formalization proves the local lemma once, for an abstract valuation: a real function on a bounded lattice that is nonnegative, monotone and modular, , with and . Relative dimension on subspaces and the uniform probability on subsets of a finite set are the two instances used.
Let be subspaces with dependency sets , and let satisfy for every . Then
All of these are proved on Prove2Me and can be found by name (tag quantum-lll):
QLLL.Valuation.lll.QLLL.quantum_lll_symmetric.QLLL.SAT.classical_lll, QLLL.SAT.classical_lll_symmetric.QLLL.SAT.sat_of_degree_le.QLLL.PiQSAT.inf_ker_extendOp_ne_bot on Mathlib's tensor product, and QLLL.QSAT.satisfiable_of_degree_le for orthogonal projectors.QLLL.SAT.exists_assignment_forall), and the local lemma for infinite index sets under a continuity hypothesis (QLLL.lll_iInf).The quantum local lemma gives a sufficient condition for -QSAT satisfiability that depends only on the local structure of the instance: the rank of the projectors and the number of projectors per qubit. It shows that the classical criterion survives the passage from events to subspaces, even though subspaces do not form a distributive lattice. Later work on constructive and tight versions, listed in the timeline, builds on this statement.
All results of this mission are proved and machine-checked. The Lean development was written as a complete formalization of the paper, and every statement here was uploaded together with a proof verified by the platform. What the mission adds is a reusable, Mathlib-based library: the local lemma for abstract valuations, its classical and quantum instances, -QSAT stated on Mathlib's tensor product of qubits, and linear algebra on intersections of tensor products of subspaces that Mathlib does not yet contain. Mathlib currently has no form of the Lovász Local Lemma.
The classical proof uses complements of events and the identity , together with the distributive law for events. Subspaces satisfy neither in general: the lattice of subspaces is modular but not distributive, and the orthogonal complement does not distribute over intersections. The argument has to be rebuilt from the properties of relative dimension that do hold. For -QSAT, the further difficulty is to show that constraints acting on disjoint sets of qubits are independent for relative dimension, which requires computing intersections and dimensions of tensor products of subspaces.
Conventions committed to in the Lean statements:
An infinite version of -QSAT is deliberately not included. Nonzero subspaces can have all finite intersections nonzero and zero total intersection, so the infinite statement has to be phrased with compatible families of density matrices, and the current Lean formulation does not yet restrict the constraints to positive operators.
The blueprint of the formalization, linking every paper statement to its Lean declaration, is at sattath.github.io/Quantum-Lovasz-Local-Lemma/blueprint. Natural extensions, outside the scope of this mission: the orthogonal-projector form of Corollary 16 on Mathlib's tensor product once inner products on -fold tensor products are available, Shearer-type conditions, and a measure-theoretic classical local lemma on general probability spaces.
This is my first contribution to Prove2Me, so the definitions, statements, proofs and descriptions may fall short of what an experienced contributor would produce. Some choices may be unidiomatic, some lemmas may duplicate Mathlib, and the split into entries could be better. Every proof is checked by Lean, so the theorems are correct as stated; the question is whether they are stated in the most useful way.
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 earlier values ( down to ) came from Schnirelmann's method with every constant written out. The entry used the sharp singular-series weight in a pointwise sieve bound, and its large range stopped near because the pointwise bound loses the spread of the singular series. This entry replaces that large range by Riesel and Vaughan's weighted argument, which divides out the singular series exactly, using Dirichlet characters and the large sieve. Rosser–Schoenfeld's zero-based bound is replaced throughout by Chebyshev's elementary . No zeta- or -function zero input is used, and the result matches Vaughan's .
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.
Let and . We show , then conclude with Mann's theorem. Let be the number of ordered pairs of odd primes with . Since , it suffices to show for large . Write and for the twin-prime constant.
TaoFivePrimes.siebert_prime_pair_bound), Cauchy–Schwarz gives . The kernel sum is a finite computation.MVSieve.primitive_character_large_sieve, MVSieve.large_sieve_weight_lower), with Chebyshev's bound in place of Rosser–Schoenfeld. This gives with room to spare.The argument reaches Vaughan's with no zeros of or -functions and no prime number theorem. New reusable components:
The Lean statement is the campaign template verbatim with in place of the value. The proof imports two platform theorems: RV27.middle_range (the small-shift range, ) and RV27.large_range (), and Schnir.basis_of_density (Mann's theorem). Those rest on TaoFivePrimes.siebert_prime_pair_bound, the PrimePairSieve nodes and the MVSieve large-sieve nodes.
PrimeNumberTheoremAnd (PrimeNumberTheoremAnd/IEANTN/Chebyshev.lean).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 earlier values ( down to ) came from Schnirelmann's method with every constant written out, using Chebyshev-type lower bounds for and a Selberg sieve whose singular-series weight was crude. The entry hit the limit of that crude weight. This entry replaces it by the sharp weight , using the platform's proved prime-pair sieve (TaoFivePrimes.siebert_prime_pair_bound, Siebert's bound as used by Riesel–Vaughan) and its PrimePairSieve components. No zeta-zero input is used.
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.
Let and . We show , then conclude with Mann's theorem. Write for the scale and for the twin-prime constant.
The argument stays elementary: no prime number theorem and no zeros of or -functions. New reusable components:
PrimePairSieve nodes.The Lean statement is the campaign template verbatim with in place of the value. Already proved on the platform and imported: TaoFivePrimes.siebert_prime_pair_bound, PrimePairSieve_reciprocal_weighted_sifted_bound, PrimePairSieve.divisor_kernel_comparison, PrimePairSieve.reciprocal_base_denominator_dominates_threshold, PrimePairSieve.sieve_constants_certificate, Schnir.basis_of_density.
PrimeNumberTheoremAnd (PrimeNumberTheoremAnd/IEANTN/Chebyshev.lean).All-pairs shortest paths (APSP) computes the shortest distance between every pair of vertices in a weighted graph.
We strengthen the previously formalized bound to for deterministic APSP on directed graphs with polynomially bounded integer weights and no negative cycles, using the same word-RAM model. It formalizes the improvement outlined by Alman and Vassilevska Williams in their conclusion.
A contact structure on a manifold of odd dimension is a field of hyperplanes that is as far from integrable as possible. Contact structures are the odd-dimensional counterpart of symplectic forms. They arise on every star-shaped energy level of a Hamiltonian system, on unit cotangent bundles (geodesic flows), and on links of singularities. They are the setting of Reeb dynamics and of the Weinstein conjecture.
Gray's stability theorem says that on a closed manifold contact structures have no local moduli. If , , is a smooth family of contact structures, there is an isotopy with . A contact structure can therefore be deformed only within its isotopy class, and every classification of contact structures (tight versus overtwisted, Eliashberg's classification on ) is a classification up to isotopy because of it.
Timeline.
The closed manifold is a compact submanifold of Euclidean space. Let be smooth, let be compact, and assume is surjective for every . Then is a closed smooth manifold of dimension with tangent spaces
A one-form is a smooth map , restricted to . Its exterior derivative is
This is the condition in the form of Geiges' Remark 2.3. It forces to be odd. The contact structure is . Contact structures are cooriented throughout, as in Geiges' standing assumption (§2).
For every smooth family of contact forms , , on there is an isotopy of with
stated pointwise: for , iff .
The goal concerns the contact structures. It fixes no normalization of the forms and no dimension.
The same isotopy can be chosen with smooth functions such that
Moreover, every point at which vanishes on for all stays fixed: .
The result. Gray stability is the basic rigidity statement of contact topology.
Formalizing it. The theorem is classical and has a short proof on paper. Mathlib, at the revision used here, has no differential forms on manifolds, no Lie derivative, no global flows of time-dependent vector fields on compact submanifolds, and no contact structures. The mission builds these concretely on submanifolds of :
All of these are reusable for Moser's theorem on volume and symplectic forms and for the Darboux and neighbourhood theorems.
The proof is soft, but two steps are not formal.
It has a unique solution at each point, but only because is non-degenerate on and the Reeb vector spans the kernel of . The solution must also depend smoothly on and be tangent to ; the ambient form is in general not contact off . 2. Integrating it. The isotopy is the flow of , which must exist for all and stay on . Compactness of enters exactly here. On open manifolds the statement is false (Remark 2.21(2)).
The tempting shortcut of asking for does not work. Contact forms themselves are not stable, as the Hopf family on shows (Remark 2.21(1)), and the conformal factor cannot be dropped.
Fin n → ℝ; is a compact regular level set of a smooth .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 earlier values ( down to ) came from Schnirelmann's method with every constant written out, using only weak Chebyshev lower bounds for . This entry keeps the same machinery as the entry but feeds it Chebyshev's sharper lower bound with , obtained from the weights at . No zeta-zero input is used.
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.
Let and . We show , then conclude with Mann's theorem as in the entry. Write for the scale.
PrimeNumberTheoremAnd library with explicit bounds for and ). Since , this gives . On its own it covers through .The argument stays elementary: no prime number theorem and no zeros of or -functions. New reusable components:
The Lean statement is the campaign template verbatim with in place of the value. Already proved on the platform: Schnir.sieve_ineq, Schnir.G_lower, Schnir.basis_of_density. Mathlib supplies the Chebyshev function with and the Λ² sieve framework.
PrimeNumberTheoremAnd (PrimeNumberTheoremAnd/IEANTN/Chebyshev.lean).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 earlier values ( down to ) came from Schnirelmann's method with every constant written out. Those arguments stall near because the medium range relies only on a Chebyshev lower bound for . This entry adds the small-shift idea of Riesel and Vaughan, which removes that bottleneck without any zeta-zero input.
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.
Let and . We show , then conclude with Mann's theorem as in the entry. Write for the scale.
The argument stays elementary: no prime number theorem and no zeros of or -functions. New reusable components:
The Lean statement is the campaign template verbatim with in place of the value. Already proved on the platform: Schnir.sieve_ineq, Schnir.G_lower, Schnir.pi_lower, Schnir.basis_of_density. Mathlib supplies the Chebyshev bounds (Chebyshev.psi_ge', Chebyshev.theta_le_log4_mul_x) and the Λ² sieve framework (Mathlib.NumberTheory.SelbergSieve).
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 earlier values ( down to ) came from Schnirelmann's method with every constant written out. Those arguments stall near because the medium range relies only on a Chebyshev lower bound for . This entry adds the small-shift idea of Riesel and Vaughan, which removes that bottleneck without any zeta-zero input.
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.
Let and . We show , then conclude with Mann's theorem as in the entry. Write for the scale.
The argument stays elementary: no prime number theorem and no zeros of or -functions. New reusable components:
The Lean statement is the campaign template verbatim with in place of the value. Already proved on the platform: Schnir.sieve_ineq, Schnir.G_lower, Schnir.pi_lower, Schnir.basis_of_density. Mathlib supplies the Chebyshev bounds (Chebyshev.psi_ge', Chebyshev.theta_le_log4_mul_x) and the Λ² sieve framework (Mathlib.NumberTheory.SelbergSieve).
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 argument proves the stronger statement that every odd is a sum of exactly primes; the at-most form for all odd follows.
It follows the companion entry, with every parameter pushed to the limit of the same tools. Let and . We show :
About is the floor of this method: the medium range relies on the Chebyshev constant , which forces the sieve threshold below and so inflates the sieve coefficient.
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. Reusable components:
The Lean statement is the campaign template verbatim with in place of the value. All the ingredients above except the moment bound and the final assembly are already proved on the platform (Schnir.sieve_ineq, Schnir.G_lower, Schnir.pi_lower, Schnir.basis_of_density).
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: