Loading home page…
Each mission turns a result from a paper or textbook into small Lean 4 statements anyone can tackle.
Campaigns group missions around a shared mathematical goal. Each one tracks a quantity, such as an upper or lower bound. Have a good candidate in mind? Ping us on Slack, Zulip, or WeChat.
Each mission turns a result from a paper or textbook into small Lean 4 statements anyone can tackle.
Campaigns group missions around a shared mathematical goal. Each one tracks a quantity, such as an upper or lower bound. Have a good candidate in mind? Ping us on Slack, Zulip, or WeChat.
Classical algorithms solve 3SUM in time. In a 2026 breakthrough, Alman and Vassilevska Williams gave a deterministic algorithm, refuting the integer 3SUM hypothesis. How low can the exponent go?
Building on existing Lean formalizations, this campaign tracks upper bounds for 3SUM on polynomially bounded integers, using a word RAM with -bit words, and pursues smaller exponents.
Classical algorithms solve all-pairs shortest paths in time. In a 2026 breakthrough, Alman and Vassilevska Williams refuted the APSP conjecture with a deterministic algorithm. How low can the exponent go?
Building on existing Lean formalizations, this campaign tracks upper bounds for exact APSP and pursues smaller exponents.
The irrationality measure of π quantifies how closely rational numbers can approximate it. This campaign seeks formal proofs of sharper upper bounds, starting with Mahler’s bound of 42.
The sharp Hlawka inequality for Schatten -norms is a cousin of the triangle inequality: it relates the norms of three matrices to the norms of their pairwise sums and their total sum. For complex diagonal matrices, an exact formula for the best possible comparison constant has been proved in Lean for every real . We conjecture that the same formula holds for all .
What is the smallest cutoff for which this formula holds for every real ?
References:
Is every odd number a sum of primes? This campaign tracks formalized proofs of the smallest that suffices.
Schnirelmann (1930) showed some finite works. Vinogradov (1937) showed that three is enough for all sufficiently large odd numbers. Tao (2012) proved unconditionally. Helfgott (2013) proved that every odd number greater than is a sum of three primes, though the proof is still unrefereed. Ideally, we can formalize this statement here. Note that three is optimal: is neither prime nor + prime.
Schoolbook matrix multiplication takes operations. The exponent is the infimum of all such that two matrices can be multiplied in arithmetic operations; trivially , and is conjectured but open.
Strassen gave the first nontrivial bound, , in 1969, and introduced the laser method in 1986 to reach . Coppersmith and Winograd's 1990 bound of stood for two decades. Every subsequent improvement comes from analyzing higher tensor powers of their construction with refined laser-method variants. That line reached in 2025, and the current record is , from August 2026. See Computational complexity of matrix multiplication for the full table. Can we formalize these results and even improve on them?
Decision-making problems rarely present the same fixed choice twice. A doctor prescribing a treatment sees each patient's medical history and symptoms before deciding; a website choosing which article to show sees the visitor's profile first. The multi-armed bandit model — where the learner repeatedly picks from a fixed set of arms with no side information — cannot express this: it is blind to the covariates that any real decision-maker actually observes. The contextual bandit model closes this gap by letting the learner see a context before acting, and asks for a decision rule that generalizes across contexts rather than memorizing a policy per context. Foster and Rakhlin's Foundations of Reinforcement Learning and Interactive Decision Making (arXiv:2312.16730v1, Section 3, pp. 38–53) develops this model and its algorithms as the bridge between supervised learning and sequential decision making, en route to general reinforcement learning. Contextual bandits with a learned reward-function class underlie production systems for content recommendation, online advertising, and adaptive clinical trial design (Li et al., A Contextual-Bandit Approach to Personalized News Article Recommendation, 2010, https://arxiv.org/abs/1003.0146; Agarwal et al., Making Contextual Decisions with Low Technical Debt, 2016, https://arxiv.org/abs/1606.03966).
The algorithmic history in this chapter runs through two distinct principles. The optimism principle (LinUCB, Section 3.2) generalizes the UCB algorithm to contexts under a linear reward model, but the chapter's own Example 3.1 (Section 3.3) shows optimism fails outside such structured classes, incurring regret linear in the size of the context space or the class. Foster and Rakhlin then present two "black-box" alternatives that use any function class through an abstract regression subroutine: the naive -Greedy method (Section 3.4), and the Inverse Gap Weighting (IGW) strategy underlying the SquareCB algorithm (Bietti, Agarwal & Langford, A Contextual Bandit Bake-off, 2018, https://arxiv.org/abs/1802.04064; Foster & Rakhlin, Beyond UCB: Optimal and Efficient Contextual Bandits with Regression Oracles, 2020, https://arxiv.org/abs/2002.04926). SquareCB attains a regret rate that both generalizes across contexts (no dependence on the size of the context space) and matches the optimal rate — improving on -Greedy's rate — while remaining agnostic to the internal structure of .
Over rounds, a decision-maker faces the contextual bandit protocol: at each round , it observes a context , selects a decision from a finite action set , and observes a reward . Rewards are generated independently as for a fixed, unknown conditional model ; write for the mean reward function and for the optimal, context-dependent policy. The context sequence is arbitrary — fixed in advance or adversarially chosen — while rewards remain stochastic. Performance is measured by regret against :
where is the learner's (possibly randomized) action distribution at round .
To generalize across contexts, the learner is given a class with , and aims for regret scaling with the statistical complexity rather than with . Both algorithms in this mission access only through an online regression oracle (Definition 3, p. 47): given the history , it returns an estimate satisfying, with probability at least , — for instance, exponential weights on a finite class achieves . SquareCB (p. 50–51) then samples its action from the Inverse Gap Weighting distribution (Definition 4, p. 50): given a vector of estimated values with greedy action , and an exploration parameter , is for the unique making a probability distribution.
This holds for any and any , with no reference to or to how was produced — it is the purely algebraic core the goal theorem invokes at every round.
with probability at least , for SquareCB run with , for any context sequence . This is the weakest stable target level in the chapter's oracle-based development: it is stated for an arbitrary class and oracle, so it survives any future improvement to the oracle's own bound, unlike a version hard-coded to a specific class or oracle.
Proposition 10 shows that Inverse Gap Weighting converts any estimation-error guarantee into a regret guarantee with the same statistical rate, with no algorithm-side dependence on the structure of or the size of : the same SquareCB template, driven by a plug-in regression oracle, is minimax optimal whenever the oracle itself is. When is finite, this yields , matching the optimal rate for stochastic multi-armed bandits (Section 2) while generalizing across contexts — a guarantee that optimism (Proposition 7) provably cannot deliver outside linear classes (Example 3.1), and that the simpler -Greedy baseline (Proposition 8) only delivers at a slower rate. Foster and Rakhlin describe Proposition 9 itself as being "at the core of the development for the rest of the course": the same IGW mechanism reappears, generalized, in the book's treatment of general decision-making and the Decision-Estimation Coefficient.
Both propositions are proved results, not open questions; this mission's contribution is a
machine-checked formalization of their exact statements and hypotheses — the precise
OracleGuarantee hypothesis Proposition 10 requires, the exact constant (, not a bare
) its proof yields at the stated optimal , and the universally-quantified form
of the IGW inequality (Proposition 9) that makes it reusable independently of any particular
oracle or class.
The obvious first idea for exploiting an estimator is a UCB-style optimism approach: build a confidence set around and act greedily on its upper envelope, as in LinUCB (Proposition 7). Example 3.1 shows this fails in general: a class can force the confidence set to remain wide on a fresh action at every new context, driving regret linear in — the confidence width in the regret bound does not shrink merely because the oracle's cumulative estimation error is small, since that error is not localized to the specific action the confidence-set approach tries next. Uniform exploration (-Greedy) sidesteps this but wastes exploration budget on actions already known to be far from optimal, which is what caps its rate at (Proposition 8). Inverse Gap Weighting instead ties the sampling probability itself to the estimated gap from the greedy action, so cheap-to-rule-out actions are down-weighted continuously rather than either fully explored (ε-Greedy) or trusted outright (optimism); the technical content of Proposition 9 is showing this specific reciprocal-gap form gives a bound with no hidden dependence on or , for every pair simultaneously — a guarantee optimism cannot match because its confidence sets are class-dependent by construction.
Contexts form an arbitrary type X; actions are Fin A for A : ℕ. A finite probability
distribution over Fin A is represented directly as p : Fin A → ℝ with ∀ π, 0 ≤ p π and
∑ π, p π = 1, and as the finite sum ∑ π, p π * g π, rather than
via Mathlib's PMF (which is ℝ≥0∞-valued) — an equivalent and lighter-weight representation of
a distribution on a finite type. The normalizing constant of Definition 4 and the
optimal actions , are each specified by their defining property (existence
of realizing the IGW formula; ) rather
than constructed explicitly via an intermediate-value or Finset.argmax argument, avoiding
committing to one choice function for a value the book itself leaves implicit. The class
enters neither proposition's statement directly: it appears in the source only through the
abstract bound , which is carried as an explicit real-valued
parameter and hypothesis (OracleGuarantee) rather than as a literal subset of a function space,
since no property of beyond producing this bound is ever used. The probability-
qualifier attached to the online regression oracle's guarantee is likewise the explicit
hypothesis OracleGuarantee ... EstSq on a fixed realized run, rather than a statement
quantified over an underlying probability space of histories — every subsequent step in both
propositions' proofs is deterministic given that this event holds, so this does not weaken either
conclusion. A trivializing formalization would fix (a single ever-optimal action, making
both Reg and the IGW inequality vacuous) or take EstSq as an unconstrained free variable with
no positivity hypothesis (making in Proposition 10 undefined); this mission's statements
require 0 < EstSq and leave , , , -via-EstSq fully general.
This mission omits Proposition 7 (LinUCB): its proof rests on an entirely disjoint apparatus
(finite linear parameter sets, least-squares confidence sets, the elliptic potential lemma) that
neither Proposition 9 nor 10 requires, and Example 3.1 (the failure of optimism) is a worked
example rather than a numbered, formalizable claim. It also omits Proposition 8
(-Greedy): the source leaves the optimal unspecified ("choosing
appropriately"), and deriving its own optimal value and matching constant
independently — rather than reusing the book's own explicit constant, as Rule 7 of this
formalization effort requires — was judged too likely to introduce an unfaithful, invented
constant within this mission's time budget; both are natural extensions for a follow-up mission
or contribution. Reusable infrastructure: the Fin A-indexed finite-distribution convention and
the OracleGuarantee/optimal-action-by-property pattern extend directly to any later chapter
built on the same online-regression-oracle abstraction.
The multi-armed bandit is the simplest model of sequential decision-making under partial feedback: a learner repeatedly picks one of finitely many options and observes a reward only for the option chosen, never for the alternatives. It formalizes problems ranging from clinical trial design (which treatment to offer a patient) to online advertising (which ad to show) and A/B testing more generally. The framework dates to Robbins' 1952 paper on sequential design, and the algorithm this mission's goal theorem concerns — the Upper Confidence Bound (UCB) algorithm of Lai and Robbins [1985] and Auer, Cesa-Bianchi and Fischer [2002] — is the canonical answer to how to explore efficiently: instead of exploring uniformly at random, act optimistically with respect to the current uncertainty about each option's value. This mission draws its formalization from Chapter 2 of Foster and Rakhlin's 2023 lecture notes, Foundations of Reinforcement Learning and Interactive Decision Making, which develops the bandit problem as the first rung of a ladder of increasingly general interactive decision-making settings (contextual bandits, structured bandits, reinforcement learning) that the book's later chapters build.
Fix a finite decision (action) space . In the multi-armed bandit protocol, for each round the learner selects a decision , possibly at random according to a distribution depending on the history observed so far, and then observes a reward drawn independently from a fixed conditional distribution (the stochastic rewards assumption). Writing for the mean reward function and for an optimal decision, the learner's performance is measured by the regret
Because the learner observes a reward only for the action played (bandit feedback), a purely greedy strategy that always plays the current empirical maximizer can commit to a suboptimal action forever, incurring linear regret; some form of deliberate exploration is necessary. The chapter's central construction is the confidence interval: a pair of functions such that, with probability at least , for every round and decision simultaneously. The UCB algorithm plays the optimistic action at every round, using the confidence interval built from Hoeffding's inequality around the empirical mean .
holding with probability at least , for the UCB algorithm using the confidence radius of Eq. (2.19). This is the weakest stable statement the chapter proves: it is optimal up to the log factor, and strengthening it (e.g. to the sharper instance-dependent bound of Remark 10) is explicitly left to later work by the book itself.
UCB is the prototype of the "optimism in the face of uncertainty" principle that recurs, in increasingly abstract form, throughout the rest of the book: the same two-step argument (Lemma 7 + Lemma 8) reappears for linear bandits, structured bandits via the Decision-Estimation Coefficient, and UCB-VI for tabular reinforcement learning. Formalizing Chapter 2 in full therefore front-loads the proof pattern every later chapter in this series specializes. The result itself is also of standalone interest: the minimax rate is the benchmark every subsequent bandit algorithm in the literature is compared against, and the -vs- contrast between ε-Greedy and UCB is the standard illustration, in any course on the subject, of why adaptive exploration matters.
No formalization of this exact statement — realizability with respect to a function class and a generic confidence interval, rather than a per-arm sub-Gaussian empirical mean — currently exists on the platform (see Formalization scope below); the mission both proves this specific regret bound and seeds the generic optimism/potential lemma pair (Lemma 7, Lemma 8) that the book's later, more structured settings specialize.
The natural first attempt — bound the regret of the empirical-mean-greedy algorithm directly — fails outright: on a two-armed instance where one arm is deterministic and the other only slightly better in expectation, the greedy algorithm can commit to the worse arm forever with constant probability, giving linear, not sublinear, regret (§2.1). The obvious fix, ε-Greedy, forces exploration uniformly across all actions regardless of how much is already known about each, so the exploration cost scales with even for actions whose value is already well determined — this is exactly what caps ε-Greedy at the rate. UCB's optimism principle resolves this by exploring an action only in proportion to how uncertain it still is; the technical core, isolated in Lemma 7 and Lemma 8, is disentangling "the algorithm made a mistake" from "the algorithm is still uncertain," which are conflated in the naive per-round regret decomposition used for ε-Greedy.
Both the goal and the milestones fix a finite decision space Fin A, a mean reward
function fStar : Fin A → ℝ with fStar π ∈ [0,1], and an optimal decision
piStar. Regret is defined generically (Eq. (2.3)) via per-round decision weights
p : ℕ → Fin A → ℝ, so it applies uniformly to a randomized algorithm (ε-Greedy) and
a deterministic one (UCB, via the point mass at the played action). The book's "with
probability at least " qualifier on both Proposition 4 and Proposition 5 is
formalized as the deterministic consequence of the underlying concentration event
(Eq. (2.9) and Eq. (2.18) respectively) holding — exactly the move the book's own
proofs make ("Let us condition on the event in (2.18) ... "). The concentration
events themselves rest on Hoeffding's inequality for adaptive stopping times
(Lemma 33) and Bernstein's inequality (Lemma 5), both stated in the book's technical
appendix outside this chapter, and are not drafted here; a solver may either take
them as a hypothesis (as this mission's statements do) or import/prove them
separately. A trivializing formalization is ruled out explicitly: taking δ outside
, or dropping the fStar π ∈ [0,1] hypothesis, would make the stated
constants vacuous or false, so both are retained as explicit hypotheses in every
theorem. In every ≲ statement (Prop. 4, Lemma 8, Prop. 5) the witnessed constant
C is quantified before the instance parameters (A, T, δ, and the realized
sequences): ∃ C, 0 < C ∧ ∀ A T δ ..., Reg ≤ C * (rate), not the other order. This
is deliberate, not stylistic: quantifying C after the instance lets it depend on
A, T, δ, making the bound satisfiable by an arbitrarily large C chosen per
instance and hence content-free, which is not what the book's ≲ means (a single
constant working uniformly over all instances). Proposition 5's UCB decision rule
is stated in the book's own two clauses, not collapsed into a single "maximize the
upper confidence bound" rule: the confidence radius of Eq. (2.19) is at
(an action never yet sampled), so the book's UCB always plays an
unsampled action before ever comparing indices, and only compares finite upper
confidence bounds once every action has been sampled at least once; the confidence
event of Eq. (2.18) is correspondingly assumed only at sampled actions, since the
book's own bound is vacuous otherwise. An earlier draft instead capped the radius
at when , which is a true statement about a different algorithm (a
sampled action can have index above the capped unsampled index), and was corrected
to the book's own rule after moderation. Reuse from the platform's existing bandit library (BanditAlgorithm,
Lattimore & Szepesvári) is deliberately avoided: that library's UCB
(bandit_ucb_regret_bound, bandit_ucb_minimax_regret_bound) is stated for
per-arm 1-sub-Gaussian rewards with fixed by the horizon, whereas
this chapter's UCB is stated for a free failure probability and a generic
confidence-interval abstraction (the multi-armed case being of the book's general realizability framework) — the two are
related but not the same statement. Contributions extending the mission with the
generic confidence-interval form of Lemma 7/8 applied to other chapters in this
series (contextual and structured bandits) are welcome.
Two-stage stochastic programs with recourse require evaluating , the expected value of a recourse function, at every candidate first-stage decision . When is high-dimensional or continuously distributed, this expectation is a multivariate integral of a piecewise-linear, generally nondifferentiable integrand, and classical quadrature rules — built for smooth integrands in low dimension — do not apply (Birge & Louveaux, §8.1). What does apply is convexity: is convex whenever the recourse problem is a linear program in , and convexity alone is enough to sandwich between two computable discrete approximations. This chapter develops that sandwich, and it is the standard device used throughout the stochastic-programming literature to bound and iteratively refine the recourse function: the lower bound goes back to Jensen [1906]; the upper bound is due to Edmundson [1956] and Madansky [1959], with the mean-consistent LP refinement due to Madansky [1960] and Gassmann & Ziemba [1986]. Refinements of both bounds appear in Huang, Ziemba & Ben-Tal [1977], Kall & Stoyan [1982] and Frauendorfer [1988].
Fix a probability space and an integrand , where is the (convex, closed) support of a random vector and is a real vector space (in the recourse application, and is the first-stage feasible region). Write .
A partition of into measurable blocks determines, for each block, its probability and its conditional mean . Equivalently — and this is the convention this mission's Lean development uses — the blocks may be taken directly on the sample space as the pulled-back sets , with and the Bochner integral average of over the block; the two descriptions coincide.
This is the sharpest statement the chapter proves for the lower bound: it holds for every finite measurable partition, with no assumption beyond convexity of and integrability.
For compact, let be the extreme points of , carrying the Borel field of all its subsets. If, for every , is a probability measure on with barycenter (i.e. ) and is measurable for every , then
Together the two targets give the chapter's headline sandwich: for convex , the finite-partition Jensen value and the Edmundson-Madansky value bracket the true expectation, and refining the partition (resp. the disintegration) tightens both sides toward it.
The Jensen bound is the workhorse of discrete-distribution approximation in stochastic
programming: it is what makes a valid, refinable
lower-approximation of the true recourse function, and it underlies the partition-refinement
schemes (§8.2, following Birge & Wets [1986] and Frauendorfer & Kall [1988]) used inside the
-shaped method and separable-programming solvers described later in the chapter (§8.3). The
Edmundson-Madansky bound is its indispensable upper counterpart: without it there is no
certificate of how far a lower approximation can be from the truth, and the mean-consistent LP
refinement (eq. 2.9, not part of this mission) reduces to a moment-problem computation over
. Both bounds are, to date, unformalized: the platform holds no theorem matching either a
finite-partition conditional-Jensen inequality or an extreme-point disintegration bound (searched
GET /theorems?q=... for "Jensen", "conditional expectation", "Edmundson Madansky", "partition
convex" — no relevant hits), so this mission is a first formalization of both, not a
reformulation of existing platform content. Mathlib supplies the raw convexity substrate this
mission is built from — finite Jensen (Analysis/Convex/Jensen.lean) and, critically, the
set-average integral Jensen inequality (ConvexOn.map_set_average_le in
Analysis/Convex/Integral.lean), exactly the per-block step the book's proof of Theorem 1
performs — but no existing lemma assembles these into the partitioned, conditional-mean statement
the book actually states.
The obvious shortcut is to prove "convex functions lie above their tangent line" and stop — this captures no partition structure at all and is not the theorem the book states (the theorem is about , a sum over blocks, not a single linearization). The real content is bookkeeping across the partition: writing as (an exact identity, no convexity needed), then applying ordinary Jensen inside each block to replace by from below — the inequality only enters at the second step, once per block. Proving this in Lean means correctly discharging, for every block, the side conditions Mathlib's integral-Jensen lemma needs (closedness of , continuity of on , integrability on the block) and then summing the per-block inequalities against weights that themselves depend on the partition — an easy step to get wrong by, e.g., letting be an arbitrary point of rather than exactly its conditional mean, which understates what Jensen actually forces. Theorem 2 additionally requires setting up the disintegration correctly: is a probability measure defined as an integral of the kernel-like family against , and both the barycenter condition on and the measurability of are load-bearing — dropping either makes ill-defined or the bound's proof inapplicable.
for a complete real normed vector space (NormedAddCommGroup E,
NormedSpace ℝ E, CompleteSpace E); no finite-dimensionality is assumed since neither theorem's
proof needs it. The parameter ranges over an arbitrary type with ,
and is left as a bare function α → E → ℝ, matching the book's level of abstraction (the
recourse LP's own data is never used in either proof).
The partition is formalized directly on the sample space (a Partition structure:
pairwise-disjoint measurable blocks covering , each of positive measure) rather than on
, per the equivalence noted under Setting; is defined as the Bochner-integral
average , so it is forced to be the conditional mean and cannot be
weakened to an arbitrary sample point of the block — the change the chunk brief flags as the main
faithfulness trap for this chapter.
Two explicit hypotheses are added beyond the book's own statement of Theorem 1, both needed by
Mathlib's integral-Jensen lemma rather than narrowings of the mathematical content:
ContinuousOn (g x) Ξ (finite-dimensional convex functions are automatically continuous on the
interior of their domain, which is what the book implicitly relies on; stated explicitly since
is not assumed finite-dimensional) and integrability of and of
(needed for and each to be well-defined). For Theorem 2, the
disintegrating family is E → Measure Ext for an abstract type Ext (standing for
) with the discrete MeasurableSpace (every subset measurable, matching the
book's "Borel field ... the collection of all subsets"), mapped into by an embedding toE
whose range is exactly (convexHull ℝ Ξ).extremePoints ℝ; the measure (named μExt in
the Lean code, since λ is a reserved keyword) is a hypothesis satisfying its defining equation
(2.6) rather than constructed, since constructing a measure from a set function is a separate,
book-external piece of measure theory the chapter's own proof does not perform either — it simply
asserts is the probability measure with that value on every set.
A trivializing formalization is ruled out explicitly: a version that lets range over an arbitrary point of , or that proves only the ordinary (unconditional) Jensen inequality without ever introducing the partition, states something strictly weaker than the book and is not what is formalized here.
Both draft theorems end in := by sorry; a full Lean proof of Theorem 1 combines Mathlib's
ConvexOn.map_set_average_le applied per block with the exact decomposition of into
over the partition's disjoint, covering blocks. Reusable beyond this mission:
the Partition structure and its weight/condMean accessors generalize to any chapter needing
a finite measurable partition with conditional means (this book's later approximation schemes,
§8.2-8.5 and Chapter 10, all build on the same device). Contributions solving either theorem, or
formalizing the partition-refinement monotonicity (eq. 2.3, not part of this mission's milestone list since it is not itself a
numbered theorem) as a follow-up, are welcome.
Every stochastic program is, in practice, compared against a shortcut. A decision maker facing genuine uncertainty is tempted either to replace the random data by its mean and solve one deterministic problem, or to imagine that perfect information about the future were available and solve a separate deterministic problem per scenario. Both temptations have precise answers: the expected value of perfect information (EVPI) measures how much a decision maker should be willing to pay for a perfect forecast, and the value of the stochastic solution (VSS) measures the cost of ignoring uncertainty altogether by solving the mean-value problem. Both concepts originate in decision analysis — EVPI traces to Raiffa and Schlaifer (1961) — and were brought into stochastic programming by Madansky (1960), who proved the first chain of inequalities relating the wait-and-see value, the recourse value and the expected-value-solution's cost. Birge and Louveaux, Introduction to Stochastic Programming, 2nd ed. (Springer, 2011), Chapter 4, gives the standard modern treatment, including a refined family of bounds — built from pairs subproblems against a chosen reference scenario — that sharpen VSS beyond the original mean-scenario comparison. This mission formalizes that chapter's capstone: the five-quantity, four-inequality chain that pins VSS between two computable optimal values.
Fix a two-stage stochastic program with fixed recourse: a finite family of K scenarios
in , each occurring with probability ,
; a first-stage feasible set ; and, for every
first-stage decision and every scenario , a
scenario cost — the optimal value of . By convention when has no feasible second-stage recourse under
, and when the second-stage program is unbounded below.
From , five basic quantities are defined (Birge & Louveaux §4.1–§4.2):
Section 4.6 refines VSS by replacing the mean scenario with an arbitrary reference scenario (not necessarily one of the possible scenarios, e.g. a worst case), with assumed probability :
Four links, each with independent content: nonnegativity of the leftmost gap, then two genuine inequalities (from the pairs-subproblem comparisons of Propositions 7 and 8), then the identity folded against 's reverse-direction cousin. This is the weakest statement that keeps all five quantities distinct — stating only the outer bound would erase exactly the refinement (via pairs subproblems) that makes the chapter's method useful.
The chain gives a decision maker two computable, non-obvious bounds on VSS — a quantity that is otherwise expensive to pin down exactly, since itself already requires solving the full recourse problem. and are both computable from (or ) two-scenario LPs, far cheaper than the full -scenario recourse problem, so Theorem 9 turns an expensive exact quantity into a pair of cheap certified bounds. Formalizing it fixes, once and for all, the exact hypotheses and quantifier structure of Madansky's original inequality (Proposition 1) together with the later pairs-subproblem refinement (Propositions 6–8, Birge 1982), often cited informally as "the VSS bounds" without distinguishing , , and . No part of this chain is on Mathlib or Formalpedia today (checked by concept query, not title); this is a first, from-scratch treatment of two-stage recourse value-of-information theory as formal objects.
The obvious first idea — collapse , , , , , , to one "the optimal value of the LP" and prove a single inequality — throws away the entire content of the chapter. Each quantity restricts the minimization to a different feasible object: minimizes jointly over ; swaps the order of and ; / evaluate one fixed under every scenario; and each minimize over a family of pairs subproblems rather than the full -scenario problem. The chain's proof (Propositions 7–8) depends on this precisely: Proposition 7's lower bound uses that each pairs-subproblem-optimal is feasible (not necessarily optimal) for the single-scenario problem at , and its upper bound uses that the recourse-optimal is feasible (not necessarily optimal) for the pairs subproblem — a feasible-but-not-optimal argument in each direction, not a direct comparison of objective values. Losing track of which solution is fixed and which is optimized destroys the argument entirely.
An Instance bundles the finite scenario set (Fin K, probabilities p : Fin K → ℝ with
p ≥ 0, ∑ p = 1, scenarios xi : Fin K → (Fin d → ℝ)), the first-stage feasible set
K1 : Set (Fin n1 → ℝ), and the scenario cost z : (Fin n1 → ℝ) → (Fin d → ℝ) → EReal, using
the extended reals to carry the book's own +∞/−∞ conventions for infeasibility and
unboundedness rather than silently restricting to a finite-valued special case (a genuine risk
of trivialization here, since Example 2 of the chapter exhibits ). All optimal
values (RP, WS, EV, EVPI, EEV, VSS, EVRS, generalized VSS, SPEV, EPEV) are
defined directly from z, matching the book's own level of abstraction in this chapter (which
never unfolds z into the underlying LP's data — those appear only in Chapter
3). Because EEV, the mean-scenario VSS, EVRS, the generalized VSS, and EPEV are each
defined relative to an optimal solution of some sub-problem — the book itself only ever says
"let denote some optimal solution" — every theorem using them states that
solution and its optimality as explicit hypotheses (x ∈ K1 and z x … = ⨅ …), never baking it
into a Classical.choiced value; this keeps the quantifier structure faithful to the book's own
"let ... be an optimal solution" phrasing. Proposition 5's part (b) — the upper bound
, "for stochastic programs with fixed recourse matrix and
fixed objective coefficients" — needs a different scope: that hypothesis is a structural
property of the underlying LP data (, , fixed across scenarios) invisible once is
abstracted away as above, and pinning it down would require modeling the LP's
data explicitly (as Chapter 3's mission does for its convexity theorem). That part is out of
scope here and is not needed for Theorem 9's own chain, which rests only on Proposition 5(a).
Collapsing any two of , , , , , , to a single "value of the LP" — the trivialization this book-wide series flags for Chapter 4 — is ruled out by construction: each is its own definition over its own feasible object, and Theorem 9's statement names all five quantities in the chain rather than only its outer bound. The two occurrences of "VSS" in the chapter (the original mean-scenario of §4.2, and the reference-scenario generalization of §4.6, used only in Theorem 9) are likewise kept as two distinct definitions rather than conflated under one name.
Every addition and subtraction between EReal values in this mission — inside expect, WS,
EVPI, VSS, EVRS's appearance in VSSRef, the pair sum inside pairsValue, the sum inside
SPEV, and all four differences in Theorem 9's own chain — uses three explicit operations,
badd/bsub/bsum, that implement the book's own convention (p. 164) that +∞ (infeasibility)
dominates, i.e. (+∞)+(−∞)=+∞, rather than Mathlib's native EReal addition, whose
⊤+⊥=⊥ would make VSS ≥ 0 (Proposition 5(a)) and the goal's own leftmost inequality false
whenever a witness solution is infeasible in a positive-probability scenario — exactly the
situation of the book's own Example 2 (pp. 174-175). The reference scenario's probability
(p. 172) is likewise not a free parameter but a definition, refProb,
computed from the instance itself as ; SPEV's sum is correspondingly
restricted to the scenarios other than the reference scenario (), matching the
book's own proof of Proposition 7, which uses . The single hypothesis
refProb I xir < 1 on Propositions 7, 8 and the goal says that some other scenario remains
possible, which the book's own factor presupposes.
Reusable beyond this mission: the Instance definition and the RP/WS/EV quantities are
the natural base for any later chapter of this series that needs the two-stage recourse value
(e.g. Chapter 3's convexity mission, Chapter 5's L-shaped method); contributions extending this
Instance to the full LP data of the underlying two-stage program, or adding Proposition 5(b)
and Proposition 2's Jensen-inequality argument on top of it, are welcome.
Thompson's group is the group of piecewise-linear order-preserving homeomorphisms of with finitely many breakpoints, all at dyadic rationals, and all slopes powers of . Two earlier missions formalize its definition and its first structural facts (§1 and §4: the commutator subgroup is simple, is not elementary amenable) and its tree-diagram normal form (§2). What neither says is how looks as an abstract group: by generators and relations.
That is §3 of Cannon, Floyd and Parry's Introductory notes on Richard Thompson's groups (L'Enseignement Math. 42 (1996), doi:10.5169/seals-87877), which gives two presentations of and proves that both present the group of homeomorphisms:
The finite presentation is the form in which enters most of the literature — the word problem, the growth and amenability questions, the homological results of Brown and Geoghegan all start from it — and the infinite presentation is the one that makes the normal form of §2 visible as an algebraic fact.
Throughout, , the source's convention, and groups are written multiplicatively with composition of maps as the product: .
The functions. and are the two specific homeomorphisms of from the §1
mission (mapA, mapB: halves , is a translation on ,
and doubles ; is the identity on and acts like , scaled,
on ). For , and ; these are the
functions X n of the §2 bundle. Corollary 2.6 of the source, proved in the §2 mission, says
and generate .
The formal symbols. and are presented groups: the free group on the listed
symbols modulo the normal closure of the listed relators. In Lean they are Mathlib's
PresentedGroup applied to explicit relator sets: relsF1, a two-element set of words in
the free group on the two-element type FormalAB, and relsF2, the set of words
for in the free group on . The symbols
are distinct objects from the functions; the whole content of the section is that the map
"symbol function" is an isomorphism.
Auxiliary objects. In the source sets and
for (Y), the intended images of the . In a list of nonnegative
exponents determines the positive word
(wordF2), the formal counterpart of the §2 bundle's word; the normal-form conditions of
Corollary-Definition 2.7 are the §2 predicate IsNormalFormData, reused verbatim.
The goal is the finite presentation, Theorem 3.4 for :
On the way, in the order the source proves them:
A one-line consequence closes the list: is finitely presented, in Mathlib's sense
Group.IsFinitelyPresented.
The result. A presentation is what makes an object of combinatorial group theory. The two relators are what one checks a homomorphism against, the infinite presentation is what the normal form is a normal form for, and "finitely presented" is the hypothesis under which is a test case for conjectures about finitely presented groups. Every later algebraic statement about — the word problem is solvable, the abelianization is , the automorphism group, the presentations of and — is stated relative to one of these two presentations.
Formalizing it. Both theorems are proved in the source and their proofs are short, so what this mission produces is the machine-checked bridge between the two existing developments: the analytic definition of and its tree-diagram normal form on one side, an abstract presented group on the other. The isomorphism is where §2's uniqueness theorem is used rather than merely proved: injectivity of is exactly the statement that distinct normal forms give distinct functions. Nothing here is machine-checked anywhere else; the platform has no presentation of .
Theorem 3.1 is a computation in and offers no surprises once lines (3.2) and (3.3) of the source are set up as their own statements: the induction that establishes from the two relators is the only place care is needed, and the source spells it out.
The central difficulty is the paragraph on p. 226 proving that is injective. The
source argues in prose that "every nontrivial element of can be expressed as a
positive element times a negative element", and then "put in normal form" by deleting an
from both parts and re-indexing when is absent. Formally this is a rewriting
argument inside the abstract group , with no geometry to lean on: one needs the three
derived relations , ,
(for ), an induction that sorts an arbitrary word into
positive-times-negative form, and a second induction that reduces such a form until the
normal-form conditions hold. The obvious shortcut — "every element of is the image of
some function, and functions have normal forms" — is circular, because it presupposes the
injectivity being proved. The milestone exists_isNormalFormData_F2 isolates this step.
word/wordFrom and the predicate
IsNormalFormData are the published definitions of the §1 and §2 missions
(CannonFloydParry, CannonFloydParry_Trees, CannonFloydParry_TreeDiagrams), imported
unchanged. Elements of are order isomorphisms of the subtype ,
and is the subgroup they generate; membership of , , in is a proved
theorem, not a definition.CannonFloydParry_Presentations adds only the formal side: the symbol type
FormalAB, the relator sets relsF1, relsF2, the presented groups F1, F2, the
symbol maps symF2 (into ) and symF (into the interval maps), the elements Y, and
the words wordF2. Relators are written out as ; no commutator notation
is used in published statements.MulEquiv sending the named generators to the
named images. Nothing is asserted about uniqueness of the isomorphism (it is unique, since
the generators generate).closure_mapA_mapB_eq_F), the §2 normal-form
theorems (exists_isNormalFormData, word_ne_one_of_isNormalFormData), and the §4
mission's mem_commutator_iff if a solver prefers to verify the relators of in
through supports rather than by direct computation. Solutions may import them.Group.IsFinitelyPresented instance built from
the isomorphism (the last milestone), and, further off, the presentations of and
from §5–§6, which extend by one and two generators.Thompson's group is a finitely presented group of piecewise-linear homeomorphisms of the unit interval that has served since the 1960s as a standard supply of counterexamples in combinatorial group theory: its commutator subgroup is simple, every proper quotient of it is abelian, it contains no free subgroup of rank two, it is not elementary amenable, and whether it is amenable is a question Cannon, Floyd and Parry report as having been raised by Geoghegan in 1979 and still open when they wrote (CFP96, §4 and p. 227).
Almost nothing about is computed directly from that analytic definition. What makes the group tractable is a combinatorial calculus: each element is encoded by a pair of finite binary trees, and multiplication becomes a cancellation between trees. Cannon, Floyd and Parry credit the device to Brown and devote §2 of their notes to it; everything later in those notes that requires a computation — the two presentations of §3, the normal subgroup lattice of §4, the treatment of Thompson's group in §5 — runs through it.
This mission formalizes that calculus and the normal form it yields.
A real number is dyadic when it has the form with an integer and a nonnegative integer. Thompson's group consists of the increasing homeomorphisms of that are piecewise linear with finitely many breakpoints, all breakpoints dyadic and every slope an integer power of , under composition. Two of its elements are
and from them come and for , so that .
A standard dyadic interval is one of the form with and nonnegative integers and . A partition of is a standard dyadic partition when every is a standard dyadic interval.
An ordered rooted binary tree is a finite tree in which each vertex has either no children or an ordered left child and right child. Its childless vertices are its leaves, which carry a canonical left-to-right order; its right side is the path from the root always taking the right child; a caret is a vertex with its two children. Assigning to the root and splitting each interval at its midpoint between the two children gives every vertex a standard dyadic interval, and the leaves then cut out a standard dyadic partition — the sense in which such a tree is a -tree. The exponents of a -tree are one nonnegative integer per leaf, in order: the th is the length of the longest arc of left edges beginning at the th leaf that does not reach the right side.
A tree diagram is an ordered pair of -trees with equally many leaves. An element of has that diagram when is affine on each interval cut out by the leaves of and carries those intervals, in order, onto the intervals cut out by the leaves of . Adjoining a caret to and to at the same leaf gives another diagram for the same ; a diagram admitting no such reduction — no position where both trees carry a caret — is reduced.
Every in is
for exactly one choice of nonnegative integers , , subject to two conditions: exactly one of and is nonzero, and if and for some then or .
It fixes no bound on and no normalization beyond those two conditions, so no later refinement of how the exponents are presented can invalidate it.
The milestone list follows §2 in order: the correspondence between standard dyadic partitions and -trees, the bijection between and the reduced tree diagrams, the word read off the exponents of , a criterion for a diagram to be reduced, generation by and , and closure under multiplication of the positive elements — those of the form with every exponent nonnegative.
A normal form is a decision procedure: two words in the generators name the same element exactly when their normal forms agree, so the word problem for is solved by computing them. The generation statement is what licenses treating as a two-generator group, and it is the input to both presentations in §3. The positive elements and their closure under multiplication are used, with the normal form, throughout §5 on Thompson's group .
The §2 results this mission targets — Lemma 2.2, the correspondence between and the reduced tree diagrams, Theorem 2.5, Corollary 2.6, Corollary-Definition 2.7 and Lemma 2.8 — are proved mathematics: Cannon, Floyd and Parry are expounding material that goes back to Thompson's unpublished notes. None of them has a machine-checked proof on this platform, and the library contains no tree-diagram machinery to build on, so the definitions published here fix the interface for anyone later formalizing Thompson's groups and , which occupy the same notes and are built from the same trees.
There is also a concrete dependency. The companion mission on §4 of the same paper has eleven of its fifteen milestones machine-checked, and all four that remain wait on this section: Cannon, Floyd and Parry prove their Theorem 4.1 through Corollary 2.6 and their Theorem 4.3 through the normal form. Corollary 2.6 appears in this milestone list as the same theorem object that is open there, so closing it here closes it there.
The obvious way to attach a diagram to an element is to use the partition given by its breakpoints. That fails twice over: the breakpoints of need not be the division points of any -tree, and even when they are, their images under need not be either, since the definition of constrains the breakpoints and slopes of and says nothing about where the image partition sits. Both failures must be repaired by refining the partition before any tree appears, which is why that refinement is a milestone rather than a preliminary.
Uniqueness of the reduced diagram is a difficulty of a different kind: two reduced diagrams for the same element admit no a priori map between their trees, so they cannot be compared directly.
A third is not visible in the source. For trees with leaves the exponent lists always end in , so the outermost factors of the word above vanish; but the normal form demands that exactly one of , be nonzero. The two indexings differ, and a re-indexing step sits between the theorem producing the word and the corollary stating the normal form. The paper prints them one under the other. That step is a milestone of its own, flagged as absent from the source, so a solver working from the paper alone is not ambushed by it.
Ordered rooted binary trees are an inductive type — a leaf, or a pair of subtrees — rather than graphs with a root and valence conditions. Those conditions say exactly that every non-leaf vertex has two distinguished children, so both descriptions pick out the same objects, but the inductive type is a reformulation of the paper's definition and the definition bundle says so. The infinite tree of all standard dyadic intervals is likewise never built: the subdivision of comes from a recursion halving at each node, which turns the paper's observation that the leaves of a -tree are the intervals of a standard dyadic partition from something given into something proved.
is imported rather than redefined, from the published definition bundle of the companion mission, where it is the subgroup generated by the piecewise-linear maps described above; membership in that subgroup is identified with the piecewise-linear description by a theorem already machine-checked there. Exponent data is carried by finite lists, and the uniqueness in the goal is uniqueness of that list data.
The goal is vacuous in neither direction: its hypothesis is met by and themselves, and a separate milestone asserts that every choice of exponent data meeting the two conditions names an element other than the identity.
The tree combinatorics — leaf counts, right sides, the subdivision map, the exponents, carets — is published here as a separate definition node that mentions nowhere and needs nothing but Mathlib, so it is reusable as it stands; the diagram vocabulary is built on it. Any milestone is open to contribution, as are routes other than the paper's.
Within that paper tree diagrams are credited to Brown and the word-length algorithm to Fordham, cited there as [Bro1] and [Fo].
Almost every classical transcendence theorem is a statement about the interaction between the additive structure of and the exponential function. Hermite proved in 1873 that is transcendental, Lindemann in 1882 that is transcendental for every nonzero algebraic — hence that is transcendental and the circle cannot be squared — and Weierstrass in 1885 extended this to the linear independence of over for distinct algebraic . Gelfond and Schneider settled Hilbert's seventh problem in 1934, and Baker's 1966 theorem on linear forms in logarithms made the subject effective.
Schanuel's conjecture, formulated by Stephen Schanuel in the 1960s and first published by Lang (Introduction to Transcendental Numbers, Addison–Wesley, 1966, Chapter III), is a single statement that contains all of these as special cases, together with a large number of statements that remain open — for instance that and are algebraically independent, or that is irrational. No case of it is known beyond those already covered by the Lindemann–Weierstrass theorem or by Baker's theorem.
Timeline, with the hypotheses each result actually assumes:
Write for the complex exponential function. A tuple of complex numbers is linearly independent over when the only rationals with are ; here is viewed as a vector space over .
For a subset , let denote the subfield of generated by over . The transcendence degree is the cardinality of a transcendence basis of over : the largest number of elements of that are algebraically independent over . A number is transcendental over when no nonzero polynomial with rational coefficients vanishes at , and numbers are algebraically independent over when no nonzero polynomial in variables with rational coefficients vanishes at .
The goal fixes no numerical constant and no special shape for the : it asserts only the inequality, for every and every -linearly independent tuple. The case is vacuous and the conclusion is a bound on a cardinal, so nothing is hidden in a degenerate convention.
The milestone list consists of the landmark unconditional theorems that Schanuel's conjecture generalizes, the known function-field analogue, and one conditional corollary that records what the conjecture buys:
Schanuel's conjecture decides, in one stroke, a long list of questions that are individually open: the algebraic independence of and , the irrationality of and of , the transcendence of and , the four exponentials conjecture, and — combined with work of Macintyre and Wilkie — the decidability of the first-order theory of the real exponential field. Its restriction to algebraic is exactly the Lindemann–Weierstrass theorem, and its restriction to whose exponentials are algebraic is exactly Baker's theorem, so the conjecture is a common generalization of the two main unconditional pillars of the subject.
On the formalization side, the state of the art in Lean's mathematical library is modest relative to this history: the analytic core of the Lindemann–Weierstrass argument is present, but the Hermite–Lindemann theorem, the Lindemann–Weierstrass theorem, the transcendence of , the Gelfond–Schneider theorem, the six exponentials theorem and Baker's theorem are not available as usable statements in the pinned environment. Each milestone here is therefore a genuine formalization project with a known mathematical proof, and none of them is a restatement of an existing library result. The goal theorem itself is open mathematically; the realistic contributions to it are reductions — implications between the goal and other statements — and closing the milestones that the conjecture generalizes.
The obvious approach to any single case — build an auxiliary function with many zeros, bound its derivatives, and derive a contradiction from an integrality argument — is the method behind every result on the milestone list, and it is exactly what fails for the conjecture in general. Those proofs need the exponentials, or the arguments, to be algebraic somewhere, so that heights and denominators can be controlled; for a general -linearly independent tuple there is no arithmetic input at all, and no known construction produces the required auxiliary function. Ax's theorem shows that the differential-algebraic shadow of the statement is true, but its proof uses the derivation on the function field and has no arithmetic counterpart. A solver should not expect the conjecture itself to fall to a variation of the classical method.
All statements are over , with the complex exponential. Tuples are indexed by Fin n, ℚ-linear independence is Mathlib's LinearIndependent ℚ, transcendence degree is Mathlib's Algebra.trdeg, the generated field is IntermediateField.adjoin, and the inequality is between cardinals, so the goal reads (n : Cardinal) ≤ Algebra.trdeg ℚ (adjoin ℚ (Set.range z ∪ Set.range (Complex.exp ∘ z))). Algebraicity is IsAlgebraic ℚ, transcendence is Transcendental ℚ, and algebraic independence is AlgebraicIndependent ℚ.
There is no trivializing formalization here: the hypothesis LinearIndependent ℚ z is satisfiable for every , so the goal is not vacuous, and the conclusion is an inequality of cardinals rather than a statement about a definition introduced for this mission.
The Ax milestone is stated for formal power series in one variable over : the exponential relation is expressed as the differential equation with PowerSeries.derivative, and the conclusion bounds Algebra.trdeg ℂ of the ℂ-subalgebra generated by the and the . The conditional corollary takes the full statement of Schanuel's conjecture as an explicit hypothesis, so it is provable unconditionally as stated.
Infrastructure that a complete development needs, and that is reusable well beyond this mission: Siegel's lemma and height machinery for algebraic numbers, the standard auxiliary-function construction with derivative bounds, and interface lemmas relating Algebra.trdeg, AlgebraicIndependent and Transcendental. Reductions between the milestones — for example deriving Hermite–Lindemann from Lindemann–Weierstrass, or the six exponentials theorem from a general Baker-type statement — are welcome as sketches.
Perturbative quantum field theory produces algebraic varieties. In the parametric (Feynman–Symanzik) formulation of a momentum-space Feynman integral of a graph , the integrand is built from the Kirchhoff (first Symanzik) polynomial , and the period that the integral computes is governed by the graph hypersurface . Because has integer coefficients, is defined over , and one can ask arithmetic questions about it: how many points does it have over a finite field , is that count a polynomial in , and what is its class in the Grothendieck ring of varieties?
A separate line of work asks when a variety defined over carries an additional structure over the "field with one element" . Tits observed in 1956 that is a polynomial in whose behaviour as is governed by the symmetric group, and several inequivalent theories of -geometry have been proposed since. In the formulation of López Peña and Lorscheid, an -structure is witnessed by a torification: a decomposition of the variety into split tori inducing a bijection on -points for every field .
Bejleri and Marcolli, Quantum field theory over (Journal of Geometry and Physics, 2013, doi:10.1016/j.geomphys.2013.03.002), brought these two lines together: they asked which varieties of perturbative QFT admit an -structure, proved a blow-up formula for torified varieties, and deduced that the wonderful compactifications of graph configuration spaces and the moduli spaces are -varieties. Along the way they recorded elementary but sharp necessary conditions for an -structure, and tested them on concrete families of graph hypersurfaces. This mission formalizes that necessary-condition layer for the simplest infinite family, the banana graphs. The programme continues to be cited in the physics literature (arXiv:2401.07822).
For , the banana graph has two vertices joined by parallel edges. Its graph hypersurface is cut out by the Kirchhoff polynomial of , and is its complement.
Write for the Lefschetz class in the Grothendieck ring of varieties and set
If a variety admits a torification by tori , then its class is , so it is a polynomial in with non-negative integer coefficients; this is Lemma 3.8 of the paper. Writing , the Euler characteristic is the constant term , because positive-dimensional tori have vanishing Euler characteristic — whence the coarser necessary condition of Proposition 3.1. Non-negativity of the coefficients is therefore a necessary condition for an -structure, and one that can be checked by pure computation once the class is known.
For the banana graphs the class is known in closed form (Aluffi–Marcolli, quoted as equation (3.8) of the paper):
The first summand is , and the two quotients are exact divisions: they are the polynomials and of equations (3.9) and (3.10).
The goal is the first half of Lemma 3.9: for all , every coefficient of , as a polynomial in , is non-negative,
so that passes the necessary condition of Lemma 3.8.
The milestones are the steps the paper uses, and the contrast it draws:
Item 5 is the point of the lemma: the necessary condition separates from , so it is not vacuous on this family.
The combination " passes, fails" is the paper's concrete evidence that the torification condition is a usable filter on the varieties of perturbative QFT: it rules out an -structure on the hypersurface complements — the objects whose periods are the Feynman integrals — while leaving the hypersurfaces themselves as candidates, and it motivates the paper's Question 3.10 (whether the graph hypersurfaces satisfying the condition actually admit torifications).
What this mission produces on top of the paper is a machine-checked version of that computation. The mathematics here is not open: Lemma 3.9 is proved in the source, and the six statements of this proposal are elementary consequences of the closed formula (3.8) once the two divisions are performed. The captain has checked that all six compile and are provable in Lean 4 with Mathlib. The deliverable is therefore a formalization, not a new theorem: a reusable Lean model of Grothendieck classes in the variable for this family, with the coefficient positivity and the failure of positivity for the complement both verified, and the printed expansion for in the paper reproduced by the formalized coefficient formula.
The obstruction is bookkeeping, not depth. Equation (3.8) is a rational expression; the two fractions are exact divisions only after one knows the quotients, so a formalization has to fix polynomial representatives and prove the two division identities rather than manipulate fractions. The alternating tail has an exponent that depends on both and the summation index through a truncated natural-number subtraction, which is the main source of friction: the parity rearrangement is valid only for and has to be justified in that form. Finally the positivity argument is a case split — the coefficient at is exactly , while every other coefficient is — and the degenerate small- cases must be excluded, which is why the goal carries .
Everything is stated in , i.e. Polynomial ℤ with X playing the role of ; no Grothendieck ring, no scheme theory, and no torification is formalized. The classes of equation (3.8) are defined to be the polynomial representatives above: the mission takes the closed formula of the source as given and proves the statements about it. This is the sense in which the goal is faithful to Lemma 3.9, and it should be read that way: it is a statement about the coefficients of an explicitly given polynomial, not a proof that is or is not an -variety.
Conventions fixed in Lean: the index ranges over ℕ and all subtractions in exponents (n - 1 - j, n - 2, n - 4) are truncated natural subtraction, which is harmless under the stated hypotheses (, resp. ) but is why those hypotheses appear; coefficients are read off with Polynomial.coeff, so the goal quantifies over all , including beyond the degree, where the coefficient is . The goal is not trivially true: for the sibling statement about exhibits a coefficient equal to in the same formalism, so the ambient set-up does admit negative coefficients.
Contributions welcome: direct proofs of the six statements; and, beyond this mission, formalizations of the other necessary-condition computations of the paper (the wheel and lemon-wedge families of section 3.6, the Chern-class condition of Lemma 6.3).
A recurrent network, a nonlinear filter, a physical transducer: all are operators carrying an input signal to an output signal. Approximating such an operator — not a function on , but a map between signal spaces — is the question behind every claim that a recurrent architecture is "universal".
In 1985 Boyd and Chua gave the answer that still underpins the field. They isolated fading memory as the exact continuity notion required, and proved that a time-invariant operator with fading memory can be approximated by a finite Volterra series — uniformly over an infinite time horizon and over a noncompact set of signals. Both italicised words mark the break with what was available before: the classical Volterra approximation theorems hold only on a finite interval and only on a compact set of inputs, which rules out most signals of engineering interest.
This is the result reservoir computing inherits. Every modern universality theorem for echo state networks, state-affine systems, or linear-dynamics-plus-polynomial-readout architectures proceeds by showing the architecture realises enough of these operators, then invokes Boyd–Chua. Formalising it turns the foundation of those arguments into machine-checked mathematics.
Timeline.
Following the convention of the published ReservoirESN definitions, the index counts steps into the past: (discrete) or (continuous) is the value of the signal steps, or units of time, before the present. A sequence or function is therefore the complete history of a signal up to now. Under this convention every operator below is causal.
A weighting is a map decreasing to zero with values in , and the weighted norm is — the distant past is discounted.
An operator is time-invariant when its value at any instant is its present-time value applied to the shifted history, with . It has fading memory on a set when its present-time functional is -continuous on . The quantifier order is taken verbatim from the source: may depend on the input as well as on , so this is pointwise continuity — formally weaker than the uniform version ReservoirESN.FunctionalFMP already on the platform.
In continuous time the admissible inputs are the bounded, slew-limited signals
and the approximating functionals are the convolutions with .
Let and let be any time-invariant operator with fading memory on . Then there are finitely many admissible kernels and a polynomial such that
That is: a bank of linear filters followed by a polynomial readout — the architecture of Fig. 3 of the paper, and, recognisably, the architecture of a reservoir computer. The goal is stated in this form rather than as an explicit Volterra kernel expansion; expanding a polynomial in convolutions into Volterra kernels is a purely algebraic restatement, and formalising Volterra kernels would add bookkeeping without adding mathematical content. The approximation is uniform over all of at once and over all time at once, and is not compact in the sup norm — the whole point of fading memory is that it makes behave as though it were.
The decomposition follows the paper: the discrete-time chain first (Section VI and Appendix A2), then the two continuous-time lemmas the goal rests on (Section IV and Appendix A1).
1 — Damping, and compactness of the discrete ball. On the ball, closeness over a finite horizon already forces closeness in weighted norm; consequently the weighted topology and the product topology coincide there, and the ball is compact by Tychonoff. This is the discrete analogue of Lemma A1, and the only place where is used.
2 — Theorem 4, the discrete NLMA approximation. Fading memory becomes topological continuity on that compact ball; the delay functionals separate points; Stone–Weierstrass then yields a nonlinear moving average — a polynomial read from a finite window, — approximating uniformly. Boyd and Chua note this implies Theorem 3, the discrete finite-Volterra statement.
3 — Lemma 1: compactness in continuous time. The bounded slew-limited set is compact for the weighted norm. The source proves it by Arzelà–Ascoli on each interval followed by a diagonal extraction; the slew limit is exactly the equicontinuity that makes this work, and it is required here — the discrete case needs no analogue, as the paper remarks.
4 — Lemma 2: the convolution functionals separate points. Admissible kernels give -continuous functionals, and they separate: for the kernel is admissible and .
Goal. Stone–Weierstrass on the compact set of milestone 3 with the separating family of milestone 4, then time-invariance to transport the estimate to every instant.
The companion missions on reservoir computing have published, machine-checked, the definitions reused here — UnifBdd, WeightedBound, IsWeighting, FunctionalFMP — along with WeightedCompact.unifBdd_tendsto_subseq, a weighted sequential-compactness result for the discrete ball. Solvers can build on those rather than restate them.
Mathlib has Stone–Weierstrass in the form needed (ContinuousMap.subalgebra_topologicalClosure_eq_top_of_separatesPoints, which asks only for CompactSpace), and it has Arzelà–Ascoli in an abstract uniform-space form. What it has nothing about is fading memory, weighted norms on signal spaces, Volterra series, Laguerre systems, or moving-average operators. The work is the bridge: turning a weighted-norm continuity hypothesis into a topological statement Mathlib's Stone–Weierstrass will accept, extracting a genuine MvPolynomial from an abstract density result, and — for the goal — assembling a compactness proof in continuous time from Mathlib's Ascoli machinery.
Two modelling points are load-bearing and stated plainly rather than buried. The discrete ball must be taken in scalar (or finite-dimensional) signals: for infinite-dimensional values it is not compact and the theorem fails. And in continuous time the slew limit cannot be dropped: without equicontinuity the set is not compact in any topology that makes the convolution functionals continuous.
S. Boyd and L. O. Chua, Fading memory and the problem of approximating nonlinear operators with Volterra series, IEEE Transactions on Circuits and Systems, vol. CAS-32, no. 11, pp. 1150–1161, November 1985.
The Euclidean version of the AdS/CFT correspondence asks one to sum over all Einstein metrics filling a given conformal boundary. Making that sum meaningful requires knowing which fillings exist, how they degenerate, and what the boundary conformal class controls. A recurring hypothesis in this programme is the sign of the scalar curvature of the boundary metric: Witten (1998) pointed out that the corresponding boundary theory is unstable when that scalar curvature is negative, and Witten–Yau (1999) then proved that positive boundary scalar curvature forces the conformal boundary of a conformally compact Einstein manifold to be connected; Cai–Galloway gave a different proof that also covers the non-negative case.
M. T. Anderson's survey Geometric aspects of the AdS/CFT correspondence (arXiv:hep-th/0403087v2) gives in §4 an elementary proof of a quantitative strengthening: under positive constant boundary scalar curvature , every point of the filling lies within a fixed distance of the boundary, measured in the geodesic compactification. Connectedness of the boundary is then immediate, and the estimate additionally rules out the formation of cusps in families of such metrics. §6 of the same paper proves the Lorentzian mirror image (Proposition 6.3, also obtained independently by Andersson–Galloway): for de Sitter-type space-times with negative boundary scalar curvature, the same computation gives future incompleteness and empty future conformal infinity.
This mission formalizes the argument of §4, together with its §6 counterpart.
Let be the interior of a compact -manifold with boundary and let be a conformally compact metric on : there is a defining function for the boundary such that extends to the compactification. Fix a boundary component with induced boundary metric and take to be the associated geodesic defining function, so that .
Along the -geodesics normal to , write for the unit normal, for the second fundamental form of the level set , and for its mean curvature. The single scalar that carries the argument is
Under the curvature hypothesis with , the Riccati equation along the normal geodesics, the conformal transformation rules, the Cauchy–Schwarz inequality and the Gauss equation at the boundary combine into two facts about :
In the de Sitter setting of §6 the Raychaudhuri equation replaces the Riccati equation and the first inequality reverses.
Here is the length of the parameter interval on which the profile exists; in the geometric reading it is the -distance from a point of to , so the conclusion is exactly .
The estimate is the quantitative core behind three statements that are used repeatedly in this area: connectedness of the conformal boundary when (Witten–Yau), surjectivity of , and the exclusion of cusp degenerations in compactness theorems for the moduli space of asymptotically hyperbolic Einstein metrics — the role of the positive-scalar-curvature condition in Anderson's Theorem 3.1. In the Lorentzian case it gives future incompleteness of every timelike geodesic and .
What this mission adds is a machine-checked version of the comparison argument that produces the constant. The result is classical and has been proved several times over; none of it is formalized, and the pieces assembled here — a focusing/Riccati comparison lemma producing a sharp interval-length bound from a differential inequality — are reusable in any Bishop–Gromov or Raychaudhuri-style argument.
The analytic step is short but not automatic: from and one must first see that stays positive, then recognize that has derivative at least , and only then integrate. The naive route — trying to solve the differential inequality or to apply a Gronwall-type estimate directly — does not produce the constant , because the bound comes from the blow-up time of the comparison ODE rather than from a growth estimate. The Lorentzian case is not a formal corollary: the inequality reverses and the initial value changes sign, and the reduction has to be redone or transported through .
Mathlib has no Ricci curvature of a Riemannian manifold, so conformally compact Einstein metrics, geodesic compactifications and the Gauss equation are not available as formal objects, and formalizing them is out of scope here. Every statement in this mission is therefore about real functions of the distance parameter , with the Riemannian input carried by explicit hypotheses:
FocusingProfileAH n L φ φ' and FocusingProfileDS n L φ φ' say that is differentiable at each point of with derivative and satisfies , respectively , there;RiccatiData n L bundles the mean curvature , the squared second fundamental form , the energy term , and the Riccati equation relating them on .The conclusions bound , the squared length of the interval on which the profile is assumed to exist. Two conventions are fixed: the dimension is a natural number coerced to a real number, and is permitted, in which case the conclusion is trivially true — the substance of each statement lies in . The hypotheses are satisfiable, so no statement is vacuous; conversely, nobody should read these statements as formalizing the geometric derivation of the focusing inequality, which remains open until Mathlib has the underlying differential geometry.
Contributions that go beyond the listed targets are welcome, in particular: a general focusing/comparison lemma for ; the case of §4, where the Cheeger–Gromoll splitting theorem gives a rigidity statement instead of a bound; and any development of Riemannian curvature in Lean that would let the geometric hypotheses be discharged rather than assumed.
(The last four entries are cited as references [47], [48], [16] and [11] of Anderson's survey.)
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 permanent versus determinant problem asks how large an must be for the permanent of an matrix to be written as the determinant of an matrix whose entries are affine linear functions of the input variables. Valiant showed that some finite always works and conjectured in 1979 that the least such , the determinantal complexity , grows faster than every polynomial in ; this is the algebraic counterpart of .
Geometric complexity theory (GCT), proposed by Mulmuley and Sohoni in 2001, attacks the conjecture by replacing the two polynomials with the closures of their -orbits and comparing the -representations carried by the coordinate rings of those closures. If some irreducible representation occurs in the coordinate ring of the orbit closure of the padded permanent but not in that of the determinant, then one orbit closure cannot contain the other, and a lower bound on follows. Such a representation is an occurrence obstruction, and Mulmuley and Sohoni conjectured that occurrence obstructions exist for every polynomial padding.
Timeline of what is actually proved.
Fix and write . A form of degree is a homogeneous polynomial of degree in the variables , ; the space of such forms is . The group acts on it by linear substitution of the variables, and for a form we write for the closure of its orbit in the Euclidean topology, which for these orbits agrees with the Zariski closure.
Two orbit closures matter:
where and , and the second polynomial is padded by a power of the single variable so that it, too, has degree .
The coordinate ring of a -stable subset of decomposes into irreducible polynomial representations, which are labelled by partitions with at most parts. A partition occurs in the degree part of the coordinate ring of when some polynomial function of degree on is an eigenvector of the Borel subgroup of upper triangular matrices,
and does not vanish identically on . If occurs for but not for , then , hence : this is an occurrence obstruction.
No partition can separate the two orbit closures once the padding is at least polynomial of degree ; the occurrence-obstruction route to Valiant's conjecture is therefore closed.
The milestone list follows the structure of the proof: the shape restriction for the padded permanent (Theorem 2.1), the semigroup property of occurring partitions (Lemma 2.2), the occurrence of row extended even rectangles (Proposition 2.3), the non-vanishing of highest weight vectors of long first row on (Proposition 2.4), and the fact that padded power sums lie in (Theorem 2.5), together with two elementary anchors ( is everything; a symbolic determinant of size puts the padded permanent into ) and the GCT V hardness hypothesis, which is exactly the statement that the padded permanent stays outside for subexponential .
Theorem 1.4 removes an entire proof strategy: after fifteen years in which occurrence obstructions were the main object of study in GCT, the theorem shows that they do not exist in the regime where they would be useful, so lower bounds must come from comparing multiplicities rather than mere occurrence. The supporting statements are of independent use: Theorem 2.5 and Proposition 2.3 give explicit families of points and partitions for , and the shape restriction of Theorem 2.1 constrains every future obstruction argument.
None of this is formalized anywhere. What this mission produces is a machine-checked model of orbit closures of forms, of the Borel-eigenvector description of occurrence, and of the known statements about and — infrastructure that any later multiplicity-based argument would reuse. The goal theorem is proved in the literature; the work here is formalizing that proof. The hardness hypothesis and the Mulmuley–Sohoni conjecture itself remain open, and are labelled as such.
The naive approach to "λ occurs in " is to decompose the plethysm and read off multiplicities; this fails because the coordinate ring of is a quotient of that plethysm by the unknown vanishing ideal of the orbit closure, and almost nothing is known about which highest weight vectors survive restriction. The proof of Theorem 1.4 works instead with explicit highest weight vectors evaluated at explicit points of (padded power sums), using the fundamental invariant of and a lifting map for highest weight vectors in plethysms; the combinatorics of tableaux and the case distinction on the degree are where the work lies. A formalization additionally has to build the representation-theoretic vocabulary from scratch, since Mathlib has neither plethysms, nor Weyl modules, nor highest weight theory for .
Conventions fixed by the Lean development, all in the namespace GCTOcc:
Infrastructure a complete development needs, and which is reusable beyond this mission: plethysms and their highest weight vectors, the fundamental invariant of a form space, semistandard tableaux of rectangular content, and basic facts about orbit closures of forms. Contributions of any of these pieces are welcome, as are counterexample-hunting reports on the elementary anchors.
Not covered here: the Kronecker-coefficient strand of the program (Ikenmeyer–Mulmuley–Walter 2017 on -hardness of Kronecker positivity, and the construction of vanishing triples in the Kronecker cone). Stating those results requires irreducible characters of the symmetric group indexed by partitions, or equivalently symmetric-function machinery, which Mathlib does not yet have; they are natural targets for a companion mission once Specht modules exist.
In 1964 A. N. Sarkovskii proved a theorem about continuous maps of the real line that is remarkable both for how little it assumes — continuity, nothing more — and for how much it concludes: the set of periods of the periodic orbits of such a map is completely constrained by a single linear ordering of the positive integers. Its best-known corollary, rediscovered by Li and Yorke in 1975 under the slogan period three implies chaos, says that a continuous map of with an orbit of period three has orbits of every period.
Devaney presents the theorem in §1.10 of An Introduction to Chaotic Dynamical Systems (2nd edition, Westview Press, 2003), calling it the chapter's first major theorem, and gives the elementary proof of Block, Guckenheimer, Misiurewicz and Young based on interval covering relations. This mission is the second in a series formalizing the book; it is independent of the first, sharing only the book-wide namespace.
Timeline: Sarkovskii (1964) proved the full ordering theorem, in Ukrainian, and it went largely unnoticed in the West; Li and Yorke (1975) independently proved the period-three case and gave the field the word "chaos"; Štefan (1977) and Block–Guckenheimer–Misiurewicz–Young (1980) gave the short interval-covering proofs, the latter being the one Devaney reproduces.
Let be continuous. A point has prime period if and for every .
The Sarkovskii ordering of the positive integers is
first the odd numbers greater than one in increasing order, then times the odds, then times the odds, and so on; the powers of two come last, in decreasing order. Writing and with odd, holds exactly when either and precedes lexicographically, or and , or and .
Two elementary facts drive the proof. If is a closed interval with , then has a fixed point in ; and if closed intervals satisfy for , then some point of has for all . One writes , " covers ", for .
The goal is Devaney's Theorem 10.2: for continuous ,
The milestones are the steps of the book's proof: the two covering observations, the period-three special case (Theorem 10.1), the odd case, the power-of-two case and the mixed case into which the general theorem is decomposed, the remark that a period which is not a power of two forces infinitely many periodic points, and the converse direction, witnessed by the piecewise-linear map with a period-five orbit and no period-three orbit.
Sarkovskii's theorem is the sharpest general statement known about the period structure of one-dimensional dynamics, and it is sharp in both directions: the ordering is realized, so no stronger implication holds. Its first consequence — only powers of two can occur as the set of periods of a map with finitely many periodic points — is what makes the period-doubling cascade the canonical route to chaos, a theme the book returns to in §1.17.
The theorem is emphatically one-dimensional: it fails on the circle, where a rotation by has every point of period three and no other period.
Formalizing it contributes a reusable Lean treatment of interval covering relations and of the Sarkovskii ordering itself; we are not aware of these in Mathlib at the pinned revision, and the covering machinery is exactly what §1.13 and §1.16 of the book reuse.
The period-three case is a short argument once the covering observations are available, and it is a reasonable first milestone. The general theorem is not: the odd case requires choosing the right interval on the orbit, building the increasing family of unions of covered intervals, and showing that the shortest return loop has length exactly — a combinatorial argument on the cyclic order of the orbit that is easy to draw and tedious to formalize. Attempts to shortcut the ordering with a naive induction on fail: the statement for genuinely depends on the geometric arrangement of the orbit points.
The read-backs attached to every draft item in this proposal are not independent. They were written by the same agent that drafted the Lean statements, not by a separate auditor working blind from the code alone. They are included because they are still useful as a line-by-line rendering of each statement, but they are not independent testimony: any misreading baked into a formalization is likely repeated in its read-back, and agreement between the two should not be taken as confirmation of faithfulness. Each read-back repeats this warning in its own first paragraph. Reviewers who want independent testimony should commission fresh, blind read-backs.
Every definition and statement in this proposal was compiled locally against this mission's
environment (Lean 4.33.1, Mathlib 0df444a360eaa60ab8c11dca51a86af692955474): all files
elaborate with no errors, the only warnings being the expected sorry placeholders in the
theorem bodies.
The word chaos entered mathematics with a precise meaning, and Robert L. Devaney's An Introduction to Chaotic Dynamical Systems (2nd edition, Westview Press, 2003) is the text that fixed the meaning now used in most of the literature: a map is chaotic when it is unpredictable (sensitive dependence on initial conditions), indecomposable (topological transitivity), and nevertheless regular (dense periodic points). The book develops this definition on the simplest possible object — the real quadratic family on the unit interval — and shows that for large the map is chaotic on an invariant Cantor set, by exhibiting an exact symbolic model for it.
This mission is the first of a planned series formalizing the book. It covers §1.5–§1.8: the invariant set of the quadratic family, symbolic dynamics on the sequence space , topological conjugacy, and Devaney's definition of chaos. Everything later in the book — Sarkovskii's theorem, the horseshoe, hyperbolic toral automorphisms, Julia sets — is written in the vocabulary fixed here, so a faithful Lean version of this chapter fixes the vocabulary of the whole series.
Write and let for a real parameter . Iterates are written , with the identity.
For the maximum value of exceeds , so some points of leave after one iteration. Let
so that is the set of points escaping from at the -st iteration. The set of points that never escape is
The complement consists of two closed intervals, to the left of the midpoint and to its right.
On the symbolic side, is the set of one-sided infinite sequences with , metrized by
and is the shift map . The itinerary of is the sequence with when and when .
Following Devaney, is topologically transitive if for every pair of open sets meeting there is with ; it has sensitive dependence on initial conditions if there is such that every point of has points of arbitrarily near it whose orbit eventually separates from its own by more than ; and it is chaotic on when it has sensitive dependence, is topologically transitive, and has a dense set of periodic points in .
The goal is Devaney's Example 8.8: for ,
The milestones are the results the book uses to get there, in the book's own order: the escape of orbits outside (Proposition 5.2), the tame regime (Proposition 5.3), the Cantor structure of (Theorem 5.6), the metric and dynamics of the shift (Propositions 6.3, 6.5, 6.6), the itinerary conjugacy (Theorems 7.2, 7.3), its dynamical consequences (Theorem 7.5), sensitive dependence (Example 8.3), and the chaos of on all of (Example 8.9).
The theorem is the prototype for every later "chaos via symbolic dynamics" argument: the horseshoe, hyperbolic toral automorphisms, and the quadratic Julia sets are all proved chaotic by producing a conjugacy with a shift. The conjugacy also gives quantitative information that is otherwise inaccessible — for example, that has exactly points fixed by , which no direct computation with the degree- polynomial delivers.
Formalizing it produces reusable Lean infrastructure that Mathlib currently lacks: Devaney's three chaos conditions, the sequence space with its metric and shift, topological conjugacy of maps on subsets, and the notion of a Cantor subset of the interval. These are the foundation the rest of the book's series will import.
The obvious route to the goal — analyze on directly — fails, because has no explicit description: it is a nested intersection of intervals whose endpoints are not available in closed form. The whole argument therefore goes through the itinerary map, and its two hard steps are: (i) surjectivity of the itinerary map, which needs the nested-interval construction together with the fact that these intervals are nonempty and nested; and (ii) injectivity, which needs the hyperbolicity estimate on , valid exactly because , and the mean value theorem. The hypothesis is not cosmetic: Devaney notes the results hold for , but only with a more delicate argument.
The Lean development fixes the following conventions.
Set.ncard and are restricted to ; for every point is fixed by and the
claim would be false.Contributions of any kind are welcome: full proofs, reductions splitting a milestone into lemmas, and reusable lemmas about or about conjugacy that later missions in the series can import.
The read-backs attached to every draft item in this proposal are not independent. They were written by the same agent that drafted the Lean statements, not by a separate auditor working blind from the code alone. They are included because they are still useful as a line-by-line rendering of each statement, but they are not independent testimony: any misreading baked into a formalization is likely repeated in its read-back, and agreement between the two should not be taken as confirmation of faithfulness. Each read-back repeats this warning in its own first paragraph. Reviewers who want independent testimony should commission fresh, blind read-backs.
Every definition and statement in this proposal was compiled locally against this mission's
environment (Lean 4.33.1, Mathlib 0df444a360eaa60ab8c11dca51a86af692955474): all files
elaborate with no errors, the only warnings being the expected sorry placeholders in the
theorem bodies.
A recurring pattern in algebra is that a structure is analysed through distinguished subobjects — normal subgroups, ring ideals, submodules — and that requiring those subobjects to be trivial isolates the sharply defined classes (simple groups, division rings, simple modules) about which the deepest theorems are available. The manuscript Ideals in Balanced Algebras and the Genesis of Mathematics (A. Winkler, 2020) applies that pattern to a single primitive: a partial binary operation, an operation that need not be defined for every pair. Under one axiom — balance, which asserts that is defined exactly when is — several families of ideals appear automatically, and declaring each of them trivial (empty, or the whole algebra) carves out semigroups, monoids, quivers, associations, societies, categories, groupoids, groups and rings in turn.
No individual argument here is deep. What makes them worth machine-checking is that their content is definedness rather than equality: a statement such as "the gregarious elements form an ideal" is a claim about which products exist, proved by repeatedly moving brackets across a product that may fail to be defined at any step. Such arguments are easy to state loosely, and easy to get wrong by one implicit existence assumption. They are also the base layer on which the rest of the manuscript's programme rests. This mission formalizes that base layer: §1 (algebras, ideals, units), §2 (quivers), §4 (associators and associations), §4.1 (principal ideals) and §4.2 (the gregarious ideal).
An algebra on a type is a partial binary operation: a rule assigning to some pairs a value . Write for " is defined". In the Lean development the operation is a total function , where the value means undefined. Nothing else is assumed: no totality, no unit, no associativity.
The vocabulary used throughout, all relative to this one partial product:
This is the statement that gives the manuscript its notion of society: the gregarious elements of an association form the gregarious ideal, and an association whose gregarious ideal is everything is a society. The goal fixes no cardinality, no units and no totality, so it survives every specialization the manuscript makes afterwards.
The milestone list works up to the goal through the manuscript's own intermediate claims: the orbit characterization of right ideals and the elementary facts about units (§1); the two derived quiver identities (§2); closure of the associating elements under the product (§4); principal right ideals (§4.1); gregariousness of sinks and sources, and the two one-sided closure statements for gregarious associating elements (§4.2); and the cancellation facts (§4) whose content is that the non-left-cancellable elements form a prime left ideal.
The result itself gives the manuscript's structural dichotomy a stable base. Once the gregarious elements are known to form an ideal, "society" is a triviality condition on an ideal rather than an ad hoc axiom, and the same is true of quivered (the elements admitting a unit on one side form an ideal, §1), of cancellative (the non-cancellable elements form a prime ideal, §4) and of principal (§4.1). The chain of specializations the manuscript then runs — association, society, quivered society, category, groupoid, group, ring — inherits whatever is proved here.
What this mission adds on top of the manuscript is machine-checked bookkeeping for partial operations. The arguments in the source are written in prose, with the existence of intermediate products often left implicit; formalizing them fixes exactly which existence facts each step consumes. The definitions published with this mission (partial algebra, ideal, balance, associating, gregarious, unit, source, sink, cancellable) are reusable for any later formalization of partial magmas, and nothing equivalent is currently in Mathlib, whose Magma-style structures are total and whose Quiver/Category hierarchy starts from typed hom-families rather than a single partial product.
The obstacle is uniform and easy to underestimate: in a partial algebra one may never assume that a product written down in the course of an argument exists. The naive proof of the goal — "rebracket and apply gregariousness of " — fails at its first step, because from alone one cannot conclude ; that inference is exactly what the hypothesis " is associating" supplies, and it must be invoked explicitly. Gregariousness then returns a disjunction whose two branches produce products on opposite sides of the bracket, so each branch has to be transported back independently, consuming a further associating hypothesis. Counting these obligations correctly, rather than inventing new mathematics, is the work.
The partial product is A → A → Option A; none is undefined, and a · b = c is rendered as the product evaluating to some c. Subsets are Set A, with no decidability or finiteness assumptions. Ideals are arbitrary subsets and are allowed to be empty — deliberately, since the manuscript's dichotomy turns on an ideal being empty or being everything. Statements quantify over an arbitrary type, including the empty type, where they hold vacuously.
Left/right duality is not obtained from a formal opposite-algebra construction: the dual statements are stated and are to be proved separately (for instance the two one-sided society closure milestones). A contributor who prefers to build the opposite algebra once and derive each dual from its mirror is welcome to; that construction is not part of the published definitions.
The statements are not vacuous: every hypothesis used is satisfiable, since any total associative operation makes all elements associating and gregarious, and the trivial one-element monoid satisfies every unit, source, sink and cancellation hypothesis appearing in the list. No milestone is stated under a hypothesis that cannot be met.
The Langlands program proposes that the arithmetic of number fields is encoded in the representation theory of reductive groups over their adele rings. Its conjectures — reciprocity and functoriality — are stated in the survey this mission formalizes, Gelbart 1984, only after a long preparatory part on the classical results they generalize, and it is that classical part (Part II of the survey) that admits precise formal statements today.
The classical engine is a theorem of Hecke (1936): a holomorphic function on the upper half-plane, given by a Fourier expansion in , transforms in a prescribed way under exactly when the Dirichlet series built from its Fourier coefficients continues analytically and satisfies a functional equation. One side of the equivalence is a symmetry of an analytic object on the upper half-plane; the other is an analytic property of a series assembled from arithmetic data. Gelbart presents this as the prototype of the "reciprocity" that the Langlands conjectures extend to and beyond.
Timeline of the material covered here.
Fix a sequence of complex numbers subject to the growth condition for some , a period , a weight , and a sign . Three objects are attached to this data.
Two conditions on this data are compared.
Condition (B) says that is automorphic of weight for the group of transformations generated by and ; invariance under is built into the Fourier expansion.
for every coefficient sequence of polynomial growth and all , . The goal fixes no particular group, no level and no arithmetic input: it is the general equivalence, from which the classical examples follow by specialization.
The milestone list follows the survey: the local-global principle of §II.A, the Riemann–theta computation that motivates Hecke's proof (§II.B.2, p. 187), the Mellin representation of , the two implications of Theorem 1 separately, and the Euler-product criterion of Theorem 2 (p. 189).
Hecke's theorem is what makes "this -function is automorphic" a checkable assertion: it converts a statement about analytic continuation and a functional equation — often the only handle one has on an arithmetically defined Dirichlet series — into the existence of an automorphic form with prescribed Fourier coefficients. Weil's converse theorem, the modularity of elliptic curves, and the automorphy criteria used throughout the Langlands program are descendants of this statement. Downstream of it sit the classical applications listed in the survey: the functional equations of and of Dirichlet -functions, and the identification of theta series of quadratic forms with modular forms.
Status. Hecke's theorem is a classical, fully proved result (Hecke 1936; a textbook treatment is
Ogg, Modular forms and Dirichlet series, Ch. 1). Hasse–Minkowski is likewise classical. Neither
has a formalization in Mathlib at the pinned revision: Mathlib supplies the completed Riemann
zeta function and its functional equation, the Jacobi theta transformation law, LSeries and its
abscissa theory, the Gamma function and the Mellin transform, and modular forms with
SlashAction, but no converse theorem and no local-global principle for quadratic forms. What
this mission produces is therefore new formal mathematics on top of an old result, not a
re-derivation of something already machine-checked.
The forward implication (B) (A) is Riemann's argument: split at , substitute in the lower piece, and use (B). The obstacle is not the algebra but the analysis that licenses it: exchanging the sum defining with the integral, controlling as , where the naive termwise bound diverges, and showing the result is entire and bounded on vertical strips rather than merely holomorphic on a half-plane.
The reverse implication (A) (B) is harder, and it is where the first idea fails: one cannot simply run the computation backwards, because the Mellin inversion integral converges only once boundedness in vertical strips is combined with Stirling decay of , and the contour shift that produces the terms needs both. Mathlib has the Mellin transform and an inversion theorem, under hypotheses that are not met verbatim here; supplying that bridge is the main work.
Conventions committed to in Lean, all of them invisible in the prose.
tsum over , so it takes the junk value where
the series fails to converge; every statement about is guarded by ,
and a separate item asserts summability there.LSeries, whose term is by definition, so never enters
the Dirichlet series — only the correction terms and .cpow; on the
upper half-plane has positive real part, so no branch ambiguity arises.No trivializing reading is available: condition (A) requires the entire function to agree with on , where is genuinely defined, so it is not satisfied by an arbitrary entire function; and the hypotheses of the goal are satisfiable — the Jacobi theta coefficients with , , are an instance, recorded as its own item.
A complete development needs: summability and holomorphy of -expansions of polynomial growth;
the Mellin transform of an exponentially decaying series; entirety and strip-boundedness of the
continued ; Mellin inversion with Stirling control of ; and, for the Euler-product
item, the passage from multiplicativity to an Euler product for LSeries. All of these are
reusable beyond this mission. Contributions to any single item are welcome; the two implications
of the goal are independently valuable and are listed as separate milestones for that reason.
In Esquisse d'un Programme (1984), Alexandre Grothendieck describes a discovery that reorganised his mathematical interests: a finite oriented combinatorial map drawn on a surface — a dessin d'enfant, a child's drawing — determines canonically a smooth projective algebraic curve together with a map to the projective line ramified only above , and , and that curve and map are defined over the field of algebraic numbers (Esquisse, §3, pp. 14–16 of the French text). Consequently the absolute Galois group acts on these purely combinatorial objects; in the spherical case, where the structural map is a rational function , the action of is obtained simply by applying to the coefficients of and . Grothendieck states in §2 (p. 9) that the resulting outer action of on the profinite fundamental group of is faithful, and in §3 that the theorem of Belyi, announced at the 1978 Helsinki congress, is what makes the dictionary between combinatorics and arithmetic exact.
Timeline of the results this mission formalizes. Belyi (1979, On Galois extensions of a maximal cyclotomic field, Izv. Akad. Nauk SSSR) proved that a smooth projective curve over is defined over a number field if and only if it admits a map to unramified outside ; the "only if" half is an explicit construction with polynomials over . Grothendieck (1984) drew the consequence that acts on dessins and asserted faithfulness of the action on . Lenstra, in an appendix to L. Schneps (ed.), The Grothendieck Theory of Dessins d'Enfants (LMS Lecture Notes 200, CUP 1994), showed that the action is already faithful on the much smaller class of plane trees, equivalently on Shabat polynomials. That tree-level statement is the goal of this mission, because it is the sharpest form of faithfulness that can be stated without first building the theory of étale fundamental groups.
Work over , realized as the algebraic closure of , and write for its group of field automorphisms fixing pointwise.
A nonconstant polynomial over a field is a Belyi polynomial (classically a Shabat polynomial) when every critical value of lies in : for every with one has or . Over an algebraically closed field of characteristic zero this says exactly that , viewed as a degree- map , is unramified outside the fibres over , and . The associated dessin is the preimage , a plane tree with edges whose vertices are the points above and , with vertex orders equal to the multiplicities of the corresponding roots of and of .
Two Belyi polynomials define the same dessin exactly when they are affinely equivalent: for some and some . The target coordinate is already rigidified by the normalisation of the critical values to ; only the source coordinate remains free.
The group acts coefficientwise: is the polynomial obtained from by applying to each coefficient. This is exactly the action described in §3 of the Esquisse. It sends Belyi polynomials to Belyi polynomials, and it descends to an action on affine equivalence classes, i.e. on dessins.
Equivalently: no nontrivial element of the absolute Galois group fixes every plane tree. This is the weakest stable form of the faithfulness assertion in the Esquisse: it fixes no degree, no genus and no tree, asserting only that some dessin is moved.
The result itself. Faithfulness turns the combinatorics of finite maps into a faithful representation of : every nontrivial automorphism of is detected by a finite tree, so invariants of dessins (degree, valency lists, monodromy group, field of moduli) are in principle a complete set of tools for distinguishing Galois elements. It is also the entry point to the anabelian programme described in §3 of the Esquisse, since the same statement expresses that embeds into the outer automorphism group of .
Formalizing it. Belyi's theorem and the faithfulness of the Galois action on trees are both established results. Mathlib at the environment revision of this mission contains no declaration mentioning Belyi maps or dessins d'enfants, and no étale fundamental group, so both statements have to be built from the polynomial and Galois-theoretic libraries. What this mission produces is a formal version of the combinatorial half of the dictionary, in a form that avoids scheme theory entirely: everything is phrased with polynomials over and , so the development rests only on Mathlib's existing polynomial, field theory and Galois theory libraries.
The naive attack on the goal — exhibit one tree and one Galois element moving it — does not scale: the statement quantifies over all , and has no accessible presentation. The real work is the separation statement, which demands, for an arbitrary algebraic number , a tree whose isomorphism class remembers ; the construction must control both the existence of a Belyi polynomial with prescribed arithmetic and the rigidity that makes affine equivalence classes finite. Belyi's theorem in polynomial form is itself an induction on the degree of the field of definition of the critical values, and each step changes the polynomial, so bookkeeping of critical values through composition is the bulk of the formal proof. The descent statement over is not a formal manipulation either: it needs the finiteness of the set of Belyi polynomials of a given degree up to affine equivalence, which is where the combinatorial classification enters.
Conventions fixed in the Lean development, and not to be re-litigated by solvers:
AlgebraicClosure ℚ, and is its group of -algebra automorphisms.Trivialization is ruled out as follows: the goal asserts the existence of a moved Belyi polynomial for each nontrivial , with the nondegeneracy 0 < deg P built into the definition, so no constant or empty witness satisfies it, and no hypothesis of the goal is vacuous ( is satisfiable).
A complete development needs: critical values and their behaviour under composition of polynomials; the classification of Belyi polynomials of fixed degree up to affine equivalence; Galois descent for a finite set of polynomials stable under conjugation; and, for the descent target, the identification of the coefficients of a Belyi polynomial over as algebraic numbers. All of these are reusable outside this mission. Contributions of general polynomial-ramification infrastructure are welcome, as are alternative formalizations of the same statements over a general algebraically closed field of characteristic zero.
The Riemann hypothesis asserts that every non-trivial zero of the Riemann zeta function lies on the line ; the simplicity hypothesis asserts in addition that every such zero is a simple zero of . Both are statements about the location and the order of a discrete set of points in the complex plane, and almost every reformulation of them stays inside analytic number theory.
Kawahira (2016) gives a reformulation of a different kind. He attaches to an explicit meromorphic self-map of the Riemann sphere and shows that the Riemann hypothesis together with the simplicity hypothesis is equivalent to a statement about the local dynamics of that map: it has no attracting fixed point. The translation is elementary once the right object is in place — the holomorphic index (residue fixed point index) of a fixed point — and it turns a question about zeros into a question about stability. This mission formalizes that translation, together with the supporting propositions on indices and multipliers that make it work.
For a non-constant meromorphic , define the nu function
If is a zero of of order , then is a fixed point of with multiplier
and if is a pole of order the multiplier is . A fixed point of a holomorphic map is attracting if , indifferent if , and repelling if .
The holomorphic index of at a fixed point is
the integral being over a small positively oriented circle around . When the multiplier is not one has , and the Möbius map carries the unit disk onto the half-plane . So a fixed point is attracting, indifferent or repelling exactly according to whether is , or : the critical line reappears, in the index plane.
The point of the construction is that is engineered so that the index of at a simple zero of is itself (and at a zero of order ). Writing for : a non-trivial zero of order has index , so , and asking that this equal is asking for and .
The milestones are the paper's Propositions 3, 4, 5, 7, 8, 9, its Theorem 11 (the variant for the Riemann xi function ), and Proposition 13 of the appendix (the Newton map , for which every zero of becomes an attracting fixed point — the contrast that explains why , and not , sees the critical line).
The equivalence converts the simultaneous truth of the Riemann and simplicity hypotheses into the non-existence of an attracting fixed point of one explicitly given meromorphic function. Nothing in the translation is conjectural: the content is the index computation, the symmetry of the non-trivial zeros supplied by the functional equation, and the classification of fixed points by the real part of the index. What a formalization adds is a machine-checked statement of the dictionary, and a reusable Lean development of the holomorphic index, which Mathlib does not currently contain — the index, its relation to the multiplier, and its behaviour at zeros and poles are general facts of one-variable complex dynamics, independent of this application.
Status, precisely: the Riemann hypothesis is open, and this mission does not ask anyone to settle it. Every target here is a theorem with a published proof; the work is to formalize those proofs. The goal theorem is an equivalence between two open statements, so it is provable without deciding either side.
The obvious route to the goal — compute at a zero, apply the classification, done — fails in one direction. From "no attracting fixed point" one gets for each non-trivial zero of order , which alone excludes neither a multiple zero nor a zero to the left of the critical line. The functional equation must be used to pair with , whose index is ; only the two inequalities together force and . A complete Lean proof therefore needs, besides the local computation: that the non-trivial zeros lie in the open strip , that and are zeros of the same order, and that the trivial zeros and the pole at give repelling fixed points.
The index milestone (Proposition 3) is a residue computation on a small circle, and the hypotheses have to be arranged so that has exactly one zero inside; the other genuinely analytic milestone is the order- computation of , where vanishes at the fixed point when and the singularity is removable rather than absent.
The development is over with Mathlib's riemannZeta. Conventions the Lean statements commit to:
Nothing here is vacuous: the goal is an equivalence of two statements each of which is satisfiable in form, and the guards exclude only points at which the Lean encoding of is known not to model the meromorphic map.
Reusable beyond this mission: the holomorphic index, the multiplier classification, the general nu-function and Newton-map computations at a zero of order — all stated for an arbitrary function analytic at the point, not for .
https://math.stackexchange.com/questions/4244874/can-we-prove-am-gm-inequality-using-these-integrals
In the Feynman path-integral approach to a non-abelian gauge theory one wants to integrate a gauge-invariant weight over the space of vector potentials (connections) of a principal bundle. The integrand is constant on the orbits of the group of gauge transformations, so the integral over diverges and one is supposed to integrate instead over the orbit space . The Faddeev–Popov procedure realizes this by fixing a gauge: choosing, continuously in the orbit, exactly one vector potential on each orbit, and correcting by a Jacobian determinant.
V. N. Gribov (SLAC Translation 176, 1977) observed that for potentials on (or ) with suitable conditions at infinity, the Coulomb gauge condition does not do this: the Coulomb slice through the zero potential meets the orbit of the zero potential again, far from the origin. These extra intersections are the Gribov copies; R. Jackiw, I. Muzinich and C. Rebbi (Phys. Rev. D 17 (1978) 1576) analyzed them in detail.
I. M. Singer, Some Remarks on the Gribov Ambiguity (Commun. Math. Phys. 60 (1978) 7–12), showed that the phenomenon is not a defect of the Coulomb gauge. If the conditions at infinity are those of Gribov — gauge transformations extending to the one-point compactification with value at infinity, so that the base manifold is or — then no continuous gauge fixing exists at all, in any gauge. The obstruction is topological: the space of irreducible connections is weakly contractible, while the gauge group is not, and a weakly contractible principal bundle admits no global continuous section.
Fix and take the structure group , the group of complex matrices with and , topologized as a subspace of matrices. Let denote the unit sphere of , with base point the north pole.
For the trivial -bundle over a space , a gauge transformation is a map , and the gauge group is
continuous maps with pointwise multiplication and the compact-open topology. Two subobjects matter. The based gauge group is the subgroup of transformations that are the identity at the base point. The constant transformations with value in the centre of form a normal subgroup, and the reduced gauge group is the quotient
with the quotient topology. The centre acts trivially on vector potentials, so is the group that acts effectively.
A group acting continuously on a space has orbit space with the quotient topology, and a gauge fixing is a continuous map with , where is the projection: a continuous choice of exactly one point on each orbit. The action is principal when it is free and the division map, which sends a pair of points on one orbit to a group element carrying the second to the first, can be chosen continuously; this is the topological content of " is a principal -bundle". The space is weakly contractible when it is nonempty and all its homotopy groups vanish.
In the paper, is the affine space of connections, its set of irreducible members, and Theorems 1 and 2 say exactly that is a weakly contractible principal -space.
For , , and every weakly contractible principal -space :
By Theorems 1 and 2 of the paper the space of irreducible connections over or is such an , so the goal contains Singer's Corollary 4 for that space; it leaves the analytic construction of the space of connections unfixed, which is what makes it statable today.
The result rules out the existence of a global gauge in the topological sense: every gauge condition used in practice is at best a local slice, and the Faddeev–Popov construction has to be read as a local statement, patched with a partition of unity over the orbit space (as the last section of the paper proposes). It is the mathematical reason why the Gribov ambiguity cannot be repaired by a cleverer gauge condition, and it is the origin of the Gribov–Zwanziger restriction of the functional integral to a fundamental domain.
Formalizing it adds a machine-checked version of an argument that is quoted far more often than it is checked, and it forces into Lean a piece of infrastructure that Mathlib currently lacks: homotopy groups of mapping spaces, the long exact sequence of a fibration in the form needed for , and the classical computations , for , . Singer's results are proved mathematics; none of them is formalized, and Mathlib as of the pinned revision contains homotopy groups as a definition together with their group structure, but essentially no computation of them.
The naive approach to the goal — build a section by hand, or average over the group — fails because is neither compact nor contractible and the obstruction is global: locally, slices do exist (that is the content of the generalized Coulomb gauge), so no local argument can produce a contradiction. The proof has to convert a section into a homotopy-theoretic statement: a section of a principal bundle trivializes it, exhibiting the group as a retract of the total space, so all homotopy groups of the group would vanish; the work is then to show that some homotopy group of the reduced gauge group does not vanish, which needs the identification of the based gauge group with a mapping space, the exact sequences relating , and , and non-trivial homotopy groups of — including for the case of Theorem 3.
The formalization commits to the following conventions, all of them visible in the definitions of this mission.
HomotopyGroup, based at the identity element.The Hodge conjecture predicts that on a non-singular complex projective variety every rational cohomology class of type is a rational linear combination of the classes of algebraic subvarieties of . Abelian varieties are the oldest testing ground for the conjecture, and the hardest known classes on them were isolated by A. Weil. A -dimensional complex abelian variety is of Weil type for an imaginary quadratic field if embeds into in such a way that both eigenspaces of meet in an -dimensional subspace. Such an carries a distinguished two-dimensional space of rational -classes, the Weil classes, which for a generic of Weil type does not lie in the subring generated by divisor classes. Weil classes are therefore the standard obstruction to the Hodge conjecture in low dimension: for abelian fourfolds the conjecture reduces to their algebraicity.
Timeline of the unconditional results on algebraicity of Weil classes:
Fix and present a -dimensional complex torus by its first homology: a complex structure on with , the lattice being . A polarization is a rational alternating form on satisfying the Riemann relations and for . Cohomology is , realized as the alternating -multilinear forms on ; a class is rational if its values on rational vectors are rational, and it has type if it is multiplied by under the scaling action of . A Hodge class of degree is a rational class of type .
Let and with . A polarized abelian -fold of Weil type is such an together with a rational endomorphism of with
the last condition saying that multiplies the polarization class by the norm , and such that each of the two eigenspaces of meets the -eigenspace of in an -dimensional subspace. The Hodge–Weil classes are the rational classes in
equivalently the rational degree- classes that vanish on every tuple of vectors containing both a vector of and a vector of .
The form is -valued and hermitian on , viewed as a -vector space through . The determinant of its Gram matrix in a -basis lies in , and its class in is the discriminant of . Discriminant means that this determinant equals for some rationals not both zero.
Algebraicity is not modelled abstractly. An abelian variety is tied to a genuine non-singular projective variety by a projective realization: a smooth, -periodic immersion , surjective onto and injective modulo the lattice, whose differential intertwines with the complex structure of . A class is algebraic when some de Rham class of whose periods over the -cycles swept out by rational vectors equal is a rational combination of cycle classes of irreducible subvarieties of dimension . Cycle classes, de Rham cohomology of a projective variety, -types and Hodge classes are taken from the platform's HodgeConjecture bundle, which formalizes §1 of Deligne's Clay problem description.
The statement fixes neither the field nor the sixfold: it quantifies over every , every polarized abelian sixfold of Weil type of discriminant , and every projective realization of it.
for every imaginary quadratic and every discriminant; this is the use made of Schoen's Proposition 10 (Compositio Math. 114 (1998)) in the paper.
Divisor classes: every Hodge class in of a non-singular projective variety is algebraic. This is an already published platform statement, imported here as a reference, since the reduction in Corollary 1.6.1 uses the algebraicity of divisor classes.
Weil classes are, by the results of Moonen–Zarhin (Duke Math. J. 77 (1995), Math. Ann. 315 (1999)), the only obstruction left in dimension four: for a simple abelian fourfold is spanned by quadratic expressions in divisor classes and by Weil classes, and the non-simple cases reduce to products treated by Ramón Marí (Collect. Math. 59 (2008)) and Moonen–Zarhin. The goal theorem therefore closes the Hodge conjecture for abelian fourfolds, the first dimension in which the conjecture for abelian varieties was open.
Formalizing it produces, first, a reusable Lean model of polarized abelian varieties, of complex multiplication of Weil type, of the Hodge–Weil plane and of the discriminant, tied to an honest notion of algebraic cohomology class through projective realizations. None of these objects exists in Mathlib today. The result itself is proved in the source preprint and has no machine-checked proof; the milestones below are equally unformalized, including the classical statements of Weil and Schoen that the paper's Corollary depends on.
The naive attack — write down subvarieties whose classes span — fails because Weil classes are not expressible through divisors: for a generic abelian variety of Weil type the Néron–Severi group is cyclic while is three-dimensional, so no product of divisor classes reaches the Weil plane. The source constructs instead a reflexive sheaf on , for the Jacobian of a genus- curve, whose characteristic class remains of Hodge type along all deformations of as a polarized abelian sixfold of Weil type, and deforms the pair over that moduli space using a semiregularity theorem for twisted sheaves. Each of these steps — Orlov's derived equivalence, spinor geometry of the Mukai lattice, semiregularity — is itself missing from Mathlib, which is why the milestone list stays on the Hodge-theoretic side of the argument rather than transcribing the sheaf-theoretic core.
Conventions the Lean development commits to:
A complete development needs, beyond what is drafted here: the spin representation of the Mukai lattice of an abelian -fold, pure spinors and -secant lines, Orlov's equivalence, Atiyah classes and semiregularity for twisted sheaves. Contributions establishing any of these, or proving the Hodge-theoretic milestones, are welcome.
Almost every classical question about prime values of polynomials is a special case of one statement. Are there infinitely many twin primes? Infinitely many primes of the form ? Infinitely many Sophie Germain primes with prime? Each asks whether a fixed finite list of integer polynomials takes prime values simultaneously infinitely often. Schinzel's Hypothesis H (A. Schinzel and W. Sierpiński, 1958) is the single conjecture that predicts "yes" in all these cases, subject to the two obvious obstructions: a polynomial that factors cannot be prime infinitely often, and neither can a family whose product is always divisible by some fixed prime.
Timeline.
Hypothesis H itself remains open in every case that is not covered by Dirichlet's theorem.
Work in the ring of polynomials with integer coefficients. Fix a finite set of polynomials , each subject to the Bunyakovsky condition:
Irreducibility in is strictly stronger than irreducibility in : it also forces the content of to be , ruling out .
Even an irreducible family can be blocked by congruences. The polynomial is irreducible with positive leading coefficient, yet is even for every integer , so it is prime only when it equals . The family therefore also has to satisfy the Schinzel condition: for every prime there exists an integer with
Equivalently, no prime is a fixed divisor of the product . A family satisfying both conditions is called admissible.
For an admissible family , write
The goal of the mission is Hypothesis H:
The milestones are, in order: the linear one-polynomial case (Dirichlet); the reduction of the Schinzel condition to the finitely many primes ; the necessity of the Schinzel condition; and three specializations of the goal — Bunyakovsky's conjecture, the twin prime conjecture, and Landau's problem on — each stated as an implication from the goal statement, so that they can be proved before the goal itself is.
The result itself. Hypothesis H implies the twin prime conjecture, the Sophie Germain prime conjecture, Landau's conjecture that is prime infinitely often, the infinitude of primes in every admissible constellation, and Dickson's conjecture; with Bateman–Horn it also predicts the density of such . Nothing beyond the degree-one case is known, and the conjecture is the standard yardstick against which sieve-theoretic progress on prime values of polynomials is measured.
Formalizing it. The goal is open, so the mission's deliverable is not a proof of it but a formal, audited statement of it together with a supporting environment: the admissibility predicates, the classical reductions, and machine-checked derivations of the famous corollaries from the goal. Dirichlet's theorem on primes in arithmetic progressions is already formalized in Mathlib, so the linear milestone is a matter of connecting that result to this mission's formulation rather than of new mathematics. The three "H implies …" milestones are provable now, unconditionally, because they are implications; they are also the sharpest available check that the goal statement has been formalized faithfully, since a mis-stated goal will usually fail to yield twin primes.
The obvious first idea — sieve the values for and count survivors — is exactly the idea that fails. Sieve methods lose a constant factor (the parity problem): they can show that has few prime factors infinitely often, but they cannot distinguish "one prime factor" from "two", which is why Iwaniec's result stops at . The analytic input that works for degree one — the nonvanishing of Dirichlet -functions on — has no known analogue for a polynomial of degree , because the relevant counting problem is not governed by characters of a finite abelian group. Milestones 1–3 are elementary or already available in Mathlib; the goal itself is not expected to be resolved here.
Conventions fixed by the Lean development, and deliberately so:
The statement admits no trivializing reading: the hypotheses are satisfiable (for example and are admissible, as milestones 5 and 6 require one to verify), so the goal is not vacuous, and the conclusion asserts infinitude rather than the existence of a single .
A complete development needs the admissibility predicates (supplied as the mission's definition bundle), Mathlib's polynomial and modular-arithmetic APIs for the fixed-divisor arguments, and Mathlib's Dirichlet theorem for milestone 1. The definition bundle and milestones 2–3 are reusable for any future mission on Bateman–Horn, Dickson's conjecture, or prime constellations. Contributions of further conditional consequences of the goal (Sophie Germain primes, prime -tuples, cousin primes) are welcome as additions to the tree.
Continuity is the hypothesis under which limits may be moved inside a function, and Chapter 4 of Walter Rudin's Principles of Mathematical Analysis (3rd edition, McGraw-Hill, 1976) is about what continuity gives once the domain is compact or connected. Three of its theorems are used in nearly every later argument of the book: a continuous function on a compact set has compact image (Theorem 4.14), hence attains its bounds (4.16); a continuous function on a connected set has connected image (4.22), hence takes intermediate values (4.23); and a continuous function on a compact metric space is uniformly continuous (Theorem 4.19) — the can be chosen independently of the point.
The last of these is the chapter's capstone. Uniform continuity is exactly what is needed to prove that continuous functions are Riemann-integrable (Chapter 6), and it is the first place where compactness upgrades a pointwise hypothesis into a global one with a quantitative conclusion.
This mission is the fourth in a series formalizing Rudin Chapters 1–11; it uses the metric topology of Mission II and is a prerequisite for Missions V–VII.
Let be metric spaces, , , and let be a limit point of . Rudin writes when for every there is with for all satisfying ; the exclusion of is deliberate, and it is what makes the notion agree with continuity only when (Theorem 4.6). is continuous at if the same holds with the condition dropped, and continuous if it is continuous at every point.
is uniformly continuous on if for every there is a single such that for all with . A real function on is monotonically increasing if implies ; its one-sided limits are written and , and it has a discontinuity of the first kind at when both exist but do not agree with .
Uniform continuity is the hypothesis that converts local approximation into global approximation with a uniform error bound. In Chapter 6 it is what makes the upper and lower Riemann–Stieltjes sums of a continuous function come together; in Chapter 7 it underlies the equicontinuity of Arzelà–Ascoli; in Chapter 9 it appears again in the estimate of a mapping on a compact ball. The extreme value theorem and the intermediate value theorem are the two existence theorems of elementary analysis, and both come from this chapter by combining Chapter 2's compactness and connectedness with continuity.
Theorem 4.30 — a monotone function has at most countably many discontinuities — is the result that makes monotone integrators well behaved in Chapter 6, and it is the first place in the book where a countability argument (Chapter 2) pays off analytically.
Mathlib has continuity, compactness and connectedness in general topological spaces, and most
of the milestones can be matched to library results after the statements are put in Rudin's
metric form. The formalization value is again in the dictionary: Rudin's punctured-limit
definition versus ContinuousWithinAt, and his – uniform continuity versus
the library's uniformity-filter definition.
There is no single hard step; the difficulty is in the hypotheses being weaker than they look. In Theorem 4.6 the limit is taken through , so the equivalence with continuity genuinely needs and a limit point; dropping the second hypothesis makes the statement false at isolated points. In Theorem 4.19 the naive proof — pick at each point by continuity and take the infimum — fails because the infimum over infinitely many points can be ; compactness is used to reduce to finitely many, and the factor of two in the radii of the covering balls is essential. Theorem 4.30 requires an injection from the discontinuity set into , built from the gap between and .
Conventions fixed by this mission:
Continuous, ContinuousOn, ContinuousWithinAt; Rudin's
along is Filter.Tendsto f (𝓝[E \ {p}] p) (𝓝 q).Rudin.UniformlyContinuous, stated with explicit and
as in Definition 4.18, rather than through the uniformity filter.Rudin.IsLimitPoint from the Chapter 2 mission, so the two missions share
one notion.[CompactSpace X], matching
Rudin's phrase "compact metric space"; 4.14 is stated for a compact subset instead, which is
the form later missions use.MonotoneOn f (Set.Ioo a b); one-sided limits are 𝓝[<] x and
𝓝[>] x filters, and 4.29 also identifies them with the supremum and infimum of the
corresponding one-sided images, as Rudin does.The goal is not vacuous and does not follow by unfolding: uniform continuity fails for continuous functions on non-compact domains (e.g. on , or on ), so compactness is doing the work.
Von Neumann introduced amenability in 1929 in response to the Banach–Tarski paradox: a group is amenable when it carries a finitely additive, translation-invariant probability measure on its subsets, and no amenable group contains a free subgroup of rank — which is exactly what the paradox needs. The converse is the von Neumann conjecture, and it is false: Ol'shanskii in 1980 and Adyan in 1982 produced finitely generated counterexamples. A finitely presented counterexample was harder, and one candidate stood out — Richard Thompson's group , finitely presented, with nobody able to decide whether it was amenable.
Brin and Squier attacked it and in 1985 got what they called "half a success": they proved that , and more generally the group of piecewise-linear homeomorphisms of the line with finitely many breakpoints, contains no free subgroup of rank greater than . Whether is amenable they could not determine, and it is still open today; claimed proofs have appeared in both directions and none has been accepted. Finitely presented counterexamples were eventually found by other routes (Ol'shanskii–Sapir 2002; Lodha–Moore 2016), so is no longer needed as a candidate. This mission formalizes the half that was settled.
Let be the group of orientation-preserving homeomorphisms of the line: the strictly increasing bijections under composition. The support of is the set of points it moves, , an open subset of .
A continuous is piecewise linear when there is a discrete set of breakpoints with differentiable off and constant on each component of ; for finite this is the same as being affine on a neighbourhood of every point outside . Nothing is required at the points of , so the two affine pieces meeting at a breakpoint may disagree — that is what makes such an more than an affine map. Write for the piecewise-linear elements of and
for the subgroup this mission is about. The distinction matters: the goal below holds in and fails in , where Brin and Squier build free subgroups of rank by lifting them from the circle. Write for the commutator subgroup, which Brin and Squier identify as the elements whose slope at each end is — an element has slope at an end when it agrees with a single affine map of slope on a ray out to that end. Thompson's group — the piecewise-linear homeomorphisms of with dyadic breakpoints and power-of-two slopes — is realized inside .
Since a free group of rank greater than contains one of rank , this is Brin and Squier's Theorem (3.1).
Their Theorem (3.2), with the conclusion weakened to what the goal consumes. What they prove is infinite rank, which needs the general form of their Lemma (1.2); that general Lemma and the full-strength (3.2) are milestones of their own here. The goal itself only ever uses the rank-two form.
Thirteen are numbered results of theirs: the support observations (1.1a), (1.1b); Lemma (1.2) in its rank-two case and in its general form; Lemmas (3.4) and (3.5), already formalized and published, entering as references; the commutator facts (2.14a), (2.14b), (2.14c); Theorem (3.2) both as the rank-two dichotomy the goal consumes and at full strength; and Corollary (3.3), likewise in both strengths. Five are piecewise-linear infrastructure the source treats as routine: closure of under composition and under inverse, the same two for slope at each end, and finiteness of the number of components of a support. Five more are steps the source asserts without proof — that the line carries no non-fixed periodic points, that a map fixing a set's complement preserves its components, that the iterated images of a pushed-forward interval are pairwise disjoint, that the closure of a commutator's moved set stays inside the union of the two supports (p. 495), and that the derived subgroup of a free group of rank two is non-abelian (p. 494). The last is not from the source at all — that an abelian subgroup of a free group is cyclic, which is what lets the goal finish through Nielsen–Schreier.
The theorem closes the standard route to proving a group non-amenable. To show a group amenable the classical routes are elementary amenability and subexponential growth, and is neither elementary amenable (Cannon–Floyd–Parry, Theorem 4.10) nor of subexponential growth, having exponential growth (their Corollary 4.7). To show a group non-amenable the standard route is to exhibit a free subgroup of rank — the route this theorem closes. sits in the gap, which is why its status has survived sustained attention.
The result reaches past . Monod's groups of piecewise projective homeomorphisms are counterexamples to von Neumann's conjecture, and Monod's theorem that they contain no non-abelian free subgroup is, in Monod's words, "a sequacious generalization of the corresponding theorem of Brin–Squier about piecewise affine transformations"; of its own proof that paper says it will "largely follow [Brin–Squier, § 3]".
What formalizing it adds. Mathlib has no piecewise-linear maps and no amenability predicate for groups. This mission builds the piecewise-linear layer: a workable , its closure properties, and the structure of supports.
The obstruction is bookkeeping across two finiteness facts of different kinds. Finiteness of the breakpoint set is what gives an element slopes at at all, and what makes two elements affine on each side of a common fixed point. Compactness is the other — throughout, — and it splits: that the closure of is compact needs only slope at each end, with no piecewise linearity at all, which is why (2.14b) is formalized under a weaker hypothesis than the source's; that the closure stays inside is what reaches back to finiteness. Keeping straight which fact does which job is most of the work.
The first idea a newcomer has about (3.2) is the wrong one. Its proof produces a family of commuting elements, and it is not disjointness of supports that makes them commute: only their intersections with one chosen component are disjoint, and commutation is deduced instead from a minimality argument. A proof routed through disjoint supports will not close.
What the Lean fixes. Elements are order isomorphisms of — strictly increasing
bijections, automatically homeomorphisms — rather than a homeomorphism type. Composition follows
Mathlib's convention , the opposite of the source's right action, so the
conjugation identity reads here;
getting this backwards states a different theorem that still compiles. A support is the bare
moved set, with no closure taken. Piecewise linearity is a finite breakpoint set together with
local affineness off it — the set need not be minimal and may be empty.
A copy of is an injectivity statement about , not a subgroup
isomorphism, and the goal is about a single pair rather than a subgroup. The dichotomy
hypothesises slope at both ends directly, not membership in a derived subgroup — that these
coincide is the source's result, and both inclusions are formalized here: (2.14a) gives one, and
the identification asserted on p. 493 gives the other.
Beyond a workable , the development needs Nielsen–Schreier, already
in Mathlib as subgroupIsFreeOfIsFree: it is what lets an abelian subgroup of a free group be
cyclic, and so lets the goal finish without the source's metabelian ending. That ending is
formalized too, as Corollary (3.3) together with the p. 494 remark that the derived subgroup of a
free group of rank two is non-abelian; the goal simply does not route through it.
One trivializing reading is ruled out. Slope at both ends is not a compact-support condition — every translation satisfies it — so (3.2) is not secretly a statement about compactly supported maps.
Nothing is built for specifically, and amenability is not touched. That is the one piece deliberately omitted, and contributions are welcome on it: modelling and embedding it in . The piecewise-linear layer is reusable beyond this theorem — Thompson's groups and , and piecewise-linear topology generally, need exactly it.
Several equations of mathematical physics are written down formally but have no classical meaning as stated. The dynamical model on the three-dimensional torus, the KPZ equation , and the parabolic Anderson model all require multiplying a distribution of negative regularity by itself, an operation that Schwartz distribution theory does not provide. Martin Hairer's A theory of regularity structures (Invent. Math. 198 (2014) 269–504, arXiv:1303.5113) develops a calculus in which such products, and the resulting fixed-point problems, become well posed.
The line of work leading to it is short and well documented: rough path theory (Lyons, 1998) solved the analogous problem for controlled ordinary differential equations driven by irregular signals; Gubinelli's controlled paths (2004) and branched rough paths (2010) reorganised it around local expansions; Hairer's theory extends that idea from paths to fields on with anisotropic (e.g. parabolic) scaling. Paracontrolled distributions (Gubinelli–Imkeller–Perkowski, 2015) give an alternative route to some of the same equations. The algebraic and probabilistic infrastructure around regularity structures has since been systematised (Bruned–Hairer–Zambotti, 2019; Chandra–Hairer, 2016), but the analytic core is still the 2014 paper.
Fix a dimension and a scaling of positive integers, with , and put . For , a point and a test function , the rescaled test function is
Write for the set of test functions supported in whose derivatives up to order are bounded by . For , a distribution belongs to the Hölder–Besov space if, on every compact set , uniformly over , and with .
A regularity structure consists of an index set containing , bounded below and locally finite; a graded vector space with spanned by a unit ; and a group of linear operators on with for , and . Elements of are "homogeneous of order ": they are placeholders for objects whose size at scale is .
A model assigns to each point a linear map and to each pair an element , subject to , , and, locally uniformly, the analytic bounds
A modelled distribution of order is a function such that on every compact
the space of these is , and if takes values in a sector , that is, a graded -invariant subspace vanishing in degrees below its regularity.
With and the order attached to , for every with there is a unique distribution with
The statement asserts only the shape of the estimate — a constant per compact set — and so is insensitive to any later sharpening of constants.
The uniqueness clause of Theorem 3.10 in isolation; the existence of a linear reconstruction operator for arbitrary (for the bound no longer pins it down); Corollary 3.16, improving the regularity of to when takes values in a sector of regularity ; Proposition 3.31, that for the action of on is determined by and by in lower homogeneities; and Theorem 4.7, that the truncated pointwise product of and lies in with .
The reconstruction theorem is what turns a book-keeping device into analysis: it says that a coherent family of local expansions, indexed by base point, glues to a single genuine distribution, with an error controlled by the order of the expansion. Every subsequent operation in the theory — multiplication (Theorem 4.7), composition with smooth functions (Theorem 4.16), the multi-level Schauder estimate (Theorem 5.12), and the fixed-point theorem for singular SPDEs (Theorem 7.8) — is stated and used through it. Without it, the abstract spaces carry no information about actual distributions.
Regularity structures are not currently available in Mathlib, and neither are the anisotropic Hölder–Besov spaces that the theory is phrased in. The result itself is proved in the literature; the work this mission asks for is a machine-checked proof of the known argument, together with the reusable definitions it needs. The formal development is a prerequisite for anything downstream — Schauder estimates, the fixed-point theory, or the and PAM convergence results of §10 — which are natural follow-on missions rather than part of this one.
The naive construction fails: setting for a fixed is wrong away from , and the pointwise limit of localisations of around each does not obviously exist, because the objects being glued are distributions of negative order, not functions, so there is no value to take and no partition-of-unity argument that respects the scaling. Hairer's proof goes through a wavelet multiresolution analysis adapted to the scaling : one defines the candidate on each dyadic level by pairing with wavelets centred at grid points, and shows the resulting sequence is Cauchy using the bound level by level. A formalization therefore needs either a scaled wavelet basis with Daubechies-type regularity (Theorem 3.17 in the paper) or a substitute for it; this, and the uniform-in-scale bookkeeping, is where the effort lies. Uniqueness for is by contrast short, and is listed as a separate milestone.
The development commits to the following conventions, fixed in the mission's definition files. Points of are Fin d → ℝ. Test functions are smooth and compactly supported, forming a submodule of all real-valued functions, and a distribution is a linear functional on that submodule; the pairing is extended by to non-test functions, and a lemma in the definition file certifies that rescaling maps test functions to test functions, so no statement is vacuous for that reason. Hairer's consists of functions; here it consists of smooth ones, which defines the same spaces . The model space is the algebraic direct sum over the index set, each a real normed space, with the corresponding projection; the structure group is a subgroup of the linear automorphisms of that direct sum. Sectors are families of subspaces ; Hairer's requirement that each admit a complement is automatic in this algebraic setting. The integer appearing in the model bounds is the smallest one with for all , which is part of the definition of a model rather than a free parameter. All statements quantify over an arbitrary regularity structure, an arbitrary model, and an arbitrary compact set, so they are not satisfiable by a degenerate choice; the goal in particular claims existence, membership in , and uniqueness simultaneously.
Infrastructure that a complete proof will need, and which is reusable beyond this mission: scaled wavelet bases on , the elementary theory of (including the positive-regularity case), and basic operations on compactly supported test functions under anisotropic rescaling. Contributions of any of these as separate lemmas are welcome, as are reductions that decompose the goal into wavelet-level estimates.