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?
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).Menger's theorem is the oldest of the min–max theorems of combinatorial optimization. It says that the largest number of disjoint paths joining two sets of vertices of a finite graph equals the smallest number of vertices whose removal disconnects them. The max-flow/min-cut theorem of Ford and Fulkerson (1956), the Kőnig–Egerváry theorem on bipartite matchings (1931), Whitney's characterization of -connected graphs (1932) and the integrality of network-flow polytopes all belong to its family. In operations research it underlies network reliability (how many vertex failures a network survives) and disjoint routing.
Karl Menger proved it in 1927, in a paper on curves. In Zur allgemeinen Kurventheorie (Fund. Math. 10, pp. 96–115) the graph statement is a lemma, Satz δ (p. 101), on the way to characterizing the order of a point of a regular curve by the number of arcs ending there (the subject of mission II of this series).
Timeline.
Let be a finite simple graph on a vertex set , and let be disjoint sets of vertices.
A set separates and if every walk of from a vertex of to a vertex of passes through a vertex of . The set may contain vertices of and of ; in particular always separates.
is -point connected between and ("n-punktig zusammenhängend", p. 100) if no set of fewer than vertices separates and :
A family of disjoint – paths consists of paths of , each from a vertex of to a vertex of , whose vertex sets are pairwise disjoint, end vertices included.
The degree (Grad) of is its number of edges. A part of is a spanning subgraph ; it is proper if it lacks an edge of . is irreducibly -point connected between and if it is -point connected and no proper part is. For a separating set , the side of towards is formed by the components of that meet , together with their edges to ; the side towards is defined symmetrically.
In Lean these are Menger27.Graphs.Separates, NPointConnected, HasDisjointPaths, IrreduciblyNPointConnected and sidePart.
This is the direction Menger states; the converse (disjoint paths force every separator to be large) is immediate and is not part of the mission.
The result. Satz δ is the vertex form of Menger's theorem for two sets, from which the other standard forms follow: the two-vertex form, Whitney's theorem, the edge form (through line graphs), Kőnig's theorem (for bipartite with , the two sides) and, through a standard reduction, integral max-flow/min-cut for unit capacities. Menger used it as the finite step of his theorem on -legs at points of regular curves.
Formalizing it. The theorem is proved, with many published proofs. Mathlib at the pinned revision has edge connectivity of simple graphs but no vertex separators between sets and no form of Menger's theorem; nothing on Prove2Me states it in set form. The mission produces a statement of Satz δ about Mathlib's SimpleGraph, together with the intermediate claims of Menger's own induction, so that the original argument, including the step Kőnig completed, can be checked. Related posed items on the platform are the two-vertex Whitney theorem Balinski61.Whitney.whitney_theorem (internally disjoint paths between two vertices) and Kőnig's theorem MatousekLP.Integrality.konig; neither is the set form stated here, and neither is proved yet.
The obvious argument, choosing disjoint paths one at a time, fails: a first path chosen badly can block every completion, so the paths must be chosen together. Menger's induction avoids this by passing to an irreducible part and cutting it at an -vertex separator, but it needs a vertex outside to cut at (milestone 4). When every vertex of the irreducible part lies in the part is bipartite between and , and the claim is then Kőnig's matching theorem rather than an observation; this is the gap of 1927. The gluing step (milestone 7) is also more delicate than on the page: the paths of the two sides must meet the separator only at their ends, which depends on how the sides are cut out.
Representation. Menger's gewöhnlich eindimensionaler Raum, a finite union of arcs meeting at most in end points, is read as a finite simple graph G : SimpleGraph V with [Fintype V]; and are Finset V. Vertices are the points of and the end and branch points (Menger's punktförmige Stücke); edges are the arcs between them, subdivided so that there are no loops or parallel edges. Subdivision changes neither separation nor the number of disjoint paths, and a separating point inside an arc can be moved to an end of the arc. Menger's degree (the number of arcs between consecutive punktförmige Stücke) becomes the number of edges, which a subdivision only increases; every milestone stays true.
Conventions and explicit readings of the paper's phrases.
H ≤ G; "echter Teil" is H < G.sidePart G P S), not quantified over; it has no edges at the vertices of , matching Menger's considered between and .Trivializations ruled out. Forcing separators to avoid , counting internally disjoint or edge-disjoint paths, or allowing two paths to share an end vertex would each change the theorem; none is done. No hypothesis restricts , and is the trivial case, not an excluded one.
Needed infrastructure. Walk surgery (prefixes up to the first visit of a set, concatenation, conversion of walks to paths), transfer of walks along SimpleGraph inclusions, and well-founded induction on the number of edges. Separators and disjoint path families between sets are reusable beyond this mission, for Whitney's theorem, Kőnig's theorem and flow integrality. Proofs by any method are welcome, including a proof of the goal through max-flow/min-cut or an independent argument (Göring's) bypassing the milestones.
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 manufacturer launching a new product often depends on a single supplier for a critical component, and the supplier must build capacity before demand is known. The manufacturer usually knows more about demand than the supplier does: her sales force, market research and order history give her a forecast the supplier cannot verify, and she has a reason to inflate it, since more capacity costs her nothing if the supplier pays for it. Whether contracts can make forecast sharing credible, and at what cost to the supply chain, is the subject of Cachon and Lariviere, "Contracting to assure supply: how to share demand forecasts in a supply chain" (Management Science 47(5), 2001, doi:10.1287/mnsc.47.5.629.10486). Section 6.10 of G. P. Cachon's survey chapter Supply Chain Coordination with Contracts (Handbooks in OR & MS, Vol. 11, 2003) presents a simplified version of that model, and this mission formalizes it from the author's January 2003 draft.
The section separates two regimes. Under forced compliance the supplier must build exactly the capacity the contract specifies; under voluntary compliance he may build less. The section's conclusion is that forced compliance allows both coordination and credible forecast sharing, while voluntary compliance allows forecast sharing only at the price of under-investment in capacity.
Demand has one of two types with distribution function . The page assumes for , for (so demand has an atom at ), increasing and differentiable, and stochastic dominance for all . The supplier builds capacity at cost per unit; after demand is observed he produces at cost per unit; the manufacturer earns per unit of demand satisfied; unused capacity is worth nothing.
Expected sales with units of capacity are , and the supply chain's expected profit is
An optimal capacity maximizes over , and .
In an options contract buys options at each and pays for each option exercised. With her profit is and the supplier's is . The contract with share sets and . Under a wholesale price contract with price the supplier earns ; the price inducing capacity is with , and the manufacturer then earns .
With asymmetric information only observes . Let be the supplier's minimum acceptable profit, and define the shares
The low type offers the options contract with share and initial order , the high type the one with share and initial order . Assuming and :
the supplier earns from the low type and at least from the high type, and each initial order maximizes both firms' profits. The profit comparisons are stated between the contract profit functions, not between shares.
The goal shows that with forced compliance a high-demand manufacturer can share her forecast credibly through the terms of a coordinating contract rather than its form: both types use the same contract family, the supply chain is coordinated in every state, and the only cost of asymmetric information is that the high type may be unable to push the supplier down to his reservation profit. The voluntary-compliance milestones show the other side: once the supplier may under-build, only the wholesale price affects his capacity, and the resulting capacity is strictly below the integrated optimum. Together they explain why compliance regimes matter in capacity contracting.
The results are established on the page with short arguments; none has a machine-checked proof. Formalizing them requires the derivative of expected sales for a distribution with an atom, the first-order characterization of a concave maximizer on a half-line, and careful bookkeeping of the incentive constraints. The demand and profit definitions are reusable for other capacity-procurement and newsvendor-type models.
The incentive constraints look like arithmetic on shares, but the strict inequality needs : the low type's chain profit at the high type's capacity must be strictly below its optimum. The obvious argument via uniqueness of the maximizer is not available, because the page does not assume strictly increasing, so need not be strictly concave and may have a whole interval of maximizers. Likewise needs a strict comparison of integrals of distribution functions. In the voluntary-compliance part, the derivative of needs the density at , and fails when that density is .
Each demand law is a probability measure on and is Mathlib's cdf. is required to be differentiable only on , because the page's makes it jump at . is defined by the expectation , whose integrand is integrable because almost surely. Optimal capacities are passed as arguments characterized as maximizers over , never chosen; is footnote 46's assumption. Derivatives are HasDerivAt statements.
Hypotheses added relative to the page, all disclosed in the items: and in the goal (the page divides by and needs ); for the voluntary-compliance derivative (at it vanishes); and for the non-coordination result. The page's assumption is not needed and not imposed; its strict-concavity claim on p. 101 is not stated, because it would need strictly increasing. The prior does not enter any statement. The page's "separating equilibrium" is formalized by its defining incentive and participation conditions, not by a general signalling-game solution concept; a predicate that holds by construction of (for example ) is not an acceptable substitute for the profit inequalities. The fixed-fee condition of p. 105 is pure algebra on four numbers and is not included.
All definitions are local to the namespace CachonCoord.CapacityForecast. No platform theorem formalizes this model; the Snyder–Shen newsvendor definitions (SupplyChainTheory_contracts) and the revenue-sharing model of Cachon–Lariviere 2005 (RevShareCoord.*) concern different games and are not reused. Proofs of any milestone, and a sanity instance showing the model's hypotheses are satisfiable (for example demand with an atom at and an exponential tail, ), are welcome.
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:
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.