Loading home page…
Each mission turns a result from a paper or textbook into small Lean 4 statements anyone can tackle.
Campaigns group missions around a shared mathematical goal. Each one tracks a quantity, such as an upper or lower bound. Have a good candidate in mind? Ping us on Slack, Zulip, or WeChat.
Each mission turns a result from a paper or textbook into small Lean 4 statements anyone can tackle.
Campaigns group missions around a shared mathematical goal. Each one tracks a quantity, such as an upper or lower bound. Have a good candidate in mind? Ping us on Slack, Zulip, or WeChat.
Classical algorithms solve 3SUM in time. In a 2026 breakthrough, Alman and Vassilevska Williams gave a deterministic algorithm, refuting the integer 3SUM hypothesis. How low can the exponent go?
Building on existing Lean formalizations, this campaign tracks upper bounds for 3SUM on polynomially bounded integers, using a word RAM with -bit words, and pursues smaller exponents.
Classical algorithms solve all-pairs shortest paths in time. In a 2026 breakthrough, Alman and Vassilevska Williams refuted the APSP conjecture with a deterministic algorithm. How low can the exponent go?
Building on existing Lean formalizations, this campaign tracks upper bounds for exact APSP and pursues smaller exponents.
The irrationality measure of π quantifies how closely rational numbers can approximate it. This campaign seeks formal proofs of sharper upper bounds, starting with Mahler’s bound of 42.
The sharp Hlawka inequality for Schatten -norms is a cousin of the triangle inequality: it relates the norms of three matrices to the norms of their pairwise sums and their total sum. For complex diagonal matrices, an exact formula for the best possible comparison constant has been proved in Lean for every real . We conjecture that the same formula holds for all .
What is the smallest cutoff for which this formula holds for every real ?
References:
Is every odd number a sum of primes? This campaign tracks formalized proofs of the smallest that suffices.
Schnirelmann (1930) showed some finite works. Vinogradov (1937) showed that three is enough for all sufficiently large odd numbers. Tao (2012) proved unconditionally. Helfgott (2013) proved that every odd number greater than is a sum of three primes, though the proof is still unrefereed. Ideally, we can formalize this statement here. Note that three is optimal: is neither prime nor + prime.
Schoolbook matrix multiplication takes operations. The exponent is the infimum of all such that two matrices can be multiplied in arithmetic operations; trivially , and is conjectured but open.
Strassen gave the first nontrivial bound, , in 1969, and introduced the laser method in 1986 to reach . Coppersmith and Winograd's 1990 bound of stood for two decades. Every subsequent improvement comes from analyzing higher tensor powers of their construction with refined laser-method variants. That line reached in 2025, and the current record is , from August 2026. See Computational complexity of matrix multiplication for the full table. Can we formalize these results and even improve on them?
Many hard combinatorial optimization problems — finding the maximum cut of a graph, deciding the ground state of an Ising spin system, bounding the correlation of a physical system — can be written as maximizing a bilinear form over sign vectors . Exhaustive search over sign patterns is intractable, so practitioners relax the problem: replace each sign by a unit vector in a higher-dimensional space and optimize the resulting inner products instead. This relaxation, a semidefinite program, is convex and solvable in polynomial time. The question is how much is lost in the relaxation — whether its optimal value can be far from the true, combinatorial optimum.
Grothendieck's inequality, proved by Alexander Grothendieck in 1953 in the context of Banach space theory (Résumé de la théorie métrique des produits tensoriels topologiques, Bol. Soc. Mat. São Paulo 8 (1953), 1–79), answers this for a broad class of such relaxations: replacing signs by unit vectors in an arbitrary Hilbert space changes the optimal value by at most an absolute, dimension-free constant factor. The inequality has since become a standard tool across combinatorial optimization, Banach space geometry, and (via the Goemans-Williamson algorithm for maximum cut, Section 3.6 of the source) approximation algorithms; see U. Haagerup, The Grothendieck inequality for bilinear forms on -algebras, Adv. Math. 56 (1985) for the tightest known constant, and Alon–Naor, Approximating the cut-norm via Grothendieck's inequality, SIAM J. Comput. 35 (2006), for the algorithmic connection this mission's Theorem 3.5.6 sets up.
Fix positive integers . Consider a real matrix . Say is normalized if for every choice of numbers ,
This says , viewed as a bilinear form on , has sup-norm at most . Now let be any real Hilbert space — a real vector space equipped with an inner product complete in the induced norm — and consider vectors and , each of unit norm . Replacing the scalar product by the inner product in the same bilinear form gives , a real number depending on the choice of and of the unit vectors. The question is how large this can be, uniformly over every such choice.
for every real Hilbert space and unit vectors , where is a constant depending on neither , its dimensions, nor . This mission's goal formalizes the book's own first-pass bound (Section 3.5), proved by a Gaussian truncation argument; it does not fix a numeral for , only that some absolute constant works, matching the shape of the true statement rather than a specific numeral that a sharper argument (the book's own Section 3.7 gives ) would immediately obsolete. See Formalization scope below for why this is the goal, not the sharper bound.
The result itself. Grothendieck's inequality is the single fact that makes semidefinite relaxation a provably good algorithmic strategy rather than a heuristic: whatever the true, hard-to-compute combinatorial optimum of a -valued bilinear optimization is, the tractable Hilbert-space relaxation cannot overshoot it by more than the constant . Milestone Theorem 3.5.6 makes this concrete for positive-semidefinite matrices, showing the semidefinite relaxation SDP of the integer program INT satisfies INT SDP INT — the guarantee underlying the Goemans-Williamson 0.878-approximation algorithm for maximum cut (Theorem 3.6.5 of the source, out of scope for this mission; see Formalization scope).
Formalizing it. The inequality and its two chapter milestones are proved but not previously
formalized on this platform (checked by concept search for "Grothendieck", "semidefinite",
"positive-semidefinite", and "max-cut" — no hits beyond the unrelated Grothendieck-Teichmüller
group). What remains after this mission is the sharper argument of Section 3.7
(the "kernel trick"), a separate, heavier development building on positive-definite kernels,
and full proofs of every milestone below (currently open sorry goals).
The statement of Grothendieck's inequality contains no randomness, yet every known elementary proof is probabilistic; this is itself a striking feature of the result. The obvious approach — bound directly by exploiting the normalization hypothesis on — fails because the normalization hypothesis only controls against sign vectors, and there is no way to project an arbitrary unit vector in a Hilbert space onto without losing information. The book's proof instead represents each unit vector via a scalar Gaussian random variable for a single Gaussian vector , recovering the inner products in expectation (Exercise 3.3.5); but these Gaussian variables are unbounded, so the normalization hypothesis (which bounds against bounded inputs) cannot be applied to them directly. The core technical step is a truncation argument: splitting each Gaussian variable into a bounded part and a small--norm unbounded remainder, applying the hypothesis to the bounded parts, and bounding the remainder terms by treating them as elements of the Hilbert space and invoking the very inequality being proved (Theorem 3.5.1 itself, applied with ) as a self-referential bootstrap — this is why the proof fixes as the smallest valid constant before starting, rather than building it up from scratch.
The goal and both milestones work with the real matrix and real inner product space directly;
H is required to be a complete real inner product space (NormedAddCommGroup,
InnerProductSpace ℝ, CompleteSpace), matching the book's "any Hilbert space." No
dimension bound on is imposed — the inequality's content is exactly that does not grow
with .
This mission does not formalize the sharper bound of Section 3.7, nor Theorem 3.6.5 (the 0.878-approximation guarantee for maximum cut via randomized rounding): the latter's statement quantifies over "the result of a randomized rounding of the solution of the semidefinite program," which would drag a specific algorithm into the audited statement rather than keeping it a self-contained mathematical claim (the statement/proof-separation trap this series' triage rubric flags). Grothendieck's identity (Lemma 3.6.6), the key fact behind that rounding step, is included on its own as a milestone, stated with an explicit, named random sign variable rather than an opaque "rounding procedure."
A trivializing formalization would state the goal with allowed to depend on , , ,
or — every such bound is easy (e.g. ) and carries none of the
theorem's content; the Lean statement rules this out by quantifying before every other
object. and (Theorem 3.5.6) are defined from scratch in this
chunk's namespace, using Matrix.PosSemidef from Mathlib for the positive-semidefiniteness
hypothesis (which bundles the real-symmetric condition); Mathlib has no ready-made SDP-value
construction to reuse. The sub-gaussian (Orlicz ) norm used by Theorem 3.1.1 is reused,
unchanged, from the 01-concentration mission in this series (HighDimProb.Concentration.SubgaussianNorm)
rather than redefined.
Any dataset of points can be described exactly by embedding it in for large enough — but a large is expensive: nearest-neighbor search, clustering, and streaming algorithms all scale with the ambient dimension, not with . The question that opens this mission is whether the dimension can be cut down while leaving the data's geometry — the pairwise distances between points — essentially untouched.
Johnson and Lindenstrauss answered this in 1984, while studying extensions of Lipschitz maps into Hilbert space (W. Johnson, J. Lindenstrauss, Extensions of Lipschitz mappings into a Hilbert space, Contemp. Math. 26 (1984), 189–206): points in any Euclidean space, of any dimension , can be mapped by a single linear map into a space of dimension only , distorting every pairwise distance by at most a factor of . The map does not depend on the data beyond its cardinality — a single random object works simultaneously for the whole point set with high probability. This is now one of the standard tools of randomized dimension reduction, cited across nearest-neighbor search, streaming linear algebra, compressed sensing, and machine learning pipelines that need to shrink feature dimension before a downstream algorithm runs.
Fix a probability space . A random orthogonal projection of rank in is a map , continuous and linear for each , such that almost surely is idempotent (), self-adjoint, and has range of dimension — i.e. is the orthogonal projection onto some -dimensional subspace . It is uniformly distributed in the Grassmannian (written ) when its law is rotation invariant: for every orthogonal transformation of , the conjugated map has the same law as . Conjugating a projection by is exactly the projection onto the image of its range under , so this says the law of the random subspace is invariant under the full orthogonal group — the operational definition Vershynin himself uses for a "uniformly distributed" random subspace, since no coordinate-free formula for such a subspace's law is given directly.
A companion notion drives the proof: a random vector is uniform on the Euclidean sphere of radius , , when it lies on that sphere almost surely and its law is likewise rotation invariant. And a real random variable is sub-gaussian with sub-gaussian () norm , the standard non-asymptotic measure of how light-tailed 's distribution is (a bounded or Gaussian random variable has finite norm; the tail probability then decays at least as fast as ).
for every finite , every , and every random orthogonal projection of rank uniformly distributed in . The universal quantifier over pairs sits inside the single probability event — this is the union-bound content that makes the statement a genuine simultaneous guarantee for the whole point set, not a restatement of the single-vector lemma below for one fixed pair. Both constants are the book's own unnamed absolute constants, never depending on , , , or ; this is the weakest stable form of the claim (no numeral is hard-coded for or ), matching the book's own statement exactly.
The lemma gives a universal, data-oblivious dimension-reduction guarantee: the target dimension depends only on the number of points and the desired distortion, never on the ambient dimension or on the geometry of the specific point set. This is what makes it usable as a black-box preprocessing step ahead of an algorithm whose cost scales with — the projection is drawn once, without looking at the data, and works with high probability for every pairwise distance simultaneously. The bound is also known to be essentially optimal in : Alon (Problems and results in extremal combinatorics, Discrete Math. 273 (2003)) showed a lower bound of on the target dimension, so the dependence cannot be removed.
The theorem itself has been proved for decades and admits several proof strategies (this book's route through Lipschitz concentration on the sphere; the original volume/measure-concentration argument; later "sparse" or structured variants of the projection for faster computation). This mission formalizes the classical dense-Gaussian-projection proof route as Vershynin presents it, building the sphere-concentration engine (Theorem 5.1.4) and the single-vector projection lemma (Lemma 5.3.2) that the union-bound argument for the goal rests on. No machine-checked formal proof of this chain is known to exist on the platform prior to this mission (see Formalization scope below); what is contributed is the statement infrastructure — the goal and its two direct supporting lemmas, stated with explicit, unpinned absolute constants — for solvers to close.
The natural first idea — bound the distortion of a single fixed vector under a random projection, then take a union bound over the pairwise differences — is exactly the strategy Lemma 5.3.2 and the goal use, but it does not by itself explain why the single-vector concentration bound (Lemma 5.3.2(b)) holds with the stated sub-gaussian-type tail. That bound is not elementary: it reduces to a uniform concentration statement for an arbitrary Lipschitz function of a uniformly random point on a high-dimensional sphere (Theorem 5.1.4), since , viewed as a function of a rotated copy of , is a -Lipschitz function on the sphere. Proving that every Lipschitz function concentrates — not just linear ones, for which sub-gaussianity was already established in Chapter 3 — needs a genuinely different tool: comparing the sub-level sets of an arbitrary Lipschitz function to spherical caps via an isoperimetric inequality on the sphere. This geometric input is what makes the concentration phenomenon behind Johnson-Lindenstrauss a dimension-free fact rather than a special property of coordinate projections.
is a Finset of points in EuclideanSpace ℝ (Fin n), matching "a set of points"; is
read off as X.card. The random subspace is represented throughout by the
orthogonal projection onto it (IsUniformProjection), following the book's own statements,
which are phrased in terms of rather than ; the scaled map of the goal is
written Real.sqrt (n/m) • P ω applied to x - y, using linearity of to realize
. Both "uniform on the sphere" and "uniform in the Grassmannian" are defined
operationally by rotation invariance of the underlying law, since Mathlib has no ready-made
normalized surface measure on a general-radius Euclidean sphere or Haar-measure construction on
the Grassmannian/orthogonal group to build a canonical uniform object from; rotation invariance
uniquely determines the corresponding measure among those supported on the relevant set, so the
operational and constructive definitions coincide extensionally. Every "absolute constant" in the
book ( in Theorem 5.3.1's sample-complexity hypothesis, in every failure-probability bound,
and the sub-gaussian constant of Theorem 5.1.4) is existentially quantified ahead of the
dimension, sample size, and every other object, and pinned to no numeral — a formalization that
hard-coded a specific numeral for any of these would be invalidated by the next sharper constant
in the literature and would not match what the book actually proves.
A trivializing formalization is one that states the conclusion for a single fixed pair rather than universally over all pairs inside one event; that would collapse the union-bound content that makes this a dimension-reduction statement for a whole point set (with points), rather than a restatement of the single-vector Lemma 5.3.2(b). This mission's goal statement is built to rule that out explicitly (see Formalization targets above).
Reusable infrastructure: subgaussianNorm (the Orlicz norm, restated per Vershynin
Definition 2.5.6) and the rotation-invariance idiom for "uniformly distributed" random geometric
objects are of independent interest to any later chapter needing sub-gaussian random vectors or
random subspaces/projections (e.g. Chapters 4, 6, 7, 9, 11 of this same book series). Solvers'
contributions are welcome on: the isoperimetric inequality on the sphere and its use to prove
Theorem 5.1.4 (the mission's hardest open leaf); the coordinate-projection computation underlying
Lemma 5.3.2(a); and the concentration-plus-union-bound argument closing the goal from the three
supporting lemmas.
Existence of equilibrium is the first question any model of strategic interaction must answer, and the classical answer — Nash's theorem via Kakutani's fixed point theorem — asks for a convex, compact strategy space and continuous payoffs. Many of the models economists actually use do not have that: a firm's technology set can be discrete or irregular, and a payoff need only be upper semicontinuous, not continuous. Topkis [1979] showed that when a game's structure is instead order-theoretic — each player's strategies form a lattice, and the players' incentives reinforce each other in a precise sense — an equilibrium exists without any convexity or continuity assumption at all, and the proof method delivers something Kakutani's theorem cannot: a greatest and a least equilibrium point, with the whole equilibrium set forming a complete lattice. Zhou [1994] later showed the completeness of the equilibrium lattice in full generality; this mission formalizes the resulting theorem (Topkis's Theorem 4.2.1) together with its parametric extension (Theorem 4.2.2, established independently by Milgrom and Roberts [1990a] and Sobel [1988]), which shows how the greatest and least equilibria move as a parameter of the game — its technology, its cost structure — changes. This machinery underlies monotone comparative statics for games throughout economics: oligopoly models with strategic complements, coordination games, and search and matching models with increasing returns.
A noncooperative game consists of a finite player set , a set of feasible joint strategies (allowing the set of strategies feasible for one player to depend on the others' choices, so need not be a product set), and a payoff function for each player . Write for the strategies of every player but , for the section of at — player 's feasible strategies given the others' choice — and for player 's best-response set. The best joint response correspondence is . A feasible is an equilibrium point if for every player and every feasible deviation — no player can unilaterally improve.
A lattice is a partially ordered set in which every pair of elements has a join
and a meet . A function is supermodular on a subset if for all in it, and has increasing
differences in two of its arguments if is
monotone whenever . A game is a supermodular game
if is a sublattice, is supermodular in for every fixed
and every , and has increasing differences in for every — jointly, the conditions under which each player's own
strategy components are complements and complementary to the other players' strategies
(Theorem 2.6.1 of chunk 01-lattices/02-monotonicity's book).
If is a supermodular game, is nonempty and compact, and each is upper semicontinuous in on for every and every , then
is nonempty, has a greatest and a least element, and, under the order it inherits from , is itself a nonempty complete lattice.
Let be a partially ordered set and, for each , a supermodular game with nonempty, compact, and increasing in ; suppose each is upper semicontinuous in and has increasing differences in . Then for every there exist a greatest and a least equilibrium point of game , and both are increasing functions of on — the equilibrium set moves monotonically as the parameter increases.
Two supporting results are formalized as milestones because Theorem 4.2.1's own proof uses them directly: Lemma 4.2.1 (equilibrium points are exactly the fixed points of the best joint response correspondence) and Lemma 4.2.2, parts (b) and (f) (the best joint response set is a nonempty compact sublattice for every feasible , and the correspondence is increasing in ).
The result itself. Theorem 4.2.1 is the lattice-theoretic alternative to
Nash/Kakutani existence: it needs no convexity of and no continuity of
(upper semicontinuity suffices), and in exchange it delivers a greatest and a least
equilibrium — with an explicit order-theoretic characterization via Theorem 2.5.1 of
chunk 01-lattices — and the guarantee that the entire equilibrium set is a complete
lattice, not merely nonempty. Theorem 4.2.2 gives this existence result teeth for
applied comparative statics: it says that if a firm's cost structure, a market's demand
parameter, or any other feature of the game increases (in the sense of the induced set
order on and increasing differences in the payoffs), the extremal equilibria
increase too — the qualitative content behind results such as "more competition leads
to lower prices" in supermodular oligopoly models.
Formalizing it. The platform's existing Nash-equilibrium theorem
(AGT.nash_existence, Theorem 1.8 of Algorithmic Game Theory) is a Brouwer/Kakutani
argument for finite games with mixed strategies: it needs finiteness of every player's
strategy set (so that mixed strategies form a compact convex simplex) and gives no
lattice structure on the equilibrium set at all. Theorem 4.2.1 is a different
technique entirely — it needs no finiteness, no mixing, and no convexity, and its
conclusion (a complete lattice of equilibria) is exactly the content Brouwer/Kakutani
cannot give. This mission is therefore not a restatement of Nash's theorem in different
notation, but a second, independent existence technique with a strictly different
structural payoff, formalized here for the first time on the platform. It builds
directly on chunk 01-lattices's Theorem 2.5.1 (Zhou's fixed point theorem for
increasing correspondences) and chunk 02-monotonicity's supermodularity/increasing
differences definitions, both formalized earlier in this series.
The natural first idea for existence — "the best joint response correspondence has a fixed point by some general fixed-point theorem for correspondences" — needs the correspondence to be convex-valued and upper hemicontinuous for a Kakutani argument, neither of which supermodularity or upper semicontinuity alone supply: a best-response set under only upper semicontinuity can be a disconnected, non-convex set (e.g. the maximizers of a supermodular but non-quasiconcave function). The actual route goes through order instead of topology: Lemma 4.2.2 shows the best joint response set is a compact sublattice (hence subcomplete, by Theorem 2.3.1) and that the correspondence is increasing under the induced set order, which is exactly the hypothesis Theorem 2.5.1's non-constructive supremum/infimum construction needs — no convexity anywhere. A second subtlety, which the mission is careful not to elide: the equilibrium set of a supermodular game need be neither compact nor a sublattice of when there are more than one player (Topkis's Examples 4.2.1 and 4.2.2 exhibit both failures); only the weaker claim — a complete lattice under the inherited order — is true in general, and that is what Theorem 2.5.1(b) supplies.
A joint strategy is represented as a dependent function ∀ i, Fin (m i) → ℝ over a
finite player type ι, with a player's own strategy accessed and overwritten via
Function.update, so that is never reified as a separate object — every
statement about or membership in substitutes y for
x's own i-th coordinate directly. IsSupermodularGame reuses chunk
02-monotonicity's SupermodularOn and IncreasingDifferencesOn verbatim, applied to
each player's own payoff, rather than restating the supermodularity/increasing-
differences conditions from scratch — a formalization that inlined a weaker,
ad hoc notion here (e.g. supermodularity of the joint payoff vector rather than each
player's own payoff in their own strategy) would trivialize the connection to chunk
02-monotonicity's theorems that the book's own proof relies on. Theorem 4.2.1's
"nonempty complete lattice" conclusion is formalized, as in chunk 01-lattices, via
IsLUB/IsGLB on the subtype of equilibrium points — never as membership of the
ambient supremum/infimum in the equilibrium set, which the book's own
Examples 4.2.1–4.2.2 refute; a solution that instead proved the equilibrium set compact
or a sublattice of would be proving a strictly stronger and false claim.
Only parts (b) and (f) of Lemma 4.2.2 are formalized, since those are the only two of
its eight parts the proof of Theorem 4.2.1 uses; a complete development still needs
chunk 01-lattices's Theorem 2.3.1 (subcomplete iff compact) and Theorem 2.5.1/2.5.2,
and chunk 02-monotonicity's Theorem 2.8.1 and Corollary 2.7.1, none of which are
restated here.
A recurring question in economics and operations research is: when a decision problem depends on a parameter, does the optimal decision move monotonically as the parameter changes? A firm's optimal input mix as a price rises, a consumer's optimal consumption bundle as income grows, a Cournot firm's optimal output as a rival's output changes — in each case one wants "more of the parameter implies (weakly) more of the optimum" without assuming convexity, differentiability, or a unique optimizer. The classical tool for such comparative statics questions is the implicit function theorem, which needs smoothness and a nondegenerate Hessian and breaks down the moment the optimum is not unique or the objective is not differentiable. Topkis [1978] showed that a purely order-theoretic condition — supermodularity of the objective jointly in the decision variable and the parameter — is sufficient on its own, with no smoothness, uniqueness, or convexity assumed at all, and Milgrom and Roberts [1990a, 1994] later showed this lattice-theoretic approach subsumes and strengthens the classical monotone-comparative-statics results in economics. This mission formalizes the two central results this book calls "Topkis's theorem" (Theorem 2.8.1 and Theorem 2.8.2), together with the structural fact about maximizers of a supermodular function (Theorem 2.7.1) that both rest on, and the strengthening to strictly ordered optimal selections (Theorem 2.8.4).
Let be a lattice: a partially ordered set in which every pair
has a join and a meet . A real-valued function
is supermodular on if
for all ; this is
the same relativized notion (SupermodularOn) used, with , throughout chunk I of
this series.
Now let also be a partially ordered set (the parameter set), and let be a real-valued function of the pair . has increasing differences in if, for every in , the map is monotone (order-preserving) in ; equivalently, the marginal gain from raising is itself increasing in . Replacing "monotone" with "strictly monotone" gives strictly increasing differences. To compare the resulting sets of optimizers rather than single points, this mission reuses the induced set ordering from chunk I: for , holds when and for all , .
Let and be lattices, let be a sublattice of the product lattice , and let be the section of at . If is supermodular on (jointly in the pair ), then
is increasing in , with respect to , on .
With increasing in (with respect to ), supermodular in for each fixed , and having increasing differences in on , the same conclusion — increasing in — holds. Theorem 2.8.2's joint-supermodularity hypothesis on a sublattice of automatically forces both of Theorem 2.8.1's hypotheses, so 2.8.1 is the logically weaker, more elementary statement from which 2.8.2's proof proceeds.
Under the hypotheses of Theorem 2.8.1 but with strictly increasing differences, every individual optimal solution at a larger parameter value dominates every individual optimal solution at a smaller one: , , and together force — a genuinely stronger conclusion than alone gives.
A supporting result is formalized as a milestone because both goals' proofs use it directly: Theorem 2.7.1, that is a sublattice of whenever is supermodular on — the structural fact that makes it meaningful to compare optimal-solution sets with in the first place.
The result itself. Theorem 2.8.2 is the book's own headline theorem, cited throughout the rest of the monograph: it underlies the assortative-matching existence theorem (Chapter 3), monotone optimal policies in Markov decision processes (Chapter 3), and equilibrium comparative statics in supermodular games (Chapter 4) — each a later mission in this series. Its distinguishing feature relative to the implicit function theorem is that it needs no differentiability, no uniqueness of the optimizer, and no interiority: it applies equally to discrete decision problems (integer programming, combinatorial selection) and continuous ones.
Formalizing it. Nothing in Mathlib currently states a parametric monotone-comparative-
statics result of this shape: the closest neighboring material (order-preserving maps,
MonotoneOn, lattice structures) supplies only the vocabulary, not the theorem. This
mission is the first formalization of Topkis's theorem on this platform and introduces
the increasing-differences vocabulary (IncreasingDifferencesOn,
StrictlyIncreasingDifferencesOn) that later missions in this series (matching, MDPs,
supermodular games) reuse directly.
The natural first idea — differentiate in , set the gradient to zero, and use the implicit function theorem on the resulting first-order condition — fails immediately because nothing here is assumed differentiable, and need not be a single point. The correct argument instead compares two arbitrary elements , directly through the supermodularity inequality applied to the pair against (a chain of inequalities Topkis calls "Lemma 2.8.1"), using increasing differences only to move the parameter from to inside that chain — at no point is a derivative, a selection function, or an interior point used. A second subtlety is that "increasing" in the conclusion is with respect to the induced set order , not a claim that some selection is monotone: proving the stronger, pointwise-ordered conclusion (Theorem 2.8.4) genuinely needs the strict form of increasing differences, not merely increasing differences plus an extra hypothesis.
and are kept as abstract Lattice/PartialOrder types throughout, matching the
book's own generality — Theorem 2.8.1's and 2.8.2's /
corollary via second partial derivatives (discussed in the book's prose immediately after
Theorem 2.8.2, p. 77) is not itself a numbered theorem and is not formalized here.
Supermodularity, increasing differences, and strictly increasing differences are each
formalized as a single relativized definition (SupermodularOn f S,
IncreasingDifferencesOn f S, StrictlyIncreasingDifferencesOn f S) so the same
declaration expresses both "supermodular on the whole lattice " (used by Theorem 2.7.1
and Theorem 2.8.1's per- hypothesis) and "jointly supermodular on a sublattice of
" (Theorem 2.8.2) — a formalization that instead only ever supermodularized
for fixed would collapse Theorem 2.8.2's genuinely joint hypothesis into
a restatement of Theorem 2.8.1, which is exactly the trivialization this mission's chunk
brief warns against. is written out as the set
of that dominate every other element of under , and every
conclusion is stated only for pairs at which both argmax sets are assumed
nonempty — matching the book's own restriction to , since holds
vacuously whenever either side is empty. This mission depends on chunk I's
InducedSetOrder; it introduces no reusable infrastructure beyond its own three
definitions, which later missions in the series (matching, MDPs, supermodular games) are
expected to import directly rather than redefine.
This mission formalizes §4 of Cannon, Floyd and Parry's Introductory notes on Richard Thompson's groups, together with the definition of Thompson's group from their §1. The goal is their Theorem 4.5: the commutator subgroup is simple.
In the 1960s Richard Thompson defined three groups, now written , and , whose properties have kept them in use ever since as a source of examples at the edge of what groups can do. is the smallest of the three and the least understood. It is finitely presented (§3 of the source) and torsion-free, it has no free subgroup of rank two, and whether it is amenable — whether it carries a finitely additive left-invariant probability measure defined on all its subsets — is open. Cannon, Floyd and Parry record (§4, p. 227) that Geoghegan raised the question and conjectured in 1979 both that contains no non-Abelian free subgroup and that is not amenable.
That question is what makes worth pinning down precisely. Write for the class of
amenable discrete groups, for the elementary amenable ones, and for the groups with
no free subgroup of rank two. That was noted by
Day and follows from
von Neumann; whether it is strict is the von
Neumann–Day problem. It is: Olshanskii proved in a 1984 ICM address and
Gromov gave an independent proof — but by
examples that are not finitely presented. Brin and Squier proved in 1985 that , and
is not elementary amenable (Theorem 4.10 of the source, CannonFloydParry.not_elementaryAmenable_F). So
is a finitely presented group in if it is amenable and in
if it is not — a question with no other finitely presented candidate.
Call a real number dyadic if it has the form with and .
Thompson's group , as §1 of the source defines it, is the set of piecewise linear homeomorphisms of the closed unit interval onto itself that are differentiable except at finitely many dyadic rationals, and whose derivatives, where they exist, are powers of . Since those derivatives are positive, every element preserves orientation, so the elements of are increasing. Composition of two such maps is again one, and so is the inverse of one, so is a group.
The formalization calls such a map piecewise linear over the dyadics, and defines as the subgroup generated by those maps — so that closure under composition and inverses is a theorem rather than part of the construction, as the source has it. What the model fixes rather than derives is under Formalization scope below.
Two particular elements generate it. Write
An element of is trivial near if it fixes every point of some interval , and trivial near if it fixes every point of some . The support of is the set of points of that moves. The commutator convention throughout is , and denotes the commutator subgroup.
This is the capstone of §4: it says the commutator subgroup has no normal subgroup other than itself and the trivial one. It is the goal because the rest of the section feeds it — both halves of Theorem 4.1, Theorem 4.3, and both supporting lemmas below are consumed by its proof.
So has no interesting proper quotients at all. With the first part of Theorem 4.1 this forces every nontrivial normal subgroup of to contain .
That the piecewise-linear maps are already closed under composition and inverses, so that consists of exactly those maps; a transitivity lemma on dyadic partitions of ; the fact that the subgroup of elements supported in a dyadic interval of dyadic length is isomorphic to itself; triviality of the center; that contains no non-Abelian free group; and that admits a total order invariant under multiplication on both sides.
What the results give. Theorem 4.1 identifies concretely — a subgroup defined by a global algebraic condition turns out to be cut out by local behavior at the two endpoints — and computes the abelianization, making the pair of endpoint slopes a complete invariant of modulo commutators. Theorem 4.3 and the simplicity of together determine the whole normal subgroup lattice: every normal subgroup of is trivial or contains . That lattice is the input to the elementary-amenability argument.
What formalizing adds. All of these are proved in the source; none is in Mathlib, which has no piecewise-linear homeomorphism API and no Thompson group. Four of the milestones are proved as part of this proposal: that the piecewise-linear maps form a subgroup, that elements of permute the dyadic rationals, that embeds in the group Brin and Squier work with, and the absence of a free subgroup of rank two, which follows from the already-formalized Brin–Squier theorem via that embedding. The rest are open. The piecewise-linear machinery built along the way — local affineness, dyadic-breakpoint bookkeeping, extension by the identity — is reusable for , for , and for the wider family of piecewise-linear homeomorphism groups.
The obvious approach to the goal is to argue that a normal subgroup of containing a nontrivial element must be everything, by conjugating that element around. It fails on its own: an element of is pinned down only by being trivial near the two endpoints, and one still has to manufacture — inside , not merely inside — an element carrying a prescribed pair of neighborhoods into those. That construction is what the dyadic-partition transitivity lemma supplies, and it is where the combinatorics of dyadic subdivision enters.
The second difficulty was that the source proves §4 using the tree-diagram normal form of §2.
That section is now formalized in its own mission, Cannon–Floyd–Parry §2: tree diagrams and the
normal form (mission ffd1e4ea-9f9a-4cb6-8419-78e70f2545e8), all of whose milestones are proved.
Corollary 2.6 — milestone 5 here, the same theorem object — is closed from there, and Theorem
2.5 (represents_word_exponents) and the normal form (existsUnique_normalForm) are available to
a solver attacking Theorem 4.3, so the source's argument can now be followed. A solution file
imports only definitions, so whatever it uses from §2 must be reproved inline; the §2 solutions
are public and written to be reused that way. The piecewise-linear route — dyadic-partition
transitivity, Lemma 4.4 and Theorem 4.1 — remains an alternative, and is what Theorem 4.5's own
argument uses.
The unit interval is as a subtype, and an element of is an order isomorphism of it, so orientation preservation is built into the representation rather than derived — faithful to the source's set, but assuming one sentence CFP prove. Piecewise linearity is stated as: there is a finite set of dyadic reals such that the map is affine, with slope a power of two, on every closed interval whose interior misses . Intercepts are not required to be dyadic — that is derived by induction along the breakpoints, not part of the definition.
The definition is not vacuous: and of Example 1.1 are constructed explicitly, and that is not the trivial group is one of the milestones below — so no statement here is satisfied by the trivial group. In particular the goal, which asserts simplicity and therefore nontriviality, is not trivially false.
A companion definition places the same data on the real line, each element extended by the identity outside ; that line realisation is what the bridge statement connects to Brin and Squier's group.
Write the primes in increasing order, take the absolute differences of consecutive entries, take the absolute differences of the resulting row, and repeat. Every row produced this way appears to begin with :
Gilbreath's conjecture asserts that this never fails. The observation is due to Norman L. Gilbreath (1958), who rediscovered a statement already published by François Proth in 1878 together with an argument that is not accepted as a proof. It is attractive because it is elementary to state and because it is one of the few statements about the primes whose difficulty is not visibly analytic: it concerns the combinatorics of iterated differences rather than the distribution of primes directly.
Timeline.
No proof is known.
Let be the increasing enumeration of the prime numbers, indexed from . Define the rows of the Gilbreath triangle by
Thus is an infinite sequence of natural numbers for every , row is the sequence of primes, row is the sequence of prime gaps , and each later row is the sequence of absolute differences of consecutive entries of the row above it. Only the leading entry of each row is at issue.
More generally, for an arbitrary sequence write and for the -fold iterate, so that .
This is the conjecture in its standard form: every row after the row of primes begins with . It fixes no constants and no ranges, so no computational advance can invalidate it.
The milestone list collects the statements that a proof, or a further computational verification, would be built from: the two low-level structural facts about the triangle (row is the gap sequence; from row on, the leading entry is odd and all later entries are even), a finite verification of the first rows, and the two statements underlying Odlyzko's method — the propagation lemma for an arbitrary sequence beginning and continuing in , and the reduction of the conjecture to the existence, for each row index, of an earlier row with a long enough block of entries in .
The result itself. The conjecture is not known to imply other open statements about the primes, and its interest lies elsewhere: it is a test case for how much of the fine structure of the prime sequence is forced by coarse information. The propagation mechanism shows that the conjecture for a given row index follows from purely local data about an earlier row, and that mechanism is what every verification to date has relied on. A proof would have to show that such blocks of entries in always appear early enough, which is a statement about the density of small prime gaps in disguise.
Formalizing it. Nothing here is currently formalized: Mathlib has the prime
enumeration (Nat.nth Nat.Prime) and the basic facts about it, but
not the iterated-difference triangle nor any of its properties. This mission
contributes the definition of the triangle, the structural facts about its rows, and
a machine-checked version of the reduction step that all computational work on the
problem uses. The goal theorem itself is open — the milestones are known mathematics,
and each is provable with current tools, while the goal is not.
The obvious attack is induction on the row index: to see that it suffices to know that and . But controlling requires controlling and , and so on: the invariant that closes is not "the row begins with " but "the row begins with and its next entries lie in ", and each application of the difference operator consumes one entry of that block. So a finite block of good entries only carries the conclusion a finite number of rows further down, and the conjecture needs such blocks to keep reappearing forever, arbitrarily far down the triangle. Nothing is known that produces them.
A second warning, due to Hallard Croft: the property is not specific to the primes. Sequences that start with , continue with odd numbers, and have gaps that are not too large empirically exhibit the same behaviour, so any proof that uses only such coarse features would prove a much more general statement — and conversely, an argument exploiting deep properties of primes is likely to be proving the wrong thing.
Rows are total functions , defined for every index, and the
whole triangle is a single family indexed by the row number. Differences are taken as
Int.natAbs of a difference computed in , so truncated natural
subtraction never occurs; the one place where -subtraction does appear is
the milestone identifying row with the gap sequence, where the subtraction is
justified by monotonicity of .
Primes are indexed from via Mathlib's Nat.nth Nat.Prime, so ; rows are
indexed with row the primes, and the goal quantifies over all in the
form d (k + 1) 0 = 1, with no upper bound and no extra hypothesis, so no vacuous or
finitely-truncated reading of the goal is available. The general difference operator
is stated for arbitrary sequences , which is what makes the
propagation lemma usable as a black box, and reusable beyond this mission.
A complete development needs no analytic input for the milestones: Mathlib's
Nat.nth, Nat.prime_nth_prime, Nat.nth_prime_zero_eq_two and the strict
monotonicity of the prime enumeration suffice. Contributions that would extend the
mission beyond its current list: a formal version of a concrete computational
verification (checking that the leading entries of the first rows are for an
well beyond the hand-checkable range), and formalizations of the general
statement for non-prime sequences of the Croft type.
The Riemann hypothesis (RH) asserts that every zero of the Riemann zeta function in the strip has . One of the few reformulations that turns RH into a positivity statement, rather than a statement about the location of points, goes back to A. Weil (1952): the explicit formula expresses a sum over the zeros of as a sum of local contributions over the places of , and RH is equivalent to the resulting functional being positive on elements of the form .
Connes' 1999 programme paper Noncommutative geometry and the Riemann zeta function takes this reformulation as its endpoint. It builds a geometric framework — the adele class space carrying an action of the idele class group — in which the explicit formula appears as a Lefschetz formula, the zeros of -functions appear spectrally, and the paper's concluding assertion (§3, p. 22) is that the validity of the global trace formula implies, and is in fact equivalent to, positivity of the Weil distribution, i.e. RH for all -functions with Grössencharakter.
This mission formalizes the arithmetic core of that endpoint in its simplest instance: the global field with trivial Grössencharakter, so that the -function is itself. Concretely it asks for (i) the Riemann–Weil explicit formula for in the shape of Connes' equation (11), and (ii) both directions of the equivalence between positivity of the resulting Weil distribution and RH.
A rough timeline of the statements involved: Riemann (1859) gave the first explicit formula; von Mangoldt (1895) proved it rigorously; Weil (Sur les "formules explicites" de la théorie des nombres premiers, 1952) extended it to all global fields and isolated the positivity criterion; Bombieri (Remarks on Weil's quadratic functional in the theory of prime numbers, 2000) studied the associated quadratic functional in detail; Connes (1996–1999) gave the trace-formula interpretation formalized in part here.
All objects live on the group , the module of the idele class group of , written additively through , .
A test function is a map that is and has compact support (IsTest).
Its transform is
which is Connes' in the coordinate , shifted by so that is the variable of (mellinHat). On the critical line, is the ordinary Fourier transform.
The involution is , i.e. (starInv), and convolution is (conv).
The Weil distribution of a test function collects the pole terms, the finite places and the archimedean place:
where is the von Mangoldt function and (weilDistribution, with the three pieces named mellinHat, primeSum, archTerm). The middle sum is Weil's contribution of the finite places , the last integral the contribution of the real place.
The spectral side is
the sum over the zeros of with , each counted with its multiplicity (zeroSum, IsCriticalZero, zeroMult).
This is the direction that yields RH, and it is the weakest form of the endpoint of the paper: it fixes no rate, no test-function normalization beyond , and no numerical constant.
with the sum over zeros asserted to be (unconditionally) summable.
Together with the goal this is the equivalence asserted on p. 22 of the paper, in the case , trivial Grössencharakter.
The -identity on the critical line, and the fact that is again a test function.
Weil's positivity criterion is one of the standard equivalent forms of RH, and the only one in which the arithmetic input (the primes, through ) and the archimedean input (the -factor) enter as separate, explicitly computable local terms. Formalizing it produces a machine-checked bridge between the zeros of and prime sums: the explicit formula milestone is the reusable object here, since essentially every analytic application of zeta zeros — zero-density estimates, prime-counting error terms, pair-correlation statistics — is an instance of it.
Status honesty: neither RH nor the positivity statement is known; the explicit formula and both implications relating positivity to RH are classical theorems, proved but not, as far as the catalog shows, formalized in Lean. Mathlib currently provides , its functional equation, the von Mangoldt function and , but no explicit formula of any kind. What this mission adds on top of the paper is therefore the formal proof of known results, not new mathematics.
The obvious route to the explicit formula — integrate over a vertical line, move the contour to the reflected line, collect residues — fails to be routine at exactly two points. First, moving the contour requires control of on horizontal segments between zeros, which is where the classical proof invests most of its work; Mathlib has bounds near but nothing of this shape inside the strip. Second, the sum over zeros must be shown to converge unconditionally, which needs a zero-counting bound of Riemann–von Mangoldt type () that is not in Mathlib either.
For the goal implication, the naive idea — pick a test function whose transform is supported near a hypothetical off-line zero — is unavailable: is entire whenever has compact support, so it cannot be localized. The classical argument instead exploits the symmetry of the zero set and makes the off-line quadruple contribute a negative amount in the limit along a family of test functions.
Conventions the Lean statements commit to. Test functions are -valued on , ContDiff ℝ (⊤ : ℕ∞) (so , not analytic) with HasCompactSupport; the multiplicative group is always written additively. The transform carries the -shift shown above, so the critical line is and are the two pole terms. Zeros are indexed by the subtype and weighted by (analyticOrderAt riemannZeta s).toNat; the trivial zeros are excluded. Integrals are Bochner integrals and sums are tsum, so both take the junk value when the integrand is not integrable or the family is not summable — for that reason the explicit formula is stated as a HasSum, which carries summability, rather than as an equation between tsums. The archimedean term is written with , logDeriv Complex.Gamma, rather than as a principal value, to avoid a second regularization convention.
The goal is not trivially satisfiable: its hypothesis quantifies over a nonempty class (smooth bump functions exist), and its conclusion is RH for , so no vacuous reading is available.
Infrastructure a complete development needs, all reusable beyond this mission: growth bounds for inside the critical strip, a Riemann–von Mangoldt zero-counting bound, Fourier analysis of functions (Paley–Wiener style decay of ), and the Hadamard product / functional equation package for the completed zeta function.
Out of scope, and deliberately so: Connes' operator-theoretic trace formula (equations (41) and (45) of the paper) and the spectral realization theorem of p. 17. Both are statements about traces of operators on Hilbert space, and Mathlib presently has no trace-class operator theory to state them faithfully. The mission therefore formalizes the arithmetic side of the paper's endpoint; contributions that build the missing operator theory, or that extend the statements from to Dirichlet -functions and Hecke -functions with Grössencharakter, are welcome.
Mirror symmetry was discovered in string theory as a duality between families of Calabi–Yau manifolds, and it entered mathematics as a prediction: the generating function counting rational curves on one manifold equals a period integral of a mirror manifold. In his 1994 ICM address, Homological algebra of mirror symmetry (alg-geom/9411018), M. Kontsevich proposed that these numerical coincidences are shadows of an equivalence of categories: the symplectic geometry of should be encoded by Fukaya's -category , whose objects are Lagrangian submanifolds and whose products count pseudo-holomorphic discs, and the complex geometry of the mirror by the derived category of coherent sheaves. His Homological Mirror Conjecture asserts that the derived category built from embeds as a full triangulated subcategory of .
Kontsevich states the conjecture "in slightly vague form", because Fukaya's construction was not, and still is not, available in the generality the statement needs. He therefore closes the paper with the one instance he can compute by hand, in the section Two-dimensional tori: a return: for the flat torus , the objects are closed geodesics with unitary local systems, the products are sums over triangles in the universal cover weighted by , and their structure constants are values of the classical theta-function. He predicts an equivalence with for an elliptic curve . This instance was proved by A. Polishchuk and E. Zaslow, Categorical mirror symmetry: the elliptic curve (math/9801119). Later instances include the four-torus (Abouzaid–Smith, arXiv:0903.3065) and Calabi–Yau hypersurfaces (Sheridan, arXiv:1111.0632). None of this has been formalized.
Fix a real number , and let be the torus carrying the translation-invariant symplectic form of total area ; a region of Euclidean area in coordinates has symplectic area .
A brane consists of: a primitive vector and a point , which together determine the closed geodesic ; a grading , a real lift of the direction angle normalized so that is parallel to ; and a real constant describing a flat unitary line bundle on , whose parallel transport along a path of parameter length is . Two branes are transverse when ; their geodesics then meet in the finite set , which indexes a basis of the Floer space . All of this space sits in a single degree, the Maslov index
For three pairwise transverse branes and intersection points , , , a triangle is a triple of lifts of with parallel to , parallel to , parallel to , and positively oriented. Kontsevich's structure constant is
the coefficient of in . On the complex side, denotes the complexes of -modules with bounded, coherent cohomology.
For every there exist a smooth proper curve over , an assignment of an object of to each brane, and isomorphisms
with for , carrying the products to composition in whenever .
Existence of the Fukaya -category of the torus; finiteness of with points; the Maslov relation ; together with associativity of up to coboundary; the degeneration of an -category with to a differential graded category; the theta-function shape of the structure constants; and their associativity equation.
The conjecture reorganizes mirror symmetry: the numerical predictions compare two elements of an uncountable set of power series, whereas the homological statement compares two objects in a countable set of triangulated categories, and the numerical statements are meant to follow from it. The torus case is the smallest instance in which every ingredient — Lagrangian branes, Maslov grading, disc counts, theta functions, and coherent sheaves on an elliptic curve — is present and computable, so it is the natural first target.
What this mission adds beyond the literature is machine-checked mathematics where none exists. Mathlib currently has no symplectic manifolds, no Lagrangian Floer theory, no Fukaya categories, and no -categories; it does have schemes, sheaves of modules, and derived categories of abelian categories. The mission supplies the missing layer and the torus model, and asks for the comparison theorem. The definitions, the derived category with coherent cohomology, and the theta-function estimates are reusable outside this mission.
The obvious route — "transport the Polishchuk–Zaslow proof" — stalls at the point where the two sides are compared. Establishing that the triangle sums converge and equal theta-function values is analysis that Mathlib supports; producing an elliptic curve as a scheme with prescribed parameter, computing -groups between the mirror sheaves, and matching all products simultaneously is not currently supported by any library. A second difficulty is bookkeeping: gradings, Maslov indices and shifts must line up, since the product of two morphisms is nonzero only when , and the same numerical condition controls which triples of branes bound triangles at all.
Conventions committed to in Lean. An -category is encoded as a single graded module with morphism components and products given by a map on lists, of degree , with , and Stasheff signs in the bar-construction normalization; is " then ". Triangles are normalized by requiring the first vertex to lie in , which picks exactly one representative in each -orbit; only positively oriented triangles are counted; sums are tsums, so convergence is part of the work. The hom-space isomorphisms in the goal are required to be additive, not a priori -linear, because the derived category of -modules is not equipped with a -linear structure in Mathlib; the required compatibility with the structure constants pins down the algebra anyway. The goal asks only for the existence of a smooth proper curve over ; the paper's further prediction that has parameter is deliberately left out of the statement.
The goal is not trivially satisfiable: the intersection set of two transverse branes is nonempty, so the required isomorphisms force the corresponding -groups to be nonzero of the right size, in the right degree, with the prescribed products.
The general conjecture, for an arbitrary symplectic manifold with , is not stated here, and deliberately so: without symplectic manifolds and Floer theory in Mathlib, any general statement would have to take the Fukaya category as an unconstrained parameter, which would make it either vacuous or false. Building that infrastructure — symplectic manifolds, graded Lagrangian branes, Floer cohomology, twisted complexes over an -category and their triangulated structure — is the natural way to extend this mission, and such contributions are welcome.
Before any geometry of surfaces can be done, one has to say what a surface is, in a way that supports calculus: a subset of that is locally the smooth, non-degenerate image of an open piece of the plane. Every statement in the later theory — the first and second fundamental forms, the Gauss map, curvature, geodesics — is written in local coordinates, and is therefore meaningful only once one knows that the answer does not depend on the coordinates chosen. That independence is the content of the change-of-parameters theorem, which is what makes "differentiable function on a surface" and "geometric quantity of a surface" well-defined notions.
The reference for this mission is Manfredo P. do Carmo, Differential Geometry of Curves and Surfaces, 2nd edition (Dover, 2016), §2-2 "Regular Surfaces; Inverse Images of Regular Values" (pp. 54–71) and §2-3 "Change of Parameters; Differentiable Functions on Surfaces" (pp. 72–85): Definition 1 (p. 54), Propositions 1–4 of §2-2 (pp. 59, 61, 63, 65) and Proposition 1 of §2-3 (p. 74).
This is the fourth mission of a series formalizing do Carmo's book, sharing the namespace
DoCarmoDG with the others.
A subset is a regular surface when every has an open neighbourhood such that is the image of a map , defined on an open set , satisfying the three conditions of do Carmo's Definition 1:
Such an is a parametrization, or system of local coordinates, and is a coordinate neighbourhood.
Given a differentiable on an open set , a value is a regular value of when is surjective — equivalently, nonzero — at every with (do Carmo Definition 2, §2-2).
If and are two parametrizations of a regular surface with , then
is a diffeomorphism: is differentiable, bijective, and is differentiable.
The graph of a differentiable function of two variables is a regular surface (Proposition 1); the inverse image of a regular value is a regular surface (Proposition 2); a regular surface is locally the graph of a differentiable function of one of the three coordinate pairs (Proposition 3); and an injective map satisfying conditions 1 and 3 whose image lies in a regular surface automatically has a continuous inverse (Proposition 4).
Proposition 2 is the practical criterion: it is what shows in one line that spheres, ellipsoids, tori and the level sets of generic polynomials are regular surfaces, and it is applied throughout the book. Proposition 3 is the structural statement that a regular surface is locally a graph, which is the form in which most local computations are carried out; Proposition 4 removes the awkward homeomorphism clause from the verification of examples. The change-of-parameters theorem is what allows every subsequent definition — differentiable function on a surface, tangent plane, first fundamental form, curvature — to be given in coordinates and then shown to be independent of them, and it is also the reason a regular surface carries a smooth structure at all.
Mathlib has smooth manifolds, the implicit and inverse function theorems, and ContDiffOn, but it
does not contain do Carmo's concrete definition of a regular surface as a subset of
or these four propositions about it. Establishing them is what allows the rest of this series to
work with patches while knowing that the objects so defined are coordinate-independent.
Everything here rests on the inverse function theorem, but each proposition needs it in a slightly different form. Proposition 2 requires completing to a local diffeomorphism and reading off the level set — with the complication that which partial derivative is nonzero varies from point to point, so the coordinate that is solved for is not fixed in advance. Proposition 3 needs the same case distinction on which Jacobian minor of is nonzero, and this is exactly why the conclusion is a disjunction over the three coordinate pairs. Proposition 4 is where the homeomorphism condition is shown to be redundant, and the argument goes through the local factorization .
The change-of-parameters theorem is not a direct application of the inverse function theorem to : the map is defined only on a subset of the plane and is, a priori, merely continuous. One first extends to a local diffeomorphism of a neighbourhood in and then composes; the continuity of (condition 2 of Definition 1) is what makes the domain of open, and it cannot be dispensed with.
A surface is a set S : Set (EuclideanSpace ℝ (Fin 3)), and a parametrization is a map
x : ℝ × ℝ → EuclideanSpace ℝ (Fin 3) together with an open U : Set (ℝ × ℝ). Smoothness is
ContDiffOn ℝ (⊤ : ℕ∞), matching do Carmo's "differentiable" for ; regularity is
injectivity of the Fréchet derivative at each point of U, which is do Carmo's condition 3; and
the homeomorphism condition is stated as injectivity on U together with the existence of a
continuous left inverse on the image, which is the content of "the inverse is continuous". The
neighbourhood clause of Definition 1 is x '' U = V ∩ S for an open V containing the point.
Graphs are formalized as three separate sets, one for each of , and
, so that Proposition 3 can state its disjunction faithfully; in that statement the
neighbourhood is an open set W of and the claim is W ∩ S = W ∩ graph.
The goal states the diffeomorphism property of explicitly — two maps, mutually inverse on the
relevant domains, both ContDiffOn, together with the openness of those domains — rather than
through a bundled structure, so that no library convention is assumed. There is no trivializing
reading: the domains are those forced by the two parametrizations, and in the degenerate case
where the images do not overlap the statement reduces to a true but empty claim about the empty
set, while the substance is in the overlapping case.
The local theory of curves describes what happens near one point; the global theory asks what a curve must satisfy because it closes up. Two classical statements make the difference visible. The isoperimetric inequality says that among all simple closed plane curves of a given length, the circle encloses the largest area — a question already settled in intent by the Greeks, but given a satisfactory proof only in the nineteenth century, and the short proof reproduced by do Carmo is E. Schmidt's from 1939. The four-vertex theorem says that the curvature of a simple closed convex curve has at least four critical points, so no convex oval has the curvature profile of a curve that just rises and falls once.
The reference for this mission is Manfredo P. do Carmo, Differential Geometry of Curves and Surfaces, 2nd edition (Dover, 2016), §1-7, "Global Properties of Plane Curves" (pp. 31–46): the area formula, equation (1) on p. 33; the isoperimetric inequality, Theorem 1 on p. 34; the theorem of turning tangents on p. 37; the lemma, equation (5) on p. 38; and the four-vertex theorem, Theorem 2 on p. 37.
This is the third mission of a series formalizing do Carmo's book, and shares the namespace
DoCarmoDG with the earlier ones.
A closed plane curve of length is a regular map whose derivatives of all orders agree at the two endpoints; equivalently, and as used here, a smooth -periodic map . It is parametrized by arc length when for all , in which case is its length. It is simple when it has no self-intersection: for distinct .
Write for rotation by , . For a curve parametrized by arc length the signed curvature is
which is do Carmo's convention of §1-5, Remark 1: the normal is chosen so that has the orientation of the natural basis, and then . A vertex is a parameter with . The curve is convex when, for every parameter , the whole trace lies in one of the two closed half-planes bounded by the tangent line at .
An angle function for is a smooth with ; the rotation index is . The area bounded by a positively oriented simple closed curve is given by do Carmo's equation (1),
The three equivalent forms of the area formula (1); the existence of a smooth angle function; the identity ; the theorem of turning tangents (the rotation index of a simple closed curve is ); the isoperimetric inequality with equality exactly for circles; and do Carmo's lemma (5), , which drives the proof of the goal.
The isoperimetric inequality is the ancestor of a large family of geometric inequalities, and its sharp case characterizes the circle — the first instance of the pattern "extremal configuration is the round one" that recurs throughout geometry. The four-vertex theorem is a genuinely global statement with no local counterpart: locally, the curvature of a convex arc may be strictly monotone, and it is only the requirement that the curve close up convexly that forces four critical points. Its converse, for strictly positive curvature, was proved by H. Gluck in 1971; do Carmo notes that the theorem also holds for simple closed curves that are not convex, by a harder argument.
Mathlib contains integration, the winding number of a loop in the complex plane and the Jordan curve theorem, but it does not contain the signed curvature of a plane curve, the theorem of turning tangents in this form, the isoperimetric inequality for curves with its equality case, or the four-vertex theorem. What this mission adds is that vocabulary and machine-checked proofs of the four classical statements.
Each target fails for a different reason under the naive approach.
For the area formula, the identification of with the area of the interior is exactly the Jordan-curve input that do Carmo declares he is assuming; the formalization avoids that dependency by defining the bounded area through the integral, so a solver has to prove only the integration-by-parts identities among the three forms of (1).
For the theorem of turning tangents, the difficulty is that a smooth lift of the tangent indicatrix must be produced and then shown to increase by exactly over one period — a degree-theoretic statement about a loop in the circle, where simplicity of the curve is what excludes the values .
For the isoperimetric inequality, Schmidt's proof compares the curve with a circle tangent to two parallel supporting lines and uses the arithmetic–geometric mean inequality; the equality discussion, which is where the characterization of the circle lives, is the delicate part.
For the four-vertex theorem, the obvious argument — "curvature on a compact interval attains a maximum and a minimum, so there are two vertices" — gives only two, and the whole content is the step from two to four. The lemma (5) supplies the contradiction: if changed sign only at the maximum and the minimum, a suitable line through those two points would make the integrand of (5) of one sign and not identically zero.
Curves are smooth maps ℝ → EuclideanSpace ℝ (Fin 2), closedness being -periodicity with
, which is do Carmo's condition that the curve and all its derivatives agree at the
endpoints. Unit speed is imposed globally, so the parameter is arc length and is the length.
Simplicity is injectivity on the half-open period . Convexity is stated per parameter: for
each the trace lies in one closed half-plane of the tangent line at , the choice of side
being allowed to depend on , as in the book's phrasing.
The area is defined by do Carmo's integral (1) rather than as the measure of the interior of the curve, so no Jordan curve theorem is presupposed; consequently the isoperimetric statement is formulated with the absolute value , which makes it independent of the curve's orientation and equal to the enclosed area for a positively oriented simple curve. The equality case asserts that the trace lies on a circle of positive radius.
"At least four vertices" is formalized as the existence of four pairwise distinct parameters in at which vanishes, which rules out the degenerate reading in which one vertex is counted several times.
Until 1827 the curvature of a surface in space was understood as a statement about how the surface sits inside : it was computed from the way the unit normal turns, that is, from the second fundamental form. Gauss's Disquisitiones generales circa superficies curvas showed that one particular combination of those extrinsic quantities — the product of the principal curvatures — can be recomputed from measurements made entirely inside the surface, using only lengths of curves drawn on it. This is the Theorema Egregium, and it is the reason the subject splits into extrinsic and intrinsic geometry; the latter is what becomes Riemannian geometry.
The reference for this mission is Manfredo P. do Carmo, Differential Geometry of Curves and Surfaces, 2nd edition (Dover, 2016), §4-3, "The Gauss Theorem and the Equations of Compatibility" (pp. 235–240). The theorem is stated on page 237 and derived from the Gauss formula, equation (5) of that section; the Mainardi–Codazzi equations (6) and (6a) on page 238 complete the list of compatibility equations.
This is the second mission of a series formalizing do Carmo's book; it shares the namespace
DoCarmoDG with the first, on the local theory of curves.
A regular parametrized patch is a map , defined and smooth on an open set with coordinates , whose partial derivatives satisfy at every point of ; the last condition says that is injective, so spans a -dimensional tangent plane at each point and
is a unit normal field along the patch.
The first fundamental form is the restriction of the ambient inner product to the tangent plane; in the parametrization it is recorded by the three functions
and . The second fundamental form is recorded by
and the Gaussian curvature is
The three second derivatives decompose in the basis ; the tangential coefficients are the Christoffel symbols of the patch, and the normal coefficients are , , , which is do Carmo's system (1) of §4-3:
Two patches over the same parameter domain are isometric when their first fundamental forms coincide, , , at every point: lengths of curves, angles and areas computed in the parameter domain then agree, and a local isometry between the two surfaces is obtained by matching parameters.
The Gaussian curvature of a regular patch is determined by its first fundamental form alone, although its definition uses the second fundamental form, i.e. the position of the surface in space.
The existence and uniqueness of the Christoffel symbols; the linear system (2) expressing them through and their first derivatives; the Gauss formula (5),
the Mainardi–Codazzi equations (6) and (6a); the closed formula for in an orthogonal parametrization (Exercise 1, p. 240); the invariance of under a change of parameters; and, as a corollary, that no neighbourhood of a point of the unit sphere is isometric to a piece of a plane (Exercise 4, p. 240).
The theorem is what makes intrinsic geometry possible: a quantity defined through the embedding turns out to be computable from the metric, so it survives every isometric deformation. Concrete consequences include the impossibility of a distortion-free map of the sphere — the reason every cartographic projection distorts lengths — and the equality of the Gaussian curvatures of the catenoid and the helicoid at corresponding points, which do Carmo notes immediately after the theorem. In the structure of the book, the Gauss formula is also the identity that makes the global Gauss–Bonnet theorem of §4-5 a statement about intrinsic data.
Mathlib has inner product spaces, iterated derivatives and the smooth manifold library, but it does not contain the first and second fundamental forms of a parametrized surface, the Christoffel symbols of a patch, the Gaussian curvature in this sense, or the compatibility equations. This mission produces that vocabulary together with machine-checked proofs of the classical identities. The mathematics is Gauss's, from 1827; what is open is the formalization.
The proof is a computation, but not a short one: one differentiates the system (1), uses , re-expands every second derivative through (1) again, and equates coefficients in the basis . Formally, the cost sits in three places: justifying the interchange of the mixed partial derivatives; establishing that the coefficient functions obtained pointwise from linear algebra are differentiable in the parameters; and carrying out the coefficient comparison in a basis that is not orthonormal, where one must use that rather than take inner products with an orthonormal frame.
The naive route to the Theorema Egregium — "solve the system (2) for the , then quote the Gauss formula" — is the right one, but the first step must actually be carried out: the system (2) determines the symbols only because each of its three blocks has determinant , and that is where the regularity hypothesis is used.
A patch is a curried map x : ℝ → ℝ → EuclideanSpace ℝ (Fin 3), so that the partial derivatives
and are ordinary one-variable derivatives, and the domain is an open set
U : Set (ℝ × ℝ); smoothness is ContDiffOn ℝ (⊤ : ℕ∞) of the uncurried map on U, matching
do Carmo's use of "differentiable" for . Regularity is stated as
on U, with the vector product defined componentwise. All quantities
(, , , , , , , ) are total functions of the parameters, taking junk
values off U; every statement restricts to points of U.
Christoffel symbols are not defined by a formula: a statement that mentions them quantifies over
functions assumed to satisfy do Carmo's decomposition (1) on U, and a separate
milestone asserts that such functions exist and are unique on U. The symmetry
is built into the notation, as in the book.
Isometry is formalized as equality of , , over a common parameter domain rather than as a map between surfaces; together with the milestone on invariance under change of parameters, this recovers do Carmo's statement that is invariant under local isometries. The formalization deliberately keeps the surface concrete (a patch, not an abstract manifold), which is what makes the compatibility equations expressible as identities between explicit derivatives.
This mission's definition file builds on the vector-product definition introduced in mission I of this series (Fundamental Theorem of the Local Theory of Curves), so mission I must be submitted first: its definitions have to be published before the definition file of this mission can compile.
There is no vacuous reading: the hypotheses are satisfiable — every regular patch, for instance a graph or a surface of revolution, satisfies them — and the conclusion compares two curvature functions pointwise.
The differential geometry of curves in is the entry point of every course and every textbook in the subject, and it is the first place where a geometric object is shown to be completely determined by a small list of numerical invariants. A space curve traced out by a particle moving at unit speed bends (curvature) and twists (torsion); the assertion that these two scalar functions determine the curve completely, up to a motion of space, is the prototype of every later "fundamental theorem" of the subject — for surfaces (Bonnet), for Riemannian metrics, and for submanifolds in general.
The reference for this mission is Manfredo P. do Carmo, Differential Geometry of Curves and Surfaces, 2nd edition (Dover, 2016), Chapter 1, Sections 1-4 and 1-5. The statement targeted here is the one printed on page 19 under the heading Fundamental Theorem of the Local Theory of Curves; the uniqueness half is proved on pages 20–22, and the existence half is deferred by do Carmo to the appendix of Chapter 4, where it is obtained from the existence and uniqueness theorem for linear systems of ordinary differential equations.
This is the first mission of a series formalizing do Carmo's book. The series shares one Lean
namespace, DoCarmoDG, so that later missions on regular surfaces, the Gauss map, and
Gauss–Bonnet build on the vocabulary fixed here.
Let be an open interval and let be a smooth map. The curve is parametrized by arc length if for every ; the parameter is then the arc length measured along the curve.
For such a curve one sets
The vector is the unit tangent and the scalar is the curvature at . Differentiating gives , so is orthogonal to . At a point where one defines the normal vector and the binormal vector
where is the vector product of (do Carmo §1-4). The triple is a positively oriented orthonormal basis, the Frenet trihedron. Since has constant length and is orthogonal to , the derivative is a multiple of , and the torsion is defined by
This is do Carmo's sign convention; many authors write for the same quantity, and the mission is committed to do Carmo's. With these conventions the Frenet formulas read
A rigid motion of is a map where is an orthogonal linear map with positive determinant and (do Carmo §1-5, Exercise 6).
Given smooth functions with :
The two halves are also stated separately as milestones, since they are proved by entirely different means: uniqueness by a Gronwall-free energy argument on the Frenet trihedron, existence by solving a linear ODE system.
The orthonormality of the Frenet trihedron, the Frenet formulas themselves, the characterization of straight lines by and of plane curves by , the closed formula , and the invariance of arc length, curvature and torsion under rigid motions.
The theorem is the model case of a classification result: a geometric object modulo a symmetry group is faithfully encoded by a complete set of local invariants. Downstream it is what licenses the standard practice of "prescribing curvature and torsion" — constructing curves with specified geometric behaviour, computing with the Frenet apparatus rather than with the curve itself, and recognizing that any identity among , and their derivatives is a genuine statement about the curve and not about its parametrization. In do Carmo's own development the local canonical form (§1-6) and the global results of §1-7 both rest on the Frenet apparatus fixed here.
Mathlib contains the analytic ingredients — the Picard–Lindelöf theorem, existence and uniqueness for linear ODE systems, orthonormal bases and the orthogonal group of a real inner product space — but it does not contain the Frenet trihedron of a space curve, the torsion of a space curve, or this theorem. What this mission produces is therefore a reusable formal vocabulary for the local theory of space curves, plus machine-checked proofs of the classical statements about it. The mathematics is completely classical and has been known since Frenet (1847) and Serret (1851); what is open here is the formalization, not the mathematics.
The uniqueness half is a short argument on paper — the function has vanishing derivative by the Frenet formulas — but formally it requires first establishing that the Frenet frame is differentiable and satisfies those formulas, which needs and the smoothness of away from its zeros, and then a connectedness argument on the interval.
The existence half cannot be done by exhibiting a formula: the curve is produced by solving the linear system for the frame , checking that the solution stays orthogonal (this is where the skew-symmetry of enters), and then integrating the first row. Recovering that the resulting curve has exactly the prescribed curvature and torsion, as computed by the definitions rather than as postulated by the ODE, is the step where most of the formal work sits.
The obvious shortcut — defining torsion by the closed formula — is not taken here: the definition is the book's, , and the closed formula is a milestone to be proved.
Curves are total functions ℝ → EuclideanSpace ℝ (Fin 3) that are assumed smooth only on the
open interval Set.Ioo a b; smoothness is ContDiffOn ℝ (⊤ : ℕ∞), matching do Carmo's use of
"differentiable" to mean . Because the interval is open, the ordinary deriv agrees
with the derivative along the interval at every interior point, and all derivatives in the
statements are plain iterated deriv. Curvature, normal, binormal and torsion are defined
exactly as above; at points where the normal vector takes the junk value , so every
statement that mentions , or carries the hypothesis explicitly.
The vector product is defined componentwise on EuclideanSpace ℝ (Fin 3), and a rigid motion is
a LinearIsometryEquiv of EuclideanSpace ℝ (Fin 3) with positive determinant followed by a
translation.
Degenerate intervals are not excluded: if the interval is empty and the statements hold vacuously, which is why the goal is not formulated as a statement about a single point but as a statement about all of — no hypothesis is vacuous for , and the existence clause is a genuine construction.
Contributions welcome: the Frenet apparatus and the ODE construction are the reusable parts, and both are prerequisites for the later missions of this series.
The spectral gap of a quantum many-body Hamiltonian is the difference between the energy of its ground state and the energy of its first excited state, in the limit of infinitely many particles. Whether a given microscopic interaction produces a gapped or a gapless system decides much of the macroscopic physics: gapped systems have exponentially decaying correlations and well-defined quantum phases, gapless systems sit at critical points and can display algebraically decaying correlations. Several long-standing questions — the Haldane conjecture for antiferromagnetic spin chains, the existence of gapped topological spin liquids, and the Yang–Mills mass gap — are instances of the question "given the interaction, is the system gapped?".
Cubitt, Pérez-García and Wolf proved that this question, posed for families of two-dimensional translationally invariant nearest-neighbour spin models, admits no algorithmic answer: the spectral gap problem is undecidable (Nature 528, 207–211 (2015); full version: Forum of Mathematics, Pi 10:e14 (2022), also arXiv:1502.04573).
Timeline of the ingredients the proof rests on: Turing's undecidability of the halting problem (1936); Berger's undecidability of the domino problem (1966) and Robinson's aperiodic tile set (Inventiones 12, 177–209 (1971)); Feynman's and Kitaev's circuit-to-Hamiltonian constructions, which turn a computation into a ground state; Gottesman and Irani's translationally invariant one-dimensional Hamiltonians encoding computation (FOCS 2009); and Bitansky–Vadhan-style quantum Turing machine engineering from Bernstein and Vazirani (SIAM J. Comput. 26, 1411–1473 (1997)). The 2015 result was later sharpened to one-dimensional chains by Bausch, Cubitt, Lucia and Pérez-García (PRX 10, 031038 (2020)).
Fix a local dimension and, for each side length , the square lattice with open boundary conditions. Each site carries a copy of , so the state space of the lattice has the standard product basis indexed by assignments of a level in to each site. A model is specified by three Hermitian matrices: an on-site term of size , and two interactions of size acting on horizontally and vertically adjacent pairs. The Hamiltonian of the finite lattice is
the same three matrices being used at every edge and every site, which is what translational invariance means here. The quantity is the local interaction strength.
Write for the eigenvalues and for the finite-size gap. The family is
These two conditions are not negations of each other; the construction guarantees that every instance falls into one of them. The ground state energy density is .
For a fixed universal machine and every , one explicit family of interactions, built from fixed integer-valued matrices , a diagonal projector , a rational that may be taken arbitrarily small, and an algebraic ,
with the rational whose binary expansion after the point is the binary expansion of reversed, satisfies: the local interaction strength is at most ; if the machine halts on input the family is gapped with gap at least ; and if it does not halt the family is gapless. Since halting is undecidable, no algorithm decides gappedness, even with the promise that exactly one of the two alternatives holds and even at fixed local dimension .
The milestone list follows the numbering of the full version: Lemma 8 and Theorem 9 (reduction of halting to ground state energy and to arbitrary low-energy properties), Corollary 7 (the same undecidability for unconstrained local dimension, with rational interactions), Proposition 53 and Corollary 54 (the diverging ground state energy and its promise version), and Theorem 5 (undecidability of the ground state energy density).
The result rules out a general algorithm — and therefore any complete general method — for deciding gappedness from the interaction matrices, however much computing power is available; the property genuinely depends on arbitrarily large system sizes. It also implies, via the standard link between undecidability and independence, that there are concrete finite-dimensional models whose gap is independent of the axioms of any consistent recursively axiomatized formal system (Corollary 4 of the source), and it transfers to other low-energy properties such as the existence of algebraically decaying ground-state correlations.
The theorem is proved; none of it is formalized. This mission produces the machine-checked version. The reusable infrastructure it forces into existence is substantial on its own: a formal model of translationally invariant lattice Hamiltonians and their thermodynamic-limit spectral behaviour, the tiling layer, and computational-history-state Hamiltonians. Each milestone is a self-contained statement that can be attacked without the others.
The obvious approach — encode a halting computation as an energy penalty — gives the ground state energy of a finite lattice, not a property of the limit; this is exactly what Lemma 8 achieves, and it is not enough, because a gap is a statement about the sequence of spectra as and is insensitive to any single lattice size. The construction must make the halting information visible at all sufficiently large sizes at once while a fixed finite local dimension carries every instance . That forces three separate difficulties: an aperiodic (Robinson) tiling to create squares of every size inside one translationally invariant model; a quantum phase-estimation Turing machine whose transition amplitudes encode in a single phase , so that the instance index does not inflate the local dimension; and a history-state Hamiltonian whose low-energy spectrum can be controlled well enough that a positive energy density in the halting case turns into a genuine spectral gap, and a vanishing one into a dense spectrum above the ground state.
The development commits to the following conventions, all of which are visible in the definition items of this mission.
Degenerate readings are excluded: a zero local dimension satisfies none of the statements, since a non-degenerate ground state requires a one-dimensional eigenspace and the gapless condition requires a non-empty spectrum; and every existential statement fixes the matrices before quantifying over all instances and all lattice sizes .
Contributions are welcome at any milestone, and also on the infrastructure the milestones need — Wang tilings and the Robinson tile set, Gottesman–Irani history-state Hamiltonians, and quantum Turing machines in the Bernstein–Vazirani sense — which are needed for Theorem 6 and Lemma 47 of the source and are not yet part of this mission's item list.
In 1935 Werner Burau attached to every braid on strands a matrix over the ring of Laurent polynomials . The resulting homomorphism is the oldest and most studied linear representation of the braid group, and whether it is faithful — whether a nontrivial braid can act as the identity matrix — became one of the best known questions about braid groups.
The history is short and sharp:
Let . The braid group is taken here in Artin's presentation: generators subject to
Let . The unreduced Burau representation is the homomorphism
i.e. the identity matrix altered only in the two rows and columns , . That these matrices satisfy the two families of braid relations — so that is well defined — is proved in the mission's definition file, together with the invertibility of each generator matrix (its inverse is the identity altered by the block ).
Equivalently, is the action of the mapping class group of the -punctured disk on the relative homology of the infinite cyclic cover determined by total winding number; this is the description used throughout the source paper.
A representation is faithful when it is injective.
The goal of the mission is the Main Theorem of the paper:
The milestones are three supporting results, each of which can be attacked independently:
Faithfulness of closes the classification of the faithful Burau representations: is faithful exactly for . It immediately gives faithfulness of the Jones representation of (Corollary 1.1 of the paper), since the Jones representation contains the reduced Burau representation as a summand. Beyond the statement itself, the kernel and the image of for remain poorly understood, and the paper's disk-sequence and parity technology is proposed by its authors as a tool for that problem.
For formalization, essentially nothing of this is machine-checked today: Mathlib has neither braid groups nor the Burau representation. This mission puts in place a checked definition of over (including well-definedness and invertibility), and then asks for the mathematics. Even the three-strand case — Magnus–Peluso, known since 1969 — is not formalized anywhere, and it is the natural first target.
The obvious approach fails in both directions. One cannot simply compute: a braid in the kernel would have to be found or excluded among infinitely many words, and no normal form for turns injectivity of into a finite check. Nor can one argue by a free-subgroup / ping-pong pattern, which is how non-faithfulness is proved for .
The source argument is topological. To a braid one associates the arc and the sequence of punctured disks cut out by its intersections with a fixed arc ; the Moody polynomial then obstructs membership in the kernel provided no cancellation occurs among its monomials. Three-strand braids always satisfy the relevant parity condition; four-strand braids do not, and the paper repairs this by pushing a point-pushing braid into and applying Moody's theorem there. A complete formalization therefore needs curves on punctured disks, minimal position, and the Birman exact sequence — none of which exist in Mathlib. Contributions that build any of that infrastructure are as welcome as contributions to the statements themselves.
Conventions fixed by the Lean development:
A complete development will additionally need: point-pushing subgroups and the Brunnian group , the Moody polynomial of a pair of arcs, and winding-number sequences. These are not yet formalized and are deliberately not part of the current statements; proposals for faithful formalizations of them are welcome in the mission discussion.
Quantizing a Yang–Mills theory by the Faddeev–Popov procedure requires a gauge condition that picks one representative from each gauge orbit. In the Landau gauge the condition is . Gribov showed in 1978 that this condition is not ideal: a gauge orbit can meet the surface more than once, so gauge-equivalent configurations — Gribov copies — are still being integrated over (V. N. Gribov, Quantization of non-Abelian gauge theories, Nucl. Phys. B139 (1978) 1). Infinitesimally, a copy of a transverse field corresponds to a zero mode of the Faddeev–Popov operator , which is Hermitian on transverse configurations.
Gribov's proposed remedy is to restrict the functional integral to the Gribov region , the set of transverse configurations at which is positive definite. The interest of is not only that it removes infinitesimal copies: the fact that it is a bounded region of field space is the geometric input of Gribov's confinement scenario, because restricting the integration to a bounded region deforms the gluon propagator in the infrared and produces a mass scale. Whether the restriction to is the physically correct prescription is still debated; the geometric properties of themselves are not — they are consequences of the algebraic structure of , and they are what this mission formalizes.
Timeline of the properties at issue, as recorded in §2.2.1 (pp. 188–189) of the review by N. Vandersickel and D. Zwanziger, The Gribov problem and QCD dynamics, Phys. Rep. 520 (2012) 175–251 (doi:10.1016/j.physrep.2012.07.003):
Fix a real vector space of gauge-field configurations (in the physical situation, the transverse fields ) and a finite index set on which the Faddeev–Popov operator acts (colour index times a finite basis of fluctuation modes ). The formalization works with the algebraic structure that the Faddeev–Popov operator has, and nothing else:
where
The Gribov region is
This is Eq. (2.52) of the review, with positivity as in Eq. (2.54). The boundary is the first Gribov horizon, where the lowest non-trivial eigenvalue of vanishes.
The last two clauses are stated under the assumption that is injective, i.e. that distinct configurations give distinct field-dependent parts; without it contains the whole kernel of as a linear subspace and no boundedness statement can hold.
These are Eq. (2.53) and Eq. (2.58) of the review; they are the two ingredients from which convexity and directional boundedness follow.
What the result gives: is the region to which Gribov's improved gauge fixing restricts the functional integral, and every subsequent construction in this line of work — the no-pole condition, the horizon function and the local Gribov–Zwanziger action — presupposes that the restriction is to a bounded convex region containing the perturbative point . Convexity is what makes the horizon condition a single well-posed constraint; boundedness in every direction is the property from which the infrared suppression of the gluon propagator, and hence Gribov's mass scale, is read off. Without boundedness there is no geometric mechanism for a mass gap in this scenario.
Status honesty: these statements are proved mathematics, not open problems; the arguments in §2.2.1 of the review are short. What is missing is a machine-checked account. No formalization of the Gribov region in Lean is known to the drafter of this proposal; the platform's existing Gribov material concerns Singer's topological obstruction to continuous gauge fixing, which is a different theorem about a different object.
The statements are elementary once the correct hypotheses are isolated, and the mission is calibrated accordingly: it is a faithfulness exercise rather than a depth exercise. The two places where a naive attempt fails are worth naming. First, directional boundedness does not follow from positivity alone: it needs the tracelessness of , which is what forces a direction with ; a positive semidefinite perturbation would give a region unbounded along that ray. Second, "bounded in every direction" does not imply "bounded" for a general set, and the implication used here rests on convexity together with injectivity of — the argument goes through a limit of rescaled configurations and a closure of the positivity condition, not through a uniform bound extracted directly from the ray statement.
The mission commits to a finite-dimensional linear-algebra model of the Faddeev–Popov operator, packaged as a structure carrying: the matrix together with a proof that it is positive definite; the linear map together with proofs that each is symmetric and traceless. Configurations live in an arbitrary real vector space , which carries a norm and finite-dimensionality only in the two statements where boundedness is asserted. Positive definiteness is Mathlib's notion for real matrices, which includes symmetry; the region is the set of configurations where it holds strictly, so is the open region and the horizon is not part of it.
This is a model, not the field-theoretic object: it replaces the operator acting on transverse fields by its finite-dimensional algebraic shadow, and the reviewer should audit it as such. The properties targeted here are exactly those whose proofs in §2.2.1 use only linearity in , symmetry, tracelessness, and positivity of ; results that genuinely need the infinite-dimensional setting — that every gauge orbit passes inside , and that still contains copies on its boundary — are deliberately out of scope, since they cannot be stated in this model.
The model is not vacuous: an instance exists already for , , and , with injective, so none of the statements is satisfied vacuously. Nor is any target trivially true: is a proper nonempty subset of in that instance.
Infrastructure needed: Mathlib's positive-definiteness API for matrices, the spectral theorem for real symmetric matrices (for the traceless lemma), and basic convexity and boundedness in finite-dimensional normed spaces. The traceless lemma — a nonzero symmetric traceless matrix has a direction of negative quadratic form — is reusable well beyond this mission. Contributions extending the model towards the infinite-dimensional setting, or supplying the explicit ellipsoidal bound of Dell'Antonio–Zwanziger in place of plain boundedness, are welcome.
The Riemann hypothesis asserts that all nontrivial zeros of the Riemann zeta function lie on the critical line. A classical way to measure how far the hypothesis is from failing runs through a one-parameter deformation of the Riemann function by the backward heat flow. De Bruijn (1950) introduced a family of entire functions , , with essentially the function, and showed that has only real zeros for . Newman (1976) proved that there is a finite constant , now called the de Bruijn–Newman constant, such that has only real zeros precisely when . The Riemann hypothesis is exactly the statement , and Newman conjectured the complementary bound — in his phrase, that if the Riemann hypothesis is true, then it is only barely so.
Timeline of lower bounds on , all obtained before 2018 by exhibiting Lehmer pairs, that is, pairs of adjacent zeros of that are unusually close together: (Newman 1976), (Csordas–Norfolk–Varga 1988), (te Riele 1991), (Norfolk–Ruttan–Varga 1992), (Csordas–Ruttan–Varga 1991), (Csordas–Smith–Varga 1994), (Csordas–Odlyzko–Smith–Varga 1993), (Odlyzko 2000), (Saouter–Gourdon–Demichel 2011). Rodgers and Tao closed the gap in 2020 by proving . In the other direction, de Bruijn's bound was sharpened to by Ki–Kim–Lee (2009) and to by the Polymath 15 project (2019).
For a real number put
a function that decays super-exponentially as and satisfies . For each define the entire function
Each is even and satisfies ; the function is , so the Riemann hypothesis says exactly that every zero of is real. Write
By Pólya and Newman, is the ray with .
When the zeros of are real, simple, symmetric about the origin and avoid the origin, so they can be listed as , indexed by the nonzero integers, with and . The classical locations are defined for by with
extended by ; they are the positions the zeros would occupy if the Riemann–von Mangoldt counting formula were exact. Throughout, .
The goal is stated in both forms simultaneously, so that it does not depend on any convention for the infimum of a set that might be empty or unbounded below.
The milestone list follows the architecture of Rodgers–Tao, which is a proof by contradiction: every milestone is stated under the standing hypothesis of that paper, in the time ranges the paper uses (, then , then ). In order: an upper bound for near the real axis (Lemma 4); Riemann–von Mangoldt type counting formulae for the zeros of (Theorem 9); the resulting macroscopic description of the zeros (Corollary 10); the equations of motion (Theorem 11); a quantitative lower bound on gaps between zeros (Proposition 13); a bound on the time-integrated renormalized energy (Theorem 17); and a bound on that energy at time (Proposition 26). The last of these says that at time zero the zeros are, on average, locally in the equilibrium configuration of an arithmetic progression, which contradicts known results on the local distribution of zeros of .
settles Newman's conjecture, and together with the Riemann hypothesis it would force . Unconditionally, it says that the zeros of are not in local equilibrium: infinitely often, gaps between consecutive zeros deviate from the mean spacing, which is what makes the pair correlation phenomenology of Montgomery and of Conrey–Ghosh–Goldston–Gonek–Heath-Brown incompatible with . Any proof of the Riemann hypothesis must therefore be compatible with the hypothesis being tight in this sense.
The theorem has a complete published proof (Rodgers–Tao, Forum of Mathematics, Pi, 2020); it is not an open problem. What is missing is a machine-checked proof. To the extent the material has been formalized at all, the underlying objects — the function, the heat flow , the counting function for zeros, the zero dynamics, the renormalized energies — are not available in Mathlib, so the mission produces reusable analytic infrastructure: bounds for a Fourier–Laplace type integral by the saddle point method, a Riemann–von Mangoldt counting argument via the argument principle, and a gradient-flow monotonicity framework for an infinite particle system with logarithmic interaction.
The obvious route to is the one used for every previous lower bound: exhibit Lehmer pairs of ever higher quality, since if were very negative the zeros of would repel each other and unusually close pairs of zeta zeros could not exist. Producing an infinite sequence of Lehmer pairs of arbitrarily high quality is possible under the GUE hypothesis, but the known unconditional upper bounds for small gaps between zeta zeros are too weak, even assuming the Riemann hypothesis. The proof instead upgrades repulsion to relaxation to local equilibrium: it must control the zeros of uniformly for at length scales as fine as , with only the weaker counting formulae available for negative (an error term rather than ), and must make sense of a Hamiltonian and an energy that are given by divergent series, which requires truncation, renormalization, and careful control of all the resulting boundary terms.
The Lean development commits to the following conventions. is a tsum over the positive integers and is the Bochner integral over of ; no convergence or entireness statement is built into the definition. is sInf of the set of admissible times, and the goal theorem also states the quantifier form "every admissible is nonnegative", so it cannot be satisfied by a junk value of the infimum. The zero families and the classical locations are not defined by choice functions: they enter the milestones as universally quantified functions subject to explicit predicates saying exactly which sequences they are, so a milestone asserts something about every valid enumeration. Asymptotic notation is unfolded: becomes an explicit existential constant, an explicit – statement, and a principal value sum a limit of symmetric partial sums. Where a statement asserts the value of a time integral, absolute integrability is part of the conclusion, so the statement cannot be satisfied by the convention that a non-integrable function has integral zero.
One degeneracy is inherent to the source and is stated here explicitly: since the paper argues by contradiction, each milestone carries the hypothesis (directly, or through a time range such as ). Once the goal theorem is proved, those hypotheses are unsatisfiable and the milestones become vacuously true. They are the intended attack path on the goal, not independent targets, and a solver who derives one of them from the goal theorem contributes nothing.
Contributions welcome: the analytic estimates for (Lemma 4) and the counting formulae (Theorem 9) are independent of the dynamical part and are the natural entry points; Mathlib-level infrastructure on the argument principle, the saddle point method, and Stirling asymptotics for in vertical strips is reusable well beyond this mission.
When money is off the table and the Gibbard–Satterthwaite theorem (Mission III of this series) blocks general strategyproof choice, restricted preference domains reopen the door. The two great examples both come from allocation: Shapley–Scarf's housing market (1974), where Gale's Top Trading Cycle algorithm finds the unique core allocation and Roth (1982) showed the mechanism is strategy-proof; and the Gale–Shapley marriage market (1962), where deferred acceptance produces a stable matching, the men-optimal one, which Dubins–Freedman (1981) and Roth (1982) showed cannot be manipulated by any man. This machinery runs the US medical residency match and school choice systems worldwide, and the 2012 Nobel memorial prize to Roth and Shapley cites exactly the results of this mission. Chapter 10 (Schummer–Vohra, "Mechanism Design without Money") of Nisan–Roughgarden–Tardos–Vazirani (eds.), Algorithmic Game Theory (Cambridge, 2007) is the source text; its single-peaked §10.2 is left to a possible later mission, since it needs its own preference-domain machinery.
Marriage market (§10.4): finite sets of men and of women, each agent holding a strict preference ordering over the opposite side (the preference-profile vocabulary of Mission III; reads " strictly prefers to "). Following the book's dummy-partner convention, and a matching is a bijection . A pair blocks if each prefers the other to their assigned partner; is stable if no pair blocks it. A stable is male-optimal if every man weakly prefers it to every stable alternative. A coalition dominates if it can rematch within itself with every member strictly better off; the core is the set of undominated matchings.
Housing market (§10.3): a finite set of agents, agent owning house , each with a strict preference over all houses; an allocation is a permutation of . A coalition blocks an allocation if it can redistribute the houses its members own so that all are weakly and someone strictly better off.
Any mechanism selecting the male-optimal stable matching is strategy-proof for the men: no man can misreport his ordering and obtain a wife he truly prefers.
Every marriage market has a stable matching.
Some stable matching is weakly best for every man simultaneously. This man-by-man form is Gale–Shapley's optimal assignment (1962, Theorem 2); the book's Theorem 10.11 phrases male-optimality as the absence of a stable alternative making every man weakly and some man strictly better off, which is equivalent for finite strict markets — the equivalence being a (short) theorem, the attribution follows Gale–Shapley.
A matching is stable iff it is in the core of the matching game.
The core of the housing market is a single allocation, and the mechanism selecting it is strategy-proof.
These are the foundational theorems of market design — the branch of mechanism design with the strongest record of deployed systems — and none of them exists in Lean. The mission also settles a methodological point for the series: algorithm-defined objects (deferred acceptance, top trading cycles) enter through the properties that characterize their outputs — male-optimality, core membership — so the theorems are statements about all mechanisms with the given property, and any construction of the algorithm proves the existence milestones. The matching vocabulary (bijections as matchings, blocking, stability, domination) is reusable for the college-admissions and roommates variants beyond this mission.
Existence (10.10) is the real formalization work: whether by formalizing deferred acceptance and its termination or by another route (e.g. Adachi's fixed-point formulation, which the book sketches as Theorem 10.14 via Tarski), the solver must build the proposal machinery. Male-optimality (10.11) rides on the same construction with the "no man is ever rejected by an achievable wife" invariant. The core equivalence (10.12) is deliberately light — a transposition embeds a blocking pair as a two-agent coalition. Housing uniqueness (10.6) needs the cycle-peeling induction of TTC. The two strategyproofness results are the subtle ones: both known proof routes (Dubins–Freedman's combinatorial argument, or Roth's via the blocking lemma) require careful bookkeeping of which coalitions can improve under a misreport, and the mechanism is pinned only by its defining property, so proofs must use optimality/core facts rather than algorithm internals.
Preferences are strict total orders as in Mission III (IsPrefProfile), oriented "first argument preferred". Matchings are Equivs; the book's convention enters the existence statements as the hypothesis Nonempty (M ≃ W) and nothing else about cardinalities is assumed. Domination and house-blocking quantify a rematching Equiv together with the improving coalition, coalitions being sets closed under the rematching — single-agent and pair coalitions are special cases, so no separate pair-blocking clause is needed in the core theorems. Mechanisms in the strategyproofness results are arbitrary functions constrained only by their defining property (male-optimal selection; core selection), quantified before the misreport — nothing may be chosen with hindsight. Both sides keep finiteness only where used: the core equivalence (10.12) holds for arbitrary types and carries no Fintype.
Mission III of this series ends at an impossibility: without money, incentive compatibility over three or more alternatives means dictatorship. This mission formalizes the classical escape route — quasilinear utilities and payments — and the exact price of it. Vickrey (1961) discovered that a second-price auction makes truth-telling dominant; Clarke (1971) and Groves (1973) generalized the idea to arbitrary social choice: welfare-maximizing rules can always be made truthful by the right payments. The converse program — which choice rules are implementable at all — runs through Rochet (1987) and Myerson (1981) to Saks–Yu (2005): weak monotonicity characterizes implementability on convex domains, and on single-parameter domains the characterization is complete and elementary — monotone rules with critical-value payments. Chapter 9, §§9.3 and 9.5 of Nisan–Roughgarden–Tardos–Vazirani (eds.), Algorithmic Game Theory (Cambridge, 2007), written by Nisan, is the source text.
A set of alternatives and a finite set of players. Player holds a private valuation from a publicly known domain ; utilities are quasilinear: choosing and charging gives utility . A (direct revelation) mechanism is a social choice function from valuation profiles to together with payment functions (Definition 9.14). The mechanism is incentive compatible if no unilateral misreport from the domain ever beats the truth (Definition 9.15).
A VCG mechanism (Definition 9.16) has maximizing social welfare and payments of the Groves form ; the Clarke pivot rule takes . A rule is weakly monotone (Definition 9.28) if a unilateral change of valuation that moves the outcome from to satisfies . A single-parameter domain (Definition 9.33) is given by a win set per player and bids : the valuation is on and elsewhere.
A normalized mechanism (losers pay 0) on a single-parameter domain is incentive compatible iff the rule is monotone and every winning bid pays the critical value — the threshold below which the bid loses.
Every VCG mechanism is incentive compatible.
With Clarke pivot payments, a welfare-maximizing rule makes no positive transfers, and is individually rational when valuations are nonnegative.
Necessity: incentive compatibility forces WMON, on any domain. Sufficiency: on convex domains, WMON rules admit implementing payments (Saks–Yu).
These are the working theorems of every later mechanism-design mission: the approximation mechanisms of Chapter 12, the profit-maximization results of Chapter 13, and the sponsored-search analysis of Chapter 28 all argue through Theorem 9.36's monotonicity-plus-critical-value normal form, and VCG is the benchmark they approximate. Formalizing the cluster produces the platform's quasilinear-mechanism vocabulary — domains, truthfulness, Groves payments, weak monotonicity, single-parameter settings — on top of the social-choice layer of Mission III.
The capstone and Theorem 9.17 are textbook results with complete proofs in the source; the Saks–Yu half of Theorem 9.29 is stated but not proved in the book ("quite involved"), so that milestone carries a genuinely hard formalization with a published paper proof. None have prior Lean formalizations.
Theorem 9.17 is a three-line inequality chase once the Groves form is unfolded — a deliberate warm-up. Lemma 9.20 adds the attained maximum over a finite alternative set. The necessity half of 9.29 is a two-application argument; the sufficiency half is the hard point of the mission: the known proofs walk two-cycle inequalities into a path-integral construction of payments on a convex domain, and nothing of the kind exists in Mathlib. For the capstone, the delicate part is the critical value: the book defines it as a supremum that "is undefined" when the player always wins, and the honest formal rendering — a constant payment c that is a least upper bound of the losing bids whenever losing bids exist — makes the case split explicit; the equivalence proof must thread monotonicity, the threshold structure of the winning set, and normalization through both directions.
Valuations are functions A → ℝ; domains are sets V i : Set (A → ℝ); mechanisms are total functions with every property quantified only over profiles from the domain, so behavior on invalid inputs carries no content. The Groves term hᵢ is a function of the full profile constrained to be invariant under changes of coordinate i — the standard rendering of "depends only on ". The Clarke payment uses a Finset.sup' over a finite nonempty A, so no junk supremum arises. In the single-parameter setting the valuation induced by a bid is Set.indicator, bids live in Set.Icc t0 t1 with t0 ≤ t1, and the critical value is characterized by IsLUB guarded by nonemptiness of the losing set — the book's "undefined" caveat made precise without a junk sSup. Weak monotonicity's sufficiency half carries Convex ℝ (V i) and finite A (the Saks–Yu setting); the necessity half deliberately carries no hypotheses beyond incentive compatibility itself.
Galois theory attaches to every finite Galois extension a finite group , the group of field automorphisms of fixing pointwise, and the fundamental theorem of Galois theory turns the subfield structure of into the subgroup structure of that group. The inverse Galois problem asks whether this correspondence is surjective over the rationals: given an arbitrary finite group , is there a Galois extension with ? The question was posed in the early nineteenth century and is unsolved.
What makes it a live research question rather than a curiosity is that the known positive results come from genuinely different sources, and none of them covers all finite groups.
Fix a field and a group . A Galois realization of over is a field equipped with a -algebra structure such that the extension is Galois — normal and separable — together with a group isomorphism
where denotes the group of -algebra automorphisms of under composition. The group is realizable over , written IsRealizable K G, when at least one Galois realization of over exists. No finiteness of is imposed in the definition; it is automatic once is finite, because an infinite Galois extension has infinite automorphism group.
Two base fields beyond appear throughout. denotes the field of rational functions in one variable over , written RatFunc K; and for the statement that a group is realizable over some number field, the base field ranges over the intermediate fields of .
The goal fixes no degree, no polynomial and no construction: it asserts only the shape of the truth, so no later refinement of the known constructions can invalidate it.
The last milestone is the Hilbert-irreducibility descent step; together with the geometric milestones it makes precise which half of the classical programme is missing.
The result itself would settle a two-century-old question and, with it, the surjectivity of the Galois correspondence over : every abstract finite group would be known to arise from an explicit arithmetic object, a polynomial with rational coefficients. Its absence is felt in practice — constructing a single new Galois group over is publishable work, as the recent additions of the degree- group (van Bommel–Costa–Elkies–Keller–Schiavone–Voight, 2024) and of the Mathieu group show.
Formalizing it produces something available today independently of the goal: a machine-checked library of the known realizability results. Mathlib has the fundamental theorem of Galois theory, cyclotomic extensions, the Kronecker–Weber theorem, solvability of groups and symmetric/alternating group theory, but it does not have a predicate for " is a Galois group over ", nor any of the milestones above. Every milestone here is a proved theorem of classical number theory and an unformalized one; the cyclic and abelian cases are within reach of current Mathlib, while the Shafarevich and Riemann-existence milestones are substantial formalization projects in their own right.
The obvious strategy fails at a well-understood point. Over the problem is solved: by the Riemann existence theorem every finite group occurs as the deck-transformation group of a branched cover of the projective line. Hilbert's irreducibility theorem then descends realizability from to . What is missing is the step in between: producing the cover over rather than over , i.e. showing that the geometric solution can be chosen with rational field of constants. The rigidity method makes this work for many groups, but there is no known argument covering all of them; an approach that only produces realizability over some number field is not enough, and that weaker statement is included as a milestone precisely to mark the line.
A second, purely formal difficulty: the milestones are classical but their published proofs are long. Shafarevich's theorem rests on a delicate analysis of embedding problems, and the Riemann existence theorem is analytic input that Mathlib does not currently have in the required form.
The mission fixes one definition file, published first, carrying the structure GaloisRealization and the one-field class IsRealizable. Conventions it commits to:
IsGalois K L is Mathlib's Galois condition (normal and separable); finiteness of the extension is not assumed.Equiv.Perm S for a finite type , and is alternatingGroup (Fin n); degenerate small cases are included rather than excluded.Group.IsSolvable.The statements cannot be satisfied vacuously: IsRealizable K G asserts the existence of data, so a solver must exhibit an extension; and the hypotheses of the milestones (cyclic, abelian, solvable, or none at all) are all satisfiable, so no milestone is empty. The one conditional milestone, Hilbert descent, is stated with realizability over as an explicit hypothesis.
Infrastructure a complete development needs, most of it reusable well beyond this mission: transport of a Galois realization along an isomorphism of groups and along an isomorphism of base fields; the fixed-field construction and the fundamental theorem in the form ""; Galois groups of cyclotomic fields; Dirichlet's theorem on primes in arithmetic progressions (already in Mathlib); Hilbert's irreducibility theorem (not in Mathlib). Contributions of any of these as reusable platform definitions or lemmas are welcome, as are decompositions of the harder milestones into sketches.
Chapter 6 of Walter Rudin's Principles of Mathematical Analysis (3rd edition, McGraw-Hill, 1976) constructs the Riemann–Stieltjes integral : the Riemann integral with the increments of the variable replaced by the increments of a monotonically increasing integrator . Taking recovers the ordinary Riemann integral; taking a step function turns integrals into sums, so series and integrals become special cases of one construction. This is the reason Rudin develops the theory in this generality: it unifies Chapter 3's series with the integral, and it is the natural setting for the Fourier coefficients of Chapter 8.
The chapter's capstone is the fundamental theorem of calculus (Theorem 6.21): an integrable function which is the derivative of some integrates to .
This mission is the sixth in a series formalizing Rudin Chapters 1–11; it uses the uniform continuity of Mission IV and the mean value theorem of Mission V.
A partition of is a finite set of points , with increments for a monotonically increasing . For a bounded real put , , and
The upper and lower integrals are and ; is integrable with respect to , written , when they agree, and the common value is . refines when every division point of is one of . Writing for with gives the Riemann integral .
The fundamental theorem is what makes the integral computable: it reduces integration to antidifferentiation and so links Chapters 5 and 6. Theorem 6.20 is its companion — it says the integral of a continuous function is an antiderivative — and together they show the two operations are mutually inverse to the extent that the hypotheses allow. Theorem 6.17 explains when a Stieltjes integral collapses to a Riemann integral with the density , and it is the computational tool for integrators that are differentiable; the step-function case at the other extreme (Rudin's 6.15–6.16) is what turns sums into integrals.
Mathlib has no Riemann–Stieltjes integral: it has the Bochner integral, the interval integral, and a Lebesgue–Stieltjes measure, but the upper-and-lower-sum construction of Chapter 6 is absent. This mission therefore builds the object from Rudin's definitions and develops its basic theory; that development is reusable beyond this mission — Chapter 7's interchange theorem (7.16) and Chapter 8's Fourier coefficients are stated with respect to it.
Two obstacles are specific to formalizing this chapter. First, the upper and lower integrals are an infimum and a supremum over the set of all partitions, which is not a lattice-friendly index; every comparison between partitions goes through the common refinement, and Theorem 6.4 is the workhorse that makes such comparisons possible. Second, the fundamental theorem is proved by choosing a partition on which and applying the mean value theorem on each subinterval, so the proof requires selecting an intermediate point per subinterval — a finite choice that is easy on paper and must be organized explicitly in Lean.
The integrator is only assumed monotone, so it may be discontinuous, and the theory must not assume otherwise: Theorem 6.9 needs continuity of precisely because it is not available in general.
Conventions fixed by this mission:
[a, b] is Rudin.Partition a b: the number n of subintervals together with
a monotone placement function x with x 0 = a and x n = b. Rudin allows
, and so does this structure.Rudin.upperSum, Rudin.lowerSum, Rudin.upperIntegral, Rudin.lowerIntegral,
Rudin.RSIntegrable, Rudin.RSIntegral follow Definitions 6.1–6.2 literally, with sSup and
sInf over the images .sSup/sInf on ℝ return 0 on unbounded sets, every statement carries Rudin's
boundedness hypothesis for explicitly; likewise monotonicity of is assumed as
MonotoneOn α (Set.Icc a b) rather than built into a type.Rudin.RiemannIntegrable and Rudin.RiemannIntegral are the case , in
which the goal theorem and Theorems 6.20–6.22 are stated, matching Rudin.HasDerivAt, so F' = f is stated pointwise on [a, b] with the value f x
supplied, as in Rudin's hypothesis.The goal is not vacuous, and not a restatement of a library lemma: the integral in it is the one defined in this mission, so a solution must connect the upper/lower sum construction to differentiation rather than quoting Mathlib's interval integral.
Erdős asked, repeatedly and with a rising price tag, for an asymptotic formula for the largest subset of that contains no arithmetic progression of a given length. He offered 1000 dollars for it in [Er97c] and 10000 dollars in [Er81, p.4], where he called the question "probably enormously difficult"; elsewhere he described it as "probably unattackable at present". Most of modern additive combinatorics — the density increment method, the triangle removal lemma, Gowers uniformity norms, the arithmetic regularity lemma — grew out of attempts on this single question, and the answer is still unknown, even in the first non-trivial case .
Timeline.
Every upper bound in this list is still astronomically far from Behrend's lower bound, and no candidate asymptotic formula has been proposed for any .
Fix an integer . A non-trivial -term arithmetic progression is a list of natural numbers with common difference ; the requirement is what "non-trivial" means, and it forces the terms to be distinct. A finite set is -AP-free if it contains no such progression. Write
The mission takes its formal definition of verbatim from the formal-conjectures entry for this problem, so that the goal below is literally the statement recorded there. In that development a set is called free of progressions of length when every subset of it that is an arithmetic progression of length forces . Progressions of length and count as trivial, so under that convention every set is free of them and ; the interesting range begins at . Every statement in this mission that depends on the convention carries an explicit hypothesis on .
On that range, is non-decreasing in both and , satisfies , and hence, by Fekete's subadditivity lemma, converges. Szemerédi's theorem is the statement that the limit is ; the whole difficulty of this mission lies in how fast it goes to .
This is erdos_142.variants.lower of the formal-conjectures file for Erdős 142, reproduced binder for binder, over that file's own definition of .
The headline theorem in that file, erdos_142, states with the comparison function left as an answer(sorry) placeholder, and the same is true of its variants.upper and variants.three. Those are not closed propositions and cannot serve as a mission goal: the literal request of Erdős Problem #142 — "prove an asymptotic formula for " — has no known right-hand side for any , which is exactly why the file leaves a hole there. variants.lower is the one formalizable target in the file, and it is also the strongest precisely-stated form the problem page attaches to #142: Erdős offered 5000 dollars for (essentially) exactly it, as recorded under Erdős Problem #3. It is known for — it follows from Bloom–Sisask 2020, and a fortiori from Kelley–Meka 2023 — trivial for , where , and open for every . It fixes no constants, so no future improvement can invalidate it.
Erdős remarked in [Er80, p.92] that even this separation between consecutive progression lengths is not known. Here [Er80] is the erdosproblems.com bibliography key for Erdős's 1980 paper; it is a citation, not a pointer to Erdős Problem #80, which is an unrelated question about books in graphs. This statement has no counterpart in formal-conjectures: the file for #142 contains only the , and variants above, and the only two files in that repository that mention at all are the ones for #142 and #139.
Proving for all yields, by a standard summation argument, Erdős's conjecture that every with contains arbitrarily long arithmetic progressions — the 5000-dollar Erdős Problem #3, of which the Green–Tao theorem on primes is the best-known special case. Below that threshold, quantitative bounds on control the density at which progressions must appear in any concrete set, and are the input to results on progressions in the primes, in sumsets, and in sparse random subsets of the integers.
Formalization status is uneven, and this mission is designed around that gap. Mathlib already contains the theory in a usable form: the predicate ThreeAPFree, the Roth number rothNumberNat, its subadditivity, and a complete formalization of Behrend's construction (Behrend.roth_lower_bound). Mathlib does not contain Roth's theorem, Szemerédi's theorem, or any of the modern upper bounds; to the best of current knowledge none of Roth, Szemerédi, Gowers, Green–Tao, Kelley–Meka or Leng–Sah–Sawhney has a machine-checked proof anywhere. The formal-conjectures entry states the problem but proves nothing: every declaration in it is a sorry. Two of this mission's targets are taken from that repository — the goal from its file for #142, and the Szemerédi milestone from its file for #139, which uses the same ; those are the only two files there that mention . The milestones therefore split cleanly: the first six are reachable now on top of Mathlib, and the last five are open formalization projects of independent value.
Every known upper bound for runs a density increment: if of density has no -term progression, find a long subprogression on which has density , and iterate. The bound this produces is governed entirely by two quantities — how large the increment is, and how much of the interval survives one step. For the increment is extracted from an inverse theorem for the Gowers -norm, and the best available correlation bounds there are quasipolynomial in ; iterating a quasipolynomial increment cannot do better than , which is nowhere near . Reaching requires an increment with polynomial dependence on together with a subprogression of polynomial length, and that combination is currently available only for , through the sifting and almost-periodicity machinery of Kelley–Meka. No soft or averaging argument can substitute: Behrend's construction shows the truth at is , so the answer is not a power of and cannot be produced by any argument whose output has that shape.
The mission's definition file Erdos142Basic carries two layers, and every statement in the mission is written against them.
The source definitions, ported verbatim. IsAPOfLengthWith, IsAPOfLength, IsAPOfLengthFree and r are the declarations of the formal-conjectures entry, transcribed unchanged into the mission's namespace: a set is an arithmetic progression of length with first term and difference when it has exactly elements and equals ; it is free of length- progressions when every progression of length inside it forces ; and is the supremum of over subsets free of length- progressions. The ground set is Finset.Icc 1 N, and the supremum is sSup over ; the file proves the two facts that make it a genuine maximum (le_r and r_le).
An elementary handle. HasAP k A is ∃ a d, 0 < d ∧ ∀ i < k, a + i * d ∈ A, and APFree k A its negation. This form carries no cardinality side condition in and is what a solver actually wants to induct on. The first milestone is exactly the bridge between the two layers.
Two consequences of the source convention are worth stating plainly, because the prose is silent about them. Length- and length- progressions are trivial, so every set is free of them and ; monotonicity of in therefore holds only from onward, and the corresponding milestone carries that hypothesis. Asymptotic statements use Asymptotics.IsLittleO and Filter.atTop over with real-valued casts, and real division is Lean's, so (N : ℝ) / Real.log N is at ; this is invisible to atTop.
A trivializing formalization is ruled out by construction: one milestone asserts rothNumberNat N, pinning this development against Mathlib's independently written definition of the Roth number, so a vacuous or mis-quantified notion of progression-freeness cannot survive. That milestone, the bridge milestone above it, and the monotonicity milestone have all been checked to be provable before this proposal was drafted.
A full development needs: discrete Fourier analysis on , Bohr sets and their regularity, the arithmetic regularity lemma, Gowers uniformity norms and the inverse theorem for them, and — for the lower bounds — sphere-counting in high-dimensional boxes (already in Mathlib via Behrend). All of this is reusable well beyond this mission. Contributions of any kind are welcome, including partial results: quantitative bounds weaker than the cited ones, the case of a general- milestone, and reusable Fourier-analytic infrastructure are all valuable even when they do not close a milestone.
FormalConjectures/ErdosProblems/142.lean — the source of the goal statement and of the definition of . https://github.com/google-deepmind/formal-conjectures/blob/main/FormalConjectures/ErdosProblems/142.leanAn equation for a magma constrains a binary operation without assuming that it is associative, commutative, or has an identity. Determining which equations force other equations separates the consequences of a single law from familiar properties that require additional assumptions. Restricting the underlying set to be finite can change the answer: a structural argument may depend on the fact that a surjective self-map of a finite set is injective.
The Equational Theories Project studies these implications systematically. Its December 2025 paper reports the finite implication from E677 to E255 as unresolved, while reporting a counterexample to the implication when infinite magmas are allowed. The paper also tentatively conjectures that a finite counterexample exists. This mission makes the affirmative implication its formal target and also accepts a rigorous refutation of the complete finite statement.
This mission treats the universal target as open. Supporting structural facts and conditional reductions are separately identified, so that progress on one does not assert completion of the target.
A magma here is a type with a total binary operation . Parentheses specify the order of evaluation throughout; no reassociation is permitted. The condition E677 means
The condition E255 means
These are the two laws used in Chapter 13 of the project blueprint. For a fixed element , the left multiplication map is . A fixer for is an element satisfying . This definition concerns one element ; it does not require to act as an identity on every element.
The supporting targets expose the relevant distinction between a constraint on a possible fixer and the existence of a fixer. For every finite satisfying E677, the first supporting statement is
The second supporting statement specifies any fixer:
The third supporting statement is the backward recurrence
These supporting statements come from ETP blueprint Lemma 13.1(i)–(iii); local direct proof files accompany their statements. The following universal fixer-existence assertion is retained as an explicit equivalent reformulation:
The mission goal is
For finite E677 magmas, fixer existence is equivalent to E255: E255 supplies the fixer , and Lemma 13.1(ii) converts any fixer into E255. Thus it is not presented as a strictly weaker milestone.
The active open milestone is an orbit-local producer statement. For a fixed , if two elements in the forward orbit have equal right products by , they must be equal unless has a fixer. This isolates a genuine structural step without asserting a fixer for every element. None of the displayed statements restricts the cardinality to a tested range.
A resolution determines whether this particular law gains E255 as a consequence upon restriction to finite carriers. An affirmative proof must cover every finite cardinality, every operation on each carrier, and every assignment of the universally quantified elements. A finite counterexample must supply an operation that satisfies every instance of E677 while failing E255 at some element.
The formal package provides small, reusable statements of the two laws, the left multiplication property, and the fixer constraint. Keeping these statements separate allows their precise hypotheses and conclusions to be checked individually. In particular, the second supporting result says what a fixer must be when one exists; the fixer-existence formulation records the additional mathematical content needed to ensure existence.
The left multiplication conclusion concerns maps with the left input fixed. The fixer-existence formulation instead asks about the image of the map , with its right input fixed. No assumption in the formal goal makes these two maps interchangeable. Bijectivity of every left multiplication map alone does not state that a fixer exists.
Likewise, checking a collection of finite operation tables does not quantify over arbitrary finite cardinalities. Such computation does not discharge the goal submitted here. Any proof must justify every use of finiteness and retain the displayed parenthesization of the laws.
The representation uses an arbitrary universe-polymorphic type, an explicit binary operation, and a Fintype instance for finite targets. Passing the operation explicitly avoids importing a separate magma package or imposing algebraic typeclass laws. The predicates E677 and E255 themselves do not assume finiteness; each theorem states its own finite-carrier hypothesis.
Empty carriers are included. Both laws hold vacuously on them; the pointwise fixer statement is also vacuous because there is no element . Consequently an empty carrier cannot refute the main goal. Nonempty carriers of every finite size are included without further assumptions. There is no associativity, commutativity, idempotence, identity element, or cancellation hypothesis hidden in the representation.
Infinite-horizon dynamic programming is the mathematical core of Markov decision processes and reinforcement learning: Bellman equations, value iteration, policy iteration, and their guarantees. Chapter 7 of Bertsekas, Dynamic Programming and Optimal Control, Vol. I (3rd ed., 2005) develops the finite-state theory in its cleanest generality — stochastic shortest path (SSP) problems first (Prop. 7.2.1–7.2.2), with discounted problems (Prop. 7.3.1) and average-cost problems (Prop. 7.4.1–7.4.2) derived from the SSP analysis. These propositions are cited throughout the MDP/RL literature as the base case of the theory; none of them exists in Mathlib.
States plus an implicit cost-free absorbing termination state ; finite nonempty control sets ; costs ; sub-stochastic transitions , , the deficit being the termination probability (BertsekasSSPModel). Operators
(BertsekasSSPPolicyOp, BertsekasSSPBellmanOp), -stage costs by backward recursion with policy shift (BertsekasSSPNCost), and the survival mass (BertsekasSSPSurvival). Assumption 7.2.1: for some , every admissible policy has survival mass from every state after stages. The discounted setting reuses the same model with stochastic rows and (BertsekasDiscounted*); the average-cost setting adds a designated state with the avoidance probability of Assumption 7.4.1 (BertsekasSSPAvoidProb).
Under Assumption 7.2.1, there is a vector with
and a stationary policy attaining — BertsekasDP.ssp_main_theorem (goal, Prop. 7.2.1(a),(b)). Milestones: 7.2.1(c) policy evaluation, 7.2.1(d) optimality iff greediness, 7.2.2 policy iteration, 7.3.1 the full discounted counterpart, 7.4.1 the average-cost Bellman equation, 7.4.2 average-cost policy iteration.
These are the convergence guarantees behind value iteration and policy iteration — the two algorithms at the root of dynamic programming practice and of RL analyses (Q-learning's target operator is exactly ). The SSP form is the strongest of the three: the discounted theory is its special case (termination with probability per stage) and the average-cost theory reduces to it through cycles at the recurrent state. Formalized, the chapter yields a reusable finite-MDP theory: monotone operators, -stage contractions, and the machinery for later Vol. II material. All results are proved in the book; the formalization is new.
is not a one-stage contraction in the sup-norm under Assumption 7.2.1 — only an -stage contraction, uniformly over the finitely many -stage policy prefixes; extracting the uniform contraction factor (via finiteness of the policy space) is the crux of the whole chapter. The limit of -stage costs for nonstationary policies must be established, not assumed (tail-sum estimate ). For the average-cost results the associated-SSP construction (stop on reaching ) must be built inside the proof. The liminf phrasing of average-cost optimality is deliberate: for arbitrary nonstationary policies the Cesàro limit need not exist.
Finite states Fin n, finite control type, constraint sets as Finsets with attained minima; no termination state in the carrier — termination is the sub-stochastic deficit, exactly as the book treats it computationally. Policies are sequences of stage policies (Markov); costs of nonstationary policies via the shift recursion. Convergence is Tendsto in the product topology (equivalently sup-norm, finite). Average cost uses real liminf and division with the term junk-valued at 0 (irrelevant at infinity). The discounted theorem packages parts (a)–(e) in one statement mirroring Prop. 7.3.1.
A smooth manifold is a space that can be described locally by real coordinates, even when no single coordinate chart describes the whole space. Differential geometry works with these local descriptions, whereas an embedding realizes the entire space inside one Euclidean space without losing either its topology or its infinitesimal geometry. The strong Whitney embedding theorem supplies a dimension bound depending only on the dimension of the manifold. This mission targets the precise version selected by LeanEval v1, rather than a substitute formulation.
The benchmark attributes the strong result to Hassler Whitney's 1944 paper and distinguishes it from the earlier bound of . The result is a known mathematical theorem; the remaining task here is its formal proof in Lean. The exact benchmark declaration is authoritative for the target and its hypotheses, not a reconstruction from the historical literature (source and attribution).
Let be a natural number satisfying . Let carry a topology and a smooth atlas modeled on , with the usual model having no boundary. The topology is Hausdorff: distinct points admit disjoint neighborhoods. It is second countable: there is a countable collection of open sets from which every open set can be assembled as a union. These are explicit hypotheses, alongside the chosen charted-space and smooth-manifold structures, in the Lean statement.
A topological embedding is a map that is a homeomorphism onto its image, where the image has the subspace topology inherited from the codomain. An immersion has an injective differential at every point. For a smooth map , write for the induced linear map on tangent spaces at . These are separate requirements: the target asks for global topological embedding and pointwise injectivity of the differential together, as well as infinite differentiability. Their precise Lean meanings are the existing Mathlib predicates used directly by the benchmark, not new mission-specific definitions.
For every and every with the structures and hypotheses just stated, establish
The codomain has dimension exactly . The quantifier ranges over all such manifolds, including noncompact ones. There is exactly one goal theorem and no auxiliary theorem items, definition items, or milestones. The declaration is LeanEval.Geometry.WhitneyEmbeddingProblem.whitney_embedding, with the binders and conclusion preserved from the benchmark source.
The result realizes the given manifold in a Euclidean space with a uniform dimension bound. Its value in this formulation is the simultaneous control of topology, smoothness, and the differential, without a compactness assumption. Replacing the image-topology condition with mere injectivity would omit part of the requested conclusion; replacing with an unspecified dimension would omit the quantitative constraint. Both distinctions are explicit in the benchmark's explanation.
A completed formalization would supply a reusable strong embedding theorem on top of Mathlib's manifold language. This is a long-term infrastructure task, not a claim that a short proof is available. The September 5, 2026 LeanEval v1 snapshot supplied for this task records no accepted benchmark credit for this target. That dated benchmark status is not a claim about all formalization projects, and preparing an open theorem statement does not establish the theorem or earn benchmark credit.
The existing compact embedding result discussed by the benchmark provides an embedding into some finite-dimensional Euclidean space. That does not settle the present goal: it assumes compactness and does not supply the bound. Consequently, simply invoking that result cannot discharge the unrestricted benchmark statement. The source identifies substantial differential-topological infrastructure behind the strong theorem; this proposal does not advertise an easy proof or prescribe a decomposition (benchmark discussion).
All positive dimensions remain in scope, including and . Noncompactness is not a later extension or optional strengthening. The absence of an assumption must not be replaced by an implicit restriction in a new definition or an easier surrogate theorem.
The source model is EuclideanSpace ℝ (Fin n), and the target is EuclideanSpace ℝ (Fin (2 * n)). Smoothness is expressed by ContMDiff (𝓡 n) (𝓡 (2 * n)) ∞ e; the other two conjuncts are IsEmbedding e and pointwise Function.Injective of mfderiv. The type remains universe-polymorphic. No compactness, connectedness, orientability, or nonemptiness hypothesis is added. The empty manifold is included; dimension zero is excluded. Neither properness nor closedness of the image is demanded by the conclusion (exact declaration).
Mathlib already provides the vocabulary needed to state the goal: Euclidean spaces, charts, manifold smoothness, topological embeddings, and manifold derivatives. No custom definition item is necessary. Future proof work may develop reusable infrastructure, but this draft contains only the root theorem and intentionally imposes no supporting targets. A proof must establish that exact statement, not the compact-only, immersion-only, or weak alternative.
The Riemann hypothesis concerns the zeros of a complex analytic function, yet it admits an equivalent formulation involving only positive integers, finite sums, the real exponential, and the natural logarithm. Jeffrey C. Lagarias established this formulation in An Elementary Problem Equivalent to the Riemann Hypothesis (Theorem 1.1). It connects the distribution of divisors of an integer with the analytic behavior of the zeta function. For number theorists and formalizers, the interest lies in making that connection precise without confusing an elementary statement with an elementary proof.
The objective is the known equivalence selected by LeanEval v1, not a resolution of RH. Lagarias's paper builds on results of Guy Robin concerning large values of the divisor-sum function; those results remain substantial parts of the formalization workload (Lagarias, §3).
For a positive integer , its divisor sum is
where the sum runs over positive divisors, including and . Its harmonic number is
All inequalities below are inequalities of real numbers. The symbols and denote the real exponential and natural logarithm. The Euler–Mascheroni constant is .
The Riemann zeta function is obtained by analytic continuation of from . RH asserts that its nontrivial zeros have real part . The Lagarias elementary criterion in this mission is the assertion that for every positive integer . These conventions agree with the arithmetic quantities in Lagarias, Problem E, with the precise equality-clause distinction stated below.
There are no hypotheses on the goal theorem. The quantifier ranges over all positive integers, not a bounded test set or an unspecified tail. The benchmark uses a non-strict inequality and does not include an equality characterization. Lagarias's Problem E additionally requires equality only at ; the proof of the reverse implication in Theorem 1.1, p. 8 uses the non-strict inequality alone. The stronger source formulation is therefore not silently substituted for the benchmark.
The milestone list records the following source statements, with their thresholds unchanged:
for arbitrarily large integers .
All five are taken from Lagarias, §3, pp. 6–8; the finite check is explicitly an unnumbered step, not a newly attributed lemma.
The result identifies an exact arithmetic reformulation of RH. It does not make either side unconditional. A proof of the equivalence gives a bridge between statements in different mathematical languages; it does not certify the universal inequality merely because many instances can be checked. This distinction is central to the interpretation of Lagarias's theorem.
The formalization would connect existing Mathlib definitions of the zeta function, divisor sums, harmonic numbers, and Euler's constant through a machine-checked argument. Reusable outputs include explicit harmonic/exponential comparisons, certified finite real inequalities, and formal versions of Robin's conditional and oscillation results. The mathematical results are known; this proposal supplies open formalization targets, not completed proofs. No accepted LeanEval result is claimed by creating or launching the mission.
The elementary appearance of the criterion hides its main analytic requirements. Bounding the divisor sum crudely, or checking any finite number of integers, cannot establish the universal equivalence. The conditional upper bound and especially the quantitative oscillation theorem connect zeta zeros with unusually large divisor sums. They must be proved, not packaged as definitions or presumed available because the paper cites them (Lagarias, Propositions 3.1–3.2).
The oscillation statement requires uniform positive constants and arbitrarily large indices. Replacing it with one counterexample loses essential information. The bounded computation also requires rigorous control of exponential and logarithmic values: an ordinary floating-point loop is not a Lean proof. Beyond the listed milestones, completion still requires standard growth comparisons, threshold bookkeeping, and assembly of the two implications. The short length of the source's final argument should not be read as an estimate of total formalization effort.
The goal is LeanEval.NumberTheory.riemann_hypothesis_iff_lagarias_elementary_criterion, with type RiemannHypothesis ↔ LagariasElementaryCriterion. The criterion definition is copied from the benchmark. σ 1 n is natural-valued and cast to the reals; harmonic n is rational-valued and cast to the reals. RH remains Mathlib's predicate on riemannZeta, excluding negative even trivial zeros and the point . No replacement axiom, hidden RH assumption, altered zeta function, or circular child restatement is permitted.
The goal excludes and includes . Thresholds ensure positive logarithm arguments in the analytic milestones. The oscillation milestone expresses an infinite subset of the naturals as an unbounded set, retaining ; deletion of the finitely many smaller indices does not change the source's infinitude claim. Its real exponent is represented by Real.rpow, not natural exponentiation. Constants are chosen before the arbitrary cutoff.
The benchmark pins Lean 4.33.0 and Mathlib 6f1ef4e5dd604a435bddba4747b13970cd65d2a1. The proposal targets Prove2me's supported Lean 4.33.1 environment, Mathlib 0df444a360eaa60ab8c11dca51a86af692955474. These environments are distinct; eventual benchmark credit requires the benchmark's own validation. Contributions to analytic infrastructure, source-faithful supporting results, and certified finite inequalities are welcome. The five milestones are an initial source-backed structure, not a claim that all required infrastructure is already present.