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?
Chapter I's usual stochastic order compares "how large" two random variables tend to be. A different, equally common question in operations research is "how spread out" a random variable is: two portfolios with the same expected loss can differ sharply in how much that loss varies, and a risk-averse decision maker or a convex cost function cares about exactly that difference. Shaked and Shanthikumar's Stochastic Orders (Springer, 2007) formalizes this comparison as the convex order, the book's mean-preserving-spread order (known outside OR and probability circles as the Rothschild–Stiglitz order from economics). This mission formalizes the order and its central structural result: Strassen's martingale-coupling characterization.
Let be a real-valued random variable on a probability space , and let be a real-valued random variable on a (possibly different) probability space . is smaller than in the convex order, written , if
Convex functions take their relatively largest values on the "extreme" regions outside some interval, so says is more likely than to take extreme values: is "more variable" than . Unlike the usual stochastic order, forces the two means to agree (, taking , both convex) — the convex order compares spread holding location fixed, exactly the mean-preserving-spread reading. Two equivalent forms make it tractable: comparing tail integrals of the survival/distribution functions (Theorem 3.A.1), and comparing mean absolute deviations from every point (Theorem 3.A.2).
Furthermore, can be chosen so that the conditional law stochastically increases with (in ). This is the convex-order analogue of Chapter I's Theorem 1.A.1: instead of one variable dominating the other pathwise, 's copy is a fair (martingale) randomization of 's copy whose spread only grows in the conditioning value. The book itself calls the constructive direction "not easy to prove"; this mission states the theorem faithfully, including the "Furthermore" strengthening, without attempting a proof.
The convex order is the standard way operations research and actuarial science formalize "more variable, same average": comparing the riskiness of two portfolios with matched expected return, the effect of aggregation or diversification on total claim size, or the value of information in a stochastic program (where a random variable degenerates to its mean exactly when the decision maker learns everything, the two extremes of a convex-order chain). Strassen's characterization is what turns "compare against every convex function" — an intractable universal quantifier — into a single explicit construction: exhibit one martingale coupling and the comparison is settled for every convex function at once, by Jensen's inequality. This is the technique behind bounding the effect of information or risk aggregation without checking convexity function by function, and the "Furthermore" monotonicity clause is what makes the coupling itself informative about how the spread grows with the conditioning variable, not merely that some fair coupling exists.
Formalizing this theorem fixes, for the whole book series, the exact shape every later coupling theorem for a variability-type order (the increasing convex/concave orders of Chapter IV via a submartingale, the multivariate convex order of Chapter VII) is expected to restate. No proof is attempted; the book's own remark that the constructive direction is "not easy" marks it as a genuine target for a future proof-bearing pass, not a formality.
The definitional trap mirrors Chapter I's: "for every convex " must be a genuine
universal quantifier over Mathlib's own convexity predicate, with the existence of both
expectations stated as an explicit integrability hypothesis inside the quantifier, not assumed
globally or dropped. The coupling theorem doubles the difficulty of Theorem 1.A.1's: the
conditional-expectation condition a.s. is with respect to the
-algebra generated by , not an informal "expected value given ", and must
use the martingale API's own convention (Mathlib's condExp) precisely. The "Furthermore" clause
compounds this: it is a claim about the regular conditional distribution of given
for every point , not merely the conditional expectation, and dropping it silently
(as a "remark" rather than part of the theorem) would understate what Theorem 3.A.4 actually
claims — the chapter brief flags this explicitly as a trap, and it is kept as a conjunct of the
same existential witness here.
Random variables are again measurable functions into from arbitrary measurable
spaces, ConvexOrder μ ν X Y taking on and on a separate ,
matching Chapter I's convention and this series' own pattern. Convexity is Mathlib's ConvexOn ℝ Set.univ φ; "equality in law" is again ProbabilityTheory.IdentDistrib. The martingale condition
uses Mathlib's conditional-expectation notation ρ[Ŷ | m] =ᵐ[ρ] X̂ with m the -algebra
MeasurableSpace.comap X̂ inferInstance generated by X̂ — the martingale API's own convention,
not a hand-rolled gloss. The "Furthermore" clause uses Mathlib's ProbabilityTheory.condDistrib,
the regular conditional distribution kernel of Ŷ given X̂ (available since ℝ is a standard
Borel space), and states "increasing in x in ≤st" via the kernel's survival function being
monotone in x at every threshold — restating, locally to this chapter's namespace, the same
tail-probability shape Chapter I's UsualOrder uses (drafts cannot import another mission's
definitions, per this series' convention). A trivializing formalization is ruled out explicitly:
the martingale and monotonicity conjuncts are both kept as genuine content of the existential
witness in the goal theorem, not weakened to a bare coupling or dropped as an optional remark.
This mission draws on no platform prior art (searches for "convex order", "Strassen",
"martingale", "Jensen" returned only unrelated geometry/algorithm/physics results as of
2026-09-18); Mathlib's Probability/Martingale/* supplies the conditional-expectation and kernel
machinery the coupling condition and its "Furthermore" clause are built from, but no platform
theorem states the convex order or its coupling characterization itself. Reusable beyond this
mission: the condExp/condDistrib-based martingale-coupling pattern is the shape Chapter IV's
analogous submartingale coupling (Theorem 4.A.5) and Chapter VII's multivariate convex order
(Theorem 7.A.1) are each expected to restate independently.
A device's mean residual life at age — its conditional expected remaining lifetime given that it has survived to — is one of the oldest and most interpretable summaries in reliability and survival analysis: it is what an insurer, a maintenance planner, or a hospital outcomes researcher actually wants to know about a unit still in service. Comparing two mean residual life functions pointwise gives the mean residual life order , a natural "the survivor of is worn less, on average, than the survivor of " comparison that is weaker than the usual stochastic order but not directly comparable to it (the book states plainly that neither implies the other in general). This mission formalizes the order's definition and its precise relationship to the stronger hazard rate order : under an extra monotone-ratio condition the two orders coincide, and one direction of that coincidence always holds. A third milestone gives one of the chapter's closure properties, showing that "decreasing mean residual life" (DMRL) — an aging notion used throughout reliability theory to describe units that wear out, rather than improve, with age — is preserved under adding independent noise.
Fix a probability space and a real-valued random variable with survival function and finite mean. The mean residual life function of at is
For a second random variable on with mrl function , is smaller than in the mean residual life order, , if for every . The hazard rate order, restated in this mission's own namespace (Chapter 1's version cannot be imported — see Formalization scope), is the general, absolute-continuity-free comparison for all , where is 's survival function. A random variable is DMRL (decreasing mean residual life) if its mrl function is decreasing in .
Combined with the companion milestone below, this is a genuine conditional equivalence: under the monotone-ratio hypothesis, and coincide, and in particular under that condition. Without the hypothesis, the book states explicitly (the paragraph immediately preceding Theorem 2.A.1) that neither nor implies the other.
Each milestone is stated exactly as the book states it: no constant is hard-coded, no or asymptotic approximation is involved, and the goal's monotone-ratio hypothesis is the genuine ratio , not two separately-monotone functions (a different, unrelated condition the book itself does not state).
The mean residual life order sits at a specific point in the book's own hierarchy of orders: strictly implied by the hazard rate order (Theorem 2.A.1), and — the goal theorem — reversible into the hazard rate order under one extra monotonicity hypothesis on the ratio of the two mrl functions. This "sandwich" structure is exactly the kind of comparison-of-orders result that makes Chapter 1's usual and hazard rate orders (already formalized in Chunk 01 of this series, restated locally here since drafts cannot import each other) into a genuinely connected theory rather than a list of unrelated definitions. The DMRL closure property (Theorem 2.A.11) is separately significant: DMRL is one of the book's standard "aging" notions, used in reliability engineering to model components that wear out over time, and its preservation under adding independent noise is a basic tool for building compound reliability models (e.g. a component with an added, uncorrelated failure mode) from simpler DMRL parts.
No prior art exists on the platform for either order: GET /theorems?q=mean+residual+life
returns zero hits, and GET /theorems?q=hazard+rate returns exactly one hit
(DQJSQ.theorem2_ifr), an unrelated queueing-theory IFR (increasing failure rate) lemma about
patience densities in a fluid queueing model, not this order — it names a different object under
a coincidentally similar keyword and is not reused. This mission is a foundational island for the
mean residual life order.
The mrl function is a genuinely two-case object: a real conditional expectation on , and a hard outside that region. The goal theorem's proof (not formalized here; only the statement is a milestone) differentiates and , uses the identity relating the mrl function to the hazard rate, and compares the two resulting hazard-rate expressions using the ratio's monotonicity — a genuinely analytic argument, not a routine unfolding of definitions. The chief formalization difficulty is keeping the shape of (a pointwise comparison of a derived function) visibly distinct from the function-class shape of used in Chapter 1, since the book explicitly warns that conflating the two orders is a live error (neither implies the other in general) — see Formalization scope below for how each shape is kept separate.
All three random variables in this mission's milestones are real-valued measurable functions on
a MeasureTheory.Measure space, matching this series' Chapter 1 convention (Chunk 01). The mrl
function mrl μ X t is defined as if 0 < P{X>t} then (∫ ω in {X>t}, (X ω - t) ∂μ) / P{X>t} else 0, formalizing the case split on directly via positivity of the survival probability
(its defining equivalent under the survival function's monotonicity) rather than through the
derived quantity itself. MrlOrder μ ν X Y is ∀ t : ℝ, mrl μ X t ≤ mrl ν Y t — a direct
pointwise comparison of two functions, deliberately kept a different shape from Chapter 1's
UsualOrder (a ∀ φ ∈ 𝒞, E[φ∘X] ≤ E[φ∘Y] function-class quantifier), since the book's own
warning that and neither implies the other is a warning against treating
them as interchangeable comparison shapes.
The hazard rate order is restated locally in this chapter's own namespace
(StochasticOrders.MeanResidualLife.HazardRateOrder) rather than imported from Chunk 01's
StochasticOrders.Usual.HazardRateOrder, because each chapter's mission is drafted and reviewed
as an independent Prove2Me proposal and one draft cannot import another draft's unpublished Lean;
its definition is identical in shape to Chunk 01's own restatement of the general,
absolute-continuity-free survival-function form of (not the density-ratio form, which
requires absolute continuity the book does not assume at this level of generality).
Every milestone that consumes mrl carries explicit Integrable hypotheses on the random
variables involved (Integrable X μ, and Integrable Y ν or Integrable Z μ as applicable),
formalizing the book's own standing "finite mean" hypothesis from §2.A.1's definition of the mrl
function: without it, the Bochner integral inside mrl would return its junk value 0 for a
non-integrable variable on some tail set, letting a hypothesis like MrlOrder μ ν X Y hold of a
function that is not actually the book's mean residual life function. DMRL μ X is
Antitone (mrl μ X), the book's own " is decreasing in " in the weak, non-strict
monotone sense used throughout the book for "increasing"/"decreasing".
A trivializing formalization this mission rules out: stating the goal theorem with the ratio
hypothesis as two separate monotonicity conditions on and individually (rather than
genuine monotonicity of the ratio on the region where ) would be a different,
strictly stronger and easier-to-satisfy hypothesis than the book's own — the milestone here states
MonotoneOn (fun t => mrl μ X t / mrl ν Y t) {t | 0 < mrl ν Y t}, the genuine ratio restricted to
where the denominator does not vanish, matching Theorem 2.A.2's own " increases in
" verbatim.
StochasticOrders.Usual), for the usual and hazard rate orders this
chapter's own restated definitions parallel.Chapter 2's finite-hypothesis-set learning bound is uninformative the moment is infinite — diverges — yet most hypothesis sets used in practice (linear separators, neural networks, decision trees) are infinite. Chapter 3 answers the question the previous chapter's own worked example (axis-aligned rectangles, Example 2.4) leaves open: is efficient learning from a finite sample still possible for an infinite hypothesis set, and can this be shown in general rather than case by case? The chapter's answer runs through two complementary notions of complexity — Rademacher complexity, a data-dependent measure of how well a function family correlates with random noise, and the VC-dimension, a purely combinatorial measure of the number of distinct labelings a hypothesis set can realize on a finite point set — connected by Massart's lemma and Sauer's lemma, and culminating in a generalization bound that replaces with the VC-dimension .
For a family of functions and a sample , the empirical Rademacher complexity (Definition 3.1) measures how well fits random sign noise on ; the Rademacher complexity (Definition 3.2) averages this over samples. Theorem 3.3 converts a Rademacher-complexity bound directly into a generalization bound via McDiarmid's inequality. For binary hypothesis sets , the growth function (Definition 3.6) counts the maximum number of distinct dichotomies realizes on points, and the VC-dimension (Definition 3.10) is the largest for which (i.e. shatters some set of points). Massart's lemma (Theorem 3.7) is the purely combinatorial tool bounding the expected maximum of a sum of signed vector components by , and Sauer's lemma (Theorem 3.17) bounds the growth function itself, by induction on , whenever the VC-dimension is finite.
Theorem 3.3 (Rademacher generalization bound, milestone). For and any , with probability at least over an i.i.d. sample of size , for all : .
Theorem 3.7 (Massart's lemma, milestone). For a finite with : .
Theorem 3.17 (Sauer's lemma, milestone). For with , for all : .
Corollary 3.19 — the mission's goal. For with and any , with probability at least , for all :
Corollary 3.19 is the chapter's answer to the question chapter 2 leaves open: it is Theorem
2.13's direct infinite-hypothesis-set generalization, replacing (undefined for
infinite ) with the VC-dimension (finite even for many infinite hypothesis sets, such
as halfspaces in , which have VC-dimension ). It is also the template every
later margin bound in the book specializes (Chapters 5, 9, 10's SVM, multi-class and ranking
margin bounds all replace this bound's uniform /VC-dimension term with a
scale-sensitive complexity measure derived from the same Rademacher-complexity machinery), and
Sauer's lemma is independently one of the most cited results in learning theory and extremal
combinatorics. No prior art on the Prove2Me platform is faithful to any of this chapter's
content: RademacherSymmetrization.radS_chernoff (Aether Catalog) proves a different,
Massart-optimized Chernoff bound for the empirical Rademacher complexity of a finite class —
a different object (empirical vs. population) with a different bound form from Theorem 3.3/3.5
— and sauerShelah_full proves only the trivial identity sauerShelahBound k k = 2^k, not
Sauer's lemma itself. A further hit, sauer_shelah (Aether Catalog, Algebra/SauerShelah.lean),
does state the Sauer-Shelah bound itself (F.card ≤ ∑_{i≤d} C(n,i) for a family F of subsets
of Fin n shattering no set larger than d) — checked and not reused: it is a different idiom
from Theorem 3.17 as this chunk needs it, a fixed finite ambient domain Fin n with F a
Finset of its subsets directly, rather than the book's own growth function Π_H(m) (a
supremum over point-tuples drawn from an arbitrary, possibly infinite X, Definition 3.6) that
this chunk's other items and the goal (Corollary 3.19) are built on; reusing it would require
either abandoning GrowthFunction/HasVCDim (needed faithfully by the goal itself) or a
nontrivial reduction lemma this mission's budget does not include, so sauer_lemma is drafted
fresh against this chunk's own GrowthFunction/HasVCDim. All ten items are drafted fresh.
Sauer's lemma's proof is a genuine two-parameter induction (on ) with a real combinatorial
construction: restricting to a sample of size , then splitting the restricted
family into (its restriction to the first points) and (the concepts whose
membership in changes with the addition of the -th point), with and
— a genuinely combinatorial argument, not a
statement that unfolds by simp; a weaker restatement using only the trivial bound
would be true but is explicitly not what Theorem 3.17 states (BRIEF.md's
named trivializing formalization for this chapter). Massart's lemma needs the expectation of a
supremum over a finite set of -many sign patterns kept as an honest average, not silently
replaced by a looser union bound. Corollary 3.19's own term inside the logarithm needs
the side condition carried through explicitly — Corollary 3.18's own domain restricts
to , and the bound is false, not merely unproved, without it (at , can be
smaller than , making the logarithm negative).
GeneralizationError/EmpiricalError are restated locally in this chunk's RademacherVC
namespace (byte-identical in content to chunk 02-pac's own copies), since a draft item cannot
import another chunk's draft module; this duplication is expected and will collapse once
02-pac is moderated, uploaded and listed as reusable in missions/README.md's "Published
definitions" table. EmpiricalRademacherComplexity/Massart's lemma model the Rademacher signs
σ as ranging over the finite type Fin m → Bool rather than a measure-theoretic i.i.d.
process, so the "expectation over σ" in both is the exact finite uniform average over its
2^m outcomes — faithful and simpler than a MeasureTheory construction, since σ's
distribution really is uniform on a finite set of outcomes for every finite m. GrowthFunction
takes a tuple of m points (Fin m → X) rather than a size-m subset of X, a harmless
generalization (repeated points never increase the dichotomy count) documented in the item's own
docstring. HasVCDim is a Prop parametrized by the candidate dimension rather than a total
ℕ/ℕ∞-valued function, so it does not cover the book's VCdim(H)=+\infty case (Examples
3.15-3.16); every theorem using it takes HasVCDim H d as an explicit hypothesis, matching the
book's own "let H... with VCdim(H)=d." Theorem 3.3 adds an explicit measurability
hypothesis on G (hGm) beyond the book's own displayed statement, needed to keep the Bochner
integral ∫ z, g z ∂D from silently evaluating to 0 for a non-measurable g — this is the
book's own standing assumption (footnote 3, p. 30) made an explicit hypothesis rather than an
implicit one. No numerical constant in any of the four theorems is altered from the book's own;
Corollary 3.19's side condition d ≤ m is kept explicit, per BRIEF.md's pitfall note.
Not formalized: Lemma 3.4 and Theorem 3.5 (the binary-classification specialization of Theorem
3.3 via the zero-one-loss identity ), Corollary 3.8 and
Corollary 3.9 (the intermediate Rademacher-to-growth-function and growth-function
generalization bounds), and Corollary 3.18 (the VC-dimension bound on the growth function,
for ) — five intermediate results in the proof chain
Theorem 3.3 → Theorem 3.5 → Corollary 3.8/3.9 → Sauer's lemma → Corollary 3.18 → Corollary 3.19
that are not independently drafted as milestones, per the budget guidance to keep a chunk to a
goal plus its most load-bearing 3-8 milestones rather than every numbered result on the page;
the three drafted milestones (Theorem 3.3, Massart's lemma, Sauer's lemma) are the chain's three
genuinely distinct proof techniques (McDiarmid's inequality, a probabilistic-maximum bound, and
a combinatorial induction), and the goal theorem's own statement is Corollary 3.19 exactly as
displayed, not a restatement of any intermediate corollary. Radon's theorem (Theorem 3.13,
background for the hyperplane VC-dimension example) and the worked VC-dimension examples
(intervals, hyperplanes, rectangles, convex polygons, sine functions) are illustrations, not
general results, and are not formalized — drafting only the example computations (e.g.
VCdim(hyperplanes) = d+1) instead of the general finite-H machinery is exactly the
trivializing formalization this mission avoids.
Von Neumann's minimax theorem (Chapter VIII) settles two-player zero-sum games with scalar payoffs. In 1956, Blackwell asked the natural generalization: what can a player guarantee in a repeated game with vector-valued payoffs, where "winning" means driving the average payoff into a target set rather than above a target value? For decades the resulting theory — approachability — and the regret-minimization theory this book develops were believed to be different, with approachability seen as the stronger notion. Chapter 13 closes that gap: approachability and online convex optimization are shown to be algorithmically equivalent, each reducible to the other with no loss of efficiency, and along the way this equivalence yields a constructive, rate-quantified proof of Blackwell's own theorem.
A generalized vector game (Definition 13.2) is given by bounded convex closed decision sets and a vector payoff . A set is approachable (Definition 13.3) if some non-anticipating algorithm, playing in against any sequence , drives the average payoff's distance to to zero. Blackwell's theorem (13.4) characterizes exactly which are approachable via a purely geometric condition: every column-player strategy admits a row-player best response landing the payoff in .
Section 13.2 constructs an explicit approachability algorithm from any OCO algorithm: given a best-response oracle realizing Blackwell's condition, Algorithm 37 runs the OCO algorithm on the proxy losses (the support function letting distance-to- be written, via Lemma 13.5's minimax duality, as a convex optimization problem over the unit ball), queries the oracle at the OCO algorithm's play , and averages the resulting rewards.
This chapter's headline claim — approachability and OCO are equivalent — is proved in two
directions in the book (§13.2 and §13.3); this mission drafts the direction the book itself
foregrounds as "the more interesting implication" and constructively proves: any sublinear-regret
OCO algorithm converts directly into an explicit approachability algorithm with an explicit
convergence rate, giving a self-contained, algorithmic proof of a 1956 game-theory theorem using
1990s–2000s online-learning machinery. Historically, this equivalence resolved a standing
misconception (approachability believed strictly stronger) and reframes Blackwell's theorem as a
special case of regret minimization rather than a separate theory requiring its own toolkit. No
prior art was found on the platform for Blackwell approachability (planning search:
q=Blackwell — the one hit, PRNGCompression.prng_no_free_lunch's cousin, an unrelated
Rao-Blackwellization result, is not a substitute); this mission drafts both items fresh.
Theorem 13.4's statement is a clean geometric implication, but the book is explicit that its
proof is entirely carried by Theorem 13.7 plus an unstated "explicit conclusion" left as an
exercise (the passage from a finite-horizon rate bound to the asymptotic Dist → 0 claim, using
any of the book's own sublinear-regret OCO algorithms as a witness). Theorem 13.7's own proof
combines three nontrivial facts: Lemma 13.5's minimax-duality rewriting of as a linear optimization over the unit ball (itself proved via Sion's minimax theorem, not
excerpted here), the best-response oracle's defining inequality (13.2) applied pointwise at each
round's , and the OCO algorithm's own regret guarantee applied to the specific proxy-loss
sequence built from the realized game trajectory — a genuine composition of three separate
pieces of machinery from earlier in the book (Chapters III–VIII), not a routine substitution.
IsApproachable is declared as its own definition (per BRIEF.md's explicit instruction, since
Theorem 13.4 depends on it), with the non-anticipation clause made explicit (matching the
series' IsOnlineAlgorithm convention from Chunk 03) even though the book's own Definition 13.3
states it only informally ("x_t ← A(y_1,\dots,y_{t-1})"). SupportFunction is h_S exactly as
displayed, as a real supremum (a genuine maximum given the chapter's standing "closed, bounded"
hypothesis on S). throughout is Euclidean distance, rendered as Mathlib's
Metric.infDist — confirmed the chapter uses no other distance notion (checked §13.1-13.3
directly, per the pitfall BRIEF.md flags). Theorem 13.7 transcribes Algorithm 37's
construction faithfully, including its one-round offset (using the
previous round's realized reward to build the current round's proxy loss, while the
conclusion averages the current round's rewards) — exactly as the book's own pseudocode has it,
not smoothed over.
Scope decision on Theorem 13.4's biconditional. The book states Theorem 13.4 as an ↔ but
proves, and explicitly flags as proved, only the sufficiency direction (←): "The necessity of
this condition is left as an exercise... Our reductions henceforth give an explicit proof of
Blackwell's theorem [meaning: of the sufficiency direction]." Per CAPTAIN_BRIEF.md rule 6 and
BRIEF.md's explicit instruction, this mission drafts only that direction, named as such in the
goal item's own docstring; see STATUS.md.
Not formalized (out of scope for this mission, given the remaining budget and the explicit
"exercise" status of several results on these pages): the necessity direction of Theorem 13.4;
Lemma 13.5 (minimax duality for Dist, itself relying on Sion's theorem, not separately
formalized here); Lemma 13.6 (the equivalent best-response-oracle condition); §13.3's entire
approachability-to-OCO direction (Theorem 13.9, Lemma 13.8, the cone/polar-cone machinery of
§13.3.1) and §13.3.3 (existence of a best-response oracle for the constructed set); the "explicit
conclusion" of Blackwell's theorem from Theorem 13.7, left as an exercise by the book itself.
Every algorithm in Chapters I–V observes the full cost function after playing . Many applications only reveal the scalar cost incurred — routing a network and observing total latency, or placing an ad and observing the click-through revenue, without ever seeing the cost of a path or bid not taken. This is the bandit feedback model, and Chapter 6 asks whether sublinear regret survives it. The chapter's answer is a general two-part reduction — turn a first-order full-information algorithm into a bandit algorithm by feeding it an unbiased gradient estimator built from a single scalar observation — instantiated concretely on online gradient descent to produce the first historical bandit convex optimization algorithm, the FKM algorithm (Flaxman–Kalai–McMahan).
Let be the decision set, containing the unit ball centered at , with diameter at most . At each round the player picks , an adversary has fixed a cost function (Lipschitz constant , bounded by in absolute value on ), and the player observes only the scalar — never itself or its gradient. Regret is , exactly as in the full-information setting, but now the algorithm's plays are themselves random (they depend on the sampled gradient estimates), so the guarantee is on expected regret.
The chapter's construction has two independent parts. Part 1 (Lemma 6.5) is a black-box reduction: given any first order full-information algorithm (Definition 6.4 — one that depends on each cost function only through its gradient at the played point) with a full-information regret bound , feeding an unbiased estimator of in place of the true gradient preserves the regret bound in expectation, up to evaluated at the estimators instead of the true gradients. Part 2 (Lemma 6.7) supplies such an estimator using only one scalar observation per round: sample uniformly from the unit sphere, play for a small radius , and is (for linear ) an unbiased estimator of — more precisely, an unbiased estimator of the gradient of 's -smoothed version , by a Stokes'-theorem identity relating a ball integral to a sphere integral.
for any fixed , any first order algorithm with full-information bound , and any sequence of estimators with .
The FKM algorithm (Algorithm 23: play , form , update on the shrunk set ) with , guarantees
Theorem 6.9's rate is strictly worse than the rate of full-information online gradient descent (Chapter III) — this gap, not a shared rate, is the chapter's real content: bandit feedback provably costs regret, and the FKM algorithm is the historically first algorithm to pin down how much, via the clean two-part reduction that later chapters' improved bandit algorithms (§6.5's self-concordant-barrier method, not formalized here) all refine. Lemma 6.5 is independently reusable: it is a template, quantified over an arbitrary first-order algorithm and an arbitrary unbiased-estimator family, not tied to the sphere-sampling construction that instantiates it for Theorem 6.9. No prior art was found on the platform for bandit convex optimization, gradient-free methods, or Frank–Wolfe-style estimators; this mission's three items formalize the standard textbook account fresh.
Lemma 6.5's proof is a martingale-style argument: it introduces auxiliary deterministic functions (where ) whose gradient at is exactly , applies 's full-information bound to the 's (a genuinely random cost sequence, since is random), and then takes expectations, using unbiasedness () to show and for the fixed comparator . This requires a genuine filtration and conditional expectation, not merely an unconditional expectation, since and are themselves random and adapted to different points in the history. Lemma 6.7's proof invokes Stokes' theorem to relate to , then uses the volume ratio — a calculus fact about Euclidean balls and spheres, not itself re-derived in this mission's Lean (the identity is drafted as the statement Lemma 6.7 asserts, to be proved from Mathlib's own ball/sphere volume and divergence-theorem lemmas).
IsFirstOrderOnlineAlgorithm formalizes only the substitution property of Definition 6.4 (the
book's second bullet); the first bullet, a closure condition on the admissible family of loss
functions, is a precondition on 's domain rather than a checkable mathematical property and is
not formalized — see MODERATION_NOTES.md. SmoothedFunction (Eq. (6.4)) and
IsUniformOnUnitSphere are declared once and shared by both milestones and the goal, rather than
re-derived inline. Lemma 6.5's history is modeled by an explicit filtration 𝓕 (with x t
adapted to 𝓕 t and g t to 𝓕 (t+1)), since Lean's conditional expectation needs a concrete
σ-algebra to condition on; the book's informal "history " is exactly this
filtration once the (deterministic) 's are set aside as carrying no randomness. Kδ, the
shrunk decision set Algorithm 23 actually projects onto, is kept a separate object from K
throughout (a pitfall the chapter brief flags explicitly), and in Theorem 6.9 is
rendered as an infimum, checked non-vacuous since is nonempty and the objective is bounded
below on by the chapter's own assumption.
Not formalized: §6.5's self-concordant-barrier bandit linear optimization algorithm (starred, out of the recommended goal's scope) and Corollary 6.8's ellipsoidal-sampling generalization (a routine corollary of Lemma 6.7 the book itself derives, not independently central).
Online convex optimization (OCO) asks a learner to repeatedly pick a point in a convex set , pay a cost that an adversary reveals only after the choice is made, and be judged against the best fixed point in hindsight. Chapter III of this series formalized the simplest general-purpose answer, online gradient descent (OGD): take a gradient step, project back onto . OGD's analysis, however, is tied to the Euclidean geometry of the projection step — it treats every coordinate of alike, and its regret bound degrades badly when 's natural geometry is not Euclidean (the probability simplex under the norm is the standard example, where a Euclidean-projection algorithm's regret scales with in the dimension , while an algorithm that exploits the simplex's own geometry attains regret scaling only with ).
Regularized Follow the Leader (RFTL) is the meta-algorithm this chapter introduces to fix this: rather than fixing a specific geometry, RFTL is parameterized by an arbitrary regularization function , and its regret bound depends on only through two scalar quantities the mission makes explicit — the range of over , and a -dependent "local norm" of the gradients. Choosing to match 's geometry (entropy regularization on the simplex, for instance) recovers the sharp bounds that plain OGD cannot. RFTL and its close relative Online Mirror Descent (OMD), also introduced here, are the ancestors of essentially every regularization-based online learning algorithm in use today, including the multiplicative-weights/Hedge algorithm of Chapter I as a special case (entropy regularization on the simplex) and the exponentiated-gradient algorithm this book's own Chapter VIII reuses (Corollary 5.7, a further specialization of Theorem 5.2 this mission's Theorem 5.2 underlies). The naive "Follow the Leader" strategy this chapter opens by refuting — always play the empirically best point so far — is a natural first idea and provably fails: the book gives an explicit two-point cost sequence on which it incurs regret linear in the horizon. Regularization is the fix, and quantifying exactly how much it costs and buys is this chapter's content.
Fix a convex, nonempty decision set in a real inner product space and a sequence of convex cost functions . As in Chapter III, regret after rounds is
A regularization function is a strongly convex, smooth, twice differentiable function with a positive-definite Hessian on the interior of . Its Bregman divergence measures the gap between and its own first-order Taylor approximation:
By the mean value theorem, for some point on the segment , where is the norm induced by the Hessian ; its dual norm, denoted , is the local norm at . Writing for the local norm between consecutive iterates , the -diameter of is .
The RFTL algorithm (Algorithm 13), with step size , plays , then at every round updates
The agile Online Mirror Descent algorithm (Algorithm 14, agile version) instead maintains a dual point with , updates it by , and projects via the Bregman divergence, (with defined the same way from ). RFTL and the lazy variant of OMD coincide for linear costs (Lemma 5.5, not formalized here — it is not used by either target); the agile variant's analysis is genuinely different and is the mission's second target.
This is the mission's goal: RFTL, run with any admissible regularizer, attains a regret bound governed only by the cumulative squared local norm of the gradients and 's range over . The bound is proved via two milestones: Lemma 5.3 (regret controlled by the total "prediction drift" plus ), which in turn rests on Lemma 5.4 (a "follow-the-leader beats be-the-leader" comparison inequality, proved by induction on the horizon).
A structurally similar bound for the agile variant, included as its own goal-level item since — as the book states explicitly — its proof technique is unrelated to RFTL's, not a corollary of it.
Both targets are the book's own tightest, non-asymptotic statements: neither is weakened to an form, and the book's own further (unnumbered) corollary specializing Theorem 5.2 to a uniform local-norm bound is left out, matching this series' convention of formalizing only the numbered results.
The results themselves. Theorem 5.2 is the general regret theorem behind every regularization scheme in online learning: instantiating recovers the projected-gradient bound of Chapter III (Euclidean ), the multiplicative-weights bound of Chapter I (entropy on the simplex), and — through the exponentiated-gradient specialization (Corollary 5.7, not itself a target here) — the row-player regret bound this book's own Chapter VIII cites as "Eq. (8.1)" in its reduction of zero-sum games to regret minimization. Theorem 5.6 gives the same guarantee for an algorithm (agile OMD) that, unlike RFTL, maintains a feasible point at every round, which the book notes is preferable in the adaptive-regret setting of Chapter X.
Formalizing it. Both theorems have complete, elementary proofs in the source (no gaps, no "with high probability", no hidden regularity conditions); the mission's work is converting the analytic argument — the Bregman-divergence identity, the generalized Cauchy-Schwarz inequality bounding the drift term by the local norm, and the two induction arguments underlying Lemma 5.4 — into machine-checked statements. No formalization of RFTL, OMD, or the local-norm machinery exists on the platform (checked below); the closest Formalpedia entries state a related but distinctly narrower result.
The central obstacle is that the regularizer is a hypothesis, not a fixed function: the theorem must hold for every admissible simultaneously, so nothing about beyond its stated properties (strong convexity, smoothness, twice differentiability) may be used. A newcomer's first instinct — bound the local norm by a fixed multiple of the Euclidean dual norm — fails in general and is exactly the bound RFTL is designed to avoid needing; the whole point of the local-norm formulation is that it can be tight for regularizers (like entropy) whose Hessian is very far from a multiple of the identity. A second obstacle is Lemma 5.4's induction, which compares (a minimizer over terms) against using the minimality of at exactly the right instantiation — an argument that looks almost circular until the induction hypothesis is applied at , not at the theorem's free variable.
ranges over an arbitrary real, complete inner product space (a real Hilbert space),
matching Chapters III and IV, not a fixed . The RFTL and agile-OMD update
rules are represented relationally (IsArgMinOn), since Mathlib has no canonical argmin
operator for a general convex set — mirroring IsMetricProjection's precedent from Chapter
III. The Hessian at the mean-value-theorem's intermediate point is represented via the
second Fréchet derivative of 's gradient map (HasFDerivAt), since Mathlib has no
dedicated Hessian type; the local dual norm is then any value satisfying the resulting
existential characterization (IsLocalDualNormSq), stated once and shared by both targets.
A boundedness hypothesis on over is added to Lemma 5.3's statement to keep the
-diameter from collapsing to Mathlib's junk value for an unbounded supremum — a
condition every regularizer the book actually uses (strongly convex and smooth over a
bounded ) already satisfies, so it narrows nothing.
Trivializing formalization ruled out. A regret bound stated for an "algorithm" defined
loosely enough to include the after-the-fact optimal choice would be vacuous; IsRFTLRun
and IsOMDAgileRun instead pin down the exact history-dependent update rule of Algorithms
13 and 14 (the current gradient sequence, the current regularizer, and nothing else) as a
hypothesis, so a proof must genuinely use the specific update. Theorem 5.2 and Theorem 5.6
are kept as two separate items rather than one theorem parameterized by an algorithm choice,
since — per the chapter's own remark that their analyses are unrelated — a merged statement
would either need to branch internally on the algorithm or silently identify two genuinely
different update rules.
Reuse and prior art. OnlineConvexOpt.FirstOrder.RegretT (Chapter III, published) is
imported and reused verbatim, keeping the regret functional identical across the whole
book. Definitions specific to Chapter IV (OnlineConvexOpt.SecondOrder, not yet published)
are not imported per this series' convention that a draft cannot import another draft;
quadForm is redeclared locally instead. On the platform, BanditAlgorithm.ftrl_regret_bound,
BanditAlgorithm.mirror_descent_regret_bound, and BanditAlgorithm.ftrl_simplex_exp_weights_regret
(the Bandit Algorithms series, Chapter XII) state regret bounds for FTRL and Mirror Descent
in the linear-cost, bandit-idiom setting (a fixed linear loss at
each round, regret compared via a Bregman-divergence potential at fixed points). Hazan's
Theorem 5.2 and 5.6 are for general convex and use the book's own local-norm
object, which has no counterpart in those statements; they are read in full and are not
faithful substitutes (different hypothesis class), so this mission drafts its own,
independent items rather than reusing them.
Online decision-making problems — multi-armed bandits, contextual bandits, structured bandits, and episodic reinforcement learning — look superficially different but share a common shape: a learner repeatedly acts, observes feedback, and is scored by regret against the best action in hindsight. Foster, Kakade, Qian and Rakhlin's Foundations of Reinforcement Learning and Interactive Decision Making (Foster & Rakhlin, arXiv:2312.16730v1) develops a unifying account of this shape and asks a sharper question than "does this specific algorithm work?": for a given class of possible environments, what is the best regret any algorithm can achieve? The Decision-Estimation Coefficient (DEC), introduced by Foster, Kakade, Qian and Rakhlin (2021, "The Statistical Complexity of Interactive Decision Making") and refined by Foster, Golowich, Qian, Rakhlin and Sekhari (2023), was proposed as the answer: a single real-valued complexity measure of a model class that simultaneously (i) drives a generic optimal-up-to-constants algorithm (Estimation-to-Decisions, E2D), and (ii) lower-bounds the regret of every algorithm. Item (ii) is what turns the DEC from "a complexity measure that happens to work for the algorithms we know" into a genuine characterization of statistical difficulty, in the same sense that minimax rates characterize the difficulty of estimation problems in classical statistics. This mission formalizes that lower bound.
Chapter 6 of the book (pp. 93–128) introduces Decision Making with Structured Observations (DMSO), a protocol general enough to subsume the contextual-bandit, structured-bandit and episodic tabular-RL protocols of earlier chapters. Over rounds, the learner selects a decision from a decision space ; nature draws a reward-observation pair from a fixed, unknown model , where a model maps each decision to a distribution over a reward space and an observation space . The learner has access to a model class containing (realizability). For , write for the mean reward function and for the optimal decision; regret is , exactly as in the bandit chapters, now for the general model class.
Because observations, not just mean rewards, now carry information, the DEC needs a way to measure distance between the full conditional distributions and , not just between scalars and . The chapter uses the squared Hellinger distance , one of a family of Csiszár -divergences that also includes total variation () and Kullback-Leibler () divergence. For a reference model and scale , the general Decision-Estimation Coefficient is the min-max game value
and . This mission's Lean development (FoundationsRL.GeneralDM)
formalizes discrete versions of , , for a finite outcome type, the DMSO
regret, and this DEC.
The goal is Proposition 28 (DEC Lower Bound), p. 105:
Here is the constrained DEC (§6.5.1), a variant of the offset DEC above that hard-constrains the information gain rather than subtracting it — a technical refinement needed to make the lower-bound direction go through — and the "localization condition" is a genuine hypothesis of the proposition, not a footnote. Unlike almost every other target in this series of missions, the statement quantifies over every algorithm rather than naming one: it is a genuine impossibility result. Two supporting divergence facts are included as milestones because the DEC's information-theoretic argument rests on them: Lemma 19 () and Lemma 20 (a bounded-likelihood-ratio refinement bounding in terms of ). The chapter's own matching upper bound, Proposition 26 (the E2D regret bound for the general DMSO protocol, the direct analogue of Chapter 4's Proposition 13), is included as a milestone to give the reader the matching pair the chapter presents together. Finally, Corollary 1 restates the lower bound in terms of the localized offset DEC (combining Proposition 28 with Proposition 27), included as a milestone showing the lower bound's reach beyond the constrained DEC alone.
Proposition 28 is what makes the DEC a genuine characterization of the statistical complexity of interactive decision making, rather than merely a sufficient condition for a particular algorithm family to succeed. Combined with the (uncited, technically deeper) matching upper bound for the constrained DEC — Proposition 29, stated but not proved in the book — it shows that for any finite model class, the constrained DEC is necessary and sufficient for low regret up to a factor in the localization radius: no complexity measure that is substantially different from the DEC can characterize the same problems. This is the general decision-making analogue of how minimax rates pin down statistical estimation, now for interactive protocols with adaptive feedback.
Formalizing the lower bound is new work: no result of this shape exists on the Prove2Me platform
(searches for "decision-estimation", "general divergence", "constrained DEC" and "Hellinger" — the
last of which surfaces two related-but-distinct affinity/Le Cam bounds from a different mission on
bandit lower bounds — return no faithful prior art; see MODERATION_NOTES.md). The formal
statement is the boxed proposition; the book gives a self-contained but simplified proof (two
named simplifying assumptions, §6.5.3) and cites Foster, Golowich, Qian, Rakhlin & Sekhari (2023)
for the unrestricted argument. This mission's Lean items are draft statements (:= by sorry), not
proofs; formalizing the proof itself — a two-point adaptive testing argument using the chain rule
for KL divergence and a change-of-measure step — is the open contribution this mission proposes.
The obvious first attempt is to try to prove the lower bound by exhibiting one fixed pair of hard models , as in classical two-point minimax lower bounds (Le Cam's method, Fano's inequality). This fails here because the decision-making protocol is interactive and adaptive: the algorithm's queries depend on what it has observed, so a model pair chosen obliviously (before seeing the algorithm) cannot in general be made indistinguishable to every algorithm — an adaptive algorithm can be constructed that distinguishes any two fixed models quickly by querying where they differ. The book's proof instead selects the "hard" alternative model as a function of the algorithm's own strategy (via the constrained DEC's arg max, Eq. (6.36)), so that the pair is hard specifically for the algorithm under consideration, then uses the chain rule for KL divergence plus the change-of-measure identity between the algorithm's induced distributions under and to conclude that the algorithm's realized decisions must look similar under both models — hence it cannot get low regret on both simultaneously. Every step of this argument depends on the exact game structure of the constrained DEC, not just its numerical value; a formalization that leaves as an unconstrained real parameter (rather than the actual - game with its information-gain constraint) would make the lower bound's conclusion vacuous, since the hypothesis would no longer track any actual property of .
The decision space and the outcome (reward, observation) alphabet are both taken as
finite types (Fintype); a model is a conditional probability
vector, and a reward-extraction map recovers the mean reward
. hellingerSq, totalVariationDiscrete,
klDivDiscrete specialize the book's general dominating-measure divergence formula (Eq. (6.5)) to
the counting measure on this finite type; klDivDiscrete returns an ENNReal so its
case (when is not absolutely continuous w.r.t. ) is represented honestly. The DEC, the
constrained DEC and the localized subclass are literal sInf-of-sSup/sSup-of-sSup
transcriptions of the book's min-max games — the same convention this series uses for the
Chapter-4 DEC — not opaque free real numbers, which rules out the trivializing formalization named
above.
Three deviations from this series' usual convention of pinning every constant to the value the
book's own proof derives are deliberate and disclosed. First, the numerical constant in
is explicitly called "not important" by the authors themselves
(footnote a, p. 105); it is existentially quantified (∃ c > 0) rather than pinned to a numeral.
Second — added at moderation, round 2, 2026-09-19, after the constant was found to be pinned
incorrectly — the lower bound's own multiplicative constant is also existentially quantified
(∃ c' > 0) rather than pinned to 1/20. The book's printed proof (§6.5.3, pp. 107–110) derives
1/20 (p. 110, not p. 109 as an earlier draft of this mission stated) only under two named
simplifying assumptions the theorem's hypotheses do not carry (p. 107, "Simplifications": a
class-wide bounded-curvature hypothesis, Eq. (6.34); and a bound on the unaugmented
rather than the officially-defined,
augmented this mission's decC implements). Since
augmenting either supremum's domain can only raise its value, the printed proof's bound on the
narrower, unaugmented quantity does not license a pinned 1/20 against the fully general decC
this theorem states; the book itself attributes the proof of the general statement to an external
reference (Foster, Golowich, Qian, Rakhlin & Sekhari 2023) not in this document. The existential
c' matches the book's own unpinned for Proposition 28 as printed on pp. 105–106.
Third, "any algorithm" and are formalized, as throughout
this series, without a full stochastic-process/history model: regret is a deterministic quantity
evaluated at a fixed realized decision-distribution sequence , rather than an expectation over an adaptive, history-dependent algorithm's own
randomness. Formalizing the fully adaptive, measure-theoretic version of "any algorithm" — with an
explicit filtration and expectation over the induced process law — is future work a solver
could add; the current statement is faithful to the book's deterministic-per-realization content
but not to its full generality over randomized, history-dependent strategies. The DMSO protocol
(Def_FoundationsRL_GeneralDM_Protocol) and the DEC (Def_FoundationsRL_GeneralDM_DEC) are
restated locally rather than imported from Chapter 4's mission (FoundationsRL.Structured), since
draft items cannot import another chunk's drafts; contributions extending either mission to reuse
the other's substrate once both are published are welcome.
A multistage stochastic program's exact deterministic equivalent grows exponentially with the number of periods, even when each period's random data takes only a handful of values (Chapter 9's concern was the growth in the number of realizations; Chapter 10 adds growth in the number of periods). One remedy, generalizing Chapter 8's single-period Jensen bound, is to replace the exact per-period random data by a coarser, aggregated version — conditional expectations over a partition of the history space at each stage — and solve the resulting smaller deterministic equivalent instead. This is only useful if the aggregated problem's optimal value is provably a bound (here, a lower bound) on the exact problem's, and Birge & Louveaux's Chapter 10, §10.1, Theorem 1 is exactly the statement that makes this legitimate, together with a genuinely necessary extra condition the book states explicitly two paragraphs before the theorem: "if not [i.e. if the extra condition fails], then the conditional expectation form ... may not actually achieve a bound." This mission formalizes that theorem.
The book's exact multistage stochastic linear program (Eq. 1.1, p. 418) is
min c¹x¹ + E_Ω[c²x² + ⋯ + cᴴxᴴ]
s.t. W¹x¹ = h¹, Tᵗ⁻¹xᵗ⁻¹ + Wᵗxᵗ = hᵗ (t=2,…,H, a.s.), xᵗ ≥ 0 a.s., xᵗ nonanticipative (Σᵗ-measurable),
over the exact event space Ω = Ω₁ × ⋯ × Ω_H. Given a consistent nested partition of each
Ωᵗ = Ω₁ × ⋯ × Ωₜ into finitely many blocks Sᵗ₁, …, Sᵗ_νₜ, and aggregated data (h̄ᵗᵢ, T̄ᵗᵢ) = E^{Sᵗᵢ}[(hᵗ,Tᵗ)] (the conditional expectation of the true random data over block i), the
aggregated problem (Eq. 1.2, p. 419) replaces the exact recursion by a finite tree of blocks, one
decision per block, linked to its parent block's decision. Both (1.1) and (1.2) are, structurally,
the same kind of object — a finite-tree deterministic-equivalent recourse LP — differing only in
which tree and which node data they use; this mission formalizes that shared shape once
(Tree, Instance, Feasible, obj) and instantiates it twice.
Formalized as: a shared Tree H structure (a finite node type, per-node stage, anc, and a
root), the same representation Chunk 06's Multistage.Tree uses for the exact scenario tree of
its own (different) chapter, restated here rather than imported (a draft cannot import another
chunk's draft). An Instance H n m T bundles a tree's node-varying LP data
(c, W, Tmat, h, p); Feasible/obj give its feasible set and objective. The exact
problem (1.1) is Instance H n m TFine for a fine/exact tree TFine; the aggregated problem
(1.2) is Instance H n m TCoarse for a coarser tree TCoarse, connected to TFine by an
aggregation map agg : TFine.Node → TCoarse.Node.
agg respects the tree structure (root, stage, ancestor);
W, c agree between the fine and coarse instances (up to agg);
coarse.h, coarse.Tmat are the p-weighted conditional expectations of fine.h, fine.Tmat over
each aggregation fiber;
∀ coarse nodes i,i' at the same stage sharing a "current-period outcome",
coarse.h i = coarse.h i' ∧ coarse.Tmat i = coarse.Tmat i'
⟹ zCoarse ≤ zFine
This is the mission's only formalization target: BRIEF.md records that no separately numbered
lemma precedes Theorem 1's proof in this section to serve as an independent milestone (the proof
is a direct LP-duality argument against the theorem's own hypotheses), and that Chapter 8's
Theorem 1 — the two-period case this theorem generalizes — is a cross-chapter dependency
belonging to Chunk 08's own mission, not a milestone here. milestones.yaml is accordingly empty;
see STATUS.md for the explicit accounting of what else in this chapter was considered and left
out (Theorem 3, the aggregation error bound of §10.2, an unrelated and substantially heavier
result).
Theorem 1 is what licenses every aggregation-based approximation scheme the rest of the book's
multistage material builds on: it says precisely when replacing a multistage recourse problem's
random data by within-period conditional expectations preserves a valid lower bound, and precisely
identifies the condition (aggregated nodes sharing a current-period outcome must carry identical
aggregated data) whose failure breaks the bound — a condition the book states is not decorative
("if not, then the conditional expectation form ... may not actually achieve a bound," p. 418).
Formalizing it gives Prove2Me a first structural result connecting Chapter 8's single-period Jensen
bound (Chunk 08) to genuinely multistage approximation, using the same finite-scenario-tree
deterministic-equivalent representation Chunk 06 uses for the exact nested Benders decomposition
— the two missions' shared representation choice (documented in both STATUS.md files) means a
future mission relating them formally (e.g. instantiating Chunk 06's exact tree as this mission's
TFine) has a compatible object to work with, even though neither imports the other's draft.
The theorem's proof (p. 419-420) is a direct LP weak-duality argument: given an optimal dual
solution to the aggregated problem, the book constructs a dual-feasible solution to the exact
problem attaining the same value, using precisely the "common outcome ⟹ equal aggregated data"
hypothesis to make the constructed dual solution well-defined across the exact tree's finer
structure. This is a real argument, not a citation, but it is left as sorry: formalizing the
proof would need the multistage LP duality machinery (the "multistage version of Theorem 3.13" the
book's own proof invokes, itself left as Exercise 1) that no chunk of this series has built. The
value of this mission is the faithful statement of the bound and its exact hypotheses.
(ωt−1,ωt) ∈ Stj if and only if there exist some (ω̂t−1,ωt) ∈ Stj" —
S^t_j appears on both sides of the "if and only if," where the sentence's own subject ("S^t_i
and S^t_j that have a common outcome") requires the left side to range over S^t_i. Confirmed
against a direct render of PDF page 436 (uv run --with pymupdf python), not assumed from OCR:
the PDF's own typesetting has this repetition, not an artefact of text extraction. This
formalization reads the corrected clause as "S^t_i and S^t_j project onto the same set of
period-t outcomes" and states it via an explicit label type Θ and curOutcome : TCoarse.Node → Θ, since the aggregated tree alone does not carry a literal per-period outcome
space to project onto (see Setting above — Tree records only history-node structure, not the
underlying product space Ω = Ω₁ × ⋯ × Ω_H).W, c shared exactly, not aggregated, matching the book's explicit assumption that the
recourse matrix and per-stage cost are deterministic and identical across (1.1) and (1.2)
("Wt known and not random," "ct = ct," p. 418) — formalized as direct equality hypotheses
(hW_agree, hc_agree) rather than folding W/c into the conditional-expectation machinery
that h/Tmat go through.zFine/zCoarse are hypothesis-characterized, not sInf-defined, avoiding the real
infimum's junk value 0 on an unbounded-below or empty feasible set
(reference/FAITHFULNESS_TRAPS.md trap 5) — neither tree-LP's feasible set is shown bounded or
nonempty by the hypotheses alone.p·h/p·Tmat, not h/Tmat
alone, matching the book's own E^{Sti}[·] = (h̄ti,T̄ti) read as "the fiber-sum of p·(h,T)
equals p_i·(h̄ti,T̄ti)" — the standard definition of a conditional expectation against counting
measure on a finite partition. Instance's own hp_pos (every node's probability is strictly
positive) rules out the degenerate case a bare unweighted equation would need to guard
separately (a coarse node of probability 0, which cannot occur, is what the read-back of this
theorem flags as the one case where the weighted equation would not pin down h_coarse/
Tmat_coarse themselves — moot here since hp_pos excludes it).coarse.h/coarse.Tmat
be arbitrary constants unrelated to fine.h/fine.Tmat (dropping the conditional-expectation
defining equations) would still typecheck a "lower bound" conclusion but assert nothing about
aggregation — exactly the risk BRIEF.md flags: "a formalization that treats (h̄ti,T̄ti) as
arbitrary constants rather than as conditional expectations over a partition of the scenario
space at time t loses the theorem's actual content." Both hCoarse_h/hCoarse_T (the
defining equations) and hCommonOutcome (the theorem's own extra hypothesis) are load-bearing
and present.Two-stage stochastic programs with recourse — choose a first-stage decision now, observe a random outcome , then choose a second-stage recourse decision to repair whatever left infeasible or suboptimal — are the workhorse model of the field, used for capacity planning, inventory and financial portfolio problems since the 1950s (Dantzig 1955; Beale 1955). When ranges over a finite set of scenarios, the recourse function that averages the second-stage cost over scenarios is piecewise linear and convex in , so the overall problem is itself a large linear program — but one whose constraint matrix has a scenario for every column block and can be far too large to hand to a general-purpose LP solver directly. Van Slyke and Wets' L-shaped method (1969), the subject of this mission, is the algorithm that made two-stage recourse problems with finite scenario sets practically solvable: it is Benders decomposition specialized to this block structure, alternating between a small master program over (and a scalar approximating the recourse cost) and, at each candidate , a batch of second-stage linear programs that either certify 's second-stage feasibility or supply a linear underestimate — a cut — of around . Birge & Louveaux's Introduction to Stochastic Programming (2nd ed., Springer 2011), Chapter 5 §5.1, gives the algorithm and proves its two central guarantees: a shortcut feasibility test for a special case (Theorem 1) and the algorithm's finite convergence in general (Theorem 2), which is this mission's goal.
A two-stage recourse instance consists of a first-stage feasible region for , and, for each of finite scenarios (occurring with probability ), second-stage data defining the recourse subproblem
where the recourse matrix is fixed — the same across every scenario, the case this chapter treats. is the set of for which every scenario's subproblem is feasible, and the two-stage problem is
A basis of the recourse subproblem is an injective choice of of 's columns (where is 's row count); each basis determines a simplex multiplier , and when attains the true optimum of , LP duality gives — the mechanism that turns a batch of second-stage LP solves into linear cuts on .
The L-shaped algorithm proceeds in three steps, repeated until neither applies:
Formalized as: starting from the empty cut set, there is a finite-length run of the algorithm's Step-1/2/3 transition relation, of length bounded by the total number of distinct feasibility- and optimality-cut witnesses available, ending at a state admitting no further step — at which point either the master program has become infeasible (certifying ) or its optimum is second-stage feasible, passes every fresh Step-3 test, and is optimal for the two-stage problem.
A shortcut avoiding separate feasibility LPs at Step 2: under these structural assumptions on , checking feasibility at the single componentwise-worst right-hand side certifies feasibility at every scenario simultaneously.
Van Slyke and Wets' method (and Benders decomposition more generally, of which it is the recourse-problem specialization) underlies essentially every large-scale two-stage stochastic program solved in practice, and its finite-convergence guarantee — not merely that an optimum exists, but that this specific cutting-plane procedure reaches it in finitely many outer iterations — is what makes the method a decision procedure rather than a heuristic. The proof's content is an explicit finiteness argument (the number of distinct simplex bases of the recourse subproblem and the feasibility-test LP is finite, so the algorithm cannot generate infinitely many distinct cuts before either exhausting the feasible region or converging), not a general compactness or fixed-point argument; formalizing it means formalizing the cutting-plane mechanism itself as a transition system and proving termination combinatorially, over the finite type of available bases, rather than proving only that some optimal exists.
The natural shortcut — state only "an optimal exists, or " — is not Theorem 2's actual content and is not what this mission targets: that weaker claim would already follow from being a nonempty polyhedron (or empty), with no reference to the algorithm at all, and would not require the finiteness-of-bases argument the book's proof turns on. The genuine difficulty is representing Steps 1-3 faithfully as a relation on accumulating cut sets, and pinning the termination bound to the actual combinatorial object the book cites (the finite set of bases of the two LPs the algorithm solves at each iteration) rather than to a numeral or an abstract compactness bound. A second, quieter difficulty is Step 1's own optimum: once optimality cuts exist, the master program optimizes jointly, but before the first one it optimizes alone; conflating the two (e.g. always requiring to be part of the optimum) does not match Step 1 as the book states it.
First-stage and second-stage vectors are Fin n1 → ℝ / Fin n2 → ℝ; the finite scenario set is
Fin K with probability vector p. A basis is {b : Fin m2 → Fin n2 // Function.Injective b} (m2 = the recourse matrix's row count), matching "an injective choice of columns of
"; its finiteness is definitional, from Fin m2 → Fin n2 being finite. Simplex multipliers use
Matrix.inv, whose junk value 0 on a singular matrix is never reachable in a proof because
multipliers are only ever used through an IsOptimalAt/IsFeasBasisOptimalAt hypothesis that
pins the basis to one genuinely attaining the LP's true optimum. The recourse value
is EReal-valued (reusing this series' Instance/QVal convention from Chunk 03), so an
optimality-cut witness's claimed value is compared to it by an explicit EReal cast, never by
EReal arithmetic. The algorithm's state is a pair of finite sets of witnesses recorded so far
(Finset (Fin K × FeasBasis n2 m2) × Finset (Fin K → Basis n2 m2)); Step is an inductive
relation with one constructor per Step-2 and Step-3 branch, each requiring its witness not already
recorded, and the goal states a bounded-length Step-path from the empty state to a state
admitting no further Step. This mission does not restate Chapter 3's polyhedrality fact
about as a separate lemma: the finiteness fact it is invoked for is already exposed directly
and structurally by the finite Fintype bound on the number of bases, so no additional axiom
stands in for it (see MODERATION_NOTES.md). Lemmas 3-9 and Theorem 10 of §5.2 (Regularized
Decomposition, a different algorithm) are out of scope. The trivializing formalization this
mission rules out is exactly the one named under Difficulty above: a bare existence-of-optimal-or-
infeasible- statement with no reference to Steps 1-3 or to a finite bound on the number of
iterations — such a statement would be true of any nonempty polyhedron and would not be Theorem 2.
Von Neumann introduced amenable groups in 1929 to explain the Hausdorff–Banach–Tarski paradox, and showed that the class of amenable groups contains all finite and all abelian groups and is closed under four processes: (I) subgroups, (II) quotients, (III) extensions and (IV) directed unions. Day named the smallest class with these properties , the elementary amenable groups. For fifty years these were the only amenable groups anyone could exhibit, and von Neumann's question whether every non-amenable group contains a free subgroup on two generators — whether equals the class of groups without such a subgroup — was open. (It was answered in the negative by Ol'shanskii in 1980, the year of this paper, by different methods.)
Ching Chou's Elementary amenable groups (Illinois J. Math. 24 (1980) 396–407, doi:10.1215/ijm/1256047608) gives the structure theory of that everything later relies on. Its central result is that the class can be built from finite and abelian groups by extensions and directed unions alone — subgroups and quotients add nothing (Proposition 2.2). From that description three things follow: periodic elementary amenable groups are locally finite, so the periodic non-locally-finite groups of Golod and Novikov–Adjan show (Theorem 2.3); a finitely generated simple elementary amenable group is finite (Corollary 2.4); and Wolf's conjecture holds in : a finitely generated elementary amenable group is almost nilpotent or has exponential growth (Theorem 3.2, extending Milnor and Wolf's theorem for solvable groups). A final section introduces a packing property (P) of groups and proves it for every elementary amenable group (Proposition 4.2) and every residually elementary amenable group (Corollary 4.7).
On this platform the definition of is already published
(the bundle Chou_ElementaryAmenable, from the mission
Cannon–Floyd–Parry: Thompson's group F and the simplicity of its commutator subgroup),
together with the theorem that Thompson's group is not elementary amenable
(Theorem 4.10) and, from Brin and Squier, that has no free subgroup on two
generators (CannonFloydParry.no_free_subgroup_of_rank_two). This mission formalizes
Chou's paper on top of that definition.
The class and its constructible core. Chou.ElementaryAmenable G is an inductive
predicate on groups: finite groups and abelian groups are in the class, and the class is closed
under isomorphism, subgroups, quotients, extensions and directed unions of subgroups; each rule
is a constructor of the published bundle Chou_ElementaryAmenable, where it is stated precisely. Chou builds the hierarchy
by transfinite recursion, applying only extensions and directed unions to the finite and
abelian groups, and proves that is closed under subgroups and
quotients, hence equals . The union is realised here without
ordinals, as the inductive predicate Chou.Constructible, whose constructors are of_finite,
of_commGroup, of_mulEquiv, extension and directedUnion; Chou's transfinite induction
over becomes structural induction over a derivation, with the same case analysis.
Periodic and locally finite groups. A group is periodic if every element has finite order
(Mathlib's IsMulTorsion) and locally finite if every finitely generated subgroup is finite
(Chou.IsLocallyFinite). Day's class is Chou.NoFreeSubgroupOfRankTwo: no homomorphism
from the free group on two generators into is injective.
Growth. For a finite generating set of , Chou.wordBall S n is the set of products
of at most factors, each in or with inverse in . has exponential growth if for
some finite generating set the ball of radius has at least elements for some
and all ; it is exponentially bounded if for some finite generating set and every
the balls are eventually smaller than . Chou works with for products of exactly
elements of a finite generating set ; for symmetric and containing the identity the
two agree, and Wolf's observation that the growth type is independent of the generating set is
one of the milestones. "Almost nilpotent" is Mathlib's Group.IsVirtuallyNilpotent: a
nilpotent subgroup of finite index. A free subsemigroup on two generators means two elements
such that distinct positive words in are distinct in
(Chou.HasFreeSubsemigroupOfRankTwo).
Packings. A pair of subsets is a packing of if is a
bijection (Chou.IsPacking), and has property (P) if every finite
subset lies in a finite for which some is a packing (Chou.HasPackingProperty).
is residually elementary amenable if every survives in some elementary amenable
quotient (Chou.ResiduallyElementaryAmenable).
The goal is Chou's description of the class, Proposition 2.2 (b) (p. 397): “ is the smallest
class of groups which contains all finite groups and all abelian groups and is closed under
processes (III) and (IV).” It is stated as the equivalence ElementaryAmenable G ↔ Constructible G.
The milestones follow the paper's order.
Section 2. Proposition 2.1 in two halves — the constructible groups are closed under subgroups and under quotients — which is the whole proof of the goal. Theorem 2.3: periodic elementary amenable groups are locally finite; and its consequence that is nonempty. Corollary 2.4: finitely generated simple elementary amenable groups are finite.
Section 3. Lemma 3.1 (an extension of almost nilpotent by almost nilpotent is almost nilpotent or of exponential growth), Theorem 3.2 and Rosenblatt's sharpening Theorem 3.2′, together with the facts Chou uses on the way: a finite-by-nilpotent group is almost nilpotent; a free subsemigroup forces exponential growth; Wolf's independence of the generating set; and Milnor's existence of the growth rate, in the form "exponentially bounded means not of exponential growth".
Section 4. Property (P) for finite groups, for , for finitely generated abelian groups; Lemma 4.1 (directed unions and extensions preserve (P)); Proposition 4.2 (every elementary amenable group has (P)); Lemma 4.6 (a) and Corollary 4.7 (residually elementary amenable groups have (P)); and the free groups.
Chou's Section 3 rests on results the paper cites rather than proves, none of which is in Mathlib. They are stated here as milestones in their own right, so that the dependence is visible and each is a well-defined target: the Milnor–Wolf theorem (a finitely generated solvable group that is exponentially bounded is almost nilpotent); M. Hall's theorem that a finitely generated group has finitely many subgroups of each finite index; that finitely generated nilpotent groups are finitely presented and that a group with a finitely presented subgroup of finite index is finitely presented; Milnor's Lemmas 1–2 in the form Chou states on p. 400 (in a finitely generated exponentially bounded group, a normal subgroup with finitely presented quotient is finitely generated); and Rosenblatt's variant of Lemma 3.1. Section 4 needs one more: free groups are residually finite. Lemma 3.1 and Theorems 3.2, 3.2′ can be closed only once these are; every other milestone is provable from Mathlib and the published library.
Two remarks on Theorem 2.3. Chou's witness for is a periodic group that is not locally finite (Golod; Novikov–Adjan), whose existence is not formalized. The platform already holds a different witness: Thompson's group is not elementary amenable (Cannon–Floyd–Parry, Theorem 4.10) and has no free subgroup on two generators (Brin–Squier); both are published and proved, and the milestone is proved from them. The inclusion itself is von Neumann's theorem that amenable groups contain no free subgroup of rank two, which passes through the definition of amenability and is not part of this mission.
The ordinal-indexed hierarchy and the remark that it stabilises at some (Proposition 2.2 (a)) are replaced by the inductive predicate. Chou's two examples of finitely generated groups in that are not almost solvable (p. 402), the Golod–Shafarevich discussion, and Lemma 4.6 (b) (ordinal-indexed normal series) are omitted. Propositions 4.3–4.5 on almost convergent sets, and Milnor's remark that exponentially bounded groups are amenable, need invariant means on ; amenability itself is the subject of Garrido I.
Given independent random variables , when does converge? Not absolutely — that question is settled by and is usually too strong. The interesting question is when the partial sums converge for almost every outcome, and here independence buys something that holds for no general sequence: convergence is not a delicate matter of cancellation but is decided, once and for all, by three numerical series.
Chapter 2 of Rick Durrett's Probability: Theory and Examples (Version 5, 2019) reaches this in section 2.5. Kolmogorov's three-series theorem fixes a truncation level , replaces each by , and asserts that converges almost surely if and only if
Three deterministic conditions on the distributions decide an almost-sure question about paths, and the answer does not depend on which is chosen. Through Kronecker's lemma this is also the route to the strong law of large numbers, which is how the chapter uses it.
Let be independent real random variables on a probability space, with partial sums . Say that converges almost surely when for almost every the sequence has a real limit; following Durrett, " converges" means exists, not that it converges absolutely.
Three tools from the same section support the theorem. Kolmogorov's maximal inequality strengthens Chebyshev from to the maximum of the whole path,
for independent, centred, square-integrable summands. From it comes the convergence criterion: if and then converges almost surely. Kronecker's lemma is the deterministic bridge to averages: if and converges then . And the Hewitt–Savage 0-1 law says that for an i.i.d. sequence every permutable event — one unchanged by rearranging finitely many coordinates — has probability or .
Both directions are asserted, as Durrett states the theorem. The truncation level is arbitrary and fixed in the statement; that the three conditions hold for one exactly when they hold for every is a consequence, not an assumption.
Kolmogorov's maximal inequality (2.5.5); the convergence criterion under summable variances (2.5.6); Kronecker's lemma (2.5.9); and the Hewitt–Savage 0-1 law (2.5.4).
The result itself. The three-series theorem is the complete answer to a question that has no complete answer without independence, and the shape of the answer is the interesting part: a pathwise, almost-sure property is equivalent to three conditions each computable from the marginal distributions alone. Each of the three does a separate job — the first says and its truncation differ only finitely often, so Borel–Cantelli lets them be exchanged; the second controls the drift of the truncated sums; the third controls their fluctuation. The theorem is also the standard route to the strong law: applying it to and then Kronecker's lemma gives , which is why section 2.5 sits where it does.
Formalizing it. Mathlib has the strong law of large numbers (strong_law_ae), both
Borel–Cantelli lemmas, and Kolmogorov's 0-1 law for the tail σ-field. It has none of the
following: Kolmogorov's maximal inequality, the almost-sure convergence criterion for random
series with summable variances, Kronecker's lemma, the Hewitt–Savage 0-1 law, or the three-series
theorem. The mission therefore contributes the whole of section 2.5, and the pieces are reusable
well beyond it — the maximal inequality and Kronecker's lemma in particular are standard tools with
no probabilistic content in the second case at all.
The maximal inequality is the step where the argument stops being routine. Chebyshev bounds and no more; controlling the maximum over the whole path needs the first passage decomposition and the observation that is measurable with respect to the first variables while is independent of them, so the cross terms vanish. That is a stopping-time argument in disguise, and it is what makes the whole section work.
The sufficiency half of the goal is then assembly: the third series and the convergence criterion give convergent, the second adds the means back, and the first plus Borel–Cantelli replaces by . Necessity is the harder direction, and Durrett does not prove it in Chapter 2 at all — he defers it to Example 3.4.12, where it follows from the Lindeberg–Feller central limit theorem. A solver attacking the goal should expect the reverse implication to need machinery from outside this section.
The Hewitt–Savage law has a difficulty of its own kind: the natural statement is about a σ-field of events on a sequence space, and the proof approximates a permutable event by cylinder events and then applies the permutation that swaps the first coordinates with the next .
Random variables are measurable real-valued functions on a probability space and independence is
Mathlib's iIndepFun. Variance is Mathlib's variance, and square-integrability is stated as
membership in where the maximal inequality and the convergence criterion need it. The
three-series theorem itself assumes no integrability: the truncated variables are bounded, so
their means and variances exist automatically, which is exactly why the truncation is there.
" converges" is formalized as convergence of the sequence of partial sums to a real
limit, not as Summable, which in Mathlib means unconditional and hence absolute convergence for
real series. This distinction is not pedantic here: condition (ii) of the theorem is convergence of
in Durrett's sense and would be a strictly stronger condition if read as
summability. Conditions (i) and (iii) are series of non-negative terms, where the two notions
agree, and are stated as Summable.
Almost-sure convergence of is "for almost every there exists a real with " — the limit is not asserted to be measurable in , and does not need to be for the statement to say what it should.
For the Hewitt–Savage law the sequence space is the countable product carrying
the infinite product of copies of one law, which is Mathlib's Measure.infinitePi, and a
permutable event is a measurable set invariant under every finitely supported permutation of the
coordinates. That is Durrett's exchangeable σ-field stated directly rather than constructed as a
σ-field object.
Contributions welcome beyond the listed items: the converse direction via Lindeberg–Feller (Example 3.4.12); the derivation of the strong law from the three-series theorem and Kronecker's lemma; the Marcinkiewicz–Zygmund law (2.5.12); and the rates of convergence of section 2.5.1.
Many hard combinatorial optimization problems — finding the maximum cut of a graph, deciding the ground state of an Ising spin system, bounding the correlation of a physical system — can be written as maximizing a bilinear form over sign vectors . Exhaustive search over sign patterns is intractable, so practitioners relax the problem: replace each sign by a unit vector in a higher-dimensional space and optimize the resulting inner products instead. This relaxation, a semidefinite program, is convex and solvable in polynomial time. The question is how much is lost in the relaxation — whether its optimal value can be far from the true, combinatorial optimum.
Grothendieck's inequality, proved by Alexander Grothendieck in 1953 in the context of Banach space theory (Résumé de la théorie métrique des produits tensoriels topologiques, Bol. Soc. Mat. São Paulo 8 (1953), 1–79), answers this for a broad class of such relaxations: replacing signs by unit vectors in an arbitrary Hilbert space changes the optimal value by at most an absolute, dimension-free constant factor. The inequality has since become a standard tool across combinatorial optimization, Banach space geometry, and (via the Goemans-Williamson algorithm for maximum cut, Section 3.6 of the source) approximation algorithms; see U. Haagerup, The Grothendieck inequality for bilinear forms on -algebras, Adv. Math. 56 (1985) for the tightest known constant, and Alon–Naor, Approximating the cut-norm via Grothendieck's inequality, SIAM J. Comput. 35 (2006), for the algorithmic connection this mission's Theorem 3.5.6 sets up.
Fix positive integers . Consider a real matrix . Say is normalized if for every choice of numbers ,
This says , viewed as a bilinear form on , has sup-norm at most . Now let be any real Hilbert space — a real vector space equipped with an inner product complete in the induced norm — and consider vectors and , each of unit norm . Replacing the scalar product by the inner product in the same bilinear form gives , a real number depending on the choice of and of the unit vectors. The question is how large this can be, uniformly over every such choice.
for every real Hilbert space and unit vectors , where is a constant depending on neither , its dimensions, nor . This mission's goal formalizes the book's own first-pass bound (Section 3.5), proved by a Gaussian truncation argument; it does not fix a numeral for , only that some absolute constant works, matching the shape of the true statement rather than a specific numeral that a sharper argument (the book's own Section 3.7 gives ) would immediately obsolete. See Formalization scope below for why this is the goal, not the sharper bound.
The result itself. Grothendieck's inequality is the single fact that makes semidefinite relaxation a provably good algorithmic strategy rather than a heuristic: whatever the true, hard-to-compute combinatorial optimum of a -valued bilinear optimization is, the tractable Hilbert-space relaxation cannot overshoot it by more than the constant . Milestone Theorem 3.5.6 makes this concrete for positive-semidefinite matrices, showing the semidefinite relaxation SDP of the integer program INT satisfies INT SDP INT — the guarantee underlying the Goemans-Williamson 0.878-approximation algorithm for maximum cut (Theorem 3.6.5 of the source, out of scope for this mission; see Formalization scope).
Formalizing it. The inequality and its two chapter milestones are proved but not previously
formalized on this platform (checked by concept search for "Grothendieck", "semidefinite",
"positive-semidefinite", and "max-cut" — no hits beyond the unrelated Grothendieck-Teichmüller
group). What remains after this mission is the sharper argument of Section 3.7
(the "kernel trick"), a separate, heavier development building on positive-definite kernels,
and full proofs of every milestone below (currently open sorry goals).
The statement of Grothendieck's inequality contains no randomness, yet every known elementary proof is probabilistic; this is itself a striking feature of the result. The obvious approach — bound directly by exploiting the normalization hypothesis on — fails because the normalization hypothesis only controls against sign vectors, and there is no way to project an arbitrary unit vector in a Hilbert space onto without losing information. The book's proof instead represents each unit vector via a scalar Gaussian random variable for a single Gaussian vector , recovering the inner products in expectation (Exercise 3.3.5); but these Gaussian variables are unbounded, so the normalization hypothesis (which bounds against bounded inputs) cannot be applied to them directly. The core technical step is a truncation argument: splitting each Gaussian variable into a bounded part and a small--norm unbounded remainder, applying the hypothesis to the bounded parts, and bounding the remainder terms by treating them as elements of the Hilbert space and invoking the very inequality being proved (Theorem 3.5.1 itself, applied with ) as a self-referential bootstrap — this is why the proof fixes as the smallest valid constant before starting, rather than building it up from scratch.
The goal and both milestones work with the real matrix and real inner product space directly;
H is required to be a complete real inner product space (NormedAddCommGroup,
InnerProductSpace ℝ, CompleteSpace), matching the book's "any Hilbert space." No
dimension bound on is imposed — the inequality's content is exactly that does not grow
with .
This mission does not formalize the sharper bound of Section 3.7, nor Theorem 3.6.5 (the 0.878-approximation guarantee for maximum cut via randomized rounding): the latter's statement quantifies over "the result of a randomized rounding of the solution of the semidefinite program," which would drag a specific algorithm into the audited statement rather than keeping it a self-contained mathematical claim (the statement/proof-separation trap this series' triage rubric flags). Grothendieck's identity (Lemma 3.6.6), the key fact behind that rounding step, is included on its own as a milestone, stated with an explicit, named random sign variable rather than an opaque "rounding procedure."
A trivializing formalization would state the goal with allowed to depend on , , ,
or — every such bound is easy (e.g. ) and carries none of the
theorem's content; the Lean statement rules this out by quantifying before every other
object. and (Theorem 3.5.6) are defined from scratch in this
chunk's namespace, using Matrix.PosSemidef from Mathlib for the positive-semidefiniteness
hypothesis (which bundles the real-symmetric condition); Mathlib has no ready-made SDP-value
construction to reuse. The sub-gaussian (Orlicz ) norm used by Theorem 3.1.1 is reused,
unchanged, from the 01-concentration mission in this series (HighDimProb.Concentration.SubgaussianNorm)
rather than redefined.
Any dataset of points can be described exactly by embedding it in for large enough — but a large is expensive: nearest-neighbor search, clustering, and streaming algorithms all scale with the ambient dimension, not with . The question that opens this mission is whether the dimension can be cut down while leaving the data's geometry — the pairwise distances between points — essentially untouched.
Johnson and Lindenstrauss answered this in 1984, while studying extensions of Lipschitz maps into Hilbert space (W. Johnson, J. Lindenstrauss, Extensions of Lipschitz mappings into a Hilbert space, Contemp. Math. 26 (1984), 189–206): points in any Euclidean space, of any dimension , can be mapped by a single linear map into a space of dimension only , distorting every pairwise distance by at most a factor of . The map does not depend on the data beyond its cardinality — a single random object works simultaneously for the whole point set with high probability. This is now one of the standard tools of randomized dimension reduction, cited across nearest-neighbor search, streaming linear algebra, compressed sensing, and machine learning pipelines that need to shrink feature dimension before a downstream algorithm runs.
Fix a probability space . A random orthogonal projection of rank in is a map , continuous and linear for each , such that almost surely is idempotent (), self-adjoint, and has range of dimension — i.e. is the orthogonal projection onto some -dimensional subspace . It is uniformly distributed in the Grassmannian (written ) when its law is rotation invariant: for every orthogonal transformation of , the conjugated map has the same law as . Conjugating a projection by is exactly the projection onto the image of its range under , so this says the law of the random subspace is invariant under the full orthogonal group — the operational definition Vershynin himself uses for a "uniformly distributed" random subspace, since no coordinate-free formula for such a subspace's law is given directly.
A companion notion drives the proof: a random vector is uniform on the Euclidean sphere of radius , , when it lies on that sphere almost surely and its law is likewise rotation invariant. And a real random variable is sub-gaussian with sub-gaussian () norm , the standard non-asymptotic measure of how light-tailed 's distribution is (a bounded or Gaussian random variable has finite norm; the tail probability then decays at least as fast as ).
for every finite , every , and every random orthogonal projection of rank uniformly distributed in . The universal quantifier over pairs sits inside the single probability event — this is the union-bound content that makes the statement a genuine simultaneous guarantee for the whole point set, not a restatement of the single-vector lemma below for one fixed pair. Both constants are the book's own unnamed absolute constants, never depending on , , , or ; this is the weakest stable form of the claim (no numeral is hard-coded for or ), matching the book's own statement exactly.
The lemma gives a universal, data-oblivious dimension-reduction guarantee: the target dimension depends only on the number of points and the desired distortion, never on the ambient dimension or on the geometry of the specific point set. This is what makes it usable as a black-box preprocessing step ahead of an algorithm whose cost scales with — the projection is drawn once, without looking at the data, and works with high probability for every pairwise distance simultaneously. The bound is also known to be essentially optimal in : Alon (Problems and results in extremal combinatorics, Discrete Math. 273 (2003)) showed a lower bound of on the target dimension, so the dependence cannot be removed.
The theorem itself has been proved for decades and admits several proof strategies (this book's route through Lipschitz concentration on the sphere; the original volume/measure-concentration argument; later "sparse" or structured variants of the projection for faster computation). This mission formalizes the classical dense-Gaussian-projection proof route as Vershynin presents it, building the sphere-concentration engine (Theorem 5.1.4) and the single-vector projection lemma (Lemma 5.3.2) that the union-bound argument for the goal rests on. No machine-checked formal proof of this chain is known to exist on the platform prior to this mission (see Formalization scope below); what is contributed is the statement infrastructure — the goal and its two direct supporting lemmas, stated with explicit, unpinned absolute constants — for solvers to close.
The natural first idea — bound the distortion of a single fixed vector under a random projection, then take a union bound over the pairwise differences — is exactly the strategy Lemma 5.3.2 and the goal use, but it does not by itself explain why the single-vector concentration bound (Lemma 5.3.2(b)) holds with the stated sub-gaussian-type tail. That bound is not elementary: it reduces to a uniform concentration statement for an arbitrary Lipschitz function of a uniformly random point on a high-dimensional sphere (Theorem 5.1.4), since , viewed as a function of a rotated copy of , is a -Lipschitz function on the sphere. Proving that every Lipschitz function concentrates — not just linear ones, for which sub-gaussianity was already established in Chapter 3 — needs a genuinely different tool: comparing the sub-level sets of an arbitrary Lipschitz function to spherical caps via an isoperimetric inequality on the sphere. This geometric input is what makes the concentration phenomenon behind Johnson-Lindenstrauss a dimension-free fact rather than a special property of coordinate projections.
is a Finset of points in EuclideanSpace ℝ (Fin n), matching "a set of points"; is
read off as X.card. The random subspace is represented throughout by the
orthogonal projection onto it (IsUniformProjection), following the book's own statements,
which are phrased in terms of rather than ; the scaled map of the goal is
written Real.sqrt (n/m) • P ω applied to x - y, using linearity of to realize
. Both "uniform on the sphere" and "uniform in the Grassmannian" are defined
operationally by rotation invariance of the underlying law, since Mathlib has no ready-made
normalized surface measure on a general-radius Euclidean sphere or Haar-measure construction on
the Grassmannian/orthogonal group to build a canonical uniform object from; rotation invariance
uniquely determines the corresponding measure among those supported on the relevant set, so the
operational and constructive definitions coincide extensionally. Every "absolute constant" in the
book ( in Theorem 5.3.1's sample-complexity hypothesis, in every failure-probability bound,
and the sub-gaussian constant of Theorem 5.1.4) is existentially quantified ahead of the
dimension, sample size, and every other object, and pinned to no numeral — a formalization that
hard-coded a specific numeral for any of these would be invalidated by the next sharper constant
in the literature and would not match what the book actually proves.
A trivializing formalization is one that states the conclusion for a single fixed pair rather than universally over all pairs inside one event; that would collapse the union-bound content that makes this a dimension-reduction statement for a whole point set (with points), rather than a restatement of the single-vector Lemma 5.3.2(b). This mission's goal statement is built to rule that out explicitly (see Formalization targets above).
Reusable infrastructure: subgaussianNorm (the Orlicz norm, restated per Vershynin
Definition 2.5.6) and the rotation-invariance idiom for "uniformly distributed" random geometric
objects are of independent interest to any later chapter needing sub-gaussian random vectors or
random subspaces/projections (e.g. Chapters 4, 6, 7, 9, 11 of this same book series). Solvers'
contributions are welcome on: the isoperimetric inequality on the sphere and its use to prove
Theorem 5.1.4 (the mission's hardest open leaf); the coordinate-projection computation underlying
Lemma 5.3.2(a); and the concentration-plus-union-bound argument closing the goal from the three
supporting lemmas.
A recurring question in economics and operations research is: when a decision problem depends on a parameter, does the optimal decision move monotonically as the parameter changes? A firm's optimal input mix as a price rises, a consumer's optimal consumption bundle as income grows, a Cournot firm's optimal output as a rival's output changes — in each case one wants "more of the parameter implies (weakly) more of the optimum" without assuming convexity, differentiability, or a unique optimizer. The classical tool for such comparative statics questions is the implicit function theorem, which needs smoothness and a nondegenerate Hessian and breaks down the moment the optimum is not unique or the objective is not differentiable. Topkis [1978] showed that a purely order-theoretic condition — supermodularity of the objective jointly in the decision variable and the parameter — is sufficient on its own, with no smoothness, uniqueness, or convexity assumed at all, and Milgrom and Roberts [1990a, 1994] later showed this lattice-theoretic approach subsumes and strengthens the classical monotone-comparative-statics results in economics. This mission formalizes the two central results this book calls "Topkis's theorem" (Theorem 2.8.1 and Theorem 2.8.2), together with the structural fact about maximizers of a supermodular function (Theorem 2.7.1) that both rest on, and the strengthening to strictly ordered optimal selections (Theorem 2.8.4).
Let be a lattice: a partially ordered set in which every pair
has a join and a meet . A real-valued function
is supermodular on if
for all ; this is
the same relativized notion (SupermodularOn) used, with , throughout chunk I of
this series.
Now let also be a partially ordered set (the parameter set), and let be a real-valued function of the pair . has increasing differences in if, for every in , the map is monotone (order-preserving) in ; equivalently, the marginal gain from raising is itself increasing in . Replacing "monotone" with "strictly monotone" gives strictly increasing differences. To compare the resulting sets of optimizers rather than single points, this mission reuses the induced set ordering from chunk I: for , holds when and for all , .
Let and be lattices, let be a sublattice of the product lattice , and let be the section of at . If is supermodular on (jointly in the pair ), then
is increasing in , with respect to , on .
With increasing in (with respect to ), supermodular in for each fixed , and having increasing differences in on , the same conclusion — increasing in — holds. Theorem 2.8.2's joint-supermodularity hypothesis on a sublattice of automatically forces both of Theorem 2.8.1's hypotheses, so 2.8.1 is the logically weaker, more elementary statement from which 2.8.2's proof proceeds.
Under the hypotheses of Theorem 2.8.1 but with strictly increasing differences, every individual optimal solution at a larger parameter value dominates every individual optimal solution at a smaller one: , , and together force — a genuinely stronger conclusion than alone gives.
A supporting result is formalized as a milestone because both goals' proofs use it directly: Theorem 2.7.1, that is a sublattice of whenever is supermodular on — the structural fact that makes it meaningful to compare optimal-solution sets with in the first place.
The result itself. Theorem 2.8.2 is the book's own headline theorem, cited throughout the rest of the monograph: it underlies the assortative-matching existence theorem (Chapter 3), monotone optimal policies in Markov decision processes (Chapter 3), and equilibrium comparative statics in supermodular games (Chapter 4) — each a later mission in this series. Its distinguishing feature relative to the implicit function theorem is that it needs no differentiability, no uniqueness of the optimizer, and no interiority: it applies equally to discrete decision problems (integer programming, combinatorial selection) and continuous ones.
Formalizing it. Nothing in Mathlib currently states a parametric monotone-comparative-
statics result of this shape: the closest neighboring material (order-preserving maps,
MonotoneOn, lattice structures) supplies only the vocabulary, not the theorem. This
mission is the first formalization of Topkis's theorem on this platform and introduces
the increasing-differences vocabulary (IncreasingDifferencesOn,
StrictlyIncreasingDifferencesOn) that later missions in this series (matching, MDPs,
supermodular games) reuse directly.
The natural first idea — differentiate in , set the gradient to zero, and use the implicit function theorem on the resulting first-order condition — fails immediately because nothing here is assumed differentiable, and need not be a single point. The correct argument instead compares two arbitrary elements , directly through the supermodularity inequality applied to the pair against (a chain of inequalities Topkis calls "Lemma 2.8.1"), using increasing differences only to move the parameter from to inside that chain — at no point is a derivative, a selection function, or an interior point used. A second subtlety is that "increasing" in the conclusion is with respect to the induced set order , not a claim that some selection is monotone: proving the stronger, pointwise-ordered conclusion (Theorem 2.8.4) genuinely needs the strict form of increasing differences, not merely increasing differences plus an extra hypothesis.
and are kept as abstract Lattice/PartialOrder types throughout, matching the
book's own generality — Theorem 2.8.1's and 2.8.2's /
corollary via second partial derivatives (discussed in the book's prose immediately after
Theorem 2.8.2, p. 77) is not itself a numbered theorem and is not formalized here.
Supermodularity, increasing differences, and strictly increasing differences are each
formalized as a single relativized definition (SupermodularOn f S,
IncreasingDifferencesOn f S, StrictlyIncreasingDifferencesOn f S) so the same
declaration expresses both "supermodular on the whole lattice " (used by Theorem 2.7.1
and Theorem 2.8.1's per- hypothesis) and "jointly supermodular on a sublattice of
" (Theorem 2.8.2) — a formalization that instead only ever supermodularized
for fixed would collapse Theorem 2.8.2's genuinely joint hypothesis into
a restatement of Theorem 2.8.1, which is exactly the trivialization this mission's chunk
brief warns against. is written out as the set
of that dominate every other element of under , and every
conclusion is stated only for pairs at which both argmax sets are assumed
nonempty — matching the book's own restriction to , since holds
vacuously whenever either side is empty. This mission depends on chunk I's
InducedSetOrder; it introduces no reusable infrastructure beyond its own three
definitions, which later missions in the series (matching, MDPs, supermodular games) are
expected to import directly rather than redefine.
This mission formalizes §4 of Cannon, Floyd and Parry's Introductory notes on Richard Thompson's groups, together with the definition of Thompson's group from their §1. The goal is their Theorem 4.5: the commutator subgroup is simple.
In the 1960s Richard Thompson defined three groups, now written , and , whose properties have kept them in use ever since as a source of examples at the edge of what groups can do. is the smallest of the three and the least understood. It is finitely presented (§3 of the source) and torsion-free, it has no free subgroup of rank two, and whether it is amenable — whether it carries a finitely additive left-invariant probability measure defined on all its subsets — is open. Cannon, Floyd and Parry record (§4, p. 227) that Geoghegan raised the question and conjectured in 1979 both that contains no non-Abelian free subgroup and that is not amenable.
That question is what makes worth pinning down precisely. Write for the class of
amenable discrete groups, for the elementary amenable ones, and for the groups with
no free subgroup of rank two. That was noted by
Day and follows from
von Neumann; whether it is strict is the von
Neumann–Day problem. It is: Olshanskii proved in a 1984 ICM address and
Gromov gave an independent proof — but by
examples that are not finitely presented. Brin and Squier proved in 1985 that , and
is not elementary amenable (Theorem 4.10 of the source, CannonFloydParry.not_elementaryAmenable_F). So
is a finitely presented group in if it is amenable and in
if it is not — a question with no other finitely presented candidate.
Call a real number dyadic if it has the form with and .
Thompson's group , as §1 of the source defines it, is the set of piecewise linear homeomorphisms of the closed unit interval onto itself that are differentiable except at finitely many dyadic rationals, and whose derivatives, where they exist, are powers of . Since those derivatives are positive, every element preserves orientation, so the elements of are increasing. Composition of two such maps is again one, and so is the inverse of one, so is a group.
The formalization calls such a map piecewise linear over the dyadics, and defines as the subgroup generated by those maps — so that closure under composition and inverses is a theorem rather than part of the construction, as the source has it. What the model fixes rather than derives is under Formalization scope below.
Two particular elements generate it. Write
An element of is trivial near if it fixes every point of some interval , and trivial near if it fixes every point of some . The support of is the set of points of that moves. The commutator convention throughout is , and denotes the commutator subgroup.
This is the capstone of §4: it says the commutator subgroup has no normal subgroup other than itself and the trivial one. It is the goal because the rest of the section feeds it — both halves of Theorem 4.1, Theorem 4.3, and both supporting lemmas below are consumed by its proof.
So has no interesting proper quotients at all. With the first part of Theorem 4.1 this forces every nontrivial normal subgroup of to contain .
That the piecewise-linear maps are already closed under composition and inverses, so that consists of exactly those maps; a transitivity lemma on dyadic partitions of ; the fact that the subgroup of elements supported in a dyadic interval of dyadic length is isomorphic to itself; triviality of the center; that contains no non-Abelian free group; and that admits a total order invariant under multiplication on both sides.
What the results give. Theorem 4.1 identifies concretely — a subgroup defined by a global algebraic condition turns out to be cut out by local behavior at the two endpoints — and computes the abelianization, making the pair of endpoint slopes a complete invariant of modulo commutators. Theorem 4.3 and the simplicity of together determine the whole normal subgroup lattice: every normal subgroup of is trivial or contains . That lattice is the input to the elementary-amenability argument.
What formalizing adds. All of these are proved in the source; none is in Mathlib, which has no piecewise-linear homeomorphism API and no Thompson group. Four of the milestones are proved as part of this proposal: that the piecewise-linear maps form a subgroup, that elements of permute the dyadic rationals, that embeds in the group Brin and Squier work with, and the absence of a free subgroup of rank two, which follows from the already-formalized Brin–Squier theorem via that embedding. The rest are open. The piecewise-linear machinery built along the way — local affineness, dyadic-breakpoint bookkeeping, extension by the identity — is reusable for , for , and for the wider family of piecewise-linear homeomorphism groups.
The obvious approach to the goal is to argue that a normal subgroup of containing a nontrivial element must be everything, by conjugating that element around. It fails on its own: an element of is pinned down only by being trivial near the two endpoints, and one still has to manufacture — inside , not merely inside — an element carrying a prescribed pair of neighborhoods into those. That construction is what the dyadic-partition transitivity lemma supplies, and it is where the combinatorics of dyadic subdivision enters.
The second difficulty was that the source proves §4 using the tree-diagram normal form of §2.
That section is now formalized in its own mission, Cannon–Floyd–Parry §2: tree diagrams and the
normal form (mission ffd1e4ea-9f9a-4cb6-8419-78e70f2545e8), all of whose milestones are proved.
Corollary 2.6 — milestone 5 here, the same theorem object — is closed from there, and Theorem
2.5 (represents_word_exponents) and the normal form (existsUnique_normalForm) are available to
a solver attacking Theorem 4.3, so the source's argument can now be followed. A solution file
imports only definitions, so whatever it uses from §2 must be reproved inline; the §2 solutions
are public and written to be reused that way. The piecewise-linear route — dyadic-partition
transitivity, Lemma 4.4 and Theorem 4.1 — remains an alternative, and is what Theorem 4.5's own
argument uses.
The unit interval is as a subtype, and an element of is an order isomorphism of it, so orientation preservation is built into the representation rather than derived — faithful to the source's set, but assuming one sentence CFP prove. Piecewise linearity is stated as: there is a finite set of dyadic reals such that the map is affine, with slope a power of two, on every closed interval whose interior misses . Intercepts are not required to be dyadic — that is derived by induction along the breakpoints, not part of the definition.
The definition is not vacuous: and of Example 1.1 are constructed explicitly, and that is not the trivial group is one of the milestones below — so no statement here is satisfied by the trivial group. In particular the goal, which asserts simplicity and therefore nontriviality, is not trivially false.
A companion definition places the same data on the real line, each element extended by the identity outside ; that line realisation is what the bridge statement connects to Brin and Squier's group.
Write the primes in increasing order, take the absolute differences of consecutive entries, take the absolute differences of the resulting row, and repeat. Every row produced this way appears to begin with :
Gilbreath's conjecture asserts that this never fails. The observation is due to Norman L. Gilbreath (1958), who rediscovered a statement already published by François Proth in 1878 together with an argument that is not accepted as a proof. It is attractive because it is elementary to state and because it is one of the few statements about the primes whose difficulty is not visibly analytic: it concerns the combinatorics of iterated differences rather than the distribution of primes directly.
Timeline.
No proof is known.
Let be the increasing enumeration of the prime numbers, indexed from . Define the rows of the Gilbreath triangle by
Thus is an infinite sequence of natural numbers for every , row is the sequence of primes, row is the sequence of prime gaps , and each later row is the sequence of absolute differences of consecutive entries of the row above it. Only the leading entry of each row is at issue.
More generally, for an arbitrary sequence write and for the -fold iterate, so that .
This is the conjecture in its standard form: every row after the row of primes begins with . It fixes no constants and no ranges, so no computational advance can invalidate it.
The milestone list collects the statements that a proof, or a further computational verification, would be built from: the two low-level structural facts about the triangle (row is the gap sequence; from row on, the leading entry is odd and all later entries are even), a finite verification of the first rows, and the two statements underlying Odlyzko's method — the propagation lemma for an arbitrary sequence beginning and continuing in , and the reduction of the conjecture to the existence, for each row index, of an earlier row with a long enough block of entries in .
The result itself. The conjecture is not known to imply other open statements about the primes, and its interest lies elsewhere: it is a test case for how much of the fine structure of the prime sequence is forced by coarse information. The propagation mechanism shows that the conjecture for a given row index follows from purely local data about an earlier row, and that mechanism is what every verification to date has relied on. A proof would have to show that such blocks of entries in always appear early enough, which is a statement about the density of small prime gaps in disguise.
Formalizing it. Nothing here is currently formalized: Mathlib has the prime
enumeration (Nat.nth Nat.Prime) and the basic facts about it, but
not the iterated-difference triangle nor any of its properties. This mission
contributes the definition of the triangle, the structural facts about its rows, and
a machine-checked version of the reduction step that all computational work on the
problem uses. The goal theorem itself is open — the milestones are known mathematics,
and each is provable with current tools, while the goal is not.
The obvious attack is induction on the row index: to see that it suffices to know that and . But controlling requires controlling and , and so on: the invariant that closes is not "the row begins with " but "the row begins with and its next entries lie in ", and each application of the difference operator consumes one entry of that block. So a finite block of good entries only carries the conclusion a finite number of rows further down, and the conjecture needs such blocks to keep reappearing forever, arbitrarily far down the triangle. Nothing is known that produces them.
A second warning, due to Hallard Croft: the property is not specific to the primes. Sequences that start with , continue with odd numbers, and have gaps that are not too large empirically exhibit the same behaviour, so any proof that uses only such coarse features would prove a much more general statement — and conversely, an argument exploiting deep properties of primes is likely to be proving the wrong thing.
Rows are total functions , defined for every index, and the
whole triangle is a single family indexed by the row number. Differences are taken as
Int.natAbs of a difference computed in , so truncated natural
subtraction never occurs; the one place where -subtraction does appear is
the milestone identifying row with the gap sequence, where the subtraction is
justified by monotonicity of .
Primes are indexed from via Mathlib's Nat.nth Nat.Prime, so ; rows are
indexed with row the primes, and the goal quantifies over all in the
form d (k + 1) 0 = 1, with no upper bound and no extra hypothesis, so no vacuous or
finitely-truncated reading of the goal is available. The general difference operator
is stated for arbitrary sequences , which is what makes the
propagation lemma usable as a black box, and reusable beyond this mission.
A complete development needs no analytic input for the milestones: Mathlib's
Nat.nth, Nat.prime_nth_prime, Nat.nth_prime_zero_eq_two and the strict
monotonicity of the prime enumeration suffice. Contributions that would extend the
mission beyond its current list: a formal version of a concrete computational
verification (checking that the leading entries of the first rows are for an
well beyond the hand-checkable range), and formalizations of the general
statement for non-prime sequences of the Croft type.
The Riemann hypothesis (RH) asserts that every zero of the Riemann zeta function in the strip has . One of the few reformulations that turns RH into a positivity statement, rather than a statement about the location of points, goes back to A. Weil (1952): the explicit formula expresses a sum over the zeros of as a sum of local contributions over the places of , and RH is equivalent to the resulting functional being positive on elements of the form .
Connes' 1999 programme paper Noncommutative geometry and the Riemann zeta function takes this reformulation as its endpoint. It builds a geometric framework — the adele class space carrying an action of the idele class group — in which the explicit formula appears as a Lefschetz formula, the zeros of -functions appear spectrally, and the paper's concluding assertion (§3, p. 22) is that the validity of the global trace formula implies, and is in fact equivalent to, positivity of the Weil distribution, i.e. RH for all -functions with Grössencharakter.
This mission formalizes the arithmetic core of that endpoint in its simplest instance: the global field with trivial Grössencharakter, so that the -function is itself. Concretely it asks for (i) the Riemann–Weil explicit formula for in the shape of Connes' equation (11), and (ii) both directions of the equivalence between positivity of the resulting Weil distribution and RH.
A rough timeline of the statements involved: Riemann (1859) gave the first explicit formula; von Mangoldt (1895) proved it rigorously; Weil (Sur les "formules explicites" de la théorie des nombres premiers, 1952) extended it to all global fields and isolated the positivity criterion; Bombieri (Remarks on Weil's quadratic functional in the theory of prime numbers, 2000) studied the associated quadratic functional in detail; Connes (1996–1999) gave the trace-formula interpretation formalized in part here.
All objects live on the group , the module of the idele class group of , written additively through , .
A test function is a map that is and has compact support (IsTest).
Its transform is
which is Connes' in the coordinate , shifted by so that is the variable of (mellinHat). On the critical line, is the ordinary Fourier transform.
The involution is , i.e. (starInv), and convolution is (conv).
The Weil distribution of a test function collects the pole terms, the finite places and the archimedean place:
where is the von Mangoldt function and (weilDistribution, with the three pieces named mellinHat, primeSum, archTerm). The middle sum is Weil's contribution of the finite places , the last integral the contribution of the real place.
The spectral side is
the sum over the zeros of with , each counted with its multiplicity (zeroSum, IsCriticalZero, zeroMult).
This is the direction that yields RH, and it is the weakest form of the endpoint of the paper: it fixes no rate, no test-function normalization beyond , and no numerical constant.
with the sum over zeros asserted to be (unconditionally) summable.
Together with the goal this is the equivalence asserted on p. 22 of the paper, in the case , trivial Grössencharakter.
The -identity on the critical line, and the fact that is again a test function.
Weil's positivity criterion is one of the standard equivalent forms of RH, and the only one in which the arithmetic input (the primes, through ) and the archimedean input (the -factor) enter as separate, explicitly computable local terms. Formalizing it produces a machine-checked bridge between the zeros of and prime sums: the explicit formula milestone is the reusable object here, since essentially every analytic application of zeta zeros — zero-density estimates, prime-counting error terms, pair-correlation statistics — is an instance of it.
Status honesty: neither RH nor the positivity statement is known; the explicit formula and both implications relating positivity to RH are classical theorems, proved but not, as far as the catalog shows, formalized in Lean. Mathlib currently provides , its functional equation, the von Mangoldt function and , but no explicit formula of any kind. What this mission adds on top of the paper is therefore the formal proof of known results, not new mathematics.
The obvious route to the explicit formula — integrate over a vertical line, move the contour to the reflected line, collect residues — fails to be routine at exactly two points. First, moving the contour requires control of on horizontal segments between zeros, which is where the classical proof invests most of its work; Mathlib has bounds near but nothing of this shape inside the strip. Second, the sum over zeros must be shown to converge unconditionally, which needs a zero-counting bound of Riemann–von Mangoldt type () that is not in Mathlib either.
For the goal implication, the naive idea — pick a test function whose transform is supported near a hypothetical off-line zero — is unavailable: is entire whenever has compact support, so it cannot be localized. The classical argument instead exploits the symmetry of the zero set and makes the off-line quadruple contribute a negative amount in the limit along a family of test functions.
Conventions the Lean statements commit to. Test functions are -valued on , ContDiff ℝ (⊤ : ℕ∞) (so , not analytic) with HasCompactSupport; the multiplicative group is always written additively. The transform carries the -shift shown above, so the critical line is and are the two pole terms. Zeros are indexed by the subtype and weighted by (analyticOrderAt riemannZeta s).toNat; the trivial zeros are excluded. Integrals are Bochner integrals and sums are tsum, so both take the junk value when the integrand is not integrable or the family is not summable — for that reason the explicit formula is stated as a HasSum, which carries summability, rather than as an equation between tsums. The archimedean term is written with , logDeriv Complex.Gamma, rather than as a principal value, to avoid a second regularization convention.
The goal is not trivially satisfiable: its hypothesis quantifies over a nonempty class (smooth bump functions exist), and its conclusion is RH for , so no vacuous reading is available.
Infrastructure a complete development needs, all reusable beyond this mission: growth bounds for inside the critical strip, a Riemann–von Mangoldt zero-counting bound, Fourier analysis of functions (Paley–Wiener style decay of ), and the Hadamard product / functional equation package for the completed zeta function.
Out of scope, and deliberately so: Connes' operator-theoretic trace formula (equations (41) and (45) of the paper) and the spectral realization theorem of p. 17. Both are statements about traces of operators on Hilbert space, and Mathlib presently has no trace-class operator theory to state them faithfully. The mission therefore formalizes the arithmetic side of the paper's endpoint; contributions that build the missing operator theory, or that extend the statements from to Dirichlet -functions and Hecke -functions with Grössencharakter, are welcome.
Mirror symmetry was discovered in string theory as a duality between families of Calabi–Yau manifolds, and it entered mathematics as a prediction: the generating function counting rational curves on one manifold equals a period integral of a mirror manifold. In his 1994 ICM address, Homological algebra of mirror symmetry (alg-geom/9411018), M. Kontsevich proposed that these numerical coincidences are shadows of an equivalence of categories: the symplectic geometry of should be encoded by Fukaya's -category , whose objects are Lagrangian submanifolds and whose products count pseudo-holomorphic discs, and the complex geometry of the mirror by the derived category of coherent sheaves. His Homological Mirror Conjecture asserts that the derived category built from embeds as a full triangulated subcategory of .
Kontsevich states the conjecture "in slightly vague form", because Fukaya's construction was not, and still is not, available in the generality the statement needs. He therefore closes the paper with the one instance he can compute by hand, in the section Two-dimensional tori: a return: for the flat torus , the objects are closed geodesics with unitary local systems, the products are sums over triangles in the universal cover weighted by , and their structure constants are values of the classical theta-function. He predicts an equivalence with for an elliptic curve . This instance was proved by A. Polishchuk and E. Zaslow, Categorical mirror symmetry: the elliptic curve (math/9801119). Later instances include the four-torus (Abouzaid–Smith, arXiv:0903.3065) and Calabi–Yau hypersurfaces (Sheridan, arXiv:1111.0632). None of this has been formalized.
Fix a real number , and let be the torus carrying the translation-invariant symplectic form of total area ; a region of Euclidean area in coordinates has symplectic area .
A brane consists of: a primitive vector and a point , which together determine the closed geodesic ; a grading , a real lift of the direction angle normalized so that is parallel to ; and a real constant describing a flat unitary line bundle on , whose parallel transport along a path of parameter length is . Two branes are transverse when ; their geodesics then meet in the finite set , which indexes a basis of the Floer space . All of this space sits in a single degree, the Maslov index
For three pairwise transverse branes and intersection points , , , a triangle is a triple of lifts of with parallel to , parallel to , parallel to , and positively oriented. Kontsevich's structure constant is
the coefficient of in . On the complex side, denotes the complexes of -modules with bounded, coherent cohomology.
For every there exist a smooth proper curve over , an assignment of an object of to each brane, and isomorphisms
with for , carrying the products to composition in whenever .
Existence of the Fukaya -category of the torus; finiteness of with points; the Maslov relation ; together with associativity of up to coboundary; the degeneration of an -category with to a differential graded category; the theta-function shape of the structure constants; and their associativity equation.
The conjecture reorganizes mirror symmetry: the numerical predictions compare two elements of an uncountable set of power series, whereas the homological statement compares two objects in a countable set of triangulated categories, and the numerical statements are meant to follow from it. The torus case is the smallest instance in which every ingredient — Lagrangian branes, Maslov grading, disc counts, theta functions, and coherent sheaves on an elliptic curve — is present and computable, so it is the natural first target.
What this mission adds beyond the literature is machine-checked mathematics where none exists. Mathlib currently has no symplectic manifolds, no Lagrangian Floer theory, no Fukaya categories, and no -categories; it does have schemes, sheaves of modules, and derived categories of abelian categories. The mission supplies the missing layer and the torus model, and asks for the comparison theorem. The definitions, the derived category with coherent cohomology, and the theta-function estimates are reusable outside this mission.
The obvious route — "transport the Polishchuk–Zaslow proof" — stalls at the point where the two sides are compared. Establishing that the triangle sums converge and equal theta-function values is analysis that Mathlib supports; producing an elliptic curve as a scheme with prescribed parameter, computing -groups between the mirror sheaves, and matching all products simultaneously is not currently supported by any library. A second difficulty is bookkeeping: gradings, Maslov indices and shifts must line up, since the product of two morphisms is nonzero only when , and the same numerical condition controls which triples of branes bound triangles at all.
Conventions committed to in Lean. An -category is encoded as a single graded module with morphism components and products given by a map on lists, of degree , with , and Stasheff signs in the bar-construction normalization; is " then ". Triangles are normalized by requiring the first vertex to lie in , which picks exactly one representative in each -orbit; only positively oriented triangles are counted; sums are tsums, so convergence is part of the work. The hom-space isomorphisms in the goal are required to be additive, not a priori -linear, because the derived category of -modules is not equipped with a -linear structure in Mathlib; the required compatibility with the structure constants pins down the algebra anyway. The goal asks only for the existence of a smooth proper curve over ; the paper's further prediction that has parameter is deliberately left out of the statement.
The goal is not trivially satisfiable: the intersection set of two transverse branes is nonempty, so the required isomorphisms force the corresponding -groups to be nonzero of the right size, in the right degree, with the prescribed products.
The general conjecture, for an arbitrary symplectic manifold with , is not stated here, and deliberately so: without symplectic manifolds and Floer theory in Mathlib, any general statement would have to take the Fukaya category as an unconstrained parameter, which would make it either vacuous or false. Building that infrastructure — symplectic manifolds, graded Lagrangian branes, Floer cohomology, twisted complexes over an -category and their triangulated structure — is the natural way to extend this mission, and such contributions are welcome.
Before any geometry of surfaces can be done, one has to say what a surface is, in a way that supports calculus: a subset of that is locally the smooth, non-degenerate image of an open piece of the plane. Every statement in the later theory — the first and second fundamental forms, the Gauss map, curvature, geodesics — is written in local coordinates, and is therefore meaningful only once one knows that the answer does not depend on the coordinates chosen. That independence is the content of the change-of-parameters theorem, which is what makes "differentiable function on a surface" and "geometric quantity of a surface" well-defined notions.
The reference for this mission is Manfredo P. do Carmo, Differential Geometry of Curves and Surfaces, 2nd edition (Dover, 2016), §2-2 "Regular Surfaces; Inverse Images of Regular Values" (pp. 54–71) and §2-3 "Change of Parameters; Differentiable Functions on Surfaces" (pp. 72–85): Definition 1 (p. 54), Propositions 1–4 of §2-2 (pp. 59, 61, 63, 65) and Proposition 1 of §2-3 (p. 74).
This is the fourth mission of a series formalizing do Carmo's book, sharing the namespace
DoCarmoDG with the others.
A subset is a regular surface when every has an open neighbourhood such that is the image of a map , defined on an open set , satisfying the three conditions of do Carmo's Definition 1:
Such an is a parametrization, or system of local coordinates, and is a coordinate neighbourhood.
Given a differentiable on an open set , a value is a regular value of when is surjective — equivalently, nonzero — at every with (do Carmo Definition 2, §2-2).
If and are two parametrizations of a regular surface with , then
is a diffeomorphism: is differentiable, bijective, and is differentiable.
The graph of a differentiable function of two variables is a regular surface (Proposition 1); the inverse image of a regular value is a regular surface (Proposition 2); a regular surface is locally the graph of a differentiable function of one of the three coordinate pairs (Proposition 3); and an injective map satisfying conditions 1 and 3 whose image lies in a regular surface automatically has a continuous inverse (Proposition 4).
Proposition 2 is the practical criterion: it is what shows in one line that spheres, ellipsoids, tori and the level sets of generic polynomials are regular surfaces, and it is applied throughout the book. Proposition 3 is the structural statement that a regular surface is locally a graph, which is the form in which most local computations are carried out; Proposition 4 removes the awkward homeomorphism clause from the verification of examples. The change-of-parameters theorem is what allows every subsequent definition — differentiable function on a surface, tangent plane, first fundamental form, curvature — to be given in coordinates and then shown to be independent of them, and it is also the reason a regular surface carries a smooth structure at all.
Mathlib has smooth manifolds, the implicit and inverse function theorems, and ContDiffOn, but it
does not contain do Carmo's concrete definition of a regular surface as a subset of
or these four propositions about it. Establishing them is what allows the rest of this series to
work with patches while knowing that the objects so defined are coordinate-independent.
Everything here rests on the inverse function theorem, but each proposition needs it in a slightly different form. Proposition 2 requires completing to a local diffeomorphism and reading off the level set — with the complication that which partial derivative is nonzero varies from point to point, so the coordinate that is solved for is not fixed in advance. Proposition 3 needs the same case distinction on which Jacobian minor of is nonzero, and this is exactly why the conclusion is a disjunction over the three coordinate pairs. Proposition 4 is where the homeomorphism condition is shown to be redundant, and the argument goes through the local factorization .
The change-of-parameters theorem is not a direct application of the inverse function theorem to : the map is defined only on a subset of the plane and is, a priori, merely continuous. One first extends to a local diffeomorphism of a neighbourhood in and then composes; the continuity of (condition 2 of Definition 1) is what makes the domain of open, and it cannot be dispensed with.
A surface is a set S : Set (EuclideanSpace ℝ (Fin 3)), and a parametrization is a map
x : ℝ × ℝ → EuclideanSpace ℝ (Fin 3) together with an open U : Set (ℝ × ℝ). Smoothness is
ContDiffOn ℝ (⊤ : ℕ∞), matching do Carmo's "differentiable" for ; regularity is
injectivity of the Fréchet derivative at each point of U, which is do Carmo's condition 3; and
the homeomorphism condition is stated as injectivity on U together with the existence of a
continuous left inverse on the image, which is the content of "the inverse is continuous". The
neighbourhood clause of Definition 1 is x '' U = V ∩ S for an open V containing the point.
Graphs are formalized as three separate sets, one for each of , and
, so that Proposition 3 can state its disjunction faithfully; in that statement the
neighbourhood is an open set W of and the claim is W ∩ S = W ∩ graph.
The goal states the diffeomorphism property of explicitly — two maps, mutually inverse on the
relevant domains, both ContDiffOn, together with the openness of those domains — rather than
through a bundled structure, so that no library convention is assumed. There is no trivializing
reading: the domains are those forced by the two parametrizations, and in the degenerate case
where the images do not overlap the statement reduces to a true but empty claim about the empty
set, while the substance is in the overlapping case.
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.