Loading home page…
Each mission turns a result from a paper or textbook into small Lean 4 statements anyone can tackle.
Campaigns group missions around a shared mathematical goal. Each one tracks a quantity, such as an upper or lower bound. Have a good candidate in mind? Ping us on Slack, Zulip, or WeChat.
Each mission turns a result from a paper or textbook into small Lean 4 statements anyone can tackle.
Campaigns group missions around a shared mathematical goal. Each one tracks a quantity, such as an upper or lower bound. Have a good candidate in mind? Ping us on Slack, Zulip, or WeChat.
How much larger can block sensitivity be than sensitivity for a total Boolean function?
For a total Boolean function , a block of coordinates is sensitive at if flipping every bit in that block changes . Let count sensitive singletons and be the maximum number of pairwise disjoint sensitive blocks. Define and .
This campaign seeks larger exponents for which there exists an infinite family of total Boolean functions , indexed by , satisfying
Here denotes a quantity tending to zero as . Higher is better. The classical exponent is , and Huang's bound gives a ceiling of .
OpenAI's construction achieves an exponent strictly greater than .
One sufficient way to establish an exponent is to find a single total Boolean function with and . Input and output normalization followed by self-composition then yields the required asymptotic family.
Turn proposed improvements to integer multiplication into complete Lean proofs, and push the exponent saving further.
Harvey and van der Hoeven established an algorithm in 2021. This campaign builds on that foundation, the OpenAI manuscript, and subsequent community constructions to pursue a strict asymptotic improvement.
For two -bit integers, the target is
A positive beats asymptotically; larger is better. Every entry must exhibit one deterministic multitape Turing machine, with a fixed finite alphabet and tape count, that computes the exact product at every positive input length and meets the eventual worst-case time bound. The tracked number measures an asymptotic exponent saving.
Classical algorithms solve 3SUM in time. In a 2026 breakthrough, Alman and Vassilevska Williams gave a deterministic algorithm, refuting the integer 3SUM hypothesis. How low can the exponent go?
Building on existing Lean formalizations, this campaign tracks upper bounds for 3SUM on polynomially bounded integers, using a word RAM with -bit words, and pursues smaller exponents.
Classical algorithms solve all-pairs shortest paths in time. In a 2026 breakthrough, Alman and Vassilevska Williams refuted the APSP conjecture with a deterministic algorithm. How low can the exponent go?
Building on existing Lean formalizations, this campaign tracks upper bounds for exact APSP and pursues smaller exponents.
The irrationality measure of π quantifies how closely rational numbers can approximate it. This campaign seeks formal proofs of sharper upper bounds, starting with Mahler’s bound of 42.
The sharp Hlawka inequality for Schatten -norms is a cousin of the triangle inequality: it relates the norms of three matrices to the norms of their pairwise sums and their total sum. For complex diagonal matrices, an exact formula for the best possible comparison constant has been proved in Lean for every real . We conjecture that the same formula holds for all .
What is the smallest cutoff for which this formula holds for every real ?
References:
Is every odd number a sum of primes? This campaign tracks formalized proofs of the smallest that suffices.
Schnirelmann (1930) showed some finite works. Vinogradov (1937) showed that three is enough for all sufficiently large odd numbers. Tao (2012) proved unconditionally. Helfgott (2013) proved that every odd number greater than is a sum of three primes, though the proof is still unrefereed. Ideally, we can formalize this statement here. Note that three is optimal: is neither prime nor + prime.
Schoolbook matrix multiplication takes operations. The exponent is the infimum of all such that two matrices can be multiplied in arithmetic operations; trivially , and is conjectured but open.
Strassen gave the first nontrivial bound, , in 1969, and introduced the laser method in 1986 to reach . Coppersmith and Winograd's 1990 bound of stood for two decades. Every subsequent improvement comes from analyzing higher tensor powers of their construction with refined laser-method variants. That line reached in 2025, and the current record is , from August 2026. See Computational complexity of matrix multiplication for the full table. Can we formalize these results and even improve on them?
The first three missions in this programme settle the ordinary magic squares end to end: Mission I proved MacMahon's count , Mission II his semi-magic count , and Mission III classified the normal squares (Lo Shu uniqueness). All three work with the plain magic condition.
This mission counts the two special classes that are singled out by requiring more than magicness, in the opposite directions one expects:
Writing and for the two counting functions, the goal is to determine both for every line sum :
Everything is built on the vocabulary of MagicSquares (Mission I):
IsPanMagic — semi-magic, and every broken diagonal in both directions has
the line sum, indices read modulo ;IsSymmetric — ;panMagicCount, symmetricMagicCount — the cardinalities of the two filtered
finsets of arrays over Fin (t+1), which is lossless because every entry of a
square of line sum is at most .The new definition module MagicSquaresSpecial3 records the two explicit shapes
that the proofs produce: constSquare3 e (the array all of whose entries are
, read over the ambient Fin (3e+1)) and
together with the parameter set symmParamSet e and its
cardinality symmParamCount e.
special_three_count: for every natural number , the pair of equalities
displayed above. The proof splits on and reduces to four child nodes.
pan_three_card). Writing the
array as , the twelve line equations form a linear system
whose only nonnegative solution is . So .symmetric_magic_three_classify).
Symmetry identifies three pairs of entries, leaving five free cells and five
line equations; the anti-diagonal forces , and the rows give
.symm_three_bij). Sending a symmetric magic
square of line sum to is a bijection onto
; hence .pan_three_otherwise,
symm_three_otherwise). Both classes consist of magic squares, and an
order-three magic square has centre (center_of_order_three), so
forces both counts to vanish.The results. The three order-three counts behave completely differently in the same parameter: MacMahon's is quadratic, the symmetric count is linear, and the panmagic count is constant. That contrast is the point of the order-three study — order three is small enough to be completely understood, and the special classes show how differently the two natural strengthenings of the magic condition act. It is also exactly what is lost at order four, where no closed form is known for any of the three.
Formalizing them. The mathematical content is elementary, but the two classes require genuinely different proof techniques, which is what makes the mission worth formalizing:
omega call. The only work is exposing the twelve
equations, which requires reducing the index arithmetic and
on Fin 3.Truncated subtraction, in the admissibility direction. The classification
M = symmMagic3 e (M 0 0) is true for every , without any bound on ;
the bound only appears when asking which members of the family are squares of
line sum . Keeping those two statements apart is what makes the bijection
proof manageable: classification is a pure omega computation, while
admissibility is a one-line argument that forces .
Finite but not decidable. panMagicCount and symmetricMagicCount are
cardinalities of filtered finsets over a function type, so the proofs cannot be
decide or norm_num — the platform forbids native_decide in any case. Both
counting theorems are therefore stated as Finset.card_bij / card_eq_one
arguments over explicit bijections, not as finite evaluations.
center_of_order_three.Fin 3 with a single omega.Additive combinatorics studies what arithmetic structure follows from statistical signals. The Balog–Szemerédi–Gowers theorem is its central regularity statement: a pair of finite sets with large additive energy (many additive quadruples) contains large subsets whose sumset is small. Balog and Szemerédi proved the first version in 1994 using the regularity lemma, which gave a tower-type dependence between the parameters; Gowers obtained a polynomial dependence in 1998. The theorem powers results across the field — from sum-product estimates to the structure of sets with small doubling — and its proof assembles three reusable machines: dependent random choice, the popular-sum graph, and Ruzsa calculus.
Work in an arbitrary abelian group (Lean: AddCommGroup G). For finite
, the additive energy counts quadruples
with ; the trivial maximum is when
. The sumset is , and the difference set
is defined pointwise. A set has small doubling when is
linear in . The Lean development uses Finset.addEnergy and
Finset.addConvolution from Mathlib.
A bipartite graph here is an edge set of type Finset (G × G) with
, not a Mathlib SimpleGraph; solvers should state
graph hypotheses that way. Given such an , the partial sumset
is , following Tao–Vu Definition 2.28.
The mission goal is the two-set (equal-cardinality) form:
This statement is assembled from the sources rather than quoted from them: Tao–Vu Lemma 2.30 supplies the energy-to-graph step, Fox–Sudakov §5.1 (the same theorem as Tao–Vu Theorem 2.29) supplies the graph-level bound, and Ruzsa calculus converts a sumset bound into the difference-set bound above. No cited work states this exact form, and the goal deliberately keeps and existential; the explicit-constant variant is proved separately in the mission with .
The four milestones follow the sources' own numbering and are, in dependency order, Fox–Sudakov Lemma 5.1, Fox–Sudakov Lemma 5.2, the Fox–Sudakov §5.1 / Tao–Vu Theorem 2.29 graph bound with explicit constants, and Tao–Vu Lemma 2.30. The first three lie on the goal's proof path; the fourth is the reusable packaging of the energy-to-graph step.
The result converts a purely statistical hypothesis (many additive quadruples) into genuine algebraic structure (a large subset with a small difference set) with polynomial losses — the step that makes energy methods usable. It is a standard tool behind quantitative Freiman-type arguments.
Formalizing it matters because the constants are the content: the development
tracks explicit constants through dependent random choice (graph level
and ; energy level
and ),
which paper proofs often leave implicit. Fox–Sudakov state the application for
sets of integers; the formalization is over an arbitrary AddCommGroup, with
no further hypothesis on the group. Mathlib at the pinned revision (v4.33.1)
contains no BSG statement, so this fills a genuine upstream gap.
The hard step is dependent random choice: sampling a random vertex subset of the popular-sum graph must simultaneously keep many vertices and keep the induced subgraph dense, and the two requirements fight each other. The naive first idea — take the densest neighborhood — loses control of the vertex count; the fix is a two-stage Markov-plus-payoff selection whose density analysis needs the exact path-count lower bound, not just an order estimate.
Two places where the formalization departs from Fox–Sudakov are recorded on the affected statements rather than hidden: the length-three path count admits degenerate paths (the source's and terms are dropped, which weakens the conclusion and is sound for the BSG use), and the density parameter is instantiated at a guaranteed lower bound rather than the exact edge density.
Sets are Finset G in an AddCommGroup G with DecidableEq; energy is
Finset.addEnergy; graphs are edge sets Finset (G × G), with the pointwise
sumset and difference operations from open scoped Pointwise. Density
hypotheses are stated with explicit real constants. The counting lemmas at the
bottom of the development (sum_addConvolution_eq_card_product,
path3_count_le_triple_rep_count, restricted_sumset_via_multiplicity) are
unconditional; the statements that need them carry the nonemptiness,
equal-cardinality and density hypotheses that exclude degenerate zero-energy
configurations. Welcome contributions: the single-set polynomial
Freiman–Ruzsa consequences, and non-abelian variants.
Finset.pluennecke_ruzsa_inequality_nsmul_add;
see G. Petridis, New proofs of Plünnecke-type estimates for product sets in
groups, Combinatorica 32 (2012), 721–733
(arXiv:1101.3507).Combinatorics/Additive/BalogSzemerediGowers and
BSGEnergyToGraph.The first two missions in this programme counted order-three squares. Mission I proved MacMahon's magic count and Mission II his semi-magic count . What neither does is classify: counting tells you how many squares there are, but not what they look like.
This mission closes that gap for the most classical case of all. A normal magic square of order three is a array containing each of exactly once, whose rows, columns and two main diagonals all sum to the magic constant . The statement to be proved is the uniqueness of the Lo Shu square:
every normal magic square of order three is one of the eight images of under the symmetry group of the square.
In particular there are exactly of them, and they form a single orbit under the dihedral group .
MacMahon's parametrization (already formalized in MagicSquaresParam3) writes
every order-three magic square of line sum as
with ranging over the finite admissible set paramSet e. For a normal
square the magic constant is , so and the centre entry is .
Normality (IsNormal) means every entry lies in and the nine entries
are pairwise distinct — equivalently, they are a permutation of .
together with the identification of those eight parameter pairs. By the
bijection magic_three_param_bij this is exactly the statement that there are
eight normal magic squares of order three, i.e. that Lo Shu is unique up to the
symmetry group of the square.
magic_three_normal_classify). Within that range,
is normal exactly when is one ofThe eight surviving pairs are precisely those with distinct corners of
the Lo Shu square; the excluded ones are those with , for which the
entry collides with the centre .
3. Converse (magic_three_normal_converse). Each of the eight pairs really
does give a normal square.
The result itself. The uniqueness of Lo Shu is the oldest non-trivial classification in combinatorics — it is the order-three case of the classification problem for magic squares, and the reason is special: for there are normal squares (up to symmetry) and for no classification is known. Formalizing it shows that the counting machinery of Missions I and II can be turned around and used as a classification tool: the parametrization plus a finite verification give the complete list, not just the cardinality.
Formalizing it. The whole proof is a finite case check over parameter pairs, so the mathematical content is small and the formalization difficulty is concentrated in making the finiteness usable. Two things have to be arranged before automation can see the problem:
IsNormal is stated with a Function.Injective, which is not decidable
as stated; it must first be rewritten into an explicit conjunction of
entrywise bounds and pairwise inequalities over Fin 3.Fin 3 do not unfold by simp alone; one needs
Fin.forall_fin_succ to expand them before norm_num can decide the
resulting ground instances.Finiteness must be manufactured. Nothing in IsNormal mentions a bound on
or , so the first step is to derive from the entrywise
bounds of normality. Skipping it leaves an infinite search that interval_cases
cannot start.
Truncated subtraction. The parametrization is written over , so entries such as and truncate at zero. Every ground instance must be evaluated with the truncation in place — which is why the classification is carried out by evaluating the actual entries rather than by manipulating symbolic inequalities.
IsNormal).MagicSquaresParam3 and the bijection of Mission I.IsNormal for
Fin 3 (and the Fin.forall_fin_succ technique for unfolding finite
quantifiers), the list of the eight Lo Shu parameters, and the order-three
classification itself.The distinct-distances problem asks how few distinct distances a finite planar point set can determine. Guth and Katz proved the near-optimal bound in 2015. Their argument passes through incidence geometry: distances become incidences between points and curves, and the Elekes–Sharir framework converts the problem into an incidence bound for lines in three-space. Pach and de Zeeuw showed the same pipeline works for points on a fixed algebraic curve, replacing line incidences with curve incidences. The algebraic prerequisite for that replacement — that two bounded-degree real plane curves with no shared component meet in finitely many points, with an explicit degree-dependent bound — is what this mission formalizes.
A real plane curve here is the real zero set of a nonzero bivariate polynomial , written . Its total degree is the maximum over monomials with nonzero coefficient. A curve is irreducible when its polynomial is irreducible.
The paper says two curves have a common component when their polynomials
share a nonconstant factor. The Lean development uses a different, weaker
hypothesis, NoCommonCurveComponent: no infinite irreducible real curve lies
inside both sets. A shared factor whose real zero set is finite (for example
) violates the paper's hypothesis but satisfies the Lean one, so the
Lean theorem covers strictly more pairs of curves than the paper's statement.
Currying views as a univariate polynomial in one coordinate whose
coefficients are polynomials in the other. In the Lean code the polynomial
variable is coordinate and the coefficient (base) variable is coordinate ;
this description writes the base coordinate as and the fiber coordinate as
, so a line is called vertical. The resultant of two
curried polynomials is a polynomial in alone. The development uses one
direction of its defining property: if the two specializations at share a
real root, the resultant vanishes at . All Lean statements use
MvPolynomial (Fin 2) ℝ for plane polynomials and EuclideanSpace ℝ (Fin 2)
for points.
The mission's goal is a finite-intersection bound in the spirit of Theorem 2.1 of Pach–de Zeeuw (Bézout's inequality), but it is not that theorem. It differs in both directions:
The six milestones are the algebraic inputs: coefficient-root counting, the two
resultant-nonvanishing criteria, the fiber bound, and the two mixed
vertical/nonvertical pair bounds that carry the constant . The
nonvertical–nonvertical pair bound (primitive_nonvertical_pair_intersection_bound)
carries the cruder constant . Above the
milestones sit the irreducible-pair assembly with constant and
the factorized assembly with constant , from which the goal
follows.
The result is the algebraic input to the Pach–de Zeeuw distinct-distances theorem for points on curves: without a uniform finite-intersection bound, the incidence count that drives the distance bound cannot even be stated. The formalization pins down every constant and every non-degeneracy hypothesis (non-verticality, no shared infinite component, coprimality) that the argument consumes.
The proof composes four toolkits — univariate root counting, Sylvester-matrix
resultant degree bounds, normalized-factor decompositions, and a smooth
implicit-function nonsingularity argument — whose interfaces must agree
exactly. The resulting lemmas (resultant criteria, fiber bounds,
partial-derivative degree bounds) are reusable for other real-algebraic
incidence formalizations over MvPolynomial.
The central difficulty is elimination with explicit constants: the resultant converts a two-variable intersection problem into a one-variable root count, but every step (currying, specialization, factor-pair summation) must preserve a usable degree bound, and the degenerate configurations (vertical fibers, shared factors with finite real zero set, singular points) each need a separate finite bound.
The textbook route — Bézout's inequality over , then observing that real intersection points are complex ones — is not taken, for two reasons. Mathlib has no plane-curve Bézout theorem to invoke. And under the weaker Lean hypothesis the two polynomials may share an irreducible factor with finite real zero set, in which case the complex intersection is infinite and no complex count applies; that branch is closed by bounding the singular points of the shared factor instead.
Points are EuclideanSpace ℝ (Fin 2); curves are MvPolynomial (Fin 2) ℝ
zero sets; finiteness is Set.Finite with Set.ncard bounds. The development
commits to total degree (not weighted degrees) and to the currying order that
eliminates Lean coordinate ; variable-style implicit degree bounds
are explicit {d₁ d₂ : ℕ} binders on the platform. No statement is
vacuous: every intersection bound carries the non-degeneracy hypothesis
(non-associated irreducibles, non-divisibility, nonzero partials) that excludes
the infinite-intersection cases. Contributions welcome: the sharp
general bound (currently an existential constant), the paper's hypothesis form
(no common factor at all), and the incidence assembly that consumes this
mission's output.
PachDeZeeuw.AlgebraicPrelim and PachDeZeeuw.Bezout (mathlib-only,
axiom-clean).Set cover is the standard worked example of the primal-dual method, and Chapter 2 of Buchbinder's thesis uses it that way: it is where the machinery of §2.1 is first turned on a concrete NP-hard problem. Two analyses appear. The greedy algorithm, analysed by dual fitting, buys the set with the best cost-per-newly-covered-element ratio and charges the price to the elements it covers; the resulting element prices form an infeasible dual that becomes feasible after scaling by . The primal-dual algorithm instead raises the price of an uncovered element until some set's constraint goes tight, buys that set, and repeats; the resulting dual is feasible, and each bought set is paid for by elements of frequency at most , giving an -approximation.
Both analyses have the same shape, and it is the shape that matters for the rest of the series: the algorithm never sees the optimum. It maintains a dual solution, and the approximation ratio falls out of comparing the primal it built against the dual it accumulated.
An instance consists of a finite type of elements, a finite type indexing available sets, an assignment , and a nonnegative cost . Every element is assumed to lie in at least one available set; the source leaves this implicit, and without it no cover exists and the approximation statements are vacuous. The covering LP and its packing dual are
The frequency of an element is the number of sets containing it, and denotes the maximum frequency over all elements.
The two standing assumptions — nonnegative costs, and every element lying in some available set — are carried by a bundled SetCoverInstance, not passed as loose hypotheses. Every source-facing statement in the mission takes such an instance and reads those facts off its fields, so none of them can be instantiated at data violating either. The two indicator lemmas are the exceptions and are labelled as generalized assisting results: one has no cost function in scope at all, and the other's hypothesis that a given covers is strictly stronger than coverability of the family.
Costs are permitted to be zero and the ground type is permitted to be empty. No Nonempty E hypothesis appears anywhere; when is empty, and the -approximation bound reads , which the certificate's tightness clause forces to be rather than anything false.
The results are stated about certificates, not about executable algorithms. This is the central modelling decision of the mission and it is deliberate: the mathematical content of the source's proofs is entirely a statement about the invariants the output satisfies, and separating that from the question of whether a particular procedure produces such output keeps each half provable on its own.
A primal-dual certificate is a pair where covers , is dual-feasible, and every has a tight dual constraint, .
For any primal-dual certificate and any fractional cover ,
Since this holds against every fractional cover, it holds in particular against an optimal one, so the cover costs at most times the fractional optimum and a fortiori at most times the integral optimum.
The one substantive step of the goal is split out as its own target: for a primal-dual certificate,
Tightness rewrites the cover's cost as a double sum over chosen sets and their elements; exchanging the order groups it by element, each charged at most times. With this and weak duality, the goal is two lines.
A greedy certificate at ratio is a cover and a nonnegative with and for every . For such a certificate and any fractional cover ,
Instantiating is what recovers the source's greedy guarantee; the harmonic bound itself is already in Mathlib.
Every dual packing is bounded by every fractional cover, ; the fractional optimum is at most the integral optimum; and both optima are attained, not merely bounded below. Attainment of the fractional optimum is a genuine linear-programming fact and is the hardest supporting item in the mission.
This is where the series first converts a dual-feasibility invariant into an approximation ratio on a concrete combinatorial problem, and the two certificate predicates are reused verbatim by the online covering missions later in the series. Set cover approximation has, as far as we can determine, no prior formalization in Mathlib or in any public Lean library: there is no set-cover problem statement, no greedy analysis, and no -approximation result to build on.
The two certificate bounds are finite-summation arguments of moderate length — the work is in a double-counting step that reindexes a sum over chosen sets into a sum over elements, weighted by frequency. Attainment of the fractional optimum is different in kind: it needs a compactness or vertex argument about the covering polytope and is the item most likely to need real work. Zero-cost sets are permitted throughout, so any later algorithm definition that divides by a cost must handle that case explicitly.
Definitions cover §2.2 of the source, excluding §2.2.2 (randomized rounding), which is deferred to a separate mission because its expected-cost and failure-probability analysis is measure-theoretic and shares no infrastructure with the deterministic results.
Two theorems are not in this mission: that the greedy algorithm produces a greedy certificate, and that the primal-dual algorithm produces a primal-dual certificate. Those require defining the algorithms and proving termination and coverage, and are planned as a second wave. Until that wave lands, the source's Theorems 2.4 and 2.6 should not be described as fully formalized — what this mission establishes is the certificate-to-ratio half of each.
This is the second mission in the magic-squares formalization programme, and it takes up the case the first one deliberately left open.
Counting semi-magic squares — arrays of nonnegative integers whose rows and columns all share a common line sum, with the diagonals unconstrained — is the "honest" version of the enumeration problem. For order three the magic count (mission I) is only a quasi-polynomial: it vanishes unless and equals on . The semi-magic count has no such periodicity. MacMahon computed it in 1915:
It is an honest polynomial in of degree , and that degree is not an accident: Ehrhart and Stanley proved that for every order the function is a polynomial of degree satisfying the reciprocity law . The order-three formula above is the smallest nontrivial instance of that theorem, and the only one small enough that every step of the derivation can still be exhibited explicitly.
So this mission is the natural companion to mission I: same objects, same platform vocabulary, but the counting step is genuinely harder — the parameter space is four-dimensional rather than two, and the parametrization is not injective until it is normalized.
Fix and a line sum . A square of order is an array of nonnegative integers.
For the whole family is governed by the six permutation matrices. Split them into the three even ones — the identity and the two -cycles — whose supports are the transversals
and the three odd ones — the transpositions — with supports
Adding them with multiplicities (even) and (odd) gives
whose six line sums all equal ; so this is a semi-magic square of line sum whenever the multiplicities sum to .
This is the goal because it is the weakest statement that still pins down the answer: it asserts the shape of without naming the parametrization, and it survives verbatim as the case of Stanley's theorem that is a polynomial of degree .
sm3_canonical). Every semi-magic
square arises from the display above, and the representation becomes unique
after normalizing: put , , , subtract the
corresponding even permutation matrices, and the residual odd multiplicities
satisfy . The normalization is necessary — without it the
single relationidentifies distinct -tuples — and it is exactly what makes the count a
partition rather than an inclusion–exclusion.
2. Bijection (sm3_bij). The map from normalized coefficient vectors to
semi-magic squares is a bijection, so .
3. Stars and bars (comps_card). The number of -tuples of nonnegative
integers summing to is ; the case is what the
count needs.
4. Evaluating the parameter count (sm3_params_card). Partitioning the
normalized vectors according to the first zero among writes
as
which collapses to by two applications of Pascal's identity.
The result itself. is the case of a theorem that launched a subject: Stanley's proof that counts lattice points in the Birkhoff polytope makes an Ehrhart polynomial, and the order-three formula is the first nontrivial value of it. Beck, Cohen, Cuomo and Gribelyuk (Amer. Math. Monthly 110 (2003), 707--717) revisited exactly this computation on the way to their quasi-polynomial theorem for the magic counts, and Beck and Zaslavsky later pushed the same technique to the panmagic and symmetric refinements. Getting machine-checked therefore validates the whole hierarchy at its base.
Formalizing it. Nothing here is open; the mathematics is a century old. What is missing is the formalized artifact, and the difficulty is concentrated in two places that are formalization difficulties rather than mathematical ones.
First, surjectivity of the permutation-matrix parametrization. The usual proof quotes Birkhoff–von Neumann, which in turn needs Hall's marriage theorem. For order three one can instead do it by hand: subtract the three even transversal minima and show that the residual satisfies . That last step is a six-case argument in linear arithmetic — if then each of the three ways for the transversal to have minimum zero forces — and it is precisely the kind of step that is invisible on paper and must be made explicit in a proof assistant.
Second, the counting step. The parameter set is a filtered finset of
functions Fin 6 → Fin (t+1), while the formula is stated with binomial
coefficients over . Connecting them requires stars-and-bars, proved
from scratch (by induction on the number of parts plus the hockey-stick
identity), because the available library results count sub-multisets rather
than compositions. And the final collapse to MacMahon's form is a chain of
Pascal identities that must be applied in the right order to stay inside
, where subtraction is truncated.
Two traps deserve to be named.
Uniqueness needs the normalization. The representation by six multiplicities is not injective: . Any formalization that counts -tuples directly will overcount, and the correction is not a subtraction but a choice of canonical representative. Deciding "first zero among " is what turns the count into a genuine partition.
Truncated subtraction. The decomposition is expressed over , so every identity — in particular the recovery of the multiplicities from a square — must be stated with the admissibility inequalities as explicit hypotheses. A truncated subtraction is only correct because normalization forbids the truncation, and that side condition has to be discharged rather than assumed.
Fin n; semiMagicCount n t is the cardinality of a
finset of arrays over Fin (t+1) — lossless, since every entry is at most
.Counting magic squares — arrays of nonnegative integers whose rows, columns and two main diagonals all share a common line sum — is one of the oldest problems in enumerative combinatorics, and the testing ground on which the general theory was built. MacMahon computed the order-three count in 1915 by hand; sixty years later Stanley, and then Beck, Cohen, Cuomo and Gribelyuk (Amer. Math. Monthly 110 (2003), 707--717), showed that for general order the counting functions are quasi-polynomials in the line sum, by identifying them with Ehrhart quasi-polynomials of rational polytopes. The order-three case is the oldest nontrivial instance of that theory and the one where every step can still be checked by hand.
The subject therefore has a curious status: the enumerative answer for has been known for over a century, and the structural facts behind it (a magic square is determined by two corner entries; opposite cells sum to twice the centre) are folklore — but none of it has a machine-checked proof. This mission formalizes the classical derivation end to end.
Fix an order and a type of entries. A square of order is an array with entries in ; its row sums, column sums, and the two diagonal sums (main and anti-diagonal) are the sums of the entries along those lines.
No distinctness of entries is required. Let denote the number of semi-magic and the number of magic squares of order with nonnegative integer entries and line sum . Every entry of such a square is at most , so these are finite counts.
For the whole family is parametrized. If has line sum then the centre cell equals , and writing and the eight line identities force
All nine entries are nonnegative exactly when
and substituting , turns these into : the ball of radius in .
together with the companion vanishing when . This is the count of magic squares of line sum with nonnegative integer entries (entries need not be distinct). It is the goal because it is the weakest stable statement: it asserts only the shape of the answer, not the intermediate parametrization, and it survives verbatim as the case of the general quasi-polynomial theorem.
That the map is a bijection from the magic squares of line sum onto the admissible parameter pairs, and that the latter are counted by the -ball cardinality. This is the route the mission actually takes; the count is its corollary.
, the analogous count for semi-magic squares, is a genuinely different and harder quasi-polynomial. It is listed as a stretch target, not a milestone.
The result itself. MacMahon's formula is the base case of the Ehrhart-theory reading of magic-square enumeration; Beck--Cohen--Cuomo--Gribelyuk's quasi-polynomial theorem for general degenerates to it at , so it is the sanity check any generalization must pass. The parametrization behind it is what makes the "how many" question finite-dimensional at all: it reduces a search over arrays to a count of lattice points in a two-dimensional ball. Downstream, the same parametrization governs the classification of normal magic squares (the Lo Shu square and its symmetries) and the associativity identity .
Formalizing it. The mathematics is classical and proved; nothing here is
open. What is missing is the formalized artifact. The order-three structural
lemmas — the centre identity, the opposite-cell identity, and the two directions
of the parametrization — are already machine-checked on this platform. The
remaining work is the counting step: exhibiting a concrete bijection between
two finsets whose elements live in different types (arrays over Fin (3e+1)
versus pairs of naturals) and evaluating a finite sum. That is where the
formalization, not the mathematics, is hard.
The obvious attack — "each magic square is determined by , so just count
the pairs" — fails at exactly one point, and it is not a mathematical point. The
counting function is defined as the cardinality of a finset of arrays with
entries in Fin (3e+1) (a finite type, so that Finset.univ exists), whereas
the parametrization lives over . Proving the counts agree therefore
requires a honest Finset.card_bij in both directions:
mkMagic3 from an admissible pair, coerce every entry into
Fin (3e+1) using the bound , and show the round trip is
the identity.Neither direction is deep, but the coercions are unforgiving: a truncated
subtraction in mkMagic3 is only correct because admissibility forbids the
truncation, and that side condition must be discharged explicitly rather than
assumed. The second difficulty is the cardinality of the ball: the
identification needs the elementary identity
, after which the count is
.
Fin n; the anti-diagonal uses Fin.rev, and broken
diagonals use addition modulo . Counting functions are cardinalities of
finsets of arrays over Fin (t+1) — lossless, since every entry is at most
— and return natural numbers.mkMagic3 is defined over with truncated subtraction. Every
row/column/diagonal identity therefore carries the admissibility inequalities
as explicit hypotheses; no identity is asserted unconditionally.Square, IsSemiMagic,
IsMagic, IsPanMagic, IsAssociative, IsNormal, magicConstant, and the
four counting functions ), the symmetry/affine toolbox, and
the order-three structural lemmas. Contributions are welcome on the
semi-magic count , on panmagic and associative refinements, and on the
extension to general .An online algorithm must commit to decisions before it knows the rest of its input, and it is judged by competitive analysis: the ratio between its cost and the cost of an optimal solution computed with full knowledge of the input. A recurring obstacle in this area is that each problem seems to need its own ad hoc potential-function argument. Buchbinder's thesis develops a single method that replaces those arguments — formulate the offline problem as a covering linear program, let the online algorithm raise the dual variables of its packing dual, and read the competitive ratio off the ratio between the primal and dual increments. The same recipe then yields algorithms for online set cover, weighted caching, ad-auction revenue, routing, and load balancing.
This mission formalizes the chapter where the method is introduced on its smallest example, the ski-rental problem. A customer needs skis for an unknown number of days: renting costs per day and buying costs once. The customer must decide, each morning, whether to rent again or buy, without knowing how many ski days remain. Despite its size the problem is the canonical rent-or-buy dilemma, and it has two classical tight results: a deterministic -competitive algorithm, and a randomized algorithm whose competitive ratio tends to , due to Karlin, Manasse, McGeoch and Owicki (1994). The primal-dual derivation of both is the content of Chapter 3.
An instance is a pair : the purchase price , a positive integer, and the number of ski days, which the online algorithm does not know. An offline solution either buys at once, paying , or rents on every day, paying ; so the offline optimum is
Chapter 3 casts this as a linear program (Figure 3.1, p. 18). The primal is a covering program with one buy variable and one rent variable per day :
Its dual is a packing program with one variable per day:
The online structure enters in a single way: a new ski day appends a new covering constraint to the primal and a new variable to the dual, and previously raised primal variables may never be decreased. That monotonicity is what "previous decisions cannot be regretted" means formally.
The fractional primal-dual algorithm maintains , initially . On each new day, while it sets , then raises
and sets ; once has reached it does nothing further. The free parameter is then pinned to the value that makes reach exactly after days,
The coefficient is the exact finite- ratio , left in closed form rather than replaced by a constant. This is deliberate: increases to , so and therefore for every finite . A goal asserting -competitiveness at finite would be false, and a goal asserting some rounded constant would be invalidated by any sharpening. The closed-form coefficient is the weakest statement that is stable under improvement.
The classical constant is recorded here, as a limit of the coefficient sequence, and nowhere else.
Chapter 3's other result, independent of the fractional development.
The ski-rental bounds themselves are classical and tight, and nothing here is mathematically open. What the chapter contributes, and what this mission captures, is the derivation: it is the template instantiated by every later chapter of the thesis, so the artifacts built here — a covering/packing LP pair, its weak-duality instance, a monotone online variable with a closed-form growth law, and the primal-to-dual increment ratio as the source of the competitive factor — are the vocabulary in which the rest of the series will be stated.
On status: the mathematics is proved, published, and standard. It is not, to the best of a search of Mathlib at revision 0df444a, formalized — that revision contains no competitive-analysis or online-algorithm framework, no ski-rental development, and no general linear-programming weak-duality theorem. So the work this mission asks for is formalization of a known proof, not new mathematics, and the reusable output is infrastructure that does not currently exist in the library.
The offline problem is trivial, and a newcomer's first move — prove is the optimum and stop — solves the wrong problem. The content is entirely in the online constraint. Three specific places where the obvious argument stalls:
The optimum is never observed. The algorithm's cost must be compared against without being available to it. The comparison is routed through the dual instead: the dual objective the algorithm accumulates is a lower bound on every feasible primal solution, hence on the optimum, and the algorithm's own primal cost is a fixed multiple of that dual objective.
The growth law is piecewise. The update fires only while . Summing the per-day increments therefore does not telescope uniformly: days before reaches contribute each and later days contribute nothing, and the index at which the switch happens is exactly — which is a theorem about the recurrence, not an assumption.
The constant is forced, not chosen. is not a free tuning parameter; it is the unique value for which the geometric sequence hits at , which is in turn what makes the dual solution feasible (). Dual feasibility and the choice of are the same fact.
Conventions this development commits to. The purchase price is a natural number with , because Chapter 3 uses simultaneously as a price, as a day index ("buy skis on the th day"), and as the exponent in ; costs are real numbers, with and coerced. Days are indexed from , so day of the prose is index , and Fin k indexes the days. Real division is total, so ; the hypothesis is what keeps every reciprocal in the development genuine, and without it would evaluate to and the recurrence would collapse to the constant zero sequence. The algorithm's x < 1 guard is part of the formalized definition, not an informal aside: without it the cost would keep growing past day .
A documented discrepancy in the source. The prose on p. 17 relaxes the integer program by letting and each range over ; Figure 3.1 on p. 18 prints only , . This mission takes the prose version, and , as the canonical fractional program, and also records the nonnegativity-only region exactly as printed. Two separate theorems establish that both have least value , so the discrepancy is resolved inside the mission rather than silently chosen. Solvers should note which of the two predicates a given statement uses.
Ruling out a trivializing formalization. The offline optimum is defined independently, as , and is not derived from the algorithm's own behaviour; a separate theorem certifies that this value really is the least attainable objective value of the canonical program, so the goal cannot be satisfied by redefining the benchmark. The goal inequality is also tight — both sides are equal to times the number of days on which — so it cannot be weakened into vacuity without becoming false.
Infrastructure, and what is reusable. The development needs only Mathlib big operators over Fin k, basic real analysis for the limit, and IsLeast. Two items are explicitly infrastructure rather than ski-rental content: the specialized weak-duality theorem for this covering/packing pair, and the Figure 3.1 optimum. Both are candidates for generalization by the later mission on Chapter 2's general linear-programming duality, and a solver who proves the general form there should expect this instance to be derivable from it rather than duplicated.
Out of scope here. The final paragraph of p. 19 rounds the fractional solution into a randomized algorithm by sampling a threshold uniformly and buying on the day whose increment of contains . That step needs a probability space and an expectation argument, and is deferred to the immediate follow-up mission, Primal-Dual Online Algorithms II: Randomized Rounding for Ski Rental. Contributions here should not anticipate it.
Bayesian filtering estimates an unobserved state from measurements arriving over time. A filter combines what the state dynamics predict with what the newest observation says. In neural decoding, for example, the state may describe an intended movement while the observation contains activity from many recorded neurons. The observation can have many more coordinates than the state and need not follow a linear Gaussian observation model.
The Discriminative Kalman Filter (DKF) uses a Gaussian approximation to the state conditional on the newest observation. It combines that approximation with a Gaussian state transition and a correction for the stationary state distribution. The resulting recursion retains a mean vector and covariance matrix. Burkhart et al. developed this construction and proved an asymptotic justification in Theorem 2 of Appendix B.
The historical starting point is the linear Gaussian filter of Kalman (1960). The 2020 DKF paper changes how observation information enters the update and establishes a corresponding approximation theorem. The present mission concerns formal verification of that published theorem.
The state space is for a positive finite dimension . Write for the ordinary multivariate Gaussian density with mean and symmetric positive-definite covariance . Densities and their distances are with respect to Lebesgue measure.
The state model has a matrix and positive-definite covariance matrices satisfying
Its stationary density and transition density are
For an integrable density , prediction gives
The discriminative update combines a previous filtering density with a density for the state given the current observation:
This expression is a probability density when its nonnegative weight has a finite, strictly positive integral. Dividing by is part of the standard DKF under consideration.
For Gaussian inputs with parameters and , define
The DKF step returns mean and covariance when the precision is invertible and the covariance is positive definite. The recursive filter starts from mean zero and covariance , using the current observation's functions and as the Gaussian input mean and covariance. These are the updates in equation (2.7) of the paper.
Fix sequences of probability densities , indexed by positive integers, whose exact normalized updates
are well defined for every index. Fix Gaussian density sequences , a point , and a probability measure . The five assumptions are
Here denotes weak convergence, characterized by convergence of expectations of every bounded continuous real function; is the unit point mass at . The measure need not have a density and may be degenerate.
The main goal is the complete conjunction of Theorem 2's conclusions, with separate milestones for each:
is a well-defined Gaussian density for all sufficiently large .
A sixth milestone is Lemma 1 (DKF equation): the normalized Gaussian-input update has the explicit mean and covariance above whenever valid, and the two input weak limits imply its eventual validity and convergence to . It includes both the exact equation and the asymptotic assertion from the source.
In addition to neurodecoding with intracortical brain-computer interfaces, the DKF has also found applications in optimization and sequential data augmentation (see references). The original study was successfully reproduced by Casco-Rodriguez, et al. in ReScience C.
The inverse stationary density can grow in the tails, so small errors in the input densities do not immediately control the error after division and renormalization. Normalizing constants must remain finite and nonzero. The candidate Gaussian covariance must also become positive definite as a conclusion of the assumptions, rather than through an extra validity assumption imposed at every index.
There is a second distinction between convergence to a point mass and approximation in . Two sequences may concentrate at the same point while retaining different shapes at shrinking scales. The C5 target therefore requires the full approximation argument, beyond the weak-convergence conclusions.
Lean represents states as Fin d → ℝ and covariance matrices as real square matrices. The Gaussian density is the standard determinant-and-quadratic-form formula. The definition of Gaussian PDF includes positive-definite covariance and equality of densities almost everywhere. Thus null-set changes do not constrain the theorem artificially.
Probability density validity explicitly includes nonnegativity almost everywhere, integrability and total integral one. The quantity is an extended nonnegative integral. The update's validity explicitly requires measurable weight and a finite, strictly positive normalizer. Total expressions outside that domain supply no assumed probability interpretation; C3 establishes validity on a tail.
All density sequences use positive integer indices. The limit measure is a Mathlib probability measure. Weak convergence is tested against Mathlib bounded continuous functions using the actual measures generated by the densities. The stationary model, standard recursive DKF, exact update and approximate update are defined independently of the theorem conclusions.
The mission addresses deterministic Theorem 2 of Appendix B. The random-sequence extension in Remark 4, conditions implying a Bernstein–von Mises theorem, and induction over filtering time are separate developments. The proof plan follows the appendix through C1–C2, Lemma 1, C3–C4, and the five-term comparison for C5.
A foundation model trained on tokenized electronic health record (EHR) timelines can be used to predict clinical outcomes without ever being finetuned for a specific prediction task: condition the model on a patient's observed timeline, autoregressively sample many possible futures, and report the fraction of sampled futures in which the outcome of interest occurs. This generative approach to inference powers a growing family of EHR foundation models— including Event Stream GPT (McDermott et al., 2023), Foresight (Kraljevic et al., 2024), ETHOS (Renc et al., 2024), and Curiosity (Waxler et al., 2025)—and it is attractive for its zero-shot approach to predicting a variety of outcomes.
It is also expensive. Reproducing one published pipeline required more than A100 GPU-hours of inference. Worse, the estimator built from sampled futures takes values in , so its resolution is tied to the sampling budget: for an outcome of prevalence , sampled futures fail more than of the time to rank a patient at ten times average risk above an average one. The most consequential clinical decisions turn on exactly such low-prevalence, high-impact outcomes.
Solo et al. (arXiv:2602.03730) observe that Monte Carlo discards almost everything the model produces: at every step the model emits a full next-token distribution and the sampler keeps only the token it drew. The paper introduces two estimators that consume the discarded probabilities instead, and proves that doing so costs no bias and—for one of them—never costs variance.
Let generate token sequences from a countable vocabulary , with designated outcome token . The next-token probabilities may depend on the complete preceding history. The time threshold is initially unexceeded. Its crossing may depend on several kinds of time-spacing tokens and on their accumulated duration.
For a sampled timeline , is the first position occupied by , or if it never appears. The time is the first position at which the threshold has been exceeded. Assume almost surely. Timelines are retained through the actual threshold crossing, even if the outcome appears earlier. Thus is not reassigned after an outcome.
The threshold is reached almost surely, but the number of tokens required may be arbitrarily large. No deterministic bound or finite expected token count is assumed. For REACH, assume also that removing the outcome token and renormalizing defines a sampler that reaches the same threshold almost surely.
For independent original timelines, the Monte Carlo estimator is
The SCOPE estimator is
For REACH, sample independent outcome-free timelines by setting the next-token probability of to zero and renormalizing the probabilities of the other tokens. Using the original model probabilities along those timelines, define
The targets are:
Expectations and variances use each estimator's specified sampling law.
The claims concern the probability assigned by the generative model. They provide unbiasedness and a comparison of sampling variance. SCOPE is kept unclipped, as in the paper's unbiasedness result. All five target statements have accompanying local Lean proofs.
A pathwise finite stopping time need not have a common finite bound or a finite mean. An expectation involving the stopped SCOPE sum therefore needs justification beyond finite-sum linearity. REACH uses a different sampling law, so its unbiasedness and variance comparison also require a proved connection between the original event and the two-stage experiment. The equal-probabilities milestone records that connection explicitly.
Lean represents each sampled timeline by a finite list ending at its first threshold crossing. Arbitrary finite lengths are included in the same sample space. Path probabilities are products of next-token probabilities, and the laws are countable sums of these path masses. Requiring each law to have total mass one expresses almost-sure termination of that sampler; it is not a uniform length bound. The vocabulary can be finite or countably infinite.
The stopping predicate examines a complete prefix and is not restricted to a single terminal token. The original law continues through outcomes until the threshold. A separate almost-everywhere hypothesis excludes equal outcome and threshold times. The code proves that the actual threshold time is finite almost surely and that the strict event is the event used by the internal calculations.
The two-stage experiment explicitly samples conditionally independent Bernoulli trials using the original hazards. Its conditioning information retains the complete indexed pool of outcome-free timelines. The Rao–Blackwell target uses Mathlib's conditional expectation. The variance target uses Mathlib's variance, and proves square integrability rather than assuming it.
Essentially every quantitative model written as a rate of change — a mechanical system, a chemical reaction network, a population model, a control loop — is an ordinary differential equation (ODE) together with an initial condition. Before anything can be computed about such a model, two questions must be settled: does a solution through the given initial state exist, and is it the only one? The classical answer is the Picard–Lindelöf theorem: a Lipschitz right-hand side yields a unique local solution. Uniqueness is not a technicality — it is what licenses speaking of the trajectory through a point, hence of a flow, and so it underwrites the entire qualitative theory of dynamical systems that the source text builds afterwards (vector fields, tubular flow, -limit sets, Poincaré–Bendixson, Grobman–Hartman, stable manifolds).
This mission is the first in a series formalizing Augusto Armando de Castro Júnior's lecture notes Curso de Equações Diferenciais Ordinárias (2009), a graduate ODE course that develops the theory directly in Banach spaces, not only in . The book proves existence and uniqueness once, in that general setting, and then reuses it throughout; this mission formalizes that foundation.
Let be a real Banach space, , , and . Write for the closed ball and
A map is Lipschitz with respect to the second variable with constant if
the same serving for every (Definição 2.1.1 of the source).
Given , the Cauchy problem (initial value problem) with initial data asks for a curve , defined on a nondegenerate interval , such that for all , , and for all — one-sided derivatives at the endpoints of (Definições 1.0.1 and 1.1.1). Equivalently, by the Fundamental Theorem of Calculus, is continuous with graph in and satisfies the integral equation
Finally, put and .
The goal theorem is Teorema 2.1.2 (Picard) of the source: if is continuous, bounded, and Lipschitz in the second variable, then the Cauchy problem , has a solution on , and any two solutions on that interval whose graphs stay in coincide there:
The milestones are the results the source uses to get there, in its own order: the contraction fixed point theorem (Teorema 0.2.10), the equivalence between the Cauchy problem and the integral equation (Capítulo 2, opening paragraphs), the sufficient condition for Lipschitz dependence via a bounded partial derivative (Proposição 2.1.4), and the global version on a whole interval (Corolário 2.1.3).
Picard's theorem is what makes the initial value problem well posed in the sense of Hadamard's first two requirements. Downstream in the same book it is the hypothesis behind maximal solutions and the escape-from-compacts property (§2.3), continuous and differentiable dependence on initial conditions and parameters (Chapter 3), and the local flow of a vector field (Chapter 4). Without uniqueness none of these statements can even be phrased.
As for formalization status: Mathlib already contains a Picard–Lindelöf development
(IsPicardLindelof, ODE_solution_unique and relatives) and a Banach fixed point theorem
(ContractingWith.exists_fixedPoint). The work this mission asks for is therefore not the
discovery of a proof but a faithful bridge: stating the source's hypotheses as the source states
them — a closed ball, a supremum bound , the radius , Lipschitz in the
second variable with one constant for all times, uniqueness among solutions whose graph stays in
the domain — and deriving them from, or proving them alongside, the library's own formulation.
Such bridges are where unfaithful formalizations usually hide, and they are reusable by every
later mission in the series.
The obvious route is "cite the library and close the goal". It does not go through unchanged, for three reasons. First, the hypothesis shapes differ: the library packages its assumptions in a structure with its own choice of ball, bound and time radius, and matching with a supremum-defined requires the boundedness argument to be redone at the interface. Second, uniqueness here is asserted for solutions in the sense of this mission's definition — derivative within the interval, one-sided at the two endpoints, graph inside — so a Grönwall-type uniqueness statement must be transported to that formulation, including the endpoint cases. Third, the source works with an arbitrary Banach space and only assumes bounded, rather than assuming finite dimension; compactness arguments are unavailable by design.
The remaining genuine mathematical content sits in the milestones: the iterate estimate used by the source to make some iterate of the Picard operator a contraction, and the mean value inequality on a convex open set behind Proposição 2.1.4.
Conventions this proposal fixes, all visible in the definitions item:
A complete development needs the Bochner and interval integrals, the contraction mapping API, the mean value inequality for Fréchet derivatives, and the ODE files. Contributions of independent interest to the series: the Picard iterate factorial estimate, and the conversion between the library's Picard–Lindelöf hypotheses and the ones above.
Mathlib/Analysis/ODE/PicardLindelof.lean and Mathlib/Analysis/ODE/Gronwall.lean,
https://github.com/leanprover-community/mathlib4.In 1918 Emmy Noether published Invariante Variationsprobleme (Nachrichten der Königlichen Gesellschaft der Wissenschaften zu Göttingen, Math.-phys. Klasse, 235–257), answering a question raised by Hilbert and Klein about the status of energy conservation in the general theory of relativity. The paper proves two theorems that tie the symmetries of a variational integral to structural properties of its Euler–Lagrange equations: continuous symmetries depending on finitely many parameters produce divergence identities ("conservation laws"), while symmetries depending on arbitrary functions produce identities among the Euler–Lagrange expressions themselves, so that some of the field equations are consequences of the others. The first theorem is the source of the correspondence between time translation and energy, space translation and momentum, rotation and angular momentum; the second underlies the Bianchi-type identities of generally covariant theories and the gauge identities of field theory.
This mission formalizes the two theorems of §1 of the paper, together with the chain of identities of §2 and §3 by which Noether derives them, in the case of first-order Lagrangians.
Fix integers (independent variables), (dependent variables). Points of the base are , and a field is a map , written componentwise . Write for the derivative of a scalar function on along the -th coordinate direction, and
for the divergence of a vector field on .
A Lagrangian is a function of the point , of the field value , and of the array of first derivatives . Along a field one writes , and the integral under study is . The momenta are
and the Lagrange expressions — the left-hand sides of the Euler–Lagrange equations — are
An infinitesimal transformation is given by generators on the independent variables and on the dependent ones. Noether's equation (9) replaces them by the variation at fixed ,
and the corresponding variation of the Lagrangian is
Two vector fields organise the boundary terms: the partial-integration vector of equation (3), and Noether's
Invariance of enters through Noether's equation (11), the pointwise identity
which the paper derives in §2 from the vanishing of over every region.
The goal theorem is Theorem I of the paper, in the first-order case, in the form Noether states as equation (13). Given generators , , each satisfying the invariance identity (11) with its own from (9), one has for every and every
The milestones are the intermediate statements of the paper, in the order in which it proves them: the central identity (3), the passage from the invariance of the integral to the pointwise identity (11), the single-generator divergence identity (12), the conservation law on solutions of the Euler–Lagrange equations (§3), the converse of Theorem I (§3), and Theorem II in the form of the dependency relations (16) for a group depending on arbitrary functions entering to first order.
Theorem I is the general statement behind every "first integral from a symmetry" argument in mechanics and field theory; Theorem II is the statement that a variational theory invariant under a group of arbitrary functions has field equations that are not independent — of them follow from the rest — which is the group-theoretic form of the failure of a proper energy conservation law in general relativity that Hilbert had asserted. The two theorems are used constantly and stated loosely; a formal version fixes exactly which hypotheses are needed and what the conclusion says.
Mathlib contains the differential-calculus and measure-theoretic infrastructure used here (Fréchet derivatives, integration on , compactly supported test functions, and the standard vanishing lemma for locally integrable functions tested against smooth compactly supported functions), but no calculus of variations: there is no Euler–Lagrange operator, no first-variation formula, and no Noether theorem. This mission supplies the first-order, finite-dimensional-base version of that material, with definitions that later missions (higher-order Lagrangians, the -th order identity (6), mixed groups) can extend.
The algebraic core — the central identity (3) and the passage to (12) — is a product rule plus a reindexing, and the real work is elsewhere.
Two steps are genuinely analytic. First, Noether's inference from "the integral of the integrand vanishes over every region" to "the integrand vanishes pointwise" (equations (10)–(11)) requires the regularity of the integrand to be used explicitly. Second, Theorem II's equation (16) requires integrating by parts against an arbitrary function and then applying the fundamental lemma of the calculus of variations in : the arbitrary functions of the group must be specialized to compactly supported test functions before the boundary terms can be discarded.
The remaining difficulty is bookkeeping: every statement must carry the differentiability hypotheses that make each derivative in it meaningful, since in Lean an undefined derivative silently evaluates to zero rather than failing.
The formalization is in the first-order setting: the Lagrangian depends on , on , and on the first derivatives of only. The base is with fixed but arbitrary, and fields are globally defined maps ; no boundary conditions, no manifolds, and no jet bundles are used. The group is not formalized as a group: as in §2 of the paper, only its infinitesimal generators , enter, and the invariance hypothesis is Noether's identity (11). The linear independence of the divergence relations, which Noether argues from the essentiality of the parameters, is not part of the formal statements.
Derivatives are Fréchet derivatives: is the derivative of at applied to the -th standard basis vector, and partial derivatives of the Lagrangian are derivatives of the corresponding partially applied function. Because Lean's derivative operator returns at points of non-differentiability, each statement carries explicit differentiability hypotheses for exactly the functions whose derivatives it mentions; a solver may not assume more.
The statements are not vacuous: the hypotheses of every milestone are satisfied, for instance, by smooth Lagrangians and smooth fields, and the invariance hypothesis (11) is satisfied by the classical examples (a Lagrangian independent of with , ). Degenerate parameter values are admitted and behave as expected: for or the sums are empty and the identities reduce to , and for the goal quantifies over an empty index set.
Contributions of independent interest that this mission would welcome: a reusable statement of the fundamental lemma of the calculus of variations on in the form needed for (16), and the higher-order analogue of the central identity, Noether's equation (6).
Transformer sequence models modulate attention scores by a function of the relative position between a query and a key: the attention logit between token and token is scaled by a fixed profile . Realizing this modulation the naive way means evaluating once per pair and materializing an adjustment over the whole sequence — quadratic in the sequence length . Rotary Position Embedding (RoPE) Su et al. 2021 avoids this entirely: it rotates the query at position and the key at position independently, each by an angle depending only on its own position, so that the pairwise quantity falls out of the dot product of the two separately rotated vectors — is never evaluated pairwise, and no matrix is ever built. This is what lets RoPE stay a linear, per-token preprocessing step compatible with efficient (sub-quadratic) attention implementations, rather than an modulation. The catch is that RoPE's specific log-linear frequency schedule bakes in one particular profile: a monotone, decaying . That schedule is a poor fit whenever the correlation structure of the data is not monotonically decaying with distance — the leading example being periodicity: in sequential recommendation, interactions separated by exactly one day or one week are more correlated than interactions separated by, say, half a day, and a decaying profile cannot express that "attention comes back" at the period.
Chen, Ainslie, Choromanski et al., ClockRoPE: Random Fourier Rotations for Temporal Routine Modeling (arXiv:2607.26369), ask a more general question first: which attention-modulation profiles can be realized at all by this same per-token, pairwise-iteration-free rotation trick — rotate each token once, on its own, and let the pairwise profile emerge from the dot product — and by what rotation-frequency schedule? Their answer is a random-features construction — sample the rotation frequencies from the kernel's own Fourier transform, rather than fixing them log-linearly — that realizes any continuous, normalized, positive-definite profile in expectation, with a quantified concentration rate, all while keeping the exact same per-token rotate-then-dot-product computation RoPE already uses. ClockRoPE is the periodic instance of this general theory, later deployed in a production-scale generative-retrieval system.
Fix an embedding dimension and group a vector into consecutive feature pairs for . For an angle , let
be the (Givens) rotation matrix. A real kernel is positive definite if for every finite family of points and complex coefficients , has nonnegative real part; it is normalized if . When is also continuous and Lebesgue-integrable, its Fourier transform
is (by Bochner's theorem) a genuine probability density on : this is the distribution the mission's rotation frequencies are sampled from.
Given a query at position , a key at position , and i.i.d. frequencies , the Random Fourier Rotation (RFR) estimator is
is exactly the modulated attention logit computed by rotating query/key feature pairs with per-pair, sampled RoPE frequencies — the same operation standard RoPE performs, but with drawn from instead of fixed by a log-linear schedule.
for every . This is the mission's central target: it upgrades the mean identity below into a quantitative, non-asymptotic guarantee that the sampled estimator is close to the target profile with high probability, at a rate that is exponential in the embedding dimension .
The expectation identity that the concentration bound above sharpens; it is the feasibility half of the claim ("this construction is correct on average") that the convergence half needs as its starting point.
For a continuous, positive-definite, -periodic with and Fourier coefficients ,
The periodic specialization needed to apply the goal and first milestone with a discrete frequency distribution over harmonics — the regime ClockRoPE actually deploys, since daily/weekly routines are periodic rather than merely decaying.
The result gives a general recipe — sample, don't hand-design — for turning any admissible attention-modulation profile into a RoPE-compatible rotation schedule, with a concentration guarantee that says how many feature pairs are needed before the sampled schedule reliably approximates the target profile. Crucially, the recipe changes only which frequencies the per-token rotation uses — it never touches the computational shape of RoPE itself: each query and key is still rotated once, independently, by an angle depending only on its own position, and the target pairwise profile is still recovered purely from the dot product of the two rotated vectors. So realizing an arbitrary positive-definite this way costs exactly what realizing RoPE's own log-linear profile costs — linear in the sequence length, with no pairwise evaluation of and no matrix ever materialized — rather than the quadratic cost a direct, per-pair implementation of an arbitrary modulation function would require. This subsumes standard RoPE's log-linear schedule as one instance and explains, via the periodic corollary, why a schedule built from the kernel's own spectrum (rather than an arbitrary log-linear one) is the right way to encode periodicity: nothing about the construction, or its efficiency, is specific to decay. The paper reports this translated into measured gains in a production-scale generative-retrieval system, which is unusual weight of practical evidence behind a Bochner/Herglotz-style spectral argument.
At the time of writing, none of these three results have a machine-checked proof; this mission asks for the first formalization of all three, together with the shared scaffolding (feature-pair extraction, the rotation estimator, and the notion of a positive-definite kernel) they are stated over.
The natural first attempt at the concentration bound is a direct union bound or a naive variance argument, but the estimator is a sum of terms that are each bounded (each rotated pair lies on a fixed-radius circle) rather than governed by a variance bound that shrinks with under a fixed frequency; the source proof instead applies McDiarmid's bounded-differences inequality, treating each sampled frequency as one coordinate of the input and bounding the one-coordinate change in by via the maximal distance between two points on the unit circle — not by directly bounding a variance term. Establishing Proposition 3.1 itself already requires care: it requires justifying that , defined purely as an integral transform of , is in fact a legitimate probability density (Bochner's theorem), and then a real/complex bookkeeping argument identifying the real inner product of rotated pairs with the real part of a product of complex exponentials.
The mission works over the reals and represents feature pairs as functions
Fin (2 * n) → ℝ sliced into Fin n-indexed pairs, matching the " feature pairs,
dimension " convention used throughout; rotations are ordinary
Matrix (Fin 2) (Fin 2) ℝ values built with Matrix.mulVec/Matrix.dotProduct, and
expectation over i.i.d. -distributed frequencies is formalized as integration
against the product measure MeasureTheory.Measure.pi of n independent copies of
the measure with density (MeasureTheory.Measure.withDensity) — this is
mathematically equivalent to, and more directly usable in Lean than, introducing an
abstract probability space with named i.i.d. random variables.
Since a general continuous positive-definite kernel need not have an
integrable Fourier transform (the periodic case in Corollary 3.3 is exactly the
counterexample: its "Fourier transform" is a discrete measure, not a density) — the
goal and first milestone add Integrable f as an explicit hypothesis beyond what the
paper states in prose, so that is genuinely a density rather than a junk value.
This is not a strengthening of the target profiles the paper cares about in practice
(Gaussian, Laplace, and the cosine/Gaussian priors used by ClockRoPE itself are all
integrable) and mirrors the paper's own split between the density case (Propositions
3.1–3.2) and the discrete, purely-periodic case (Corollary 3.3). A formalization that
dropped this hypothesis and instead let the Fourier integral silently evaluate to
Lean's junk value (0 for non-integrable integrands) would make the goal statement
possible to "prove" vacuously and must be avoided.
Definitions needed: a positive-definite-kernel predicate, the real-valued Fourier transform of a kernel, feature-pair extraction, the rotation matrix, and the RFR estimator itself — all reusable by any future mission formalizing RoPE-family positional encodings (e.g. STRING, nD-RoPE) or other random-Fourier-feature results. McDiarmid's inequality, if not already in Mathlib in the needed form, is itself a independently reusable contribution.
An o-minimal structure is a setting in which every definable subset of the line is tame: a finite union of points and open intervals. This single axiom rules out oscillation, space-filling behavior, and other pathologies, and it makes one-variable definable functions tractable. The central consequence is the Monotonicity Theorem: every definable function on an interval is piecewise constant or strictly monotone and continuous, with only finitely many pieces.
The result originates in the work of Pillay and Steinhorn on o-minimality and is presented systematically in Lou van den Dries, Tame Topology and O-minimal Structures, Chapter 3 (Cambridge University Press, 1998). A concise expository account is given in Mário Edmundo, O-minimal structures (arXiv:math/0012051). This mission formalizes the one-dimensional monotonicity theorem and its supporting lemmas in Lean 4 against Mathlib, as a verified entry point to o-minimal geometry.
Let be a type equipped with a dense linear order without endpoints : an irreflexive, transitive, trichotomous relation in which every strict inequality admits an interpolant and every element has strict predecessors and successors. Finite Cartesian powers are represented as coordinate tuples , with coordinate projections, deletion, and append operations defined explicitly.
An o-minimal structure over is a family of collections of subsets of , closed under finite unions and intersections, containing diagonals and the order relation, closed under products, coordinate reindexing, and existential projection, and satisfying the o-minimality axiom: every member of is a finite union of points and open intervals. A definable function with domain and codomain is a dependent function on the corresponding subtypes whose domain, codomain, and graph are all members of .
For in , the open interval is the set of coordinate tuples whose single coordinate lies strictly between the two endpoint values, with endpoint variants allowing and . A function is strictly increasing (respectively strictly decreasing) on when implies (respectively ) in the first output coordinate. Continuity at a domain point is the graph-based epsilon-delta predicate: belongs to exactly when the graph meets every sufficiently small box around in the graph of a locally oscillation-free correspondence. Finiteness and infinitude of one-dimensional sets are expressed through first-coordinate listings.
An open cell is good when restricted to is constant, or strictly increasing and continuous there, or strictly decreasing and continuous there. The number of cut points is finite and depends on , , and ; no bound on is asserted.
The result itself. The Monotonicity Theorem is the foundation of one-dimensional o-minimal geometry. It implies that definable sets have finitely many connected components, that definable functions have finite limits at endpoints, and that higher-dimensional cell decomposition can proceed by induction on dimension. Without it, the correspondence between definability and geometric tameness remains unestablished.
Formalizing it. The classical proofs are known and appear in the references above; what is missing is a machine-checked version with explicit definability bookkeeping. This mission produces Lean 4 declarations for the order, interval, monotonicity, graph, and continuity predicates together with the theorem and its lemmas, all verified against the pinned Mathlib revision. The definability infrastructure (products, projections, fiber extraction) is reusable for subsequent cell-decomposition missions. Status honesty: the one-dimensional interval-extraction lemmas are machine-checked; the local constancy-or-injectivity lemma, the injective-to-monotone lemma, the finite-partition assembly, and the goal theorem itself remain open targets.
The naive argument fixes a point and inspects nearby values, but definability does not by itself provide any neighborhood on which behavior is uniform. The fiber dichotomy illustrates the obstruction: knowing that each fiber is definable does not decide whether some fiber contains an interval or every fiber is finite, and the two cases require different constructions (a constancy interval versus an injective-selection interval). Similarly, injectivity alone does not yield monotonicity without partitioning the domain by local sign patterns and applying o-minimality to select a uniform pattern on a subinterval. Each step fails until the relevant definable set is exhibited and the one-dimensional interval lemma is applied to it.
Lean represents one-dimensional points as functions , with order, intervals, and finiteness stated through the first coordinate. Definability is always the structure membership predicate , never an informal attribute. Continuity is the graph-based predicate applied to ; a submission that discharges a continuity goal from the domain inclusion alone, or that replaces the continuity predicate by the domain set, does not satisfy the statement. The goal quantifies over cut points with , , and strict increase at each step; the intervening sets are the open intervals determined by consecutive finite endpoints.
Contributions welcome: direct proofs of the open leaves (fiber definability, the finite-fiber injective-interval construction, the injective-to-monotone step, the finite-partition assembly), sharper statements with explicit endpoint bounds, and reusable o-minimal infrastructure beyond this mission. Out of scope: higher-dimensional cell decomposition, differentiability, and integration of definable functions.
The fundamental lemma is a family of identities between orbital integrals on a reductive group and stable orbital integrals on a smaller group attached to it, its endoscopic group. Langlands isolated these identities in the 1970s as the last missing ingredient in the comparison of trace formulas, and Langlands and Shelstad formulated them precisely in 1987; Waldspurger reformulated the statement for Lie algebras and proved that the Lie algebra form implies the group form. The Lie algebra statement was proved in equal characteristic by Bao Chau Ngo in Le lemme fondamental pour les algebres de Lie, Publ. Math. IHES 111 (2010), 1-169 (DOI), by a global geometric argument built on the Hitchin fibration; Waldspurger's earlier work transfers the result to mixed characteristic. The identity is the engine behind the stabilization of the trace formula and behind the computation of the cohomology of Shimura varieties.
Both sides of the identity carry a normalizing factor built from the discriminant, and the exact power of relating the two normalizations is fixed by a purely root-theoretic computation carried out in Ngo's §1.10-§1.11. That computation is the subject of this mission. It is self-contained, it uses no geometry, and it is the first piece of the paper that can be stated in Lean today.
Let be a split reductive group over a field with maximal torus , character lattice , cocharacter lattice , root system and Weyl group . Write for the Cartan subalgebra, so that each root has a differential , a linear form on . Ngô's discriminant is the product
a -invariant polynomial function on and hence a function on the space of characteristic polynomials.
An endoscopic datum is an element of the dual torus . The endoscopic group attached to it is the group whose root system is
with Weyl group and its own discriminant . Choose a subset containing exactly one root out of each pair of opposite roots outside , and set
Finally let be a non-archimedean local field with valuation and residue cardinality , and recall Ngô's normalizing factors and .
for a point of the endoscopic Cartan with image . Equivalently with : this is exactly what lets one pass between the two forms of the fundamental lemma, and .
The identity above is the image under of the divisor identity of 1.10.3, which in turn rests on the fact that — which depends on a choice of — is nevertheless -invariant, and on the fact that really is a root subsystem. The milestone list follows that order.
Theorem 1 of Ngô's paper, the Langlands-Shelstad conjecture for Lie algebras, is the identity for corresponding regular semisimple stable classes, under the hypothesis that twice the Coxeter number of is smaller than the residue characteristic. Nothing in that statement can be written in Lean today: reductive group schemes over a discrete valuation ring, endoscopic data, Kostant sections, orbital integrals and affine Springer fibers are all absent from Mathlib. What can be written, faithfully and without any placeholder, is the root-theoretic layer that fixes the transfer factor, and that is what this mission asks for. It is a genuine prerequisite: the two displayed forms of Theorem 1 differ precisely by the identity above.
The mission also produces reusable infrastructure — the discriminant of a root system, the notion of a closed subsystem and its Weyl group, the endoscopic subsystem cut out by an element of the dual torus — none of which currently exists in Mathlib, and all of which any future formalization of endoscopy will need.
Only one of the four milestones is a routine manipulation. Splitting into pairs and collecting squares is bookkeeping; that is -invariant is immediate because permutes . The content is in Lemma 1.10.2: is not stable under , so carries to , where counts the roots of sent into ; the claim is that is always even. The naive attempt — check it on the generating reflections of — is exactly where a careless argument goes wrong, since it is false for reflections in roots outside . Ngô's argument identifies the sign with , the ratio of the sign characters of and , and observes that both compute the determinant of acting on the same reflection representation.
Root systems are modelled with Mathlib's RootPairing ι R M N: the module plays the role
of , the module the role of and of the Cartan on which the differentials
are evaluated, and is the linear form . The endoscopic
subsystem is cut out by an element of the dual torus, taken as a group homomorphism
from the cocharacter lattice to an arbitrary commutative group, and is expressed over
coefficients as in the definition of a root datum. Products over and are
finite products over a Fintype index, and a choice is a Finset satisfying an
exclusive-or condition, which automatically rules out the degenerate case .
The identity 1.10.3 is stated as an identity of functions on the Cartan rather than as an identity of divisors, so the unit is carried explicitly rather than discarded. Lemma 1.10.2 is stated over for an honest root system, since the sign argument uses the reflection representation. The goal 1.11.3 is stated for an additive valuation with values in , which is what makes the two sides comparable when a discriminant vanishes.
There is no trivializing formalization here: the hypotheses of every item are satisfiable — any root system with any closed subsystem and any choice of gives an instance — so none of the statements is vacuous, and none of them is an identity between two occurrences of the same expression.
Contributions of the surrounding theory are welcome: a positive system compatible with a subsystem, the sign character of a Weyl group, and the reducedness of the discriminant divisor (the remaining half of Lemme 1.10.1) are all natural next steps.
A coset partition of a group is a finite family of left cosets that are pairwise disjoint and cover . In 1974 Herzog and Schönheim asked whether the indices of such a partition, with , can be pairwise distinct. They cannot when — there a coset partition is an exact covering system of the integers, and Davenport–Rado and Mirsky–Newman showed the largest modulus must repeat — but for general groups the question is still open, even for finite solvable groups.
Progress has come in two styles. Structural: Berger, Felzenbaum and Fraenkel settled finite nilpotent groups in Canad. Math. Bull. 29 (1986) 329–333 and finite pyramidal groups in Fund. Math. 128 (1987) 139–144. Order-bounded: Ginosar and Schnabel (2011) settled every whose order has at most two prime divisors, and Margolis and Schnabel (2019) verified all .
The paper formalized here, Z.-W. Sun, J. Algebra 273 (2004) 153–175, takes a third route: it constrains the subgroups rather than the group, and simultaneously weakens "partition" to "uniform cover". Its hypothesis — that the be subnormal — costs nothing in the nilpotent case (every subgroup of a nilpotent group is subnormal) yet applies to arbitrary, possibly infinite, ambient groups . It also answers negatively an open question of the same paper, generalizing one of Erdős: the indices of such a cover cannot all be large if each occurs only boundedly often.
Let be a group, written multiplicatively. For a finite system
of left cosets, the covering function counts memberships,
If is constant, say , then is a uniform cover of of weight ; the case is exactly a coset partition. A uniform cover is trivial when for every , and this is the only degenerate case that must be excluded. Uniform covers are genuinely more general than partitions: one may have no disjoint subcover at all.
A subgroup is subnormal if some finite chain reaches , each term normal in the next. Normal subgroups are subnormal; in a nilpotent group every subgroup is; and shows a subgroup of a solvable group need not be.
Write for the indices, always assumed finite, and
for their least common multiple, whose prime divisors are exactly those of . Let and denote the least and greatest prime divisors of , let be Euler's totient, and let
be the largest multiplicity with which an index is repeated. The Herzog–Schönheim conjecture says .
The goal theorem is Theorem 4.3(i) of the source: for a nontrivial uniform cover of any group by cosets of subnormal subgroups of finite index, some index divisible by the largest prime is repeated at least times,
In particular . Two weaker consequences are separate targets. Since , this gives the Herzog–Schönheim conjecture for subnormal uniform covers,
and the quantitative step behind it is a Burshtein-type inequality, which after clearing denominators reads
The result itself. It is the widest structural class in which Herzog–Schönheim is known, and the only one that does not require to be finite: subnormality of the is a condition on the subgroups, so itself is arbitrary. It strictly contains the nilpotent case of Berger–Felzenbaum–Fraenkel, and being quantitative it also yields the Burshtein conjecture in this setting — a bound no purely qualitative statement gives. Because the conclusion is a lower bound on growing with , it answers the paper's open question: one cannot make all the indices of a uniform cover large while keeping every multiplicity bounded.
Formalizing it. Nothing here is open, and the mission is the machine-checked version of a known
proof. What it adds is a formal vocabulary for uniform covers — Mathlib has
Mathlib/GroupTheory/CosetCover.lean (B. H. Neumann's theorems, ) but no
notion of covering multiplicity — and the arithmetic of subnormality, in particular that
divides when the are subnormal. Mathlib has
Subgroup.IsSubnormal with the basic closure properties but nothing about indices of subnormal
subgroups, and that divisibility is the whole reason subnormal covers behave. The totient measure
this proof runs on is already formalized: Sun's Lemma 3.1 is Berger–Felzenbaum–Fraenkel's equation
(14), already proved on the platform as BFFPyramidal.muMeasure_divisorClosure_image_mul, and
this mission reuses that definition file rather than duplicating it.
Status disclosure. Complete Lean proofs of the goal and of every milestone below already exist and will be submitted at launch, so this mission is not an open frontier: its value is the verified artifact, the reusable vocabulary, and the fact that the development turned up two places where the published argument needs repair or can be simplified (see Formalization scope). Alternative proofs, sharper variants, and the analytic parts excluded below remain genuinely open contributions.
The reciprocal identity is the first thing anyone writes down and it is not enough: a uniform cover of weight satisfies , and pairwise distinct can do that.
The real obstruction is that a cover does not descend to a quotient. A part need not lie in one coset of a chosen normal subgroup, so the induction that proves the finite nilpotent case has nothing to induct along once may be infinite and the are merely subnormal. Sun's replacement is a lower bound for the size of a union of cosets, Theorem 3.1: if for all and , then the number of cosets of inside is at least the number of divisible by some . The union is compared not with the but with a purely numerical shadow of itself in , and it is here that subnormality enters, through the divisibility (Lemma 2.1) — for arbitrary finite-index subgroups Poincaré gives only the inequality , which is too weak.
The second difficulty is arithmetic and is where the source spends its effort. Turning Theorem 3.1 into a bound on multiplicities (Theorem 3.2) requires computing the density of a union , and the identity the paper uses (Lemma 3.4) expresses that density as times an infinite sum of reciprocals over -smooth elements of the union. Along that route the full series is needed: truncating it loses precisely the geometric factors that produce the divisor sum in the conclusion.
It is worth saying, though, that this analytic detour is avoidable — a solver need not take it. Theorem 3.2 can also be reached by a purely finite argument: bound the density from below by injecting each index into the divisor , which is sharp in the same cases as the series argument. Lemma 3.4 remains a faithful and separately interesting milestone of the paper, but it is not on the critical path to the goal. The naive version of the finite estimate — bounding the density below by — is genuinely false, as shows, so the injection is the content, not a one-liner.
The development commits to the following conventions, worth stating because the prose leaves them implicit.
Covers are indexed families rather than sets of cosets: IsUniformCover K a w asserts that for
every the number of indices with is exactly w, counted as
Nat.card of a subtype so that no decidability hypothesis is needed. Indexing by Fin k keeps
multiplicities visible, which matters because every conclusion counts indices, not distinct
subgroups. Nontriviality is never folded into the definition; it appears as the explicit
hypothesis ∃ i, K i ≠ ⊤, and without it every statement here is false (take , ).
is an arbitrary group — not assumed finite. Finiteness enters only through
Subgroup.FiniteIndex on each , which the source assumes implicitly when it writes "the
(finite) indices". Indices are Subgroup.index and is H.relIndex (K i). For a
subgroup that is not assumed normal, G ⧸ H is still the type of left cosets and
Nat.card (G ⧸ H) = H.index; Theorem 3.1 is stated with that type, since the it is applied
to is not normal.
Densities are never limits. The density of a union is taken as the
finite ratio for an explicit common multiple ,
which is exactly equal to the asymptotic density and keeps Lemma 3.4 free of any analysis on the
left-hand side; the right-hand side genuinely is an infinite sum and is stated with HasSum over
.
Inequalities are cleared of denominators and stated in wherever possible, so that appears as . Readers should check the direction: subtraction truncates, so is only the intended quantity because every here is prime, hence .
⚠️ Parts (ii)–(iv) of the source's Theorem 4.3 are out of scope. Those bound the primes
dividing the indices, their number, and by and similar, and they rest on Mertens' third theorem,
, which Mathlib does not have. It is worth
being precise about what Mathlib does have, since the gap is narrower than it looks: the prime
counting function Nat.primeCounting, Chebyshev's and with the machinery around
them (Mathlib/NumberTheory/Chebyshev.lean), Euler products
(Mathlib/NumberTheory/EulerProduct/), and the constant itself
(Real.eulerMascheroniConstant) are all present — what is missing is Mertens' asymptotic tying
them together, and the asymptotics. Supplying that is a substantial number-theory
project in its own right, so this mission stops at the arithmetic core, part (i), which is what
implies Herzog–Schönheim. Contributions adding the analytic parts are welcome and would complete
Theorem 4.3.
Two things the development established that the paper does not state. First, Lemma 2.1 is true in a stronger form: needs only subnormal, not both, and needs no finiteness hypothesis at all (with Mathlib's convention that an infinite index is ). Second, Theorem 4.1's passage from the largest prime to the smallest can be isolated as a self-contained arithmetic inequality, , which is tight at prime powers; it is listed as its own milestone for that reason.
Reusable beyond this mission: the uniform-cover vocabulary, the subnormal index divisibility of Lemma 2.1, and Theorem 3.1's union bound, which applies to any attack on Herzog–Schönheim including the still-open solvable case. The source also leaves Conjecture 4.1 open — that for a nontrivial uniform cover by subnormal subgroups the largest index is repeated at least times, its least prime factor — which would be a natural follow-on target.
This mission curates the formalized output of Alethean — an Autonomous Logic Engine for Theorem Hunting, Exploration, And Navigation (alethean.org). Alethean autonomously generates research directions, develops them into research papers, and formalizes their results in Lean 4 — an "ever-expanding registry of absolute mathematical truths," built with the Aristotle reasoning engine. "The unconcealed truth between conjecture and proof."
The corpus's public home is the Alethean Lean 4 Catalog — the central registry of formalized theorems across the ecosystem, browsable as research packages (each with its article, research paper, interactive view, future directions, and Lean 4 proof files). This mission is the platform-side mirror of that registry: 2,799 definition bundles and 7,517 theorems compiled and verified against the pinned toolchain (Lean v4.30.0, Mathlib c5ea003), spanning analytic number theory, combinatorics, probability, information theory, quantum information, tropical algebra, and machine-learning theory.
The corpus arrives fully proved. The goal theorem is the corpus's universal error-detection bound for random checksums — the capstone of the Almost-Lossless compression thread (Compression Beyond the Pigeonhole Bound): appending an independent random checksum makes the probability of silent corruption at most , uniformly over all source strings and all inner decoders. The milestones are capstone theorems from across the corpus: sphere-packing and VC-dimension bounds, second moments of central -values, tropical Arrow-type impossibility, sums-of-three-cubes obstructions, and more.
Every milestone is a verified platform theorem: study the proofs, reuse them as imported lemmas, or rebuild them from first principles. The interesting open work is extension: the corpus's research-direction papers (browsable at alethean.org under Future Directions) state quantitative sharpenings — explicit constants, wider parameter ranges — that are not yet formalized. Pick a direction, formalize its statement, and the verification pipeline does the rest.
53c2925a02)c5ea00351c28e24afc9f0f84379aa41082b1188faether-catalog.A coset partition of a group is a finite family of left cosets of subgroups that are pairwise disjoint and cover . Asking which multisets of indices can occur is a question with two independent origins. For the cosets are arithmetic progressions and a coset partition is an exact covering system of the integers; Erdős asked whether the moduli of such a system can be pairwise distinct, and Davenport and Rado, and independently Mirsky and Newman, showed they cannot — the largest modulus must repeat. For general groups, Herzog and Schönheim (1974) asked the same question: in any coset partition with , must two of the indices coincide? That question is still open.
Progress has come by restricting the group. Berger, Felzenbaum and Fraenkel proved the conjecture for finite nilpotent groups in Canad. Math. Bull. 29 (1986) 329–333, and the paper formalized here extends it to a wider class defined by a chain condition. Later work bounds the order instead of the structure: Ginosar and Schnabel (2011) settle every whose order has at most two prime divisors, and three prime divisors when , while Margolis and Schnabel (2019) verify all . The conjecture remains open even for finite solvable groups.
Let denote the least prime factor of and the greatest, and let be Euler's totient function.
A finite group is pyramidal if it admits a chain of subgroups
in which every step has index equal to the least prime factor of the order of the preceding term:
A subgroup whose index is the smallest prime dividing the order is automatically normal, so the chain is a composition series; consequently every pyramidal group is solvable, and every supersolvable group is pyramidal. Pyramidality is therefore a chain condition sitting between supersolvability and solvability.
Given a coset partition of , write
The goal theorem is the multiplicity lower bound of Berger–Felzenbaum–Fraenkel. If is pyramidal and the cosets , , partition with , then at least
of the subgroups have the same order.
Two consequences are separate targets. Since whenever , the bound yields the Herzog–Schönheim conjecture for pyramidal groups:
and it likewise settles Burshtein's conjecture in this setting, which concerns the case and bounds the primes dividing in terms of the largest multiplicity.
The bound is quantitative where the Herzog–Schönheim conjecture is qualitative: it does not merely assert that a repetition exists but forces a repetition of prescribed multiplicity, growing with the largest prime factor of . That is what makes it strong enough to also imply Burshtein's conjecture, which no purely qualitative statement does.
The class it covers is also of independent interest. Nilpotent groups are pyramidal, so the result subsumes the authors' earlier theorem, and it reaches groups that are solvable but far from nilpotent. It remains, more than three decades later, among the structural (as opposed to order-bounded) cases in which the conjecture is known.
No part of this development is currently formalized: Mathlib has the ingredients — Sylow theory, Hall subgroups of solvable groups, Euler's totient with Gauss's identity — but neither coset partitions as a structure, nor pyramidality, nor any case of Herzog–Schönheim. The mission produces the first machine-checked proof of a structural case of the conjecture, together with a reusable formal vocabulary for coset partitions.
The reciprocal identity is immediate and useless on its own: distinct indices can satisfy it, so no counting argument over the indices alone can succeed.
The natural attack — induct along the chain, quotienting by — fails because a coset partition does not descend to a quotient. A part need not lie inside a single coset of : if then it meets every coset of , and the induced family on is a cover with multiplicity rather than a partition. Controlling that dichotomy is the first obstacle, and it is precisely where the definition of pyramidality is used, the index being the least prime factor of rather than an arbitrary one.
The second obstacle is that the conclusion counts subgroups of equal order, so the induction must carry a lower bound on the size of a union of cosets that is sensitive to the orders and not merely to their number. The paper's device is a measure on the naturals with , evaluated on the divisor closure of the set of orders; Gauss's identity makes interact correctly with divisibility, and the required inequality is genuinely a statement about the group, not about the multiset of orders. The final step splits off the Sylow -subgroup against a Hall complement, which exists only because pyramidal groups are solvable.
The development commits to the following conventions, all fixed in Lean and worth stating because the prose leaves them implicit.
Coset partitions are indexed families rather than sets of cosets: IsCosetPartition K a asserts
that for every there is a unique index with . Indexing by Fin t
keeps multiplicities visible, which matters since the conclusion counts indices, not distinct
subgroups; and uniqueness encodes disjointness and covering simultaneously. Groups are finite via
[Finite G], and orders and indices are Nat.card and Subgroup.index.
Pyramidality is stated as the existence of a length and a chain c : ℕ → Subgroup G with
c 0 = ⊤, c n = ⊥, and Subgroup.relIndex (c (k+1)) (c k) = Nat.minFac (Nat.card (c k)) for
k < n. Normality of each step is a consequence, not a hypothesis, and is deliberately not assumed.
The greatest prime factor is maxPrimeFac m = m.primeFactors.sup id, which is for
; the floor in is natural-number division, so the goal statement is
(maxPrimeFac l * Nat.totient l) / l + 1 ≤ …. Note that the bound is vacuous at — there
and — so is a necessary hypothesis and is present in every
statement that needs it; a formalization omitting it would be trivially true and is ruled out.
A complete development needs, beyond the goal: the coset intersection lemma; the least-prime-index dichotomy; uniqueness of the Sylow -subgroup of a pyramidal group; the scaling law for the divisor-closure measure; the union lower bound; and solvability of pyramidal groups. The coset-partition vocabulary and the union bound are reusable for any other case of Herzog–Schönheim, including the still-open solvable case, and contributions of alternative proofs or sharper variants are welcome.
Quantum algorithms for stochastic optimization are usually presented one paper at a time: a schedule is fixed, a quantum mean estimator is substituted for a classical minibatch, and a new rate is derived from scratch. The derivations are near-identical, and the step that actually differs — the price of one gradient query — is buried inside each proof rather than exposed as a parameter.
This mission publishes a Lean 4 development in which the oracle is a parameter, not an assumption. One rate theorem, instantiated at different oracle contracts and cost models, yields the classical rate, the inexact-gradient rate, and the quantum rate. All constants are explicit; nothing is asymptotic.
The published results it reproduces or corrects:
Let be a real inner-product space, an objective, and a map supplied as a parameter in place of the gradient. The smoothness hypothesis is the descent-lemma inequality
written ; this is exactly what rate proofs consume, and it is implied by a Lipschitz gradient. Write for the initial gap, for the target accuracy, for the gradient-noise scale, for the mean-squared smoothness constant, and for the ambient dimension.
A cost model converts a target accuracy into a query count as a power law with exponent . Its member is the classical minibatch bill, scaling as ; its member is the quantum mean-estimation bill, scaling as . That single exponent is where classical and quantum part company.
The goal theorem is the exact crossover between the two SPIDER bills. Writing and for the dominant terms of the quantum and classical query totals,
the target asserts, for and ,
Every supporting rate is also published and proved: the two SPIDER query totals, SPIDER's correctness, the SGD and PL rates, the exact and inexact gradient-descent rates, the two variance-purchase bills, and the two query counts.
The results. The crossover makes the dimension-versus-accuracy trade-off of quantum stochastic optimization quantitative rather than folkloric. Two readings follow directly: at fixed the quantum advantage disappears as , so the speedup lives at moderate accuracy, not asymptotically; and at fixed the advantage requires . Note what cancels — , and the -exponent all drop out, leaving only against .
The formalization. Because the oracle and the cost exponent are parameters, the classical and quantum rates are one theorem evaluated twice rather than two proofs. This mission is unusual in that its frontier is already closed: every node arrives with a machine-checked proof, transplanted from a green build. What it offers the platform is a reusable, fully-proved layer for first-order convergence analysis — function classes, cost models, a one-step descent recursion, accumulation laws including a stopped-time version, and the SPIDER schedule — on which further rates can be built by instantiation.
The apparent difficulty is not where a newcomer expects. Deriving a rate from the one-step recursion is routine telescoping. What is delicate is keeping the constants honest while the oracle varies: a rate proof that quietly assumes an exact gradient, or a global lower bound on , will produce the right-looking exponent from the wrong hypotheses.
Two specific places carry real content. Evaluating an error recursion at a random return time breaks the unconditional variance bound, because conditioning on destroys independence; the stopped-time accumulation law is what repairs it. And reproducing a published constant exactly — rather than up to — is what certifies that the parametrized machinery has not silently degraded the bound it generalizes.
Smoothness is QuadUpper on an explicitly supplied g; no differentiability or convexity is assumed anywhere, and the only lower-bound hypothesis is at the terminal iterate rather than globally. Cost models are an inductive family with a power-law member, so the classical and quantum instances are and of one definition. Half-integer powers are written with Real.sqrt, so no real exponentiation appears in any statement. Stochastic results use a genuine Filtration and a conditional oracle contract; the tower property is derived, not assumed.
Two honesty notes. Several statements carry hypotheses that Lean marks unused; these are recorded as such in the individual nodes rather than presented as load-bearing. And the library records a discrepancy in Sidford--Zhang's Algorithm 7 parameter block, documented in its own STATUS notes; the formalization follows the corrected parameters.
lean-optrates, github.com/shiy1022/lean-optrates at commit 4c0b8498, Apache-2.0, by Yueheng Shi. The platform copy renames the root namespace OptRates to ShiOptRates; no statement or proof is otherwise altered.Discrepancy theory asks how unbalanced a two-coloring of a combinatorial structure must be in the worst case. Concretely: given sets over an -element ground set, color each element or so that every set is as close to balanced as possible. The question is classical (Beck–Fiala 1981; Spencer 1985) and the answer for general (dense) set systems is one of the sharpest gaps between a naive probabilistic bound and the truth known in combinatorics: assigning colors uniformly at random only guarantees discrepancy , yet a coloring with discrepancy always exists — the logarithmic factor is an artifact of the naive argument, not of the problem. This mission formalizes that removal, following T. Rothvoß's lecture-note exposition of J. Spencer's entropy method (MIT 18.095, "Discrepancy theory"), the standard modern presentation of the technique (see also Matoušek, Geometric Discrepancy, Ch. 4). The entropy method is the ancestor of the whole "partial coloring" family of arguments used throughout discrepancy theory and combinatorial algorithm design, so a machine-checked account of its base case is reusable well beyond this one theorem.
Fix and an matrix with entries in , thought of as the incidence matrix of sets over an -element ground set: iff element lies in set . A coloring is a map , and the discrepancy of row under is , the signed imbalance of set . The discrepancy of the matrix is the value achieved by the best coloring, minimizing the worst row.
The entropy method bounds this via the partial coloring lemma: rather than coloring all elements at once, one repeatedly colors a constant fraction of the currently uncolored elements while keeping every row's contribution small, then recurses on what remains. Each round is itself produced by an entropy/pigeonhole argument: quantize each row's signed sum (under a uniformly random coloring) into "shells" of width (where is the number of active elements); a short computation shows this quantization carries very little Shannon entropy once the shell width exceeds a threshold; subadditivity of entropy across the rows then bounds the joint quantization entropy, which by pigeonhole forces an exponentially large set of colorings landing in the same joint shell; Kleitman's theorem on the diameter of a large subset of the Hamming cube then extracts two such colorings that are far apart in Hamming distance, and their difference is the sought partial coloring.
Goal.
This is the qualitative, constant-suppressed form of Spencer's theorem: it asserts discrepancy with a single universal constant, and deliberately leaves that constant unspecified. This is the right goal for this mission because it is the weakest statement that is still stable: any future improvement to the constant (down to Spencer's sharp , or beyond) refines this theorem rather than invalidating it.
The removal of the factor is the entire content of Spencer's theorem: it is what separates discrepancy theory from a corollary of concentration inequalities, and the partial-coloring/entropy method it introduced underlies later results throughout the field (Beck–Fiala-type bounds, the Komlós conjecture literature, and constructive/algorithmic discrepancy minimization). Formalizing it is formalizing the base case that every later partial-coloring argument specializes.
This mission's goal theorem, spencer_discrepancy_sqrt_n_bound, is already proved (zero sorrys), by a from-scratch entropy-method development: the per-row shell-entropy bound, the joint pigeonhole-and-Kleitman assembly for one round, and the outer geometric iteration and induction combining rounds into a full coloring. What remains open in this mission is shannonEntropy_shellFin_le (Lemma 9 in Rothvoß's notes) — the per-row entropy bound is currently imported as an assumption by the one-round lemma lemma8_partial_coloring_round, which is therefore only conditionally proved pending it. A separate, harder mission on this platform (Komlos.spencer_six_deviations) targets Spencer's sharp constant via a tighter, non-standard numeric derivation; that is a distinct, substantially harder target and this mission does not duplicate it.
The obvious argument is: fix a target bound , use a Chernoff/Hoeffding bound to show each row fails with probability at most , union-bound over the rows, and take a coloring outside the bad event. This works to prove a single good coloring exists — but it is not strong enough to survive being iterated to remove the entire uncolored set, because a per-row union bound loses a factor of that a fixed cannot always absorb once the active column count is close to : for the scaling family where the row count and the active set shrink together, the naive union bound's failure probability grows linearly in , not exponentially, exactly canceling the exponential decay one is trying to exploit. The fix is to bound the joint entropy of all rows' quantizations at once (subadditivity of Shannon entropy), rather than union-bounding row-by-row failure events; this is genuinely a different technique, not a tightening of the same one, and it is the reason the entropy method is presented as its own tool rather than a Chernoff-bound corollary.
Matrices are Fin n → Fin n → ℝ with an explicit ∀ i j, A i j = 0 ∨ A i j = 1 hypothesis; colorings are represented two ways in this development — Fin m → Bool internally (via the platform definition RSign converting to ) during the entropy/Kleitman argument, and directly as Fin n → ℝ constrained to pointwise in the goal theorem's statement, matching the usual -coloring convention. The row-sum shell quantization is the platform definitions rowSumB, shellIdx, shellFin (an integer-valued "round to nearest shell" construction, packaged into a fixed Fin (2m+3) type for entropy purposes). The active column set during the outer iteration is tracked as a shrinking Finset (Fin n) of the original index type throughout, rather than moving between different Fin m types round to round, which keeps the induction free of type-level bookkeeping.
Reusable, already-Proved infrastructure this development builds on: shannonEntropy_pi_le (subadditivity across independent rows), shannonEntropy_pigeonhole, choose_sum_le_exp_mul_binEntropy, and kleitman_diameter, all already Proved on the platform independent of this mission. The one genuinely open piece — and the mission's standing invitation — is shannonEntropy_shellFin_le (Lemma 9): a self-contained Shannon-entropy computation about the shellFin quantization that does not depend on anything else in this mission and can be attempted independently.
Quantum low-density parity-check codes encode quantum information using sparse parity constraints. A standard way to construct them is to translate binary chain complexes into Calderbank--Shor--Steane codes and to combine complexes by tensor product. Homology identifies the logical operators of the resulting code, while the smallest Hamming weight of a nontrivial homology class controls one of its distances. Determining how this distance behaves under a tensor product is therefore a basic structural question, not merely a parameter calculation.
Weilei Zeng and Leonid P. Pryadko studied products in which one factor is an arbitrary finite binary chain complex and the other is the one-complex induced by a binary matrix. Their paper was published as “Higher-Dimensional Quantum Hypergraph-Product Codes with Finite Rates,” Physical Review Letters 122, 230501 (2019). Its main distance result is Eq. (13) in the arXiv version: for this particular tensor factor, the usual product upper bound is always exact. The result extends the familiar two-complex setting of quantum hypergraph-product codes to the local structure occurring in complexes of any dimension.
A based binary chain complex consists of finite-dimensional vector spaces over , each equipped with a specified coordinate basis, and linear boundary maps
such that . Its degree- homology is . The homological distance is measured in the chosen basis:
Following the paper, the minimum of an empty set is . Thus when is trivial.
The endpoint convention is also the one stated explicitly after Eq. (1). For an -complex, is the zero matrix and is the zero matrix. Consequently
and
For an binary matrix , the one-complex has in degree one, in degree zero, and boundary . Its two distances are
and
In particular, unless has full row rank, in which case . The degree- chain group of is
with the standard tensor-product boundary. Over the usual sign in that boundary has no effect.
The first milestone is Eq. (11) for two arbitrary finite-length based binary chain complexes:
Let and . The second milestone is Theorem 1, including both of its cases:
and
The goal is Eq. (13):
No full-rank hypothesis is imposed on .
The equality determines the product distance exactly from four component distances. General tensor-product arguments immediately provide the upper bound, but an exact formula requires ruling out lower-weight homology classes that mix the two direct-sum blocks. Once established, the formula can be applied repeatedly to tensor products of one-complexes, which is the step used in the paper to obtain higher-dimensional quantum hypergraph-product code families and to compute their distances.
For formalization, the mission contributes reusable definitions of finite based binary chain data, homological distance valued in , the one-complex of a binary matrix, and the relevant tensor-product boundary maps. Mathlib contains Hamming weight and general homological-algebra infrastructure, while QECLean contains a closely related based length-three homological-code interface. Neither the selected Mathlib environment nor the inspected QECLean development currently supplies this rank-sensitive exact distance theorem.
The central issue is that Hamming weight depends on the chosen bases and is not preserved by arbitrary homological isomorphisms. A Künneth isomorphism describes the product homology and readily produces low-weight representatives, which is enough for the upper bound, but it does not by itself exclude a still lighter representative obtained by cancellation between the two tensor blocks. The lower bound must also remain valid at the endpoints of the complex and in singular cases where one or more homology groups vanish and the relevant distance is .
The theorem cannot be reduced to a dimension calculation. It must reason about supports and Hamming weights of based representatives while respecting the quotient by boundaries, and it must cover both and .
The Lean development works over ZMod 2. A finite basis in degree is
represented by Fin (dimension i), and a chain group is the function space
from that coordinate type to ZMod 2. BasedBinaryChainComplex stores the
dimension and boundary in every nonnegative degree, the chain condition, and a
finite length above which all dimensions are zero. Thus the first milestone
quantifies over genuinely arbitrary finite lengths for both and
, rather than over a local window or a one-complex specialization.
If the stored length is , the zero-dimensional source in degree
makes the unique zero map, just as the
zero-dimensional target below degree zero makes
the unique zero map. Hence both singular endpoint
cases in Eqs. (1) and (4) are represented directly.
Distances use WithTop ℕ. Their definitions are actual minima of Hamming
weights of nontrivial representatives, with ⊤ produced by the empty-set
case; infinite distance is not an extra hypothesis or a separately hard-coded
branch. Coordinate types may be empty, which covers missing endpoint blocks.
The binary matrix is represented as a linear map between two finite based
function spaces. Its row and column coordinate types need not be nonempty,
and no injectivity or surjectivity assumption is added.
The degree- product group is indexed by the disjoint union of all coordinate products for . Consequently its Hamming norm is the sum of the weights of all tensor-degree blocks. The product boundary is the standard signed tensor boundary; its sign disappears over . A formal proof verifies that every pair of consecutive product boundaries composes to zero; the cancellation of the two mixed terms uses characteristic two. Thus the product distance is taken from an actual chain complex, rather than from unrelated adjacent linear maps. A basis-free tensor product or an abstract homology group alone is insufficient for the target, because either would discard the weight data on which the statement depends. The mission does not formalize the asymptotic code-family construction later in the paper, the transposed cohomological distance, or the CSS-code parameter translation. Those are natural downstream missions; they should reuse rather than alter the present based-chain definitions.
Computability theory studies which questions admit algorithms and how the unsolvable questions compare with one another. A decision problem can be represented by a set of natural numbers: the question on input is whether belongs to the set. Even when there is no algorithm that always answers this question, there may be an algorithm that eventually recognizes every positive instance. Understanding the relative difficulty of such problems is the setting of the Friedberg–Muchnik theorem.
The original paper by Richard M. Friedberg appeared in 1957 under the title Two recursively enumerable sets of incomparable degrees of unsolvability (solution of Post's problem, 1944). It supplies the historical paper source for this formalization. A. A. Muchnik's independent contribution appeared in Russian in 1956. Friedberg, PNAS 43(2), 236–238; Muchnik, Math-Net bibliography, 1956 entry.
A set is computably enumerable, abbreviated c.e., if membership has a semidecision procedure: on input , the procedure halts exactly when . The older terminology is recursively enumerable, abbreviated r.e. The Lean predicate CEnumerable A uses Mathlib's REPred for this property. A computable set has a decision procedure that terminates on every input and answers membership correctly; this is expressed separately by ComputableSet A using ComputablePred.
For each set , define its characteristic function by
An oracle for answers requests for this function's values. It always supplies an answer, even if membership in cannot be computed without an oracle. The declaration setOracle A represents this total function inside Mathlib's type of partial functions from natural numbers to natural numbers.
Write when an algorithm with access to the membership oracle for computes on every input. This is Turing reducibility, expressed by SetTuringReducible A B. The algorithm may make several queries, with later queries depending on earlier answers. Incomparability requires both and ; it is stronger than saying the two sets merely have different degrees. These conventions specify the mathematical reading of the supplied Lean definitions.
The goal is the following unconditional existence statement:
Its Lean name is Computability.friedberg_muchnik. No enumeration, pair of sets, or oracle program is supplied as a hypothesis. Both sets must be obtained as witnesses to the conclusion. The statement matches Theorem 26.2 in Arnold W. Miller's Lecture notes in Recursion Theory, Section 26, with the theorem on page 51 and its proof on pages 51–54. Miller, December 3, 2008 version.
The target establishes that the c.e. problems have incomparable levels of computational difficulty. Its witnesses cannot be computable: a computable membership procedure would also work in the presence of any other oracle simply by making no queries, contradicting the required nonreducibility. The stronger historical consequence is a positive solution of Post's problem: a c.e. degree can lie strictly between the computable degree and the halting degree. Miller records this consequence separately as Corollary 26.3 on page 54. Miller, Section 26.
The mathematical theorem is established; the work requested here is its Lean 4 formalization. A completed development must construct witnesses, prove their computable enumerability, and exclude oracle computations in each direction using Mathlib's actual reducibility relation. The provided goal currently ends in sorry. Successful compilation of this statement checks its formulation and imports; it does not constitute a proof of the existence result.
The main obstacle is preserving decisions about oracle computations while both sets are still being enumerated. An additional element in one set can change an oracle answer used by an earlier computation, undermining the attempt to separate the other set from it. There are infinitely many candidate programs in both directions. Thus a formal treatment has to justify the eventual stability of the relevant computations as well as the effectiveness of the enumeration. This is the setting of the finite injury argument developed in Miller's proof of Theorem 26.2. Miller, pages 51–54.
The sets are arbitrary Set ℕ, including the natural number zero in their ambient domain. The oracle answers use natural numbers, with one for membership and zero for nonmembership. Classical reasoning is used to define the oracle for an arbitrary set; it supplies no assertion that this function is computable. Each oracle is nevertheless total. Replacing it with a partial membership recognizer would change the meaning of the target.
The foundation consists of Mathlib.Computability.RE and Mathlib.Computability.TuringDegree, together with the supplied definitions in namespace Computability. SetTuringEquivalent records reducibility in both directions. degreeOfSet maps a characteristic-function oracle to its Turing degree, and CEnumerableDegree says that a degree has a c.e. representative. These additional definitions are retained as useful interfaces, while the root theorem itself is expressed directly with sets and TuringIncomparable.
A complete proof will need representations of effective finite stages and oracle computations, and lemmas relating those representations to the imported predicates. Such infrastructure can support later formalizations involving oracle use, computable enumerations, and priority constructions. Contributions should establish these connections with Mathlib's definitions and finish the unconditional target. The theorem must not be replaced by mere degree inequality, weakened reducibility, or a conditional assertion that assumes the required incomparable sets already exist.
The Kerr metric (Kerr, 1963) is the exact solution of the vacuum Einstein equations that describes the exterior gravitational field of a rotating mass. It is the working model for astrophysical black holes: gravitational-wave templates, black-hole imaging and the classification results of the uniqueness theorems all take it as their starting point. Its form in the coordinates of Boyer and Lindquist (1967) is the one found in every textbook, and the statement that this line element has vanishing Ricci tensor is the single most-cited computation of the subject. That computation is long, it is almost never printed, and in practice it is trusted because computer-algebra systems agree on it. The parent project of this mission builds a certified-discovery pipeline for exact solutions of Einstein's equations in which a symbolic verifier is the oracle; this mission asks for the Kerr instance of that oracle's verdict to be re-established inside a proof assistant, so that the pipeline's benchmark result rests on a kernel-checked proof rather than on a simplification routine.
Timeline: Kerr (1963) found the metric in Kerr-Schild and in his original coordinates; Boyer and Lindquist (1967) introduced the coordinates in which the metric below is written and described its maximal analytic extension; Carter (1968) established the separability structure that underlies the closed-form inverse. None of these results has, to the authors' knowledge, a machine-checked proof.
Fix real parameters and . A point of is written ; in Lean it is a function Pt := Fin 4 → ℝ. Write , and
The Boyer-Lindquist Kerr metric is the symmetric matrix of functions
with all other entries zero (signature , ). Its closed-form inverse has , and a block with denominator . The regular coordinate domain is
For any matrix of functions with candidate inverse , the coordinate partial derivative is the one-variable derivative at of the slice , and the coordinate Christoffel symbols and coordinate Ricci tensor are
These four definitions (pd, christoffel, ricci, ricciOf) form the definition bundle KerrBL_CoordGeometry; the metric, its inverse and the regular domain form KerrBL_Kerr_Metric.
KerrBL.vacuum_Kerr)For all real and every with :
The goal deliberately bundles the inverse identity and the two differentiability clauses with Ricci-flatness. Without the first, ricciOf g ĝ with a wrong could vanish trivially; without the other two, the derivative in the definition of could be Mathlib's default value at a non-differentiable slice. With them, the last clause is a statement about the genuine coordinate Ricci tensor.
The milestones follow the three layers of the proof: (I) the inverse identity; (II) the bridge from the generic definitions to explicit closed forms, through derivative certification of the metric, the Christoffel bridge, derivative certification of the generic Christoffel symbols, and the Ricci bridge ; (III) the vanishing of the explicit expression for each of the eight components that are not structurally zero, as rational identities in the seven variables under , , , and finally the vanishing of all sixteen generic components.
The result itself is classical: the Boyer-Lindquist Kerr family is a vacuum solution wherever the coordinates are regular. What the mission adds is a proof in which the trusted base is explicit and small: a 45-line generic layer defining , and , and the transcription of five metric components from a hash-locked source file, with source-lock lemmas proving that the compact definitions equal the transcriptions. Everything else, including roughly 120 kB of generated closed forms, is bridged by proof; a wrong closed form can make a bridge theorem unprovable but never a false theorem provable. The generic layer and the bridge pattern are reusable for any coordinate metric in four dimensions, and the pattern of certifying a computer-algebra derivation through polynomial witnesses checked by linear_combination is reusable for any rational-function identity.
Status: the theorem is proved in the classical sense since 1963 and verified by every computer-algebra system; the machine-checked coordinate proof is what this mission records. At launch every node of the mission carries an accepted proof.
The obvious argument is to compute. The difficulty is size and control, not ideas. The Ricci components of Kerr are rational functions whose numerators have up to a few hundred monomials in seven variables; a normalisation tactic applied to the raw expression does not terminate in practice, and a naive -based unfolding of the double sums over produces terms whose elaboration alone exceeds the server budget. The proof therefore has to be organised: opaque atoms for and so that denominators are monomials, per-term clearing lemmas over a common denominator, and a single polynomial identity per component certified by explicit quotient witnesses of the relations , , . Mathlib's derivative also needs care: deriv returns where a function is not differentiable, so every derivative used in the Ricci formula must be accompanied by a HasDerivAt witness, and the differentiability of the generic Christoffel symbols has to be transferred from their closed forms by a locality argument on the open regular domain.
The Lean representation commits to the following. Points are Fin 4 → ℝ with , , , ; there is no manifold, no chart, no periodicity of and no range restriction on . Derivatives are Mathlib's deriv of coordinate slices. The candidate inverse is data; its correctness is a theorem. The parameters are arbitrary reals: the mission proves Ricci-flatness of the Boyer-Lindquist Kerr family on the regular coordinate domain used by the formalization, not a global Lorentzian-manifold theorem and not a statement restricted to the black-hole regime , . The axis is excluded (the inverse carries ) although the metric is smooth there; the loci and are excluded. Nothing is asserted about signature, uniqueness, symmetry of (all sixteen components are proved separately) or any coordinate-independent curvature quantity. A trivialising formalization is ruled out by the goal's first clause: the Ricci tensor of the specification layer takes the inverse as an argument, and the goal certifies that argument.
Independent blind read-back of the definitions and main statements, performed by a separate agent that saw only the Lean text, returned the following honest statement, recorded here verbatim: "For every pair of real numbers , and every point at which , and , all sixteen numbers obtained by evaluating the explicit coordinate formula [...] vanish, where is the explicitly transcribed Boyer-Lindquist Kerr component matrix, is an explicitly transcribed matrix that (by ginv_mul_g_Kerr, under the same hypothesis) satisfies at that point, and is Mathlib's one-variable deriv of the coordinate slice." The two should-fix findings of that read-back (inverse coupling; junk derivative values) are addressed by the first three clauses of the goal.
Infrastructure: three definition bundles (KerrBL_CoordGeometry, hand-written; KerrBL_Kerr_Metric, generated from the source file and human-auditable; KerrBL_Kerr_ClosedForms, generated and untrusted). Reusable beyond the mission: the generic layer, the locality lemma, and the bridge pattern. Natural extensions welcome after release: the two-sided inverse, the reduction to Schwarzschild, and curvature invariants such as the Kretschmann scalar.
Classical Eilenberg correspondence theorems connect algebraic descriptions of finite-state behavior with language-theoretic closure principles. The version developed by Juan Climent Vidal and Enric Cosme Llópez replaces one-sorted monoids by many-sorted algebras, so that operations may accept arguments of several prescribed sorts and return a value of another sort. This is the natural algebraic setting for typed term languages: a signature records the permitted input and output sorts of each operation, and a language is a family of sets indexed by sorts. The paper proves that two ways of organizing finite-state behavior—through finite-index congruences and through regular languages—determine the same ordered structure. The source is the final section of Climent Vidal and Cosme Llópez, Eilenberg theorems for many-sorted formations, published in the Houston Journal of Mathematics 45(2), 2019.
The companion manuscript A Kleene theorem for free many-sorted algebras develops the free-term and recognizability infrastructure used by this formalization. It supplies a concrete Lean representation of sorted signatures, free algebras, homomorphisms, terms, and finite many-sorted carriers. The present mission begins from that reusable core and formalizes the formation-level theorem of the HJM paper, rather than repeating the already completed Kleene development.
Fix a finite type of sorts and an -sorted signature . For an -sorted set , write for the free -algebra on . A congruence on a many-sorted algebra is a family of equivalence relations , one on each carrier sort, compatible with every basic operation. Its index is finite when the entire sorted quotient family
is finite. A sorted language is -saturated when membership in is constant on every -class. The syntactic congruence is the greatest algebra congruence that saturates , and is regular when has finite index.
A finite-index congruence formation selects, for every variable family , a nonempty filter of finite-index congruences on . The selection is closed under intersections, upward inclusion, and pullback along homomorphisms whose composite with the relevant quotient projection is surjective at every sort.
A regular-language formation selects regular languages in each . It contains every language saturated by the universal congruence; whenever it contains every language saturated by ; and it satisfies the corresponding pullback-saturation condition for quotient-surjective homomorphisms.
The two constructions are
and
The capstone is the paper's final formation theorem: the ordered sets of finite-index congruence formations and regular-language formations are order-isomorphic, with the isomorphism fixed to be exactly the two displayed constructions.
The milestones establish the universal property of the syntactic congruence, closure of finite-index congruences under the filter operations, the well-definedness of each construction, and the two recovery identities
These identities determine the inverse maps and prevent the goal from being satisfied by an unrelated abstract order equivalence.
The theorem packages a family of finite quotients and a family of regular languages as interchangeable data. On the algebraic side, closure is expressed by filters of congruences and quotient-surjective pullbacks. On the language side, the same information is expressed through saturation by syntactic congruences. The result therefore gives a systematic translation between quotient-based and language-based classifications in a typed, many-sorted setting.
Formalizing the theorem adds congruence, quotient-index, saturation, syntactic-congruence, and formation interfaces to the existing free many-sorted algebra library. These components are reusable for future formalizations of recognizability, Myhill–Nerode principles, finite algebra formations, and varieties or pseudovarieties of typed algebras. The mathematical theorem is already proved in the cited 2019 paper; the remaining task is to produce machine-checked Lean proofs of the source-faithful statements.
The two maps are simple to write down but their inverse laws are not pointwise tautologies. A finite-index congruence must be reconstructed from the family of all languages it saturates, and a language formation must be reconstructed from all selected finite-index congruences. In the many-sorted case, finiteness applies to the entire quotient family, including its support across sorts, and intersections and pullbacks must preserve this global condition. The quotient-surjectivity premise is also essential: replacing it by ordinary surjectivity of the original homomorphism would change the formation axiom.
The syntactic congruence creates a second layer of care. It must be characterized as the greatest compatible sorted equivalence saturating a language, not merely as the kernel of the language's characteristic function, which need not itself respect the algebra operations. Thus an argument that treats saturation as an arbitrary set-theoretic equivalence misses the algebraic compatibility required by the theorem.
The Lean development uses the existing MSKleene representation of sorted sets, signatures, argument tuples, algebras, homomorphisms, terms, and free algebras. Congruences are sort-indexed setoids with explicit compatibility for every signature operation. Their order is inclusion of relations. Intersection and the universal congruence are concrete constructions, while pullback is defined along an algebra homomorphism.
Finite index is represented by finiteness of the sigma-type of all quotient carriers, matching the paper's finite sorted-set convention; it is not weakened to separate finiteness of each inhabited component. The sort type is assumed finite in the finite-index filter and formation correspondence theorems, as required in the final section of the source. Languages are arbitrary sorted subsets of free term algebras, including empty components. No nonemptiness assumption on variable carriers or algebra sorts is added.
The syntactic congruence is defined internally as the supremum-style least upper bound of all congruences saturating a language, rather than postulated together with its universal property. The formation structures contain only the source closure axioms. In particular, neither correspondence map nor either inverse identity is stored as a structure field; doing so would trivialize the capstone. Contributions are welcome on the foundational universal-property and finite-index lemmas, the two formation constructors, and the recovery identities that assemble into the final order isomorphism.
The third mission in the series formalizing Allen Hatcher's Algebraic Topology (Cambridge University Press, 2002; pi.math.cornell.edu/~hatcher/AT/AT.pdf) turns to the second main topic of Chapter 1, covering spaces (Section 1.3, pp. 56–78). The first mission used the covering to compute , and the second proved van Kampen's theorem. This mission develops the general theory of covering spaces of a fixed space : the lifting properties (pp. 60–62), the classification of connected covering spaces by subgroups of (pp. 63–68), and deck transformations and group actions (pp. 70–72). Its goal is the classification theorem (Theorem 1.38, p. 67), Hatcher's "Galois correspondence" between path-connected covering spaces of and subgroups of , together with its companions Proposition 1.39 (deck groups and normal covers) and Proposition 1.40 (covering space actions and orbit spaces).
All statements live in the Lean namespace Hatcher used by the earlier missions.
A covering space of (p. 56) is a space with a map such that every has an open neighborhood whose preimage is a disjoint union of open sets each mapped homeomorphically onto ; may be empty, so need not be surjective. This is Mathlib's IsCoveringMap. For a covering space with basepoints we write
for the induced homomorphism (Hatcher.coverHom) and its image (Hatcher.coverSubgroup).
is semilocally simply-connected (p. 63, Hatcher.IsSemilocallySimplyConnected) if each has a neighborhood such that every loop at contained in is null-homotopic in . The bundle Hatcher_Covering also fixes: the structure CoveringSpace X (a total space and a covering map ) and its pointed version PointedCover X x₀ (with and associated subgroup PointedCover.subgroup); isomorphism of covering spaces (p. 67), a homeomorphism with , with or without preservation of basepoints (IsIsomorphic, IsPointedIsomorphic); the deck transformation group (p. 70, deckGroup), the self-homeomorphisms of commuting with ; normal covering spaces (p. 70, IsNormalCover); Hatcher's condition for a covering space action of a group on (p. 72, IsCoveringSpaceAction); and the orbit space with its quotient map (OrbitSpace, orbitProj).
Let be path-connected, locally path-connected and semilocally simply-connected, with basepoint . Then:
Together these say that is a bijection from basepoint-preserving isomorphism classes of path-connected covering spaces to subgroups, inducing a bijection from isomorphism classes to conjugacy classes of subgroups.
The result itself. The classification theorem is the central structural fact about covering spaces: the connected coverings of are "the same as" the subgroups of , with the universal cover corresponding to the trivial subgroup and normal coverings to normal subgroups. Proposition 1.40 is the standard method for computing fundamental groups of orbit spaces (, , lens spaces) and is used throughout Hatcher's later chapters.
Formalizing it. Mathlib (at this environment's revision) already has the lifting theory for covering maps: path and homotopy lifting (IsCoveringMap.liftPath, liftHomotopy), the monodromy action (IsCoveringMap.monodromy), the injectivity of (injective_path_homotopic_map, cited there as Proposition 1.31), the unique-lifting statement (IsCoveringMap.eq_of_comp_eq), and the lifting criterion itself (existsUnique_continuousMap_lifts_of_range_le, cited as Proposition 1.33). For quotient maps by a free properly discontinuous action it has IsQuotientCoveringMap, with the homomorphism and its kernel and surjectivity. Milestones 1, 4, 5 and 16 are therefore expected to be short reductions to Mathlib, and Mathlib's quotient-covering theory should carry most of milestones 14–15. Mathlib has no notion of semilocal simple connectivity, no construction of the universal cover or of the coverings , no classification theorem, and no deck transformation groups or normal coverings; milestones 6–13 and the goal are new.
The heart of the mission is the construction of the universal cover (pp. 63–65): the points are homotopy classes of paths from , the topology is generated by the sets for in the basis of path-connected open sets on which dies, and one must verify that this is a topology basis, that is a covering map, and that the result is simply connected. Proposition 1.36 then passes to a quotient by and checks that the projection remains a covering map. Both are elementary but long, and formalizing them requires a systematic treatment of path homotopy classes as points of a space.
Propositions 1.37 and 1.39 follow from the lifting criterion and unique lifting; the deck-group homomorphism in 1.39(b) sends a loop in to the deck transformation produced by the lifting criterion, and its kernel is computed by Proposition 1.31. Proposition 1.40(a) needs the quotient topology on and the evenly covered neighborhoods from condition ; part (b) is the observation that a deck transformation of a path-connected cover is determined by one value. Milestone 3 is orbit–stabilizer for the monodromy action.
CoveringSpace X bundles a total space in the same universe as with a covering map; the classification quantifies over covering spaces in this sense. Since the universal cover and the coverings are constructed from paths in , they live in that universe, so nothing is lost.MulAut.conj; "number of sheets equals the index" is stated as a bijection with the coset space.Normal instance in the statement; the final clause of 1.39 and 1.40(b) are stated as the existence of group isomorphisms, the latter with its action on prescribed.MulAction.orbitRel.Quotient with the quotient topology.Contributions welcome: a reusable construction of the space of path classes with its topology, the covering , and the deck-group homomorphism; the short reductions to Mathlib for Propositions 1.31, 1.33 and 1.34 are good first contributions.
Mathlib/Topology/Covering/Basic.lean (covering maps). https://github.com/leanprover-community/mathlib4/blob/0df444a360eaa60ab8c11dca51a86af692955474/Mathlib/Topology/Covering/Basic.leanMathlib/Topology/Homotopy/Lifting.lean (path and homotopy lifting, monodromy, the lifting criterion). https://github.com/leanprover-community/mathlib4/blob/0df444a360eaa60ab8c11dca51a86af692955474/Mathlib/Topology/Homotopy/Lifting.leanMathlib/Topology/Covering/Quotient.lean (quotient covering maps for group actions). https://github.com/leanprover-community/mathlib4/blob/0df444a360eaa60ab8c11dca51a86af692955474/Mathlib/Topology/Covering/Quotient.lean