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?
Fix machines and jobs arriving one at a time in the order . Job carries a whole vector of nonnegative loads , one per machine, with no assumed relationship between the entries — the same job may be cheap on one machine and unplaceable on another. This is the unrelated machines model. When job arrives its load vector becomes visible, and the algorithm must commit it to a single machine immediately and irrevocably, knowing nothing about the jobs still to come. A machine's load is the sum of over the jobs assigned to it.
The setting formalized here is one normalized phase: loads are already scaled by a guessed makespan, so machine counts as eligible for job exactly when . The phase is allowed to give up rather than assign badly — it fails if an arriving job has no eligible machine, or if an internal weight grows past .
The algorithm keeps a weight per machine, initialized to . Job goes to the eligible machine minimizing ; that machine's weight is then scaled by , so a machine becomes exponentially unattractive as it fills. The weights are the primal variables of the covering LP
and each assignment raises one dual variable to . The guarantee follows from weak duality rather than a bespoke potential argument, which is the point of the primal-dual method.
The goal theorem states that if the dual admits a feasible solution putting unit total mass on every job — the certificate that the guessed makespan was large enough — then the phase does not fail, every job is assigned, and every machine ends with load
The source states this as ; the explicit constant is what its proof yields.
Note that the load bound alone is not the theorem: it holds vacuously when the phase assigns nothing, and the milestones state it that way deliberately. The content is the conjunction of succeeded, assigns all, and the bound.
The doubling wrapper — guess a makespan, run a phase, double the guess and restart on failure — is what turns this phase into an -competitive online algorithm. It is outside this mission; the guarantee proved here is the conditional single-phase statement. The milestones break the argument into weak duality for finite LPs, the load bound, primal feasibility at each prefix, the primal objective identity, and the failure certificate.
Niv Buchbinder and Joseph (Seffi) Naor, The Design of Competitive Online Algorithms via a Primal-Dual Approach, Foundations and Trends in Theoretical Computer Science 3(2–3), 2009, Chapter 8, pp. 193–196 (Theorem 8.1). PDF · doi:10.1561/0400000024
Chapter Five of Jim Hefferon's Linear Algebra is one long search for a canonical form for matrix similarity, and Theorem IV.2.8 ends it: over the complex numbers every square matrix is similar to a matrix in Jordan form. That is the goal theorem of this mission and the capstone of the book. Mathlib carries the generalized eigenspace decomposition but has no Jordan canonical form, so this is a genuine target rather than a wrapper around an existing lemma; the Jordan block and the block-diagonal Jordan matrix are supplied as a mission definition. The milestones are the three results the proof is assembled from: diagonalizability as the existence of an eigenbasis, Cayley-Hamilton, and the canonical form of a nilpotent map, which is Jordan form applied to on each generalized eigenspace.
When is a system of linear constraints infeasible? Sections 4.6-4.7 of Bertsimas-Tsitsiklis answer with the archetypal theorem of the alternative. The capstone is Farkas' lemma (Theorem 4.6): for an matrix and , exactly one of the following holds — (a) some satisfies , or (b) some satisfies and ; such a is a certificate of infeasibility, geometrically a hyperplane separating from the cone of the columns of . The mission also carries the cone-membership restatement (Corollary 4.3), the inequality form (Theorem 4.7: every solution of satisfies iff some has and ), and the application to asset pricing (Theorem 4.8: a market's prices admit no arbitrage iff there is a nonnegative state-price vector with ). The book proves Farkas' lemma from LP strong duality; Section 4.7 then reverses the arrow from first principles: every polyhedron is closed (Theorem 4.9), Weierstrass' theorem (Theorem 4.10, already in Mathlib), and the separating hyperplane theorem (Theorem 4.11: for nonempty closed convex and there exists with for all ), from which Farkas' lemma — and hence the duality theorem itself — follows geometrically.
Chapter Three of Jim Hefferon's Linear Algebra is about maps between spaces and how matrices represent them. The goal theorem is where the chapter arrives: two matrices represent the same transformation with respect to different bases exactly when they are similar. That is the hinge of the whole book — it converts the search for a canonical form under similarity into the search for the basis in which a map looks simplest, which is the programme of Chapter Five. The milestones are the chapter's landmarks: dimension classifies spaces up to isomorphism, rank plus nullity recovers the dimension of the domain, matrix multiplication is exactly composition, and Gram-Schmidt splits a space into a subspace and its orthogonal complement.
Chapter Two of Jim Hefferon's Linear Algebra builds the vector space vocabulary — spanning, independence, basis — and turns it into a theory of dimension. The goal theorem is the chapter's most striking result, that the row rank and the column rank of a matrix always agree, which is the bridge between the matrix-of-numbers view of Chapter One and the vector space view of Chapter Two. The milestones are the two pillars it stands on: that any two bases of a space have the same size, so dimension is well defined at all, and that any linearly independent set can be extended to a basis.
Is the shadow of a polyhedron again a polyhedron? §2.8 of Bertsimas–Tsitsiklis answers this with perhaps the oldest method for solving linear programming problems: Fourier–Motzkin elimination. Given , one sorts the constraints by the sign of the coefficient of — rewriting them as , , or — and forms the polyhedron whose constraints are all pairwise combinations together with the constraints not involving . The capstone, Theorem 2.10, states that is exactly the projection of onto its first coordinates: a value of can be interpolated if and only if every lower bound is below every upper bound. Though hopeless as an algorithm (the number of constraints can grow exponentially), elimination has powerful theoretical corollaries, all formalized here: projections of polyhedra are polyhedra (Corollary 2.4), the image of a polyhedron under any linear mapping is a polyhedron (Corollary 2.5), and the convex hull of finitely many vectors is a polyhedron (Corollary 2.6) — the first half of the finite-basis picture completed by the resolution theorem of Mission VII.
Chapter One of Jim Hefferon's Linear Algebra develops Gauss's method and asks what row reduction actually preserves. The answer arrives as the Linear Combination Lemma: row operations change the rows of a matrix but never the subspace those rows span, and that invariant is complete. The goal theorem is that completeness — two matrices are row equivalent exactly when they have the same row space — which is what makes reduced echelon form a genuine canonical form. The milestones are the two results the chapter builds on the way: that row operations leave a system's solution set alone, and that a solution set is always one particular solution translated by the solutions of the associated homogeneous system.
Where should one look for the optimum of a linear programming problem? Chapter 1 of Bertsimas–Tsitsiklis suggests that optima "tend to occur at corners" of the feasible polyhedron; §§2.5–2.6 turn this intuition into theorems. Not every polyhedron has a corner — a halfspace in () has none — and the exact dividing line is the presence of an infinite line: a nonempty polyhedron
has an extreme point if and only if it does not contain a line, if and only if of the vectors are linearly independent (Theorem 2.6). In particular every nonempty bounded polyhedron and every nonempty standard-form polyhedron has a basic feasible solution (Corollary 2.2). The capstone, Theorem 2.8, is the sharpest form of the corner principle: if has at least one extreme point, then for any cost vector either the optimal cost is , or there is an extreme point of that is optimal — existence of an optimal solution comes for free once the cost is bounded below. Its companion Theorem 2.7 places an optimal extreme point under the weaker assumption that an optimal solution exists, and Corollary 2.3 — the fundamental theorem of linear programming — concludes that every feasible LP either has optimal cost or attains an optimal solution, in stark contrast with nonlinear problems such as minimizing over . These results license the extreme-point search that the simplex method (Mission IV) performs.
Beneath Exp3, Exp4 and their relatives lies one algorithm: minimize past losses plus a convex regularizer. Chapters 26–28 of Lattimore–Szepesvári develop this unifying view. For a Legendre potential with Bregman divergence , both mirror descent and follow-the-regularised-leader satisfy the master bound ; the negentropy potential on the simplex recovers Exp3 exactly. The goal theorem is the payoff for adversarial linear bandits: FTRL on the unit ball with the self-concordant-flavoured potential achieves — improving the factor over the Exp3-style approach of Chapter 27 and matching the lower bound of Mission XI up to logarithms.
Real decisions come with context: a news site chooses an article for a particular user. Competing with the single best arm is then meaningless; the right benchmark is the best mapping from contexts to arms, or more generally the best of expert policies. Chapter 18 of Lattimore–Szepesvári formalizes this via Exp4 — exponential weighting over experts, fed by the importance-weighted estimator of Mission V. The goal theorem: with learning rate , Exp4 satisfies against the best of experts. Since enters only logarithmically, the learner can compete with exponentially large policy classes — the conceptual gateway from bandits to reinforcement learning with function approximation.
Formalize sample-path stability for a continuous-time, unit-rate, infinite-buffer single-server queue. Starting from cumulative arriving service work, define the reflected transient workload, the workload constructed from the infinite past, long-run offered load, and two-time stationarity. Prove that subcritical load forces finite-time coupling and consequently that every finite initial workload converges in its two-time finite-dimensional distributions to the stationary workload law.
Formalize sample-path Little's Law for deterministic continuous-time queueing trajectories, decomposed into area, sojourn, arrival-rate, boundary, and squeeze lemmas.
First raised for two variables by Ludwig Kraus in 1884 and stated in full generality by Ott-Heinrich Keller in 1939, the Jacobian conjecture asks something that sounds almost like freshman calculus: if a polynomial map from complex n-space to itself has a Jacobian determinant equal to a nonzero constant, must it be invertible by another polynomial map? That constant-Jacobian condition is precisely the algebraic shadow of the inverse function theorem, yet producing a polynomial — not merely analytic — inverse has resisted every attack for over eighty years. Shreeram Abhyankar championed the problem because it can be stated 'using little beyond a knowledge of calculus,' and Stephen Smale placed it sixteenth on his 1998 list of problems for the new century. Its notoriety is sharpened by a graveyard of published 'proofs' that later collapsed. Deep reductions exist — Bass, Connell, and Wright showed in 1982 that the general case reduces to maps of degree three — and the problem is equivalent, through work of Tsuchimoto, Belov-Kanel, and Kontsevich, to the Dixmier conjecture on the Weyl algebra. A formal statement anchors this famously slippery problem so that progress can be verified rather than merely believed.
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.
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.