Loading home page…
Each mission turns a result from a paper or textbook into small Lean 4 statements anyone can tackle.
Campaigns group missions around a shared mathematical goal. Each one tracks a quantity, such as an upper or lower bound. Have a good candidate in mind? Ping us on Slack, Zulip, or WeChat.
Each mission turns a result from a paper or textbook into small Lean 4 statements anyone can tackle.
Campaigns group missions around a shared mathematical goal. Each one tracks a quantity, such as an upper or lower bound. Have a good candidate in mind? Ping us on Slack, Zulip, or WeChat.
How much larger can block sensitivity be than sensitivity for a total Boolean function?
For a total Boolean function , a block of coordinates is sensitive at if flipping every bit in that block changes . Let count sensitive singletons and be the maximum number of pairwise disjoint sensitive blocks. Define and .
This campaign seeks larger exponents for which there exists an infinite family of total Boolean functions , indexed by , satisfying
Here denotes a quantity tending to zero as . Higher is better. The classical exponent is , and Huang's bound gives a ceiling of .
OpenAI's construction achieves an exponent strictly greater than .
One sufficient way to establish an exponent is to find a single total Boolean function with and . Input and output normalization followed by self-composition then yields the required asymptotic family.
Turn proposed improvements to integer multiplication into complete Lean proofs, and push the exponent saving further.
Harvey and van der Hoeven established an algorithm in 2021. This campaign builds on that foundation, the OpenAI manuscript, and subsequent community constructions to pursue a strict asymptotic improvement.
For two -bit integers, the target is
A positive beats asymptotically; larger is better. Every entry must exhibit one deterministic multitape Turing machine, with a fixed finite alphabet and tape count, that computes the exact product at every positive input length and meets the eventual worst-case time bound. The tracked number measures an asymptotic exponent saving.
Classical algorithms solve 3SUM in time. In a 2026 breakthrough, Alman and Vassilevska Williams gave a deterministic algorithm, refuting the integer 3SUM hypothesis. How low can the exponent go?
Building on existing Lean formalizations, this campaign tracks upper bounds for 3SUM on polynomially bounded integers, using a word RAM with -bit words, and pursues smaller exponents.
Classical algorithms solve all-pairs shortest paths in time. In a 2026 breakthrough, Alman and Vassilevska Williams refuted the APSP conjecture with a deterministic algorithm. How low can the exponent go?
Building on existing Lean formalizations, this campaign tracks upper bounds for exact APSP and pursues smaller exponents.
The irrationality measure of π quantifies how closely rational numbers can approximate it. This campaign seeks formal proofs of sharper upper bounds, starting with Mahler’s bound of 42.
The sharp Hlawka inequality for Schatten -norms is a cousin of the triangle inequality: it relates the norms of three matrices to the norms of their pairwise sums and their total sum. For complex diagonal matrices, an exact formula for the best possible comparison constant has been proved in Lean for every real . We conjecture that the same formula holds for all .
What is the smallest cutoff for which this formula holds for every real ?
References:
Is every odd number a sum of primes? This campaign tracks formalized proofs of the smallest that suffices.
Schnirelmann (1930) showed some finite works. Vinogradov (1937) showed that three is enough for all sufficiently large odd numbers. Tao (2012) proved unconditionally. Helfgott (2013) proved that every odd number greater than is a sum of three primes, though the proof is still unrefereed. Ideally, we can formalize this statement here. Note that three is optimal: is neither prime nor + prime.
Schoolbook matrix multiplication takes operations. The exponent is the infimum of all such that two matrices can be multiplied in arithmetic operations; trivially , and is conjectured but open.
Strassen gave the first nontrivial bound, , in 1969, and introduced the laser method in 1986 to reach . Coppersmith and Winograd's 1990 bound of stood for two decades. Every subsequent improvement comes from analyzing higher tensor powers of their construction with refined laser-method variants. That line reached in 2025, and the current record is , from August 2026. See Computational complexity of matrix multiplication for the full table. Can we formalize these results and even improve on them?
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.
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.
Every stochastic program is, in practice, compared against a shortcut. A decision maker facing genuine uncertainty is tempted either to replace the random data by its mean and solve one deterministic problem, or to imagine that perfect information about the future were available and solve a separate deterministic problem per scenario. Both temptations have precise answers: the expected value of perfect information (EVPI) measures how much a decision maker should be willing to pay for a perfect forecast, and the value of the stochastic solution (VSS) measures the cost of ignoring uncertainty altogether by solving the mean-value problem. Both concepts originate in decision analysis — EVPI traces to Raiffa and Schlaifer (1961) — and were brought into stochastic programming by Madansky (1960), who proved the first chain of inequalities relating the wait-and-see value, the recourse value and the expected-value-solution's cost. Birge and Louveaux, Introduction to Stochastic Programming, 2nd ed. (Springer, 2011), Chapter 4, gives the standard modern treatment, including a refined family of bounds — built from pairs subproblems against a chosen reference scenario — that sharpen VSS beyond the original mean-scenario comparison. This mission formalizes that chapter's capstone: the five-quantity, four-inequality chain that pins VSS between two computable optimal values.
Fix a two-stage stochastic program with fixed recourse: a finite family of K scenarios
in , each occurring with probability ,
; a first-stage feasible set ; and, for every
first-stage decision and every scenario , a
scenario cost — the optimal value of . By convention when has no feasible second-stage recourse under
, and when the second-stage program is unbounded below.
From , five basic quantities are defined (Birge & Louveaux §4.1–§4.2):
Section 4.6 refines VSS by replacing the mean scenario with an arbitrary reference scenario (not necessarily one of the possible scenarios, e.g. a worst case), with assumed probability :
Four links, each with independent content: nonnegativity of the leftmost gap, then two genuine inequalities (from the pairs-subproblem comparisons of Propositions 7 and 8), then the identity folded against 's reverse-direction cousin. This is the weakest statement that keeps all five quantities distinct — stating only the outer bound would erase exactly the refinement (via pairs subproblems) that makes the chapter's method useful.
The chain gives a decision maker two computable, non-obvious bounds on VSS — a quantity that is otherwise expensive to pin down exactly, since itself already requires solving the full recourse problem. and are both computable from (or ) two-scenario LPs, far cheaper than the full -scenario recourse problem, so Theorem 9 turns an expensive exact quantity into a pair of cheap certified bounds. Formalizing it fixes, once and for all, the exact hypotheses and quantifier structure of Madansky's original inequality (Proposition 1) together with the later pairs-subproblem refinement (Propositions 6–8, Birge 1982), often cited informally as "the VSS bounds" without distinguishing , , and . No part of this chain is on Mathlib or Formalpedia today (checked by concept query, not title); this is a first, from-scratch treatment of two-stage recourse value-of-information theory as formal objects.
The obvious first idea — collapse , , , , , , to one "the optimal value of the LP" and prove a single inequality — throws away the entire content of the chapter. Each quantity restricts the minimization to a different feasible object: minimizes jointly over ; swaps the order of and ; / evaluate one fixed under every scenario; and each minimize over a family of pairs subproblems rather than the full -scenario problem. The chain's proof (Propositions 7–8) depends on this precisely: Proposition 7's lower bound uses that each pairs-subproblem-optimal is feasible (not necessarily optimal) for the single-scenario problem at , and its upper bound uses that the recourse-optimal is feasible (not necessarily optimal) for the pairs subproblem — a feasible-but-not-optimal argument in each direction, not a direct comparison of objective values. Losing track of which solution is fixed and which is optimized destroys the argument entirely.
An Instance bundles the finite scenario set (Fin K, probabilities p : Fin K → ℝ with
p ≥ 0, ∑ p = 1, scenarios xi : Fin K → (Fin d → ℝ)), the first-stage feasible set
K1 : Set (Fin n1 → ℝ), and the scenario cost z : (Fin n1 → ℝ) → (Fin d → ℝ) → EReal, using
the extended reals to carry the book's own +∞/−∞ conventions for infeasibility and
unboundedness rather than silently restricting to a finite-valued special case (a genuine risk
of trivialization here, since Example 2 of the chapter exhibits ). All optimal
values (RP, WS, EV, EVPI, EEV, VSS, EVRS, generalized VSS, SPEV, EPEV) are
defined directly from z, matching the book's own level of abstraction in this chapter (which
never unfolds z into the underlying LP's data — those appear only in Chapter
3). Because EEV, the mean-scenario VSS, EVRS, the generalized VSS, and EPEV are each
defined relative to an optimal solution of some sub-problem — the book itself only ever says
"let denote some optimal solution" — every theorem using them states that
solution and its optimality as explicit hypotheses (x ∈ K1 and z x … = ⨅ …), never baking it
into a Classical.choiced value; this keeps the quantifier structure faithful to the book's own
"let ... be an optimal solution" phrasing. Proposition 5's part (b) — the upper bound
, "for stochastic programs with fixed recourse matrix and
fixed objective coefficients" — needs a different scope: that hypothesis is a structural
property of the underlying LP data (, , fixed across scenarios) invisible once is
abstracted away as above, and pinning it down would require modeling the LP's
data explicitly (as Chapter 3's mission does for its convexity theorem). That part is out of
scope here and is not needed for Theorem 9's own chain, which rests only on Proposition 5(a).
Collapsing any two of , , , , , , to a single "value of the LP" — the trivialization this book-wide series flags for Chapter 4 — is ruled out by construction: each is its own definition over its own feasible object, and Theorem 9's statement names all five quantities in the chain rather than only its outer bound. The two occurrences of "VSS" in the chapter (the original mean-scenario of §4.2, and the reference-scenario generalization of §4.6, used only in Theorem 9) are likewise kept as two distinct definitions rather than conflated under one name.
Every addition and subtraction between EReal values in this mission — inside expect, WS,
EVPI, VSS, EVRS's appearance in VSSRef, the pair sum inside pairsValue, the sum inside
SPEV, and all four differences in Theorem 9's own chain — uses three explicit operations,
badd/bsub/bsum, that implement the book's own convention (p. 164) that +∞ (infeasibility)
dominates, i.e. (+∞)+(−∞)=+∞, rather than Mathlib's native EReal addition, whose
⊤+⊥=⊥ would make VSS ≥ 0 (Proposition 5(a)) and the goal's own leftmost inequality false
whenever a witness solution is infeasible in a positive-probability scenario — exactly the
situation of the book's own Example 2 (pp. 174-175). The reference scenario's probability
(p. 172) is likewise not a free parameter but a definition, refProb,
computed from the instance itself as ; SPEV's sum is correspondingly
restricted to the scenarios other than the reference scenario (), matching the
book's own proof of Proposition 7, which uses . The single hypothesis
refProb I xir < 1 on Propositions 7, 8 and the goal says that some other scenario remains
possible, which the book's own factor presupposes.
Reusable beyond this mission: the Instance definition and the RP/WS/EV quantities are
the natural base for any later chapter of this series that needs the two-stage recourse value
(e.g. Chapter 3's convexity mission, Chapter 5's L-shaped method); contributions extending this
Instance to the full LP data of the underlying two-stage program, or adding Proposition 5(b)
and Proposition 2's Jensen-inequality argument on top of it, are welcome.
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.
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.
Many approximation problems resist the standard PCP toolkit: the best known NP-hardness factors for Max-Cut, Vertex-Cover and approximate graph colouring are far from the best known polynomial-time algorithms. To explain this gap, Khot (CCC 2002) proposed the Unique-Games Conjecture and the family of -to-1 Games Conjectures. The -to-1 conjectures assert perfect completeness: the hard instances are either fully satisfiable, or satisfiable only to a vanishing extent. Perfect completeness is what makes these conjectures usable for colouring problems, where a "yes" instance must be genuinely -colourable rather than almost so.
A line of work culminating in Khot–Minzer–Safra and Dinur–Khot–Kindler–Minzer–Safra established the almost-perfect completeness version for -to-1 games: for every there is an alphabet bound such that distinguishing value from value is NP-hard. Their route goes through Håstad's hardness for linear equations, which cannot have perfect completeness, so the loss is intrinsic to the technique. The source paper of this mission removes that loss for .
A label-cover instance (Definition 1.1 of the source) consists of a bipartite graph , two finite alphabets , and for each edge a constraint . The constraint is a projection constraint if there is with , and a -to-1 constraint if in addition for every . Given assignments and , the fraction of satisfied edges is , and
An instance all of whose constraints are -to-1 is a -to-1 game.
For , is the promise problem: given a -to-1 game with both alphabets of size at most , distinguish from . Writing for the same promise problem over all projection instances, the PCP theorem together with the parallel repetition theorem gives that is NP-hard for a suitable (Theorem 1.2 of the source); this mission takes that statement as an external input.
In Lean this is stated as a polynomial-time gap-preserving reduction: for every there is a soundness threshold such that for every source alphabet bound there is a target alphabet bound and a polynomial-time computable map sending projection label-cover instances with alphabets of size at most and value to -to-1 games with alphabets of size at most and value , and instances of value at most to -to-1 games of value at most . Combined with the NP-hardness of , this is exactly Theorem 1.6.
The milestone list follows the source's own numbering: the hardness of approximate colouring of -uniform hypergraphs that starts the construction (Theorem 3.1), the two Grassmann decoding theorems the inner PCP rests on (Theorems 3.2 and 3.3), the sunflower bound on zoom-outs (Lemma 3.8), and the linear-algebraic layer connecting NAE-satisfying bilinear forms with their tensor decompositions (Propositions 4.13, 4.14 and Corollary 4.15).
Theorem 1.6 confirms the -to-1 Games Conjecture, the first of Khot's -to-1 conjectures to be settled with perfect completeness. Via known reductions it yields: for every , it is NP-hard to -colour a -colourable graph (previously known for ); for every , it is NP-hard to find an independent set of relative size in a -colourable -uniform hypergraph; and hardness results for low-rank matrix completion.
None of this material is formalized today. Mathlib has no label cover, no PCP machinery, no Grassmann graph and no complexity classes beyond the computability layer. A complete development therefore contributes reusable infrastructure — finite two-prover games and their value, gap-preserving reductions, the Grassmann graph over and its agreement tests — well beyond this single theorem.
The obvious attempt is to redo the -to-1 construction with a perfectly complete outer PCP, namely hardness of systems of quadratic equations over in place of linear ones. This fails at composition: the Grassmann agreement test, the only known device that produces -to-1 constraints, is a test for linear functions and cannot certify quadratic constraints. Linearizing the quadratic equations by a low-rank test destroys the covering property of the outer PCP, which is what makes the composed soundness analysis work. The source paper's answer is a three-layer construction (outer, middle and inner PCP) with a lazy parallel repetition in the middle layer and an inner PCP based on a tensor of the standard Grassmann encoding with Golowich's low-rank variant.
All objects are finite and explicit. A label-cover instance carries left vertices , right vertices , alphabets and , a finite edge set, and a projection map for every pair of vertices; only projection instances are representable, as in Definition 1.1. The value is the supremum over all pairs of assignments of the fraction of satisfied edges, taken in ; when there are no edges, or no assignments at all, the convention gives value . A tripled set (Definition 4.1) is modelled as , with the triple indexed by being . The Grassmann objects live in modelled as , and all probabilities are ratios of cardinalities of finite sets of subspaces, with the convention that an empty denominator gives .
Hardness is not stated as "NP-hard" — no notion of NP is available — but as the existence
of a reduction. This matters: a reduction required only to preserve the gap, with no
computability condition, would be trivially satisfiable by a map that inspects the value of
its input and returns one of two fixed instances. The formalization therefore requires the
reduction map to be computed by a Turing machine within a polynomial time bound, using
Mathlib's Turing.TM2ComputableInPolyTime together with an explicit binary encoding of
instances. The NP-hardness of the source problem (Theorem 1.2,
i.e. the PCP theorem plus parallel repetition) is an external input and is not part of this
mission.
Contributions of intermediate infrastructure are welcome: the games of Sections 4–6 (Game1a, Game1b, Game2a, Game2b, Game2c, Game3) and their completeness and soundness lemmas are the natural next layer of milestones, as are the covering properties of Appendix C and the list-decoding bounds of Appendix E.
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.
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.
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.
In the last of the twenty-four questions that closed his 1982 survey Three-dimensional manifolds, Kleinian groups and hyperbolic geometry (Bull. Amer. Math. Soc. 6 (1982), 357–381), Thurston asked to "show that volumes of hyperbolic -manifolds are not all rationally related" (p. 380). Twenty-two of the twenty-four have since been answered — geometrization by Perelman, tameness by Agol and by Calegari–Gabai, the ending lamination conjecture by Brock–Canary–Minsky, virtual fibering by Agol — and this one is among the two that remain open.
Some rational relations are forced, and for a trivial reason: a degree cover of a hyperbolic -manifold has times its volume, so any two commensurable manifolds have rationally related volumes. The question, which remains open, is whether every rational relation arises that way — equivalently, whether some two hyperbolic -manifolds have irrational volume ratio. Remarkably, not a single such pair is known.
The bundle fixes the meaning of every term. Hyperbolic -space is the upper half-space . Its volume is Lebesgue measure with density — the Riemannian volume of the metric written out, so that no Riemannian machinery is required. The hyperbolic distance is given by its closed formula
A Kleinian action is a free, properly discontinuous action by hyperbolic
isometries; the quotient is a complete hyperbolic -manifold, discreteness and
torsion freeness being consequences rather than hypotheses. The volume of the
quotient is the measure of a fundamental domain, in the sense of Mathlib's
MeasureTheory.IsFundamentalDomain, and the set of volumes collects those that
are finite and positive.
Two conventions are stated rather than derived, and are worth flagging. Isometries are not required to preserve orientation, so the set of volumes also contains those of non-orientable quotients; this enlarges the set but not its -span, so neither goal is affected. And preservation of the hyperbolic volume is a field of the structure rather than a consequence of preserving the distance: it holds for every hyperbolic isometry, but deriving it amounts to classifying , which is not the subject of this mission.
The goal is that the volumes are not all rationally related: there are two of them, and , with for every rational .
Two milestones support it. The first is that passing to a subgroup of index multiplies the volume by , a fundamental domain for the subgroup being the union of translates of one for the whole group; this is the source of every known rational relation, and it is why the question is phrased as it is. The second is that the set of volumes is nonempty — that some finite-volume hyperbolic -manifold exists at all — without which the goal would be vacuously false rather than open.
A stronger form of the question, that the -span of the set of volumes is infinite dimensional, is also stated.
The question is a geometric statement whose difficulty is arithmetic. For the Bianchi groups of an imaginary quadratic field , Humbert's formula gives the covolume as , so the ratio of two such volumes is, up to explicit algebraic factors, a ratio of Dedekind zeta values at ; and Neumann and Yang showed that the Bloch invariant of a hyperbolic -manifold lies in a subgroup of finite -rank determined by its invariant trace field, so that manifolds sharing an invariant trace field with a single complex place, such as an imaginary quadratic one, have rationally related volumes. Producing one irrational ratio therefore means separating two such transcendentals — a statement of the same order of difficulty as the irrationality of . The value of formalizing the question is not that it will be closed, but that its statement, and the elementary relations that make its naive form false, are pinned down exactly.
Invertible modules over a commutative semiring are Zariski-locally free, so local semirings have trivial Picard group. The source asks whether the ring-theoretic semilocal conclusion survives without subtraction: must every invertible module over a semiring with finitely many maximal ideals be free? If not, is the conclusion at least true for finite semirings?
This mission turns CUHK-Shenzhen AI Math Problem 19, Picard groups of semi-local or finite semirings, into an auditable Lean campaign. The objective is not merely to transcribe notation: it is to expose the mathematical model, the capstone, and a smaller attack surface as separate artifacts that other formalizers can inspect and reuse.
The main theorem asserts freeness for every invertible module over a commutative semiring with finite maximal spectrum. A separate milestone states the finite-semiring fallback. Both are positive formulations; a concrete counterexample to either resolves that target negatively and should motivate a corrected classification.
Solving this target would settle the precise finite or analytic core represented by the Lean statement and would create reusable infrastructure in semirings, Picard groups, invertible modules, finite semirings. Even a rigorous disproof is valuable: several entries in this collection deliberately ask whether an attractive extrapolation is true, and Lean forces a counterexample to satisfy every side condition. The mission therefore treats theorem proving and model criticism as equally legitimate research outcomes.
Ring proofs use subtraction-sensitive k-ideal properties and decompositions into local factors that can fail for semirings. Finite indecomposable semirings need not be local and may have positive Krull dimension. Invertible modules are projective with strong duality, but familiar rank and determinant arguments may not survive additive noncancellation.
Formalize the known local-freeness proof from the evaluation isomorphism and study patching over finitely many principal opens. Identify exactly where partitions of unity require k-ideals. For finite semirings, enumerate idempotent matrices representing projective modules, impose the invertibility constraints, and seek either a reduction to principal rank-one modules or a minimal counterexample. Product decompositions and faithful-action lemmas should be reusable.
The Lean targets use Mathlib's commutative semiring, maximal spectrum, module, invertible-module, and free-module notions. 'Semilocal' is encoded only as finiteness of MaximalSpectrum; no unproved decomposition theorem is assumed. The finite fallback assumes the underlying semiring type is finite but does not assume the module itself finite separately. Cardinality-only variants from the source are not the capstone.
The natural-language source remains authoritative for motivation, while the Lean declaration is authoritative for what Prove2Me will verify. The mission description calls out restrictions where the current formal target is a finite-dimensional core, a fixed interpretation of informal terminology, or one sharpened subquestion from a broader classification problem. Those restrictions should not be silently generalized in a proof claim.
Resolve the finite-semiring statement, computationally or structurally, while developing the local-to-semilocal patching lemmas needed by the main theorem.
The capstone is marked as the mission's main item and is never duplicated as a milestone. Definitions precede theorem statements in the proposal order. A milestone is considered complete only when its own exact statement is proved; proving a nearby theorem with stronger-looking prose but mismatched quantifiers, signs, supports, dimensions, or asymptotic constants does not complete it.
The CUHK-Shenzhen AI Math Problems page added this problem on June 24, 2026. At the drafting date, August 31, 2026, the status and target corrections described above were checked against the source page and the cited primary material.
A contribution may prove the displayed theorem or refute it by constructing data satisfying every Lean hypothesis while negating the conclusion. Informal changes of model do not count: any proposed correction must be submitted as a separately reviewed statement with an explanation of which source ambiguity or false implication it repairs. Definitions must remain computational or mathematically constrained; fields that simply assume the desired conclusion are not acceptable. Every proof must compile against the mission's pinned Mathlib revision, use no sorry, and expose a top-level theorem solution when submitted to Prove2Me.
The main theorem is intentionally separated from a smaller milestone. Contributors should preserve that dependency order, publish reusable lemmas rather than monolithic tactics, and report whether a lemma is analytic, algebraic, combinatorial, or infrastructure-only. Numerical evidence, external computer algebra, and exhaustive search are welcome for discovery, but a final certificate must be replayable by Lean. If an external result is invoked, its hypotheses must be represented in the formal statement or proved in the dependency tree.
The files were built locally with Lean 4.30.0 and Mathlib revision c5ea00351c28e24afc9f0f84379aa41082b1188f, the supported Prove2Me environment at drafting time. The mission definition file is ordered before all theorem files, and each theorem imports exactly that public definition module or Mathlib. Independent blind read-backs accompany the draft items so reviewers can compare what the Lean code literally says with this mathematical description. Human confirmation remains required before the public proposal can be submitted for moderation.
Submission hold — source-fidelity repair (2026-09-04). The public goal restricts answers to elementary expression trees and is only a stronger subquestion. It does not formalize the source's broader special-function closed-form question. The existing published target is preserved, with this scope warning. Do not confirm or submit this version as a faithful formalization of the full source. The legacy mathematical target below is retained for traceability while the replacement is prepared.
A standard Brownian motion starts below the exponentially decaying boundary b(t)=b0 exp(-ct). The first time it crosses the boundary has a continuous density characterized by a generalized Abel--Volterra integral equation. The source asks for an explicit distribution, motivated in part by neuronal threshold models with a decaying refractory boundary.
This mission turns CUHK-Shenzhen AI Math Problem 13, First-passage time of Brownian motion to an exponentially decaying boundary, into an auditable Lean campaign. The objective is not merely to transcribe notation: it is to expose the mathematical model, the capstone, and a smaller attack surface as separate artifacts that other formalizers can inspect and reuse.
Construct one expression in a fixed elementary language whose evaluation is a continuous nonnegative density on positive times, solves the Abel equation, and integrates to one. The language contains real constants, rational constants, arithmetic, exp, log, square root, trigonometric functions, and the normal density. The first milestone drops elementary representability and normalization and asks for a continuous nonnegative Abel solution.
Solving this target would settle the precise finite or analytic core represented by the Lean statement and would create reusable infrastructure in Brownian motion, first-passage times, stochastic processes, Volterra integral equations. Even a rigorous disproof is valuable: several entries in this collection deliberately ask whether an attractive extrapolation is true, and Lean forces a counterexample to satisfy every side condition. The mission therefore treats theorem proving and model criticism as equally legitimate research outcomes.
Moving-boundary first-passage laws rarely have elementary closed forms. The Abel kernel is singular at the upper endpoint, and showing that a candidate equation solution is the actual passage density requires uniqueness and probability normalization. The capstone may be false under the selected expression language; a non-elementarity theorem would be a legitimate disproof of this precise formal target.
Formalize existence and uniqueness for the Volterra equation using weakly singular kernels, then connect it to Brownian first passage. Explore transformations suggested by the exponential boundary, Laplace transforms, and iterative resolvent kernels. Symbolic or numerical calculations may reveal special-function rather than elementary structure. If so, characterize the required extension of the expression language and prove why the current language is insufficient.
The already-published goal uses finite elementary-expression trees with arithmetic, exp/log/sqrt, sin/cos and normal density. The source explicitly permits standard special functions beyond this language. Accordingly the published declaration is a stronger elementary-only subquestion, not a faithful replacement for the full closed-form question. It is preserved as an existing result; its proof or disproof must not be reported as settling every special-function formula. The Abel-solution milestone asserts only existence of a continuous nonnegative solution; uniqueness, normalization, and identification with the first-passage density remain separate obligations. A complete source-faithful replacement needs an agreed formula class or a concrete proposed formula, not an unrestricted function renamed a closed form.
For each positive boundary height and decay parameter, there exists a continuous nonnegative solution of the stated Abel equation on positive times. This node asserts existence only, not uniqueness, unit mass, or an elementary closed form.
The CUHK-Shenzhen AI Math Problems page added this problem on June 23, 2026. At the drafting date, August 31, 2026, the status and target corrections described above were checked against the source page and the cited primary material.
A contribution may prove the displayed theorem or refute it by constructing data satisfying every Lean hypothesis while negating the conclusion. Informal changes of model do not count: any proposed correction must be submitted as a separately reviewed statement with an explanation of which source ambiguity or false implication it repairs. Definitions must remain computational or mathematically constrained; fields that simply assume the desired conclusion are not acceptable. Every proof must compile against the mission's pinned Mathlib revision, use no sorry, and expose a top-level theorem solution when submitted to Prove2Me.
The main theorem is intentionally separated from a smaller milestone. Contributors should preserve that dependency order, publish reusable lemmas rather than monolithic tactics, and report whether a lemma is analytic, algebraic, combinatorial, or infrastructure-only. Numerical evidence, external computer algebra, and exhaustive search are welcome for discovery, but a final certificate must be replayable by Lean. If an external result is invoked, its hypotheses must be represented in the formal statement or proved in the dependency tree.
The files were built locally with Lean 4.30.0 and Mathlib revision c5ea00351c28e24afc9f0f84379aa41082b1188f, the supported Prove2Me environment at drafting time. The mission definition file is ordered before all theorem files, and each theorem imports exactly that public definition module or Mathlib. Independent blind read-backs accompany the draft items so reviewers can compare what the Lean code literally says with this mathematical description. Human confirmation remains required before the public proposal can be submitted for moderation.
Linear approximation is only one instance of distance minimization. Feasible sets in optimization are typically convex rather than subspaces, so a useful certificate must compare a target point with an entire convex set and must allow an affine offset. Chapter 5 of Luenberger's Optimization by Vector Space Methods builds this certificate through geometric forms of the Hahn--Banach theorem, supporting hyperplanes, and separation of convex sets. The resulting minimum-distance theorem expresses the distance from a point to a convex set as an optimal gap measured by a norm-bounded continuous linear functional (Luenberger, §§5.12--5.13, pp. 130--137).
This mission advances the series from subspace annihilators to affine separation. It formalizes the Minkowski gauge used by the chapter, three progressively stronger separation statements, and a capstone distance-duality certificate. These results are standard infrastructure for constrained optimization: they turn a geometric exclusion or distance into a scalar inequality that can later become a multiplier or a dual bound.
Let be a real normed space and a nonempty convex set. Convexity is represented by Convex ℝ K, and topological interior, closure, and infimum distance use Mathlib's interior, closure, and Metric.infDist. A continuous affine separator is described by a continuous linear functional and a scalar level . The inequality for all places in one closed half-space.
When a convex set contains zero in its interior, its Minkowski gauge is the functional gauge K. The source characterizes it by nonnegativity, positive homogeneity, subadditivity, continuity, and the level sets
These properties are bundled into the first milestone, following Lemma 1 of §5.12 (pp. 131--132).
For two convex sets , Eidelheit separation means finding nonzero and with for and . The source assumes that has nonempty interior and that its interior does not meet . The Lean statement records the nonemptiness of explicitly, since otherwise nonzero separation is not forced.
Formalize the six gauge properties above. Then, for a convex with nonempty interior and an affine subspace disjoint from that interior, produce and such that
This is Mazur's geometric Hahn--Banach theorem as stated in §5.12, Theorem 1 (p. 133).
For , formalize a nonzero functional satisfying for all . Next formalize Eidelheit separation:
These are Theorems 2 and 3 of §5.12 (pp. 133--134).
Let have positive distance from . Produce and a real upper-bound level with , on , and
Every other feasible pair must satisfy . If realizes the distance, require to align with . This is the finite real certificate form of §5.13, Theorem 1 (pp. 136--137).
The capstone is an exact strong-duality statement for distance to a convex set. A feasible pair yields a certified lower bound on the distance, and the distinguished pair reaches the primal value. Unlike a nearest-point characterization, it remains meaningful when is not closed and no minimizing point exists. The conditional alignment clause identifies the equality case when attainment is available.
Formalizing the chapter's progression creates more than one isolated equality. The gauge package links convex geometry to sublinear analysis; Mazur separation handles affine constraints; the supporting-hyperplane and Eidelheit statements provide reusable interfaces for later multiplier rules. The results are known and proved in the 1969 text; the mission's contribution is a coherent machine-checked Lean layer that preserves the source hypotheses and can support later chapters on duality and optimization.
A direct reuse of subspace distance duality is insufficient because a general convex set is neither closed under subtraction nor described by an annihilator. An affine level is unavoidable. The common shorthand introduces a second problem: need not be bounded, so a real-valued supremum is not available for an arbitrary functional. The capstone therefore quantifies over a real upper bound and asserts its optimality through a universal inequality; this records the same finite support value without imposing boundedness absent from the source.
Topological hypotheses also differ across the milestones. Separation uses nonempty interior, whereas the final distance theorem only assumes convexity, nonemptiness, and positive distance. Replacing positive distance by mere exclusion would be invalid for a nonclosed set. Similarly, requiring closure or compactness would make formalization easier but would lose the theorem's intended infinite-dimensional scope.
The mission is restricted to real normed spaces. Sets use Set X; affine varieties use AffineSubspace ℝ X; separators use ContinuousLinearMap. The gauge is Mathlib's existing gauge, so no competing definition is introduced. The bundled gauge milestone deliberately includes both level-set identities as well as continuity, positive homogeneity for positive real scalars, subadditivity, and nonnegativity.
The Eidelheit theorem includes K₂.Nonempty, an assumption used implicitly by the source's separating conclusion. The capstone includes K.Nonempty and 0 < Metric.infDist x₁ K; it does not assume closedness, boundedness, compactness, or attainment. Its pair represents a finite support level, and the universal comparison over all feasible rules out a weakened statement in which an arbitrarily loose upper bound could trivialize existence. The optional nearest-point clause uses the exact equality and fixes the sign of alignment. Contributions may add reusable lemmas on gauges, interiors, affine subspaces, or support bounds, but the public results should remain independent of finite-dimensionality and completeness.