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.
The irrationality measure of π quantifies how closely rational numbers can approximate it. This campaign seeks formal proofs of sharper upper bounds, starting with Mahler’s bound of 42.
The sharp Hlawka inequality for Schatten -norms is a cousin of the triangle inequality: it relates the norms of three matrices to the norms of their pairwise sums and their total sum. For complex diagonal matrices, an exact formula for the best possible comparison constant has been proved in Lean for every real . We conjecture that the same formula holds for all .
What is the smallest cutoff for which this formula holds for every real ?
References:
Is every odd number a sum of primes? This campaign tracks formalized proofs of the smallest that suffices.
Schnirelmann (1930) showed some finite works. Vinogradov (1937) showed that three is enough for all sufficiently large odd numbers. Tao (2012) proved unconditionally. Helfgott (2013) proved that every odd number greater than is a sum of three primes, though the proof is still unrefereed. Ideally, we can formalize this statement here. Note that three is optimal: is neither prime nor + prime.
Schoolbook matrix multiplication takes operations. The exponent is the infimum of all such that two matrices can be multiplied in arithmetic operations; trivially , and is conjectured but open.
Strassen gave the first nontrivial bound, , in 1969, and introduced the laser method in 1986 to reach . Coppersmith and Winograd's 1990 bound of stood for two decades. Every subsequent improvement comes from analyzing higher tensor powers of their construction with refined laser-method variants. That line reached in 2025, and the current record is , from August 2026. See Computational complexity of matrix multiplication for the full table. Can we formalize these results and even improve on them?
The incompressible Navier–Stokes equations are the standard model for the motion of a viscous fluid such as water or air, used daily in engineering, meteorology and oceanography. Yet the most basic mathematical question about them is open: starting from smooth initial data in three dimensions, does a smooth solution exist for all time? This is one of the seven Millennium Prize Problems of the Clay Mathematics Institute. Its official formulation is Charles Fefferman's problem description, Existence and smoothness of the Navier–Stokes equation (2000), which offers a prize for a proof of any one of four statements: global existence and smoothness on (statement (A)) or on the torus (statement (B)), or a counterexample to either (statements (C) and (D)). This mission formalizes statement (A), together with the classical partial results that Fefferman lists as known.
Timeline.
Fix a dimension and write for Euclidean -space with its Euclidean norm ; in Lean this is NavierStokes.Vec n. A velocity field assigns to each time and point a vector ; in Lean is the field at time and is Fefferman's . A pressure is a real function . The viscosity is a positive constant. The external force of Fefferman's equation (1) is identically zero throughout, as in statement (A).
For a vector field the divergence is
in Lean NavierStokes.div, computed from the Fréchet derivative as . The Laplacian acts componentwise (Mathlib's Laplacian on inner product spaces). The gradient is Mathlib's gradient. The convective term is the derivative of at in the direction . Finally is NavierStokes.gradNormSq.
Admissible initial data (Fefferman's condition (4), NavierStokes.IsInitialData): a , divergence-free vector field that decays together with all its derivatives faster than any power,
In Lean the bound is on the -th Fréchet derivative, an equivalent family of conditions. These are exactly the divergence-free Schwartz functions.
A physically reasonable solution on a set of times (NavierStokes.IsSolutionOn; for NavierStokes.IsSolution) is a pair such that
Take and . For every admissible initial datum there exist a velocity field and a pressure forming a physically reasonable solution on :
This is NavierStokes.existence_and_smoothness_R3. It is open; a proof would settle the Millennium Prize Problem in the affirmative.
NavierStokes.local_existence_R3): for and every admissible there are and a physically reasonable solution on . Fefferman: "(A) and (B) hold ... if the time interval is replaced by a small time interval , with depending on the initial data."NavierStokes.small_data_global_existence_R3): there is an absolute constant such that, for , (A) holds for every admissible withFefferman: "(A) and (B) hold provided the initial velocity satisfies a smallness condition." The scale-invariant product is Leray's form of the condition; it implies smallness of , so Kato's theorem also applies.
3. The two-dimensional case (NavierStokes.existence_and_smoothness_R2): statement (A) with . Fefferman: "In two dimensions, the analogues of assertions (A) and (B) have been known for a long time (Ladyzhenskaya)."
A bridging lemma, NavierStokes.isInitialData_iff_schwartz, identifies the admissible data with the divergence-free elements of Mathlib's Schwartz space.
The result itself. Statement (A) asks whether the basic model of viscous flow is well posed in the classical sense, i.e. whether smooth finite-energy flows can develop singularities in finite time. A positive answer shows the equations never leave the classical regime; a negative one shows the model predicts its own breakdown. Fefferman: "since we don't even know whether these solutions exist, our understanding is at a very primitive level."
Formalizing it. None of the results in this mission has a machine-checked proof, and Mathlib contains no theory of the Navier–Stokes or Euler equations. The milestones are all proved in the literature; formalizing them requires building, on Mathlib's calculus, measure theory and Schwartz space, the heat semigroup on , the pressure equation or the Leray projection, energy estimates, and a fixed-point construction of solutions, most of which is reusable for other evolution equations. The goal is open and expected to remain so; its role is to fix in Lean the exact statement the prize asks for, so partial results are formalized against it.
The energy identity controls in and in , but in three dimensions this control is supercritical: under the scaling that preserves the equations, the energy of shrinks as , so bounded energy does not prevent concentration at small scales. Every known continuation criterion (Leray, Prodi–Serrin, Beale–Kato–Majda, Escauriaza–Seregin–Šverák) needs a quantity at or above critical scaling, none of which the energy controls. The obvious first idea, an ordinary differential inequality for , gives , which closes only for small data or short time. That is exactly why milestones 1 and 2 are theorems and the goal is not.
The formalization adds a second difficulty: the solutions of the literature live in Sobolev or Besov spaces, with pointwise smoothness of and recovered afterwards by regularity theory, and Mathlib has neither Sobolev spaces on nor the heat semigroup in usable form.
EuclideanSpace ℝ (Fin n) with Lebesgue measure; the dimension is a parameter, the goal fixes and the 2D milestone .ContDiffOn of the uncurried map on the closed half-space, i.e. all derivatives extend continuously to . The momentum equation is imposed at interior times with two-sided derivatives; by continuity of the derivatives this is equivalent to Fefferman's "".fderiv, deriv, iteratedFDeriv, gradient, Laplacian) with junk value at non-differentiable points; the smoothness hypotheses make every derivative in the statements honest.No trivializing formalization. The zero field solves the equations only for ; for any other admissible the initial condition, smoothness, the equation on and bounded energy must all hold.
Infrastructure needed and welcome contributions. The heat kernel on with Schwartz bounds; the Riesz-transform representation of the pressure or the Leray projection; energy identities for smooth decaying solutions; local existence by Picard iteration; the two-dimensional vorticity equation and its maximum principle. Theorems in the NavierStokes namespace, decompositions of the milestones, and Mathlib lemmas about ContDiffOn on half-spaces are all welcome. Statements (B), (C), (D) and the Euler equations () are out of scope.
How short can a code for a data source be, if the code must still be uniquely decodable — if every string of concatenated codewords can be unambiguously split back into the original symbols? Shannon's 1948 source coding theorem answers this exactly: the entropy of the source is a hard lower bound on the average codeword length of any uniquely decodable code, and it is also achievable up to a one-symbol slack. Entropy is not just a measure of "average surprise" — it is the literal, tight answer to a combinatorial question about how densely symbols can be packed into strings without losing decodability. This is the theorem that gives Shannon's entropy its operational meaning, and it underlies every practical lossless compression scheme (Huffman coding, arithmetic coding, Lempel–Ziv) as the benchmark they approach.
Timeline.
A source has a finite alphabet of symbols , with at least two symbols, and probability distribution (, ). A code assigns to each symbol a codeword , a finite string over a -ary code alphabet (); the code is uniquely decodable if every finite sequence of codewords is determined by its concatenation. The entropy of in base is
The expected codeword length of under is .
(For a source with symbols — see Formalization scope for why the single-symbol case must be excluded.)
The result itself. This theorem is the reason entropy is called entropy in an information-theoretic sense at all: it converts a quantity defined by an abstract formula () into the exact answer to an operational question (minimum achievable expected code length), with a slack no worse than one symbol. It is the founding theorem of lossless source coding and the benchmark every practical compressor is measured against.
Formalizing it. Mathlib recently gained genuine information-theoretic coding content: InformationTheory.UniquelyDecodable and the necessity direction of the Kraft–McMillan inequality (McMillan's 1956 result: a uniquely decodable code's lengths satisfy ) are already proved, via a counting argument on concatenations of codewords. This mission builds directly on that foundation rather than duplicating it. What Mathlib does not have — and what this mission's milestones supply — is Kraft's original 1949 sufficiency direction (existence of a uniquely decodable code realizing any length assignment satisfying the Kraft sum bound), any notion of Shannon entropy for a general finite distribution, and the source coding theorem itself.
The lower bound () is the easier half: it follows from the Kraft–McMillan inequality (already in Mathlib) via Gibbs'/Jensen's inequality applied to the two probability-like sequences and (where is the Kraft sum) — a short, self-contained convexity argument.
The achievability half is the genuine construction. Given the ideal (generally non-integer) lengths , one rounds up to (Shannon–Fano–Elias lengths); a one-line estimate shows , so the Kraft sum of the rounded lengths is still , and the bound gives immediately once a code with exactly these lengths is shown to exist. Producing that code is Kraft's sufficiency direction, and it needs an explicit construction: order the lengths, and assign to symbol the first digits of the -ary expansion of the cumulative sum . Verifying this assignment is injective, has the prescribed lengths, and is uniquely decodable (indeed prefix-free) is a careful but standard combinatorial argument — the main open piece of this mission.
The source alphabet must have at least two symbols (), not merely be nonempty. A single-symbol source forces and entropy , so the achievability conjunct would demand a codeword of length — but a uniquely decodable code can never contain the empty codeword (InformationTheory.UniquelyDecodable.epsilon_not_mem, provable from the definition: the empty string decodes ambiguously as zero or two copies of itself), so no admissible code exists and the theorem would be false, not merely hard, at . The same defect breaks Kraft's sufficiency direction (Milestone 2) whenever any prescribed length is , independent of ; that milestone accordingly requires every length strictly positive. With and full support, every strictly, so the Shannon–Fano lengths are automatically all , and the achievability construction only ever needs Milestone 2 at positive lengths. The code alphabet is likewise an arbitrary finite type (matching Mathlib's own Fintype/Nonempty conventions for the Kraft–McMillan file), with required to keep Real.logb non-degenerate. The source distribution is required strictly positive () — the standard simplifying assumption (zero-probability symbols can always be dropped without loss). Unique decodability is stated exactly as Mathlib's InformationTheory.UniquelyDecodable, not re-derived from a "prefix code" definition, so the mission's results transport directly onto Mathlib's existing Kraft–McMillan file. A trivializing route to rule out: proving only the lower bound (citing Mathlib's inequality) while leaving the existential achievability half unaddressed would not be Shannon's theorem — the sandwich is the theorem's actual content, and the lower bound alone (already essentially free from Mathlib) is not a novel contribution on its own.
Reusable output: the Kraft sufficiency construction (Milestone 2) is directly reusable for any future formalization of Huffman coding optimality, arithmetic coding, or the general "Kraft-inequality-achieving code exists" fact used throughout coding theory. Contributions are welcome starting from Milestone 2 (the open construction) or Milestone 3 (the Gibbs'-inequality lower bound, which only needs Milestone 1, already available via Mathlib).
Mathlib.InformationTheory.Coding.UniquelyDecodable and Mathlib.InformationTheory.Coding.KraftMcMillan (2026).Quantum circuits built from Clifford gates alone are classically simulable in polynomial time. Universality is recovered by adding copies of a magic state, and the fastest known classical simulators of such circuits work by writing the magic-state input as a short linear combination of stabilizer states. The length of the shortest such combination -- the stabilizer rank -- is therefore the exponent governing classical simulation of quantum computation in this model, and lower bounds on it are among the very few unconditional obstructions to classical simulation available at all.
A timeline of what is established for the standard magic state :
Between the linear unconditional lower bound and the upper bound lies the open problem this mission targets.
Index the computational basis of an -qubit system by bit strings , so a state is a vector with coordinates .
The Pauli operators are for , acting by , where counts the coordinates on which both are and is bitwise addition; the Pauli group is the set of operators . A unitary is a Clifford unitary when lies in the Pauli group for every Pauli group element , and a stabilizer state is a vector for some Clifford . There are of them up to phase -- six for a single qubit.
The stabilizer rank is the least admitting coefficients and stabilizer states with .
The magic state is , and its -fold tensor power, with coordinates where is the Hamming weight of .
The goal is a super-polynomial lower bound: for every exponent and constant there exists with
equivalently, is not for any fixed .
Stronger statements are expected but are deliberately not the goal. An exponential bound is believed and follows from hardness assumptions, but a goal naming a specific growth rate would be superseded by the next improvement; super-polynomiality is the weakest statement that settles the question of principle.
The result itself. A super-polynomial lower bound would unconditionally rule out efficient classical simulation of Clifford-plus-magic-state circuits by stabilizer decomposition, currently the leading such technique. The converse direction shows how much is at stake: a polynomial upper bound on would imply , and via postselection . There is also a purely classical payoff -- improving the known bound even to super-linear would produce a Boolean function computable in polynomial time requiring a super-linear number of summands in any decomposition into exponentials of quadratic forms over , resolving a separate open question.
Formalizing it. The goal is open, so no known proof is being transcribed. What the mission produces is a machine-checked statement of the problem together with formalizations of the established bounds, none of which has a machine-checked proof anywhere. It also produces the first Pauli/Clifford/stabilizer layer in Lean: no existing Lean library contains the -qubit Pauli group, the Clifford group, or stabilizer states, and that layer is reusable for stabilizer error correction, magic monotones, and Clifford simulation generally.
Counting settles the problem for random states: the stabilizer states are too few for short combinations to cover a generic state, so almost every state has exponential stabilizer rank. This says nothing about , which is a single explicit, highly structured vector, and the entire difficulty is that lower bounds must be proved for that specific state rather than for a typical one. Every newcomer proposes the counting argument; it does not apply.
The known techniques reduce the question to statements about decompositions of explicit Boolean functions into quadratic-form exponentials, and the barrier is quantitative: the available arguments lose a factor that caps them at linear bounds. The source of the current record documents explicitly why its method cannot pass super-linear, and the fact that going beyond linear would resolve an independent open problem in Boolean function complexity indicates the obstruction is not merely technical.
State vectors are functions and are not required to be normalised; normalisation does not affect the rank, and stabilizer states are unit vectors automatically as Clifford images of . The Pauli group is given by the explicit parametrisation rather than an abstract presentation, and the Clifford group is characterised as its unitary normaliser, equivalent to the usual generated-by- description. Because normalises the Pauli group whenever does, the stabilizer states are closed under global phase; this is harmless, as the coefficients are arbitrary complex numbers.
One trivialising reading must be excluded. The rank is defined as an infimum over a set of natural numbers, and Lean gives the empty infimum the value ; if no decomposition existed the rank would be for every state and the goal would be false rather than merely unproved. The milestone is what certifies the set is nonempty, making the rank a genuine minimum, and it should be proved first. Separately, the goal quantifies over all reals including negative values, for which the inequality is trivially satisfiable; the content lies in large positive .
A complete development needs, beyond the published definitions, the correspondence between stabilizer states and affine subspaces carrying quadratic phase functions, on which all known lower-bound arguments rest. Contributions of any milestone are welcome, as are function-level reformulations of the rank and the equivalent characterisation of stabilizer states via maximal abelian Pauli subgroups.
The separation theorem — certainty equivalence for linear-quadratic control with imperfect state information — is one of the celebrated structural results of stochastic control: the optimal controller splits into a least-squares estimator and the deterministic LQR actuator, designed independently. It underlies every LQG autopilot and Kalman-filter-based regulator. Section 5.2 of Bertsekas, Dynamic Programming and Optimal Control, Vol. I (3rd ed., 2005) proves it from the DP algorithm over information vectors, with Lemma 5.2.1 supplying the key fact that the estimation error is beyond the controller's influence. No formal analogue exists in Mathlib.
Linear dynamics and measurements
with quadratic cost , , . The initial state and the zero-mean disturbances/noises are independent with finite ranges; independence is structural — the sample space is the product of an initial-state coordinate and per-stage noise coordinates (BertsekasLQGModel, BertsekasLQGSample, BertsekasLQGProb). A policy maps the realized measurement history to ; the closed-loop process is BertsekasLQGTraj, the expected cost BertsekasLQGCost. The estimator is an explicit conditional average (BertsekasCondExpVec, BertsekasLQGEstimate); the gains come from the time-varying Riccati recursion (BertsekasLQGRiccati, BertsekasLQGGain).
— BertsekasDP.lqg_certainty_equivalence (goal). Milestone: Lemma 5.2.1 in pointwise form — the error is the same under any two policies, outcome by outcome (lqg_estimation_error_policy_independent).
This is the theorem that justifies designing estimator and controller separately — remove it and the entire LQG methodology loses its warrant. The formalization also yields the first machine-checked instance of the informational decomposition (control-dependent part + policy-independent error) that recurs throughout imperfect-information control. Notably the result needs no Gaussian assumption — only zero mean and independence — and the finite-support model makes that generality exact. The result is classical (Joseph–Tou 1961, Gunckel–Franklin 1963; the book's §5.2); the formal proof is new.
The heart is Lemma 5.2.1: showing the estimation error coincides, sample by sample, with the error of the control-free system — which requires proving that the observation-history σ-events under any policy coincide with those of the control-free system (controls are determined by the history, so they shift observations by a known amount). Then the DP argument over information histories must carry the quadratic decomposition through the backward recursion. Bookkeeping over histories-as-lists is the main formal burden; probability theory stays finite.
Finite-support randomness (all expectations are finite sums); conditional expectation with the explicit junk value 0 on zero-probability events — the goal's hypothesis is accordingly restricted to outcomes of positive probability. Policies are functions of the measurement list only (equivalent to the book's information vector for deterministic policies, since past controls are recoverable from past measurements). Matrices are time-varying; positive definiteness of makes every matrix inverse in the gains genuine. Measurement noise covariance is not assumed positive definite — the estimator is the abstract conditional expectation, not the Kalman filter (whose recursive form, §5.2.1, would be a natural follow-up mission).
Label correcting methods are the workhorse family of shortest-path algorithms — Dijkstra's method, Bellman–Ford, SLF/LLL variants and A* all fit the template analyzed in §2.3.1 of Bertsekas, Dynamic Programming and Optimal Control, Vol. I (3rd ed., 2005), where shortest paths appear as the purely deterministic face of dynamic programming. The correctness proof (Prop. 2.3.1) is short on paper but genuinely nondeterministic — any node may be removed from the candidate list, children processed in any order — so a formal proof certifies a whole family of concrete algorithms at once.
A finite directed graph with arc set , real arc lengths , origin and destination (BertsekasSPGraph). Walks are nonempty node lists whose consecutive pairs are arcs (BertsekasIsWalkFrom), with length the sum of arc lengths (BertsekasWalkLength); the shortest distance is the infimum of walk lengths in the extended reals, if no walk exists (BertsekasShortestDistance). The standing assumption of §2.3: every cycle has nonnegative length (negative arcs allowed).
The algorithm state (BertsekasLCState) carries labels , the scalar UPPER, and the candidate list OPEN. Initially , all other labels , UPPER , OPEN . One iteration (BertsekasLCStep, nondeterministic): remove any from OPEN; for each child of in any order, if set , and put in OPEN if , or update UPPER if . The algorithm terminates when OPEN is empty.
for every execution, under the nonnegative arc length assumption of §2.3 ( for every arc) — BertsekasDP.label_correcting_correctness_of_nonneg_arcs (goal). Milestones: termination — no infinite execution exists, which needs only the weaker nonnegative-cycle assumption (label_correcting_terminates) — and the workhorse invariant that every finite label is the length of an actual walk from , which needs neither (label_correcting_invariant).
The nonnegative-arc hypothesis is essential and not a formalization artifact: the algorithm prunes with the test , and with a negative arc a longer prefix can still reach more cheaply, so the pruned node is never entered into OPEN. An earlier version of this mission's goal carried only the nonnegative-cycle assumption of §2.1 and was disproved by the counterexample , , , , (a graph with no cycles at all), where the algorithm terminates with while the shortest distance is . Exercise 2.7 of the source treats the nonnegative-cycle case, which requires a modified algorithm.
Prop. 2.3.1 certifies simultaneously breadth-first search, Dijkstra (best-first), depth-first and small-label-first variants — every removal discipline is one refinement of the nondeterministic relation. Formally, the development contributes a reusable small-step framework for label-setting/correcting algorithms on which sharper results (Dijkstra's single-pass property, A* admissibility, §2.3.3) can later be built. The result is classical; the formal content is the induction along the nondeterministic step relation.
Termination is the subtle half: labels do not decrease monotonically along the run in an obvious well-founded way; the book's argument counts the finitely many distinct walk lengths below a bound — this needs the nonnegative-cycle assumption and a careful bound relating labels to simple-path lengths. The invariant proof must thread through the fold over children within a single step.
Finite node type with decidable equality; arcs as a Finset of ordered pairs; lengths total on (only arc values matter). The step relation is fully nondeterministic in pivot choice and child order (a permutation quantifier); correctness quantifies over all reachable terminal states — there is no fixed schedule to exploit. Distances live in EReal, so the no-path case is the honest empty infimum, not a sentinel. The trivializing risk of restricting to nonnegative arcs is avoided: only cycles are constrained.
The fundamental group is the first algebraic invariant a student of topology meets, and is the first computation of it that carries real content. Allen Hatcher's Algebraic Topology (Cambridge University Press, 2002; freely available at pi.math.cornell.edu/~hatcher/AT/AT.pdf) is the standard text on the subject. Its Chapter 1 opens with exactly this computation (Theorem 1.7, p. 29) and immediately draws three classical consequences from it: the Fundamental Theorem of Algebra (Theorem 1.8), the Brouwer fixed point theorem for the disk (Theorem 1.9), and the Borsuk–Ulam theorem for the sphere (Theorem 1.10).
This mission is the opening entry in a series that formalizes Hatcher's book capstone by capstone. It covers the subsection "The Fundamental Group of the Circle" of Section 1.1 (pp. 29–33): the covering-space lifting properties that drive the proof, the theorem itself, and its three applications. Later entries in the series (van Kampen's theorem, the classification of covering spaces, simplicial and singular homology) will build on the declarations introduced here, which all live in the shared Lean namespace Hatcher.
A path in a topological space is a continuous map , where . A homotopy of paths is a family , , such that the endpoints and are independent of and the associated map , , is continuous. A loop at a basepoint is a path with . The set of homotopy classes of loops at is the fundamental group ; its product is , where traverses and then , each at double speed (Hatcher, Proposition 1.3).
The circle is realised as the unit circle of , so the point is and the basepoint is . Hatcher's map
is Hatcher.circleCover. The loops
based at are Hatcher.omegaLoopN n, and is Hatcher.omegaLoop; its class is Hatcher.omegaClass.
A covering space of is a space together with a map such that every has an open neighbourhood for which is a disjoint union of open sets each mapped homeomorphically onto by (Hatcher's condition , p. 29; such a is evenly covered). A lift of a map is a map with .
is an infinite cyclic group generated by . In the form stated in Lean:
Surjectivity of says generates; uniqueness of says the group is infinite cyclic rather than finite.
The result itself. The computation assigns to every loop in the circle an integer, its winding number, and shows that this integer is the only homotopy invariant of the loop. It is the seed of degree theory, and in Hatcher's text it is the starting point for every later computation of fundamental groups (products, van Kampen, covering spaces). The three applications are the standard demonstration that a single algebraic invariant can settle purely geometric or algebraic existence questions.
Formalizing it. Mathlib (revision 0df444a) already contains the covering-space infrastructure: IsCoveringMap, path lifting (IsCoveringMap.liftPath, eq_liftPath_iff'), homotopy lifting (IsCoveringMap.liftHomotopy, eq_liftHomotopy_iff'), monodromy, and the fact that Circle.exp is a covering map (Circle.isCoveringMap_exp). It also has FundamentalGroup X x as the endomorphism group of the fundamental groupoid. It does not contain the computation , nor the two-dimensional Brouwer and Borsuk–Ulam theorems. The Fundamental Theorem of Algebra is in Mathlib as Complex.exists_root (proved by Liouville's theorem rather than by Hatcher's argument); it is kept as a milestone because it is one of the section's stated theorems, and a solver may close it directly from Mathlib. Milestones 2–4 are also within reach of the existing lifting API, but they are the lemmas Hatcher states and uses, and a faithful record of them in the mission's own namespace is what later entries in the series will import.
The obvious first idea for the goal is to define the winding number of a loop through the complex argument. That fails because is discontinuous on ; the integer has to be produced by lifting the loop through and reading off the endpoint of the lift, which is only well defined because of the uniqueness in the path lifting property. The second difficulty is uniqueness of : this needs lifting of homotopies (milestone 4), not just of paths, together with the observation that a lifted homotopy of paths has constant endpoints.
Connecting the concrete loops to Mathlib's abstract is its own obstacle. FundamentalGroup Circle 1 multiplies by composing morphisms of the fundamental groupoid, so identifying with the class of the explicit loop (milestone 6) requires reparametrization arguments for concatenated paths, for negative as well as positive.
For Theorem 1.9 the difficulty is the construction and continuity of the retraction from a fixed-point-free map, and then the non-existence of a retraction, which uses that . For Theorem 1.10 Hatcher's proof lifts a loop through and shows the lift changes by an odd integer over half a turn; making that parity argument rigorous in Lean is the substance of the milestone.
Circle (the unit circle in ) with basepoint 1; is Metric.closedBall (0 : EuclideanSpace ℝ (Fin 2)) 1; is Metric.sphere (0 : EuclideanSpace ℝ (Fin 3)) 1, with the antipodal point.IsCoveringMap p. This agrees with Hatcher's condition ; neither requires to be surjective.C(I, X) or Mathlib Paths; for homotopies of paths, the square is written I × I with Hatcher's coordinate order : the first coordinate is the path parameter, the second the homotopy parameter. In the general homotopy lifting property the domain is Y × I with an arbitrary topological space, as in Hatcher.FundamentalGroup Circle 1, and is FundamentalGroup.fromPath ⟦omegaLoop⟧. Because the goal quantifies over integer powers of a single element, the order of multiplication in FundamentalGroup is immaterial to its truth.FundamentalGroup Circle 1 ≃* Multiplicative ℤ sending to is an immediate corollary and a welcome contribution.0 < f.degree, which excludes both the zero polynomial and nonzero constants.Contributions welcome: proofs of the milestones from Mathlib's lifting API, a degree homomorphism packaged for reuse, and any lemma about concatenation and reparametrization of loops in Circle that later chapters of the series can import.
Mathlib/Topology/Homotopy/Lifting.lean (path and homotopy lifting for covering maps). https://github.com/leanprover-community/mathlib4/blob/0df444a360eaa60ab8c11dca51a86af692955474/Mathlib/Topology/Homotopy/Lifting.leanMathlib/AlgebraicTopology/FundamentalGroupoid/FundamentalGroup.lean (the fundamental group). https://github.com/leanprover-community/mathlib4/blob/0df444a360eaa60ab8c11dca51a86af692955474/Mathlib/AlgebraicTopology/FundamentalGroupoid/FundamentalGroup.leanThe strategic-form game is the basic object of noncooperative game theory, and the Nash equilibrium — a profile of randomized strategies from which no player benefits by deviating unilaterally — is its central solution concept. Nash proved in 1951 that every game with finitely many players and finite strategy sets has such an equilibrium (Nash, Non-cooperative games, Ann. Math. 54 (1951)); this single existence theorem is the reason the concept organizes the rest of the field, from the computational complexity of finding equilibria to the price of anarchy. The theorem is stated as Theorem 1.8 of Nisan–Roughgarden–Tardos–Vazirani (eds.), Algorithmic Game Theory (Cambridge, 2007), the source text of this mission series, whose first chapter (Tardos–Vazirani) also treats the two special cases that admit direct algorithmic proofs: two-person zero-sum games, where equilibria are exactly the optimal solutions of a dual pair of linear programs (von Neumann 1928; Theorem 1.11), and a simple linear market, where equilibrium prices are computed by an ascending tight-set algorithm (Theorem 1.17).
A timeline of the existence theorem: von Neumann (1928) proved the minimax theorem for two-person zero-sum games; Nash (1950, 1951) extended existence to arbitrary finite games, first via Kakutani's fixed-point theorem and then via Brouwer's. All known proofs of the general theorem pass through a fixed-point principle, and this is not an artifact: computing a Nash equilibrium is PPAD-complete (Daskalakis–Goldberg–Papadimitriou 2009; Chen–Deng–Teng 2009), and PPAD is precisely the complexity class of the fixed-point arguments.
A finite strategic-form game consists of a finite set of players, for each player a finite nonempty set of pure strategies, and for each player a payoff function ; all players are utility maximizers. A mixed strategy for player is a probability distribution on , represented as a weight function with and (a lottery). Players randomize independently, so a mixed profile induces the product distribution on pure strategy vectors, and player 's expected payoff is
A mixed profile is a (mixed) Nash equilibrium if for every player and every lottery on , replacing by does not increase .
A two-person zero-sum game is given by a matrix : the row player picks a row distribution , the column player a column distribution , and the column player pays the row player in expectation.
The market of §1.8.1 of the source has finitely many divisible goods, good in units, and finitely many buyers, buyer bringing budget and interested in a nonempty set of goods; utilities are linear 0/1, so a buyer wants any goods from her interest set and none other. Market-clearing prices are positive prices under which each buyer can spend her whole budget on cheapest goods in her interest set while every good sells out exactly.
Stated for an arbitrary finite family of finite nonempty strategy types; no bound on the number of players, no genericity assumptions.
Mathlib currently has no form of Brouwer's theorem; every known proof of Theorem 1.8 needs it (or an equivalent), so it enters the mission as an explicit milestone rather than an assumed library fact.
of the explicit two-player game with payoffs to the row player and to the column player. The source states the result as: optimal solutions of a dual pair of LPs form a Nash equilibrium of the zero-sum game; the first two conjuncts are the saddle point that LP optimality amounts to, and the third states the Nash-equilibrium clause against the mission's own game vocabulary, so "zero-sum" is formal (the two payoffs sum to zero) rather than implicit in the shape of the statement.
The source proves this by an ascending-price algorithm and also bounds its running time; the complexity half has no formal counterpart in this mission.
The capstone is the foundation of the whole mission series: correlated equilibria, price-of-anarchy bounds, and mechanism-design characterizations in later missions all quantify over or compare against Nash equilibria, and the series inherits its game vocabulary (IsLottery, IsMixedProfile, expectedPayoff, IsMixedNash) from this mission.
Formalizing it produces the first Brouwer fixed-point theorem in this environment — a well-known gap in mathlib with reuse value far beyond game theory (every degree-theoretic and equilibrium-existence argument needs it). The zero-sum milestone yields the minimax theorem, reusable for the learning-dynamics mission that follows. All results here are classical and proved on paper; the work requested is machine-checked proof, not new mathematics.
The central difficulty is Brouwer. The standard routes are (i) Sperner's lemma plus a limit argument, which needs a formal theory of simplicial subdivisions that does not exist in mathlib; (ii) algebraic topology (no retraction of the ball onto the sphere), for which mathlib has singular homology but not yet the homology of spheres in usable form; (iii) analytic proofs (Milnor–Rogers). None is short; the milestone is deliberately stated for a general nonempty compact convex set in a finite-dimensional normed space so that any route serves, and so the lemma lands in reusable generality.
Given Brouwer, Theorem 1.8 still requires Nash's gain-function construction on the product of simplices and the verification that fixed points are equilibria — bookkeeping-heavy but standard. Theorem 1.11 does not need Brouwer: mathlib's Sion minimax theorem (Mathlib.Topology.Sion) applies to the bilinear payoff on the product of standard simplices, or one can argue by LP duality directly. Theorem 1.17 needs the tight-set/max-flow argument of Lemmas 1.15–1.16 or any direct construction of the equilibrium.
Games are presented concretely: players form a finite index type, strategies a finite type per player, payoffs are functions into ; mixed strategies are weight functions with a IsLottery predicate, not measure-theoretic distributions. Deviations in the equilibrium definition range over all lotteries (not only pure strategies): the pure-deviation reduction is a lemma a solver may prove, not part of the definition. Strategy sets are assumed nonempty in the capstone; the player set need not be. In the zero-sum milestone both dimensions are positive (Fin (m+1), Fin (n+1)), payoffs flow from the column player to the row player, stdSimplex plays the role of the mixed-strategy space, and the Nash-equilibrium conjunct is stated for the Boolean-indexed two-player game built by matrixGameStrat/zeroSumPayoff/matrixGameProfile from the definitions bundle. In the market milestone all supplies and budgets are positive, every buyer's interest set is nonempty, and every good has an interested buyer, matching the standing assumptions of §1.8.1; allocations are recorded as money spent, so the clearing condition is with no division anywhere.
Trivializing readings are ruled out: the empty simplex has no lotteries, so nonemptiness hypotheses appear exactly where their absence would make an existence claim false (Brouwer on the empty set, games with an empty strategy set, zero-dimensional matrix games).
The matrix-multiplication exponent measures the asymptotic arithmetic cost of multiplying square matrices. An upper bound means that, over the field under consideration, matrices can be multiplied using arithmetic operations for every . Improvements to are a central benchmark in algebraic complexity because matrix multiplication is also a basic subroutine in linear algebra, graph algorithms, and symbolic computation.
The existing Prove2Me mission formalizes Schönhage's bound from a concrete two-summand tensor degeneration. The present mission advances the same formal development to the next clean historical construction. Pan and Winograd found a simultaneous approximate algorithm for three matrix products; Romani recorded its tensor form and the parameter choice , , which gives . Schönhage's 1981 paper reports the equivalent bound in the arbitrary-field setting. The exact formal target here is the slightly weaker rational inequality .
For a field , the matrix-multiplication tensor encodes multiplication of an matrix by a matrix:
A direct sum places several such tensors in disjoint coordinate blocks. A tensor has border rank at most when it is a polynomial degeneration of the diagonal tensor . In the Lean development this relation is Degenerates T (TensorObj.diagObj K 3 r). The argument order matters: the first tensor is the target and the diagonal tensor is the source.
The platform already defines ordinary tensor rank, asymptotic tensor rank, the tensor-rank exponent matMulExp K, the equivalent Strassen-preorder exponent matMulExp_strassen K, and Schönhage's asymptotic sum inequality. This mission reuses those declarations. No alternative definition of is introduced.
The goal has exactly the same quantified proposition as the existing mission, with only the rational endpoint changed:
The source construction to be formalized is
Each summand has volume :
The milestone chain records the degeneration, its asymptotic-rank consequence, the exact numerical implication
and the resulting Strassen-form exponent bound. The public goal then transfers the bound to matMulExp K through the already established equality of the two exponent definitions.
Mathematically, this construction improves the concrete exponent certified by the existing mission from to without changing the surrounding theory. It isolates the first genuinely new ingredient after the accepted Schönhage example: a larger simultaneous tensor degeneration rather than a sharper numerical estimate for the old witness.
For formalization, the mission tests whether the current polynomial-degeneration API can express a historically important trilinear aggregation at realistic scale. Once the explicit witness is available, the remaining declarations form a reusable template for later bounds: a source tensor degeneration, an asymptotic-rank bound, a specialization of the asymptotic sum inequality, and a final exponent transfer. This creates a trustworthy stepping stone toward the Coppersmith--Winograd tensor and later laser-method analyses.
The theorem is known mathematically; the open work is its machine-checked Lean formalization. The exact numerical endpoint and every downstream bridge from the degeneration have already been checked locally. The explicit Pan--Winograd degeneration remains the substantive open milestone.
The central difficulty is not the logarithmic comparison. It is constructing and verifying the polynomial family whose leading nonzero coefficient is exactly the tagged direct sum of the three matrix-multiplication tensors and whose earlier coefficients vanish. The family has diagonal source slots and many indexed target coordinates. A proof must account for all mixed-coordinate terms and all cancellations uniformly over an arbitrary field.
Romani's published summary states the approximate-rank inequality but does not spell out a Lean-ready map between its trilinear forms and the platform's TensorObj.bigAdd coordinate spaces. A solver must therefore recover the source indexing carefully and prove that the resulting modewise linear maps have the required coefficients. Reversing the degeneration direction, conflating tensor rank with asymptotic rank, or silently assuming a characteristic-zero scalar identity would invalidate the result.
All theorems quantify over an arbitrary type with [Field K], matching the existing Schönhage goal and the arbitrary-field statement of the source bound. Tensor spaces are finite-dimensional function spaces already packaged by MMObj; the three products are combined with TensorObj.bigAdd. Border rank is represented by the existing finitely supported polynomial-family predicate Degenerates. Because the source summary specifies approximate rank but not a leading order, the main degeneration milestone existentially quantifies that order instead of hard-coding one.
The mission includes no placeholder laser-value definition and makes no claim about the later analysis. It also excludes Schönhage's additional microscopic symmetrization improvement beyond . A valid solution must construct the stated degeneration itself; a vacuous hypothesis or a redefinition of matMulExp is outside scope.
Reusable contributions include coefficient lemmas for polynomial tensor families, finite-index equivalences for direct sums, and generic aggregation identities that specialize to the , witness. Contributions that merely restate the target under stronger field hypotheses do not close the arbitrary-field milestone.
The coupling method of Mission III asks for a coupling of two copies of a chain from every pair of starting states — often painful to construct globally. Chapter 14 of Levin–Peres–Wilmer, Markov Chains and Mixing Times (AMS, 2009) replaces that global demand by a local one. The path coupling technique of Bubley and Dyer says: put a connected graph structure on the state space, and couple one step of the chain only across edges; if each edge contracts in expectation, contraction propagates automatically along paths to arbitrary pairs of distributions. The bookkeeping runs through the transportation metric (Kantorovich distance) between distributions, whose theory — attainment by an optimal coupling, the triangle inequality — is developed on the way. The chapter's payoff is the sharpest elementary bound for sampling proper colorings (Theorem 14.8: the Glauber dynamics mixes in steps once ), and, through the sampling-to-counting reduction of Jerrum–Valiant–Vazirani, a polynomial-time approximation algorithm for counting colorings — the paradigm of the Markov chain Monte Carlo method as an algorithmic tool.
All chains live on a finite state space with a transition matrix ; is the time- distribution from , the total variation distance, the worst-case distance to the stationary distribution , and the mixing time. A coupling of distributions is a distribution on with marginals and .
Given a metric-like cost on pairs of states, the transportation metric between two distributions is the cheapest expected cost of moving one onto the other:
Given a connected graph structure on the state space with edge lengths , the path metric is the least total length of a -path from to .
For the colorings application: a -coloring of the vertices of a graph is proper when adjacent vertices receive distinct colors, and the Glauber dynamics on proper colorings picks a uniform vertex and re-samples its color uniformly among the colors legal there; its stationary distribution is uniform on the proper colorings. Throughout, is the number of vertices and the maximum degree of the graph being colored.
Theorem 14.8, the capstone of Chapter 14: for the Glauber dynamics on proper -colorings, if then
The results. Path coupling converted the coupling method from an art into a calculus: one bounds a single-edge contraction constant, and the machinery does the rest. It is the standard tool for Glauber dynamics on colorings, independent sets, and other constraint-satisfaction models, and the colorings bound is its flagship application. Theorem 14.12 is the discrete embodiment of the Jerrum–Valiant–Vazirani equivalence between approximate counting and sampling — the conceptual foundation of the entire MCMC approach to -hard counting problems.
Formalizing them. Mathlib has no transportation/Kantorovich metric in the finite setting, no path coupling, and nothing on approximate counting. The transportation-metric layer (optimal couplings, triangle inequality) is reusable far beyond this mission — it is the finite Wasserstein distance. The path-coupling theorem feeds directly into Mission IX (Ising) and is quoted throughout modern mixing literature.
The transportation metric asks for minimization over the (compact) polytope of couplings: attainment is a finite-dimensional compactness argument, and the triangle inequality requires gluing two optimal couplings along their common marginal — the classic construction that must be carried out with explicit finite sums here. Path coupling itself is an induction along geodesics of the path metric, with the subtlety that the composite coupling produced along a path need not be optimal, only admissible; the bookkeeping of the contraction constant through the induction is exactly the kind of argument Lean keeps honest. Theorem 14.8 instantiates the machinery: the single-edge coupling for colorings needs a careful case analysis of the proposed recolorings at the two endpoints (matching legal colors bijectively), and the contraction constant emerges from counting disagreeing proposals. Theorem 14.12 layers a probabilistic-amplification argument (medians of means over independent runs) on top of the mixing bound; its combinatorial core — expressing as a telescoping product of marginal probabilities — is elementary but notation-heavy, and the formal statement quantifies over explicit seed spaces, so the whole estimator is a finite object.
The transportation metric is an sInf over coupling costs (the coupling polytope is nonempty for genuine distributions, and attainment is part of the milestone, so the junk value never propagates); the path metric is an sInf over walk lengths in a connected graph. The Glauber dynamics on colorings is the restriction to proper colorings of the single-site heat-bath chain of Mission II, matching §3.3 of the book; its state space is the subtype of proper colorings, nonempty whenever (a fact the hypotheses of the goal supply). Mixing-time upper bounds are stated with the book's explicit ceilings, so no rounding slack is hidden. In Theorem 14.12 the estimator is presented concretely as a function of finitely many uniform seeds, and "with probability " is a counting inequality over the seed space — no measure theory enters. Contributions of intermediate lemmas (optimal-coupling gluing, geodesic decompositions, colorings edge-coupling) are welcome and will be reused by Mission IX.
A reversible Markov chain is an electrical network: states are nodes, and the conductance turns hitting probabilities into voltages and hitting times into resistances. This dictionary, going back to Kakutani and popularized by Doyle and Snell, converts probabilistic estimates into the physical laws of circuits — series/parallel reduction, energy minimization, monotonicity under edge removal. Chapters 9–11 of Levin–Peres–Wilmer, Markov Chains and Mixing Times (AMS, 2009) develop the dictionary and its two crown results: the commute time identity of Chandra–Raghavan–Ruzzo–Smolensky–Tiwari, , and the Matthews method bounding cover times by hitting times with harmonic-number precision.
A network is a symmetric nonnegative conductance function on pairs of vertices; the associated walk moves with probabilities
where , and . A function is harmonic at if . The voltage with boundary values at and at is , the harmonic extension of its boundary data; the current flowing out of has strength , and the effective resistance is . A flow from to is an antisymmetric edge function obeying the node law off ; its energy is . Hitting times , their expectations, the Green's function , the maximal hitting time , and the cover time (expected time to visit every state, maximized over starts) all use the trajectory calculus of Mission I.
This is Proposition 10.6, the commute time identity — the exact bridge between the probabilistic and electrical sides, and the engine of the transience/recurrence theory of Mission XII.
Reversibility and stationarity of the network walk with (§9.1); Proposition 9.1 (existence and uniqueness of harmonic extensions with given boundary values, ); Lemma 9.6 (the Green's function identity ); Theorem 9.10 (Thomson's principle: is the minimal energy of a unit flow, attained); Theorem 9.12 (Rayleigh monotonicity: lowering conductances raises effective resistance); Lemma 10.1 (the random target lemma: does not depend on ); Corollary 10.8 (the resistance triangle inequality); Theorem 11.2 (Matthews: ); Proposition 11.4 (the matching Matthews lower bound over subsets).
The results. The commute time identity computes hitting times from circuit reductions — this is how hitting times on trees, tori and glued graphs are actually evaluated — and, through Thomson and Rayleigh, makes them monotone under graph operations, something invisible probabilistically. The Matthews bounds pin cover times up to a factor in complete generality; they are the tool behind cover-time results for lamplighter groups in Mission XI's sequel. Green's function identities feed Mission XII's recurrence theory, where decides transience.
Formalizing them. Mathlib has graph Laplacians but no electrical network theory: no effective resistance, no flows, no energy, no Thomson/Rayleigh, no hitting or cover times. This mission publishes that layer over the trajectory calculus of Mission I. It is the most reusable single block of the series outside Missions I–II: effective resistance on finite networks is of independent interest to combinatorics (spanning trees, spectral sparsification) well beyond mixing times.
The identity chain behind the goal runs: Green's function of the stopped walk escape probability (via harmonic uniqueness) the Aldous–Fill occupation identity for stopping times with — each step is a manipulation of infinite series of trajectory sums whose exchange steps (splitting a path at its first visit, last-exit decompositions) need summability from Mission I's Lemma 1.13. Thomson's principle is a finite-dimensional convex minimization: existence of the minimizer needs a compactness or completing-the-square argument, and the identification of the minimizer with the current flow needs the cycle law; the naive "differentiate the energy" route must be made exact. Matthews' method is a clean but genuinely clever argument — a uniformly random ordering of targets and the harmonic-number telescoping; the formal cost is the exchangeability of the randomized order against the chain, handled combinatorially.
Networks are functions with a symmetry-and-nonnegativity predicate; loops are permitted; connectivity enters as irreducibility of the induced walk. The voltage is defined probabilistically as (the book's harmonic characterization is Proposition 9.1); is the reciprocal of the explicit current strength, with total division junk when are disconnected — statements carry irreducibility so this does not arise. Energy counts each undirected edge once, formalized as half the ordered double sum, and handles absent edges. Cover times are tail sums of the explicit event "some state unvisited". The Matthews lower bound is stated with an arbitrary lower bound for the pairwise hitting times of the subset — equivalent to the book's min over pairs and easier to instantiate.
Welcome contributions: series/parallel reduction laws, the cycle and node law API for flows, escape-probability lemmas — all reused in Mission XII's infinite-network arguments.
Modern A/B tests must infer lifetime treatment effects — e.g. customer lifetime value under a new feature — from short-horizon experiment data. Chen, Simchi-Levi and Wang (arXiv:2407.19618) model the experiment as a Markov decision process and exploit a structural fact of many practical interventions: the treatment is local, modifying the system at a single crucial state only. This mission formalizes the core asymptotic theory of the paper: for any differentiable estimator built from the experiment's transition and reward statistics, information sharing — pooling across test arms the samples collected away from the treated state — keeps the estimator asymptotically normal with the same asymptotic bias and never increases its asymptotic variance (Theorem 9), and is asymptotically efficient among unbiased estimators (Theorem 5). The route runs through a Markov chain central limit theorem with the asymptotic variance identified as the autocovariance series, and the linearization/delta method for functionals of chain statistics.
Finite Markov chains are the basic model for memoryless random dynamics: card shuffles, random walks on graphs and groups, Monte Carlo samplers, and queueing systems are all chains on a finite state space. The single most used fact about them is that an irreducible chain has exactly one stationary distribution — a probability vector with — and that this is strictly positive and encodes the long-run behaviour of the chain through the return-time identity . Every later result in the theory of mixing times (convergence theorems, coupling bounds, spectral methods, cutoff) is a statement about the distance of the chain from this , so nothing in the subject can be formalized before this mission is.
This mission is the first in a series formalizing D. A. Levin, Y. Peres and E. L. Wilmer, Markov Chains and Mixing Times (AMS, 2009), covering Chapters 1–2: the basic vocabulary of finite chains (stochastic matrices, irreducibility, period, reversibility, time reversal, random walks on graphs and groups) and the classical examples of Chapter 2 (gambler's ruin, coupon collecting, the reflection principle for simple random walk on ). Later missions in the series build on the definitions published here.
A chain on a finite state space is presented by its transition matrix, a matrix with nonnegative entries whose rows sum to . A distribution is a row vector with nonnegative entries summing to ; one step of the chain carries to , and the -step transition probabilities are the entries of the matrix power .
The chain is irreducible if for all states there is a with . The period of a state is where , and the chain is aperiodic if every state has period . A distribution is stationary if , and and are in detailed balance (the chain is reversible) if for all .
Trajectory events over a finite horizon are finite sums of path weights: a length- trajectory is a function , with weight conditional on its starting state. The tail probability of the first hitting time is the sum of the weights of the trajectories from that avoid at times , and expectations of hitting times are recovered by the tail-sum formula , formalized as a tsum over .
This is Corollary 1.17 of the book. It asserts only existence and uniqueness, leaving the finer structure of to the milestones; it is the weakest statement on which the rest of the series can stand, which is why it is the goal.
The milestone list follows the book's own route: well-definedness of the period (Lemma 1.6), positivity of some matrix power for irreducible aperiodic chains (Proposition 1.7), finiteness of expected hitting times (Lemma 1.13), existence of a positive stationary distribution together with
(Proposition 1.14), constancy of harmonic functions (Lemma 1.16), stationarity from detailed balance (Proposition 1.19), the stationary and reversible measure of simple random walk on a graph (Examples 1.12 and 1.20), the time reversal and its path-reversal identity (Proposition 1.22), and the random walks on finite groups of Section 2.6 (Propositions 2.12–2.14). From Chapter 2 the list adds the gambler's ruin formulas and (Proposition 2.1), the coupon collector expectation and tail bound (Propositions 2.3 and 2.4), and the reflection principle and the bound for simple random walk on (Lemma 2.18 and Theorem 2.17).
The result itself. Existence and uniqueness of is the pivot on which the entire quantitative theory turns: it defines the target of convergence, and the identity ties the stationary measure to return times, which later missions use for hitting-time and cover-time results. Detailed balance is the practical tool by which stationary measures of graph and group walks are computed, and the Chapter 2 examples (gambler's ruin, coupon collecting, reflection) are the standard building blocks reused throughout the book — the coupon collector bound, for instance, is exactly the estimate behind the analysis of the top-to-random shuffle in a later mission of this series.
Formalizing it. Mathlib currently has no theory of finite Markov chains: no stochastic-matrix predicate, no stationary distribution, no periodicity, no hitting times. Everything proved in this mission is new formal mathematics, and the definition layer published here (mm_basic, mm_path, mm_classical) is the shared foundation that all twelve subsequent missions of the series import. All results are classical and have textbook proofs; none has a machine-checked proof.
The delicate point is the existence proof. The natural first idea — extract from an eigenvector of for eigenvalue , or invoke a fixed-point theorem — either does not give positivity and nonnegativity without further work, or uses compactness machinery (Brouwer) that is unavailable. The book's proof instead builds and verifies by reindexing trajectory sums; formalizing it requires managing infinite series of path sums (summability from the geometric tail bound of Lemma 1.13, exchanging tsum with finite sums, splitting a trajectory at its last step). The uniqueness half is linear algebra via constancy of harmonic functions (Lemma 1.16), which is elementary but requires a maximum-principle argument over a finite state space. The reflection principle and Theorem 2.17 are finite combinatorics on paths — the bijection is easy to describe and fiddly to implement.
States form a Fintype with decidable equality; chains are Matrix V V ℝ with the row-stochasticity predicate IsStochastic; distributions are functions V → ℝ with the predicate IsDist. Everything is distribution-side: no probability space or measure theory is used. The period is formalized as , which equals when and takes the junk value otherwise. Expectations of hitting times are tsums of tail probabilities, with the usual junk value for non-summable families — the statements are arranged (e.g. multiplicatively, ) so that junk values cannot make them vacuously true. Existence statements carry a Nonempty V hypothesis; irreducibility on the empty space is vacuous, and without nonemptiness the goal would be false, not trivial. The coupon collector and the walk on are presented directly by their driving randomness (uniform draws Fin t → Fin n, uniform sign strings Fin r → Bool), so those probabilities are elementary counting; in particular the reflection principle is stated as an equality of cardinalities of sets of sign strings — this is equivalent to the probabilistic statement because all strings are equally likely.
Contributions welcome beyond the milestone list: simp lemmas for the definition layer, the taboo-matrix representation of avoidance probabilities (useful for Lemma 1.13), and any interface lemmas connecting pathWeight sums to matrix powers — these will be reused by every later mission in the series.
The classical convergence theory of smooth convex minimization. For a function that is -strongly convex and -smooth (), gradient descent converges linearly, while Newton's method exhibits its famous two phases: a damped phase in which every backtracking step decreases the objective by a fixed amount , and a quadratically convergent phase in which the scaled gradient norm squares at each step, . Together they give the iteration count of B&V (9.36),
with the Lipschitz constant of the Hessian and the backtracking parameters. This mission formalizes Chapters 9–10 of Boyd & Vandenberghe with every constant exactly as printed — a quantitative theory entirely absent from Mathlib.
The Karush–Kuhn–Tucker conditions are the central result of convex optimization: for a convex differentiable problem satisfying Slater's condition, a point is optimal exactly when primal feasibility, dual feasibility, complementary slackness and Lagrangian stationarity hold. This mission formalizes Chapters 4–5 of Boyd & Vandenberghe end to end — the first-order optimality criterion, concavity of the Lagrange dual, weak duality, Slater's strong-duality theorem with dual attainment (via the separating-hyperplane argument of §5.3.2), the saddle-point characterization, sensitivity bounds and Pareto scalarization — culminating in the full KKT characterization.
Linear programming has a complete duality theory; integer programming does not — and the Lagrangean dual measures exactly how far duality reaches. This mission formalizes the duality theory of integer programming from Section 11.4 of Bertsimas–Tsitsiklis, built on the general linear programming duality of Section 4.10. For the integer program
with integer data, the complicating constraints are dualized with multipliers over the tractable set : the dual function is
and the Lagrangean dual is . Weak duality (Theorem 11.2) always holds, but strong duality can fail. The convex hull of the integer points of a polyhedron with integer data is itself a polyhedron (Theorem 11.3, Meyer's theorem), and the capstone — Theorem 11.4, the central result of Section 11.4 — identifies the Lagrangean dual exactly: equals the optimal cost of the linear program
. This is the geometric explanation of the strength of Lagrangean relaxation, yields the bound ordering , and Corollary 11.1 characterizes exactly when the bounds collapse. The polyhedral engine is the general weak/strong duality pair (Theorems 4.17/4.18) over a primal s.t. , , and the formulation-strength comparison of Theorem 10.1 supplies the motivating principle that tighter relaxations of the same integer set give sharper bounds.
How can an unbounded polyhedron be described by finitely many geometric objects? Sections 4.8-4.9 of Bertsimas-Tsitsiklis build the cone machinery: recession cones and their rays, extreme rays (defined, like basic solutions, by linearly independent active constraints), the pointedness criterion (Theorem 4.12: is an extreme point of a polyhedral cone iff the cone contains no line iff of the constraint vectors are linearly independent), and the characterization of unbounded linear programs (Theorems 4.13-4.14: over a pointed polyhedral cone, and then over any polyhedron with an extreme point, the optimal cost is iff some extreme ray has ). The capstone is the resolution theorem (Theorem 4.15): a nonempty polyhedron with at least one extreme point equals — the convex hull of its extreme points plus the cone generated by a complete set of its extreme rays. It specializes to Theorem 2.9 / Corollary 4.4 (a nonempty bounded polyhedron is the convex hull of its extreme points) and Corollary 4.5 (a pointed polyhedral cone is generated by its extreme rays). The converse, Theorem 4.16, states that every finitely generated set is a polyhedron — in particular the convex hull of finitely many vectors is a polyhedron. Together these form the Minkowski-Weyl equivalence of the two representations of polyhedra, verified absent from Mathlib and the genuine content of this mission.
Matrix completion — recovering a low-rank matrix from a small random subset of its entries — powers recommender systems and collaborative filtering. In practice it is solved by running (stochastic) gradient descent on the non-convex objective
where and is a certain regularizer. from a random starting point, and it just works.
Ge, Lee and Ma (NeurIPS 2016 Best student paper award) explained why: the regularized objective has no spurious local minima — every local minimum is global and exactly recovers . This mission formalizes that landmark theorem in Lean 4, in its strongest known form and along its simplest known proof: the unified landscape analysis of Ge–Jin–Zheng (ICML 2017) and an improved sampling bound in Chen–Li (JMLR 2019). Conditional on an explicit good-sample predicate (which holds with high probability under Bernoulli sampling), every local minimum of satisfies .
Bandit feedback is only one point on a spectrum: a learner might see more than its own loss (full information) or less (a spam filter never learns what happened to mail it deleted). Chapter 37 of Lattimore–Szepesvári studies finite adversarial games where the loss matrix and the feedback matrix are decoupled. The goal theorem is the celebrated classification theorem: every finite partial-monitoring game has minimax regret exactly , , or — determined by two purely combinatorial conditions, global and local observability, on the game's neighbourhood structure. A single geometric dichotomy thus governs the price of information in every online decision problem with finite actions and feedback.
When actions are feature vectors and the mean reward is linear — — a bandit can generalize across arms: pulling one arm reveals information about all of them. Chapter 19 of Lattimore–Szepesvári carries the optimism principle into this setting: LinUCB (a.k.a. OFUL) plays the action maximizing over the confidence ellipsoid of Mission IX. The goal theorem: with probability , — regret independent of the number of actions. The combinatorial engine is the elliptical potential lemma, bounding how many times adaptively chosen directions can be surprising. Chapter 22's phased elimination with G-optimal design (Mission IX) sharpens this to for finite action sets.
Least-squares estimation from adaptively collected data is the statistical heart of linear bandits: the actions depend on past noise, so classical fixed-design theory does not apply. Chapter 20 of Lattimore–Szepesvári resolves this with the method of mixtures: the process is a supermartingale, and integrating over a Gaussian mixture yields the self-normalized bound — the goal theorem — , valid uniformly over all times. The resulting confidence ellipsoids for the regularized least-squares estimator (Abbasi-Yadkori et al.) calibrate every algorithm of Mission X. The mission also formalizes the Kiefer–Wolfowitz theorem of Chapter 21: G-optimal and D-optimal experimental designs coincide, with optimal value exactly — the classical equivalence theorem of optimal design theory.
Every even integer greater than is the sum of two primes. Christian Goldbach posed it in a 1742 letter to Euler, and it has resisted proof for nearly three centuries while being verified computationally up to — making it one of the oldest and most famous open problems in all of mathematics. Its ternary sibling, the weak Goldbach conjecture, was settled by Helfgott in 2013, but the strong form stated here remains wide open: the circle method controls three-prime sums yet loses control at two. This headline mission hosts the conjecture as a machine-checked target for partial results, reductions between its variants, and any future attack.
The ellipsoid method is the cutting-plane algorithm that settled the polynomial-time solvability of linear programming and, more generally, of convex optimization over any set that comes with an efficient separation oracle. It was introduced for convex minimization by Shor and by Yudin and Nemirovski in the 1970s, and Khachiyan used it in 1979 to give the first polynomial-time algorithm for linear programming. Grötschel, Lovász and Schrijver later turned it into the general equivalence between separation and optimization that underlies much of combinatorial optimization.
This mission is the second of a series formalizing S. Bubeck, Convex Optimization: Algorithms and Complexity (Foundations and Trends in Machine Learning 8(3–4), 2015; arXiv:1405.4980v2). Its goal is the convergence guarantee of the ellipsoid method, Theorem 2.4 (p. 250), together with the geometric lemma and the steps of the proof on which it rests.
Timeline:
Write for the space of real -vectors, with the dot product . An ellipsoid is a set
where is its center and is a symmetric positive definite matrix.
A convex body is a compact convex set with non-empty interior. The objective is continuous and convex on with values in , and are such that lies in the Euclidean ball of center and radius and contains some Euclidean ball of radius . A subgradient of at is a vector with for all .
The method starts from , . At step it asks for a vector :
It then replaces by the ellipsoid given by
After iterations the output is the best of the queried centers that lie in .
For and every , , some queried center lies in , and every output satisfies
and for the explicit ellipsoid (2.5)–(2.6) works. 3. The remark before Theorem 2.4 (p. 250): a point of can leave the current ellipsoid only at a step with , and then its value exceeds . 4. Two steps reused from Theorem 2.1 (pp. 246–247): for , and on .
Theorem 2.4 bounds the oracle complexity of the ellipsoid method: accuracy needs oracle calls. Each step costs arithmetic operations plus one oracle call. With the separation oracles of linear and semidefinite programs this gives polynomial overall complexity (p. 250). The rate depends on the instance only through and , so the method needs no smoothness and no strong convexity. Lemma 2.3 is also the geometric step of the ellipsoid method for linear feasibility.
The result has a textbook proof. The work of this mission is to formalize it. The same update is published on the platform from Bertsimas and Tsitsiklis's Introduction to Linear Optimization (Theorem 8.1), with a proved volume factor of . That factor is weaker than (2.4)'s and does not give Theorem 2.4's constant. The sharper factor and the optimization version of the method (subgradient cuts, the output rule and the value bound) are not formalized on the platform.
There are two difficulties: Lemma 2.3 with the sharp constant, and the bookkeeping that turns per-step volume decrease into a value bound.
For the lemma, the volume of the explicit ellipsoid is times that of . Bounding it by rather than by the cruder needs the scalar inequality of milestone 1 for every . The reduction from a general ellipsoid to the unit ball also needs determinants under an affine map.
For the theorem, the obvious argument compares with . This only works if no cut removes an optimal point and if every removed point of is worse than a queried center. At the threshold the admissible is exactly , so a non-strict volume bound alone does not close the argument there.
Fin n → ℝ with Lebesgue measure, as in the reused Bertsimas–Tsitsiklis ellipsoid definitions (LinearOptimization.ellipsoid, ellipsoidUpdateCenter, ellipsoidUpdateMatrix, IsSubgradientOn).Fin n → ℝ is the sup norm.IsEllipsoidRun. Every theorem holds for every admissible oracle answer. The update is the published one with .Conventions and hypotheses added to the page:
A run predicate whose separation branch does not require , or that accepts with an update, would make the statements false or vacuous. Both are excluded.
Lemma 2.3's volume factor is . The weaker published factor does not prove that milestone. The published theorem LinearOptimization.ellipsoid_update_halfspace_volume is included as a reference: it supplies the containment (2.3) and positive definiteness. Contributions are welcome on every milestone. A determinant formula for the volume of an ellipsoid would be reusable well beyond this mission.
Generalization bounds in statistical learning theory control the gap between the empirical and the true performance of a predictor chosen from a class . Bartlett and Mendelson (JMLR 3, 2002) showed that this gap is governed by the Rademacher complexity of a loss class built from , and that, unlike the VC dimension, this complexity can be estimated from data. Their bounds are useful only if the Rademacher complexity of a large class can be bounded in terms of simpler classes: voting methods take convex combinations of base classifiers, neural networks compose fixed squashing functions with linear combinations, and loss classes compose a class with a Lipschitz loss. Section 3.1 of the paper collects the elementary rules for such constructions in one statement, Theorem 12. These rules are used throughout the later literature on margin bounds, boosting, and neural-network generalization (e.g. Koltchinskii and Panchenko, Ann. Statist. 2002).
This mission formalizes those rules, as stated in the published journal article (J. Mach. Learn. Res. 3 (2002), pp. 463–482), Theorem 12 on p. 469.
Let be a measurable space, a probability measure on it, and an integer. A class is a set of functions ; no boundedness is assumed.
For a sample , the empirical Rademacher complexity of (Definition 2, p. 464) is
the expectation over independent uniform random signs . The Rademacher complexity is its expectation over an i.i.d. sample from :
In the Lean development these are empiricalRademacher n F x and rademacherComplexity μ n F, both valued in .
The constructions on classes are those of §2, p. 467: is the class of convex combinations of functions from ; ; is the class of convex combinations of functions from ; ; for , ; and .
For all classes of real functions:
The goal is the conjunction, each part quantified over its own classes.
Parts 1, 3, 2 and 4 are milestones, in the order of the paper's proof. Part 7 remains a theorem item in the mission and a conjunct of the goal.
The result. Theorem 12 reduces the complexity of a constructed class to the complexities of its building blocks. Part 2 says that convex combinations come for free, which is why margin bounds for boosting depend only on the base class. Part 4 converts a complexity bound for a class into one for a Lipschitz loss composed with it, which is how the risk bounds of the paper's §2 are applied to concrete losses. Parts 1, 3 and 7 are the bookkeeping rules that combine the others; the paper uses parts 1 and 3 to show part 7 is tight.
Formalizing it. The results are proved, and part 4 is due to Ledoux and Talagrand (Probability in Banach Spaces, Springer 1991, Corollary 3.17). The platform already has a one-sided contraction lemma in a different normalization (UnderstandingML.contraction_lemma, Shalev-Shwartz and Ben-David's Lemma 26.9: per-coordinate Lipschitz maps, normalization, no absolute value, bounded nonempty sets of vectors), referenced here as supporting material, and a convex-hull identity for Mohri et al.'s empirical complexity without absolute value. None of the five parts is formalized for Definition 2's complexity (factor , absolute value inside the supremum, expectation over the sample, arbitrary classes). The mission provides machine-checked versions in exactly that normalization, reusable by the other missions of this paper and by any later development of Rademacher-complexity bounds.
Parts 1, 2, 3 and 7 are pointwise statements about finite averages of suprema, but they have to be carried through the expectation over the sample and through suprema that may be infinite. Part 2 needs the supremum of the absolute value of a linear functional over a convex hull to equal its supremum over the set, including the symmetric hull .
Part 4 is the substantial one. The natural first idea, comparing with term by term for each sign vector, fails: the inequality holds only after averaging over the signs, and only with the factor caused by the absolute value. Without the hypothesis the statement fails (a constant has but for nonempty and ), so any argument must use it.
Representation. Classes are Set (X → ℝ). Signs are averaged over all vectors Fin n → Bool (encoded ). Complexities take values in ℝ≥0∞: a class unbounded on the sample has complexity , the empty class has complexity , and is the lower Lebesgue integral against Measure.pi (fun _ : Fin n => μ) with μ a probability measure. This is the paper's meaning for arbitrary classes. A real-valued formalization would not be: a real supremum over an unbounded set and a Bochner integral of a non-integrable function both evaluate to . That would make the upper bounds false for unbounded classes and every comparison trivially satisfied for others. No boundedness hypothesis is added anywhere, since Theorem 12 is about arbitrary classes. is convexHull ℝ F (finite convex combinations, no closure); is convexHull ℝ (F ∪ -F); is c • F; enters as ENNReal.ofReal |c|, and makes consistent. The Lipschitz map in part 4 is LipschitzWith Lφ φ on all of , as printed. The classes of part 7 are indexed by Fin k and summed pointwise. At all complexities are and every part holds trivially, matching the page.
Added hypothesis. Part 7 (and its conjunct in the goal) assumes that each sample function is almost-everywhere measurable for . The paper does not discuss measurability. The lower integral is monotone and positively homogeneous without it, so parts 1–4 need no such hypothesis, but it is not additive, and part 7 needs additivity. The hypothesis holds whenever each is a countable class of measurable functions.
Omitted parts. Parts 5 and 6 of Theorem 12 are not posed. Part 5, , is false as printed: its proof (p. 470) bounds correctly but drops the factor of Definition 2, and the correct conclusion is . For , , the left side is and the printed right side is . Part 6 is derived from part 5. A corrected part 5 would not be the paper's statement, so neither is included. The remark after the theorem that parts 1–3 hold for the Gaussian complexity, and the others with an extra factor, is also not included.
Contributions welcome. Proofs of the milestones; a proof of part 4 from the platform's one-sided contraction lemma, converted to Definition 2's normalization; and general lemmas about empiricalRademacher (finiteness on finite classes, measurability for countable classes) that the other missions of this paper can reuse.
Robust optimization replaces an uncertain constraint , whose parameter is random, by the requirement that the constraint hold for every in a chosen uncertainty set :
The resulting problem is deterministic and, for many shapes of , tractable (Ben-Tal, El Ghaoui and Nemirovski, Robust Optimization, 2009). The modelling question it leaves open is how to choose . A set that is too large makes every solution conservative; a set that is too small gives no protection. The practitioner's real requirement is usually probabilistic: a robust feasible should violate the uncertain constraint with probability at most .
Bertsimas, Gupta and Kallus (Data-Driven Robust Optimization, arXiv:1401.0212v2, 2014; Math. Program. 167, 2018) build uncertainty sets directly from data so that this requirement holds with high confidence. Their whole construction rests on one characterization, Theorem 1 of the paper, of when a set carries such a guarantee. This mission formalizes that characterization and the two results (Theorems 2 and 3) that turn it into a data-driven recipe.
Earlier work used the "if" direction of the characterization for bi-affine constraints when designing sets for specific distributional assumptions (Ben-Tal et al., 2009; Chen, Sim and Sun, Oper. Res. 55, 2007). The extension to every constraint concave in is due to Bertsimas, Gupta and Kallus.
Let be a probability measure on , the law of , and fix a level . Throughout, is concave in for every value of the decision variable .
The support function of a set is
The Value at Risk of the linear loss at level is
A set implies a probabilistic guarantee at level for (property (P2) of the paper) if for every , every concave in for each , and every ,
A function is bi-affine if it has the form .
In the data-driven setting, is unknown and a sample is drawn i.i.d. from it. The paper's schema fixes , takes the confidence region of a hypothesis test at level , and builds a closed convex set whose support function bounds for every and every .
(a) If is nonempty, convex and compact and
then implies a probabilistic guarantee at level for .
(b) If is nonempty and for some at which is finite, then some bi-affine violates (2).
The proof in the electronic companion (EC.1.1) is a short chain, and its steps are the milestones: the attainment property of VaR, (already proved on the platform); a strict separating hyperplane between and the superlevel set ; the bound for ; its limit ; and, for part (b), the witness at .
Theorem 2: with probability at least over the sample, implies a probabilistic guarantee at level for . Theorem 3: if the region does not depend on , then with probability at least the whole family implies the guarantee simultaneously (a), and every satisfying the level-optimized constraints (9) satisfies the joint chance constraint
(b).
Theorem 1(a) is what certifies every uncertainty set in the paper: the and sets for discrete distributions, the Kolmogorov–Smirnov and forward–backward sets for independent marginals, the marginal-sample box and the moment sets. Each construction reduces to proving one inequality between a support function and a Value at Risk, which is a statement about a single linear functional, and Theorem 1(a) lifts it to every concave constraint at once. Part (b) shows the condition cannot be dropped even for bi-affine constraints. Theorems 2 and 3 separate the statistical input (coverage of a confidence region) from the convex-analytic input (the support-function bound), and Theorem 3(b) is what allows the levels of a system of constraints to be optimized after seeing the data.
The results are proved in the paper. None of them has a machine-checked proof; the only formalized ingredient is the attainment property of VaR, which is on the platform as a proved theorem. The formalization provides a checked bridge from support-function bounds to probabilistic guarantees that the other missions of this series (II–VI) use to state their own results in the criterion form .
The informal argument is short; the difficulty is in the infinite-dimensional bookkeeping that the page leaves implicit. The superlevel set need not be bounded, so the strict separation must use compactness of alone. Closedness of this set and measurability of depend on concave functions on being continuous. The passage is continuity of a measure along an increasing union. The attainment of the infimum in the definition of VaR requires right-continuity of distribution functions. A naive attempt to separate from the zero superlevel set directly fails, because the two sets may touch.
is Fin d → ℝ; is the identity map; is the dot product u ⬝ᵥ v. The Value at Risk is the published MultistageStochastic.valueAtRisk at level , and the support function is the published RobustMDP.Shared.supportFunction. Both are real-valued sInf/sSup, which return on empty or unbounded sets, so every statement assumes , a probability measure, and an uncertainty set that is nonempty and compact (Theorem 1(a), Theorems 2–3) or nonempty with bounded above in the direction considered (Theorem 1(b)). In Theorem 1(b) and its witness this is the paper's own requirement that be finite, which its strict inequality with a real VaR forces and its proof uses by treating as a real number. Part (b) is printed with , a slip for ; the proof's separation step prints both inequalities in the same direction, a slip corrected in the strict separation milestone.
Property (P2) quantifies over the dimension of the decision variable, every function concave in for each , and every . Restricting it to affine or to would trivialize part (a) and falsify part (b), and is ruled out by the definition.
In Theorems 2 and 3 the sample is Fin N → (Fin d → ℝ) with the product law Measure.pi; the confidence region and the uncertainty set are arbitrary maps of the sample, and the coverage is a hypothesis, never the conclusion's event. Step 2 of the schema is stated with directly. The sets are assumed nonempty and compact (Step 3 says closed and convex; a finite support function that bounds VaR forces nonemptiness and boundedness). Theorem 3(b) reads the levels in , where the family is defined. Probabilities of events in the sample space are outer measures, so no measurability hypotheses are needed.
A complete development needs strict separation of a compact convex set from a closed convex set (Mathlib's geometric_hahn_banach_compact_closed), continuity of concave functions on finite-dimensional spaces, and the attainment property of VaR. Contributions are welcome on all milestones; the separation and limit steps are reusable for any chance-constraint argument based on support functions.
Hassler Whitney introduced matroids in On the Abstract Properties of Linear Dependence (Amer. J. Math. 57, 1935, doi:10.2307/2371182) to capture what linear dependence among the columns of a matrix and the circuit structure of a graph have in common. One of the central constructions of the paper is duality. For graphs, duality exists only for planar graphs (Whitney, Non-separable and planar graphs, Trans. AMS 34, 1932); for matroids Whitney showed that every matroid has a dual, and that duality has a direct linear-algebra model: the matroid of a subspace of and the matroid of its orthogonal complement are duals.
Matroid duality underlies much of combinatorial optimization: the duality between cycles and cuts in graphs, the relation between a linear code and its dual code, the exchange of rank and corank in matroid intersection and partition, and the treatment of network flows as duals of potential problems. Whitney's §§11–13 are where this structure is first defined and where its linear-algebra meaning (Theorem 28) is established.
A matroid is a finite set of elements with a rank function on its subsets; equivalently, a family of independent sets, or of bases (maximal independent sets). For a subset write for its number of elements and
for its nullity; and are the rank and nullity of the whole set of elements.
Duality (§11). Let and be matroids and a one-to-one correspondence between their elements. is a dual of (via ) if, for every subset of , with the complement in of ,
The matroid of a subspace (§12). Let be -dimensional Euclidean space with coordinates , and let be a hyperplane through the origin, which in Whitney's usage is a linear subspace of any dimension. For a set of coordinates, project onto the coordinate subspace spanned by the axes , . The matroid associated with has elements , one per coordinate, and gives the set the rank
If is the row space of a matrix , then is the rank of the columns of indexed by , so the associated matroid is the column matroid of .
In the Lean development these objects are WhitneyMatroid.Components.nullity (shared), IsDualVia M M' σ, IsDual M M', subspaceRank H S and IsAssociated M H.
Let be a subspace of and its orthogonal complement. If and are the matroids associated with and , then and are duals under the correspondence of equal coordinates:
The result. Theorem 28 identifies abstract duality with orthogonal complementation. With Theorem 23 it says that the column matroid of a real matrix whose rows span and the column matroid of a matrix whose rows span have complementary bases. This is the basis of the standard representation of the dual of a represented matroid ( and ), of the cycle/cocycle duality of graphs viewed through incidence matrices, and of the fact that a matroid representable over a field has a dual representable over the same field. Theorems 20–23 are the basic facts every later treatment of matroid duality starts from: duality exchanges rank and nullity, is symmetric, always exists, and is characterized by base complements.
Formalizing it. All of these results are classical and proved in Whitney's paper; what this mission adds is a machine-checked development of Whitney's own definition of duality, the rank identity (11.1), rather than the base-complement definition used in modern libraries. Mathlib defines the dual matroid by base complements and proves that it is a matroid; it does not, at the pinned revision, contain the rank formula (11.1) for , the matroid of a real subspace, or Theorem 28. Theorem 6 is already proved on the platform and enters as a reference. Theorems 7 and 8 are close to Mathlib lemmas and are footholds rather than new content.
The difficulty of the goal is not in the combinatorics but in the passage between the two descriptions of a subspace. The natural first idea is to compare the ranks and directly by counting dimensions of and . This does not close: is the dimension of a projection of onto coordinates, while only controls as a whole, and the rank of a complementary coordinate set in is not determined by the dimensions of and alone. Some relation between coordinate projections of and the structure of on the complementary coordinates has to be established. Theorem 27 is itself nontrivial in Lean: the rank function has to be shown to satisfy the matroid axioms, which needs a careful treatment of coordinate projections and of submodularity of dimension. On the abstract side, Theorem 23 needs both directions of the passage between the rank identity and base complements, including the counting step .
Matroid α on a finite type α whose ground set is all of α (Whitney's matroid is its finite set of elements). This finiteness and the ground set convention are part of the definitions; all theorems are stated under them.eRk, finite on a finite type and converted to integers; the nullity and the identity (11.1) are computed in . No truncated subtraction appears.σ : α ≃ β (IsDualVia) or some bijection (IsDual). It is deliberately not defined as Mathlib's M✶: with that definition Theorem 23 would be nearly definitional and Theorem 28 would lose the rank identity. A formalization that replaces (11.1) by the base-complement condition, or states Theorem 28 only for bases, is not this mission's goal.EuclideanSpace ℝ (Fin n) with its standard inner product; the orthogonal hyperplane is Hᗮ. The field is , as in the paper; the analogous statement over other fields with the dot-product annihilator is a generalization and not part of this mission.IsAssociated M H): ground set Fin n, and the rank of every set of coordinates equals the finrank of the image of under the coordinate projection onto (not of , a different set function). Existence and uniqueness is Theorem 27.M✶, and supporting lemmas on coordinate projections are welcome.Mathlib.Combinatorics.Matroid (Dual, Rank). https://github.com/leanprover-community/mathlib4