Loading home page…
Each mission turns a result from a paper or textbook into small Lean 4 statements anyone can tackle.
Campaigns group missions around a shared mathematical goal. Each one tracks a quantity, such as an upper or lower bound. Have a good candidate in mind? Ping us on Slack, Zulip, or WeChat.
Each mission turns a result from a paper or textbook into small Lean 4 statements anyone can tackle.
Campaigns group missions around a shared mathematical goal. Each one tracks a quantity, such as an upper or lower bound. Have a good candidate in mind? Ping us on Slack, Zulip, or WeChat.
Classical algorithms solve all-pairs shortest paths in time. In a 2026 breakthrough, Alman and Vassilevska Williams refuted the APSP conjecture with a deterministic algorithm. How low can the exponent go?
Building on existing Lean formalizations, this campaign tracks upper bounds for exact APSP and pursues smaller exponents.
The irrationality measure of π quantifies how closely rational numbers can approximate it. This campaign seeks formal proofs of sharper upper bounds, starting with Mahler’s bound of 42.
The sharp Hlawka inequality for Schatten -norms is a cousin of the triangle inequality: it relates the norms of three matrices to the norms of their pairwise sums and their total sum. For complex diagonal matrices, an exact formula for the best possible comparison constant has been proved in Lean for every real . We conjecture that the same formula holds for all .
What is the smallest cutoff for which this formula holds for every real ?
References:
Is every odd number a sum of primes? This campaign tracks formalized proofs of the smallest that suffices.
Schnirelmann (1930) showed some finite works. Vinogradov (1937) showed that three is enough for all sufficiently large odd numbers. Tao (2012) proved unconditionally. Helfgott (2013) proved that every odd number greater than is a sum of three primes, though the proof is still unrefereed. Ideally, we can formalize this statement here. Note that three is optimal: is neither prime nor + prime.
Schoolbook matrix multiplication takes operations. The exponent is the infimum of all such that two matrices can be multiplied in arithmetic operations; trivially , and is conjectured but open.
Strassen gave the first nontrivial bound, , in 1969, and introduced the laser method in 1986 to reach . Coppersmith and Winograd's 1990 bound of stood for two decades. Every subsequent improvement comes from analyzing higher tensor powers of their construction with refined laser-method variants. That line reached in 2025, and the current record is , from August 2026. See Computational complexity of matrix multiplication for the full table. Can we formalize these results and even improve on them?
The differential geometry of curves in is the entry point of every course and every textbook in the subject, and it is the first place where a geometric object is shown to be completely determined by a small list of numerical invariants. A space curve traced out by a particle moving at unit speed bends (curvature) and twists (torsion); the assertion that these two scalar functions determine the curve completely, up to a motion of space, is the prototype of every later "fundamental theorem" of the subject — for surfaces (Bonnet), for Riemannian metrics, and for submanifolds in general.
The reference for this mission is Manfredo P. do Carmo, Differential Geometry of Curves and Surfaces, 2nd edition (Dover, 2016), Chapter 1, Sections 1-4 and 1-5. The statement targeted here is the one printed on page 19 under the heading Fundamental Theorem of the Local Theory of Curves; the uniqueness half is proved on pages 20–22, and the existence half is deferred by do Carmo to the appendix of Chapter 4, where it is obtained from the existence and uniqueness theorem for linear systems of ordinary differential equations.
This is the first mission of a series formalizing do Carmo's book. The series shares one Lean
namespace, DoCarmoDG, so that later missions on regular surfaces, the Gauss map, and
Gauss–Bonnet build on the vocabulary fixed here.
Let be an open interval and let be a smooth map. The curve is parametrized by arc length if for every ; the parameter is then the arc length measured along the curve.
For such a curve one sets
The vector is the unit tangent and the scalar is the curvature at . Differentiating gives , so is orthogonal to . At a point where one defines the normal vector and the binormal vector
where is the vector product of (do Carmo §1-4). The triple is a positively oriented orthonormal basis, the Frenet trihedron. Since has constant length and is orthogonal to , the derivative is a multiple of , and the torsion is defined by
This is do Carmo's sign convention; many authors write for the same quantity, and the mission is committed to do Carmo's. With these conventions the Frenet formulas read
A rigid motion of is a map where is an orthogonal linear map with positive determinant and (do Carmo §1-5, Exercise 6).
Given smooth functions with :
The two halves are also stated separately as milestones, since they are proved by entirely different means: uniqueness by a Gronwall-free energy argument on the Frenet trihedron, existence by solving a linear ODE system.
The orthonormality of the Frenet trihedron, the Frenet formulas themselves, the characterization of straight lines by and of plane curves by , the closed formula , and the invariance of arc length, curvature and torsion under rigid motions.
The theorem is the model case of a classification result: a geometric object modulo a symmetry group is faithfully encoded by a complete set of local invariants. Downstream it is what licenses the standard practice of "prescribing curvature and torsion" — constructing curves with specified geometric behaviour, computing with the Frenet apparatus rather than with the curve itself, and recognizing that any identity among , and their derivatives is a genuine statement about the curve and not about its parametrization. In do Carmo's own development the local canonical form (§1-6) and the global results of §1-7 both rest on the Frenet apparatus fixed here.
Mathlib contains the analytic ingredients — the Picard–Lindelöf theorem, existence and uniqueness for linear ODE systems, orthonormal bases and the orthogonal group of a real inner product space — but it does not contain the Frenet trihedron of a space curve, the torsion of a space curve, or this theorem. What this mission produces is therefore a reusable formal vocabulary for the local theory of space curves, plus machine-checked proofs of the classical statements about it. The mathematics is completely classical and has been known since Frenet (1847) and Serret (1851); what is open here is the formalization, not the mathematics.
The uniqueness half is a short argument on paper — the function has vanishing derivative by the Frenet formulas — but formally it requires first establishing that the Frenet frame is differentiable and satisfies those formulas, which needs and the smoothness of away from its zeros, and then a connectedness argument on the interval.
The existence half cannot be done by exhibiting a formula: the curve is produced by solving the linear system for the frame , checking that the solution stays orthogonal (this is where the skew-symmetry of enters), and then integrating the first row. Recovering that the resulting curve has exactly the prescribed curvature and torsion, as computed by the definitions rather than as postulated by the ODE, is the step where most of the formal work sits.
The obvious shortcut — defining torsion by the closed formula — is not taken here: the definition is the book's, , and the closed formula is a milestone to be proved.
Curves are total functions ℝ → EuclideanSpace ℝ (Fin 3) that are assumed smooth only on the
open interval Set.Ioo a b; smoothness is ContDiffOn ℝ (⊤ : ℕ∞), matching do Carmo's use of
"differentiable" to mean . Because the interval is open, the ordinary deriv agrees
with the derivative along the interval at every interior point, and all derivatives in the
statements are plain iterated deriv. Curvature, normal, binormal and torsion are defined
exactly as above; at points where the normal vector takes the junk value , so every
statement that mentions , or carries the hypothesis explicitly.
The vector product is defined componentwise on EuclideanSpace ℝ (Fin 3), and a rigid motion is
a LinearIsometryEquiv of EuclideanSpace ℝ (Fin 3) with positive determinant followed by a
translation.
Degenerate intervals are not excluded: if the interval is empty and the statements hold vacuously, which is why the goal is not formulated as a statement about a single point but as a statement about all of — no hypothesis is vacuous for , and the existence clause is a genuine construction.
Contributions welcome: the Frenet apparatus and the ODE construction are the reusable parts, and both are prerequisites for the later missions of this series.
The spectral gap of a quantum many-body Hamiltonian is the difference between the energy of its ground state and the energy of its first excited state, in the limit of infinitely many particles. Whether a given microscopic interaction produces a gapped or a gapless system decides much of the macroscopic physics: gapped systems have exponentially decaying correlations and well-defined quantum phases, gapless systems sit at critical points and can display algebraically decaying correlations. Several long-standing questions — the Haldane conjecture for antiferromagnetic spin chains, the existence of gapped topological spin liquids, and the Yang–Mills mass gap — are instances of the question "given the interaction, is the system gapped?".
Cubitt, Pérez-García and Wolf proved that this question, posed for families of two-dimensional translationally invariant nearest-neighbour spin models, admits no algorithmic answer: the spectral gap problem is undecidable (Nature 528, 207–211 (2015); full version: Forum of Mathematics, Pi 10:e14 (2022), also arXiv:1502.04573).
Timeline of the ingredients the proof rests on: Turing's undecidability of the halting problem (1936); Berger's undecidability of the domino problem (1966) and Robinson's aperiodic tile set (Inventiones 12, 177–209 (1971)); Feynman's and Kitaev's circuit-to-Hamiltonian constructions, which turn a computation into a ground state; Gottesman and Irani's translationally invariant one-dimensional Hamiltonians encoding computation (FOCS 2009); and Bitansky–Vadhan-style quantum Turing machine engineering from Bernstein and Vazirani (SIAM J. Comput. 26, 1411–1473 (1997)). The 2015 result was later sharpened to one-dimensional chains by Bausch, Cubitt, Lucia and Pérez-García (PRX 10, 031038 (2020)).
Fix a local dimension and, for each side length , the square lattice with open boundary conditions. Each site carries a copy of , so the state space of the lattice has the standard product basis indexed by assignments of a level in to each site. A model is specified by three Hermitian matrices: an on-site term of size , and two interactions of size acting on horizontally and vertically adjacent pairs. The Hamiltonian of the finite lattice is
the same three matrices being used at every edge and every site, which is what translational invariance means here. The quantity is the local interaction strength.
Write for the eigenvalues and for the finite-size gap. The family is
These two conditions are not negations of each other; the construction guarantees that every instance falls into one of them. The ground state energy density is .
For a fixed universal machine and every , one explicit family of interactions, built from fixed integer-valued matrices , a diagonal projector , a rational that may be taken arbitrarily small, and an algebraic ,
with the rational whose binary expansion after the point is the binary expansion of reversed, satisfies: the local interaction strength is at most ; if the machine halts on input the family is gapped with gap at least ; and if it does not halt the family is gapless. Since halting is undecidable, no algorithm decides gappedness, even with the promise that exactly one of the two alternatives holds and even at fixed local dimension .
The milestone list follows the numbering of the full version: Lemma 8 and Theorem 9 (reduction of halting to ground state energy and to arbitrary low-energy properties), Corollary 7 (the same undecidability for unconstrained local dimension, with rational interactions), Proposition 53 and Corollary 54 (the diverging ground state energy and its promise version), and Theorem 5 (undecidability of the ground state energy density).
The result rules out a general algorithm — and therefore any complete general method — for deciding gappedness from the interaction matrices, however much computing power is available; the property genuinely depends on arbitrarily large system sizes. It also implies, via the standard link between undecidability and independence, that there are concrete finite-dimensional models whose gap is independent of the axioms of any consistent recursively axiomatized formal system (Corollary 4 of the source), and it transfers to other low-energy properties such as the existence of algebraically decaying ground-state correlations.
The theorem is proved; none of it is formalized. This mission produces the machine-checked version. The reusable infrastructure it forces into existence is substantial on its own: a formal model of translationally invariant lattice Hamiltonians and their thermodynamic-limit spectral behaviour, the tiling layer, and computational-history-state Hamiltonians. Each milestone is a self-contained statement that can be attacked without the others.
The obvious approach — encode a halting computation as an energy penalty — gives the ground state energy of a finite lattice, not a property of the limit; this is exactly what Lemma 8 achieves, and it is not enough, because a gap is a statement about the sequence of spectra as and is insensitive to any single lattice size. The construction must make the halting information visible at all sufficiently large sizes at once while a fixed finite local dimension carries every instance . That forces three separate difficulties: an aperiodic (Robinson) tiling to create squares of every size inside one translationally invariant model; a quantum phase-estimation Turing machine whose transition amplitudes encode in a single phase , so that the instance index does not inflate the local dimension; and a history-state Hamiltonian whose low-energy spectrum can be controlled well enough that a positive energy density in the halting case turns into a genuine spectral gap, and a vanishing one into a dense spectrum above the ground state.
The development commits to the following conventions, all of which are visible in the definition items of this mission.
Degenerate readings are excluded: a zero local dimension satisfies none of the statements, since a non-degenerate ground state requires a one-dimensional eigenspace and the gapless condition requires a non-empty spectrum; and every existential statement fixes the matrices before quantifying over all instances and all lattice sizes .
Contributions are welcome at any milestone, and also on the infrastructure the milestones need — Wang tilings and the Robinson tile set, Gottesman–Irani history-state Hamiltonians, and quantum Turing machines in the Bernstein–Vazirani sense — which are needed for Theorem 6 and Lemma 47 of the source and are not yet part of this mission's item list.
Quantizing a Yang–Mills theory by the Faddeev–Popov procedure requires a gauge condition that picks one representative from each gauge orbit. In the Landau gauge the condition is . Gribov showed in 1978 that this condition is not ideal: a gauge orbit can meet the surface more than once, so gauge-equivalent configurations — Gribov copies — are still being integrated over (V. N. Gribov, Quantization of non-Abelian gauge theories, Nucl. Phys. B139 (1978) 1). Infinitesimally, a copy of a transverse field corresponds to a zero mode of the Faddeev–Popov operator , which is Hermitian on transverse configurations.
Gribov's proposed remedy is to restrict the functional integral to the Gribov region , the set of transverse configurations at which is positive definite. The interest of is not only that it removes infinitesimal copies: the fact that it is a bounded region of field space is the geometric input of Gribov's confinement scenario, because restricting the integration to a bounded region deforms the gluon propagator in the infrared and produces a mass scale. Whether the restriction to is the physically correct prescription is still debated; the geometric properties of themselves are not — they are consequences of the algebraic structure of , and they are what this mission formalizes.
Timeline of the properties at issue, as recorded in §2.2.1 (pp. 188–189) of the review by N. Vandersickel and D. Zwanziger, The Gribov problem and QCD dynamics, Phys. Rep. 520 (2012) 175–251 (doi:10.1016/j.physrep.2012.07.003):
Fix a real vector space of gauge-field configurations (in the physical situation, the transverse fields ) and a finite index set on which the Faddeev–Popov operator acts (colour index times a finite basis of fluctuation modes ). The formalization works with the algebraic structure that the Faddeev–Popov operator has, and nothing else:
where
The Gribov region is
This is Eq. (2.52) of the review, with positivity as in Eq. (2.54). The boundary is the first Gribov horizon, where the lowest non-trivial eigenvalue of vanishes.
The last two clauses are stated under the assumption that is injective, i.e. that distinct configurations give distinct field-dependent parts; without it contains the whole kernel of as a linear subspace and no boundedness statement can hold.
These are Eq. (2.53) and Eq. (2.58) of the review; they are the two ingredients from which convexity and directional boundedness follow.
What the result gives: is the region to which Gribov's improved gauge fixing restricts the functional integral, and every subsequent construction in this line of work — the no-pole condition, the horizon function and the local Gribov–Zwanziger action — presupposes that the restriction is to a bounded convex region containing the perturbative point . Convexity is what makes the horizon condition a single well-posed constraint; boundedness in every direction is the property from which the infrared suppression of the gluon propagator, and hence Gribov's mass scale, is read off. Without boundedness there is no geometric mechanism for a mass gap in this scenario.
Status honesty: these statements are proved mathematics, not open problems; the arguments in §2.2.1 of the review are short. What is missing is a machine-checked account. No formalization of the Gribov region in Lean is known to the drafter of this proposal; the platform's existing Gribov material concerns Singer's topological obstruction to continuous gauge fixing, which is a different theorem about a different object.
The statements are elementary once the correct hypotheses are isolated, and the mission is calibrated accordingly: it is a faithfulness exercise rather than a depth exercise. The two places where a naive attempt fails are worth naming. First, directional boundedness does not follow from positivity alone: it needs the tracelessness of , which is what forces a direction with ; a positive semidefinite perturbation would give a region unbounded along that ray. Second, "bounded in every direction" does not imply "bounded" for a general set, and the implication used here rests on convexity together with injectivity of — the argument goes through a limit of rescaled configurations and a closure of the positivity condition, not through a uniform bound extracted directly from the ray statement.
The mission commits to a finite-dimensional linear-algebra model of the Faddeev–Popov operator, packaged as a structure carrying: the matrix together with a proof that it is positive definite; the linear map together with proofs that each is symmetric and traceless. Configurations live in an arbitrary real vector space , which carries a norm and finite-dimensionality only in the two statements where boundedness is asserted. Positive definiteness is Mathlib's notion for real matrices, which includes symmetry; the region is the set of configurations where it holds strictly, so is the open region and the horizon is not part of it.
This is a model, not the field-theoretic object: it replaces the operator acting on transverse fields by its finite-dimensional algebraic shadow, and the reviewer should audit it as such. The properties targeted here are exactly those whose proofs in §2.2.1 use only linearity in , symmetry, tracelessness, and positivity of ; results that genuinely need the infinite-dimensional setting — that every gauge orbit passes inside , and that still contains copies on its boundary — are deliberately out of scope, since they cannot be stated in this model.
The model is not vacuous: an instance exists already for , , and , with injective, so none of the statements is satisfied vacuously. Nor is any target trivially true: is a proper nonempty subset of in that instance.
Infrastructure needed: Mathlib's positive-definiteness API for matrices, the spectral theorem for real symmetric matrices (for the traceless lemma), and basic convexity and boundedness in finite-dimensional normed spaces. The traceless lemma — a nonzero symmetric traceless matrix has a direction of negative quadratic form — is reusable well beyond this mission. Contributions extending the model towards the infinite-dimensional setting, or supplying the explicit ellipsoidal bound of Dell'Antonio–Zwanziger in place of plain boundedness, are welcome.
The Riemann hypothesis asserts that all nontrivial zeros of the Riemann zeta function lie on the critical line. A classical way to measure how far the hypothesis is from failing runs through a one-parameter deformation of the Riemann function by the backward heat flow. De Bruijn (1950) introduced a family of entire functions , , with essentially the function, and showed that has only real zeros for . Newman (1976) proved that there is a finite constant , now called the de Bruijn–Newman constant, such that has only real zeros precisely when . The Riemann hypothesis is exactly the statement , and Newman conjectured the complementary bound — in his phrase, that if the Riemann hypothesis is true, then it is only barely so.
Timeline of lower bounds on , all obtained before 2018 by exhibiting Lehmer pairs, that is, pairs of adjacent zeros of that are unusually close together: (Newman 1976), (Csordas–Norfolk–Varga 1988), (te Riele 1991), (Norfolk–Ruttan–Varga 1992), (Csordas–Ruttan–Varga 1991), (Csordas–Smith–Varga 1994), (Csordas–Odlyzko–Smith–Varga 1993), (Odlyzko 2000), (Saouter–Gourdon–Demichel 2011). Rodgers and Tao closed the gap in 2020 by proving . In the other direction, de Bruijn's bound was sharpened to by Ki–Kim–Lee (2009) and to by the Polymath 15 project (2019).
For a real number put
a function that decays super-exponentially as and satisfies . For each define the entire function
Each is even and satisfies ; the function is , so the Riemann hypothesis says exactly that every zero of is real. Write
By Pólya and Newman, is the ray with .
When the zeros of are real, simple, symmetric about the origin and avoid the origin, so they can be listed as , indexed by the nonzero integers, with and . The classical locations are defined for by with
extended by ; they are the positions the zeros would occupy if the Riemann–von Mangoldt counting formula were exact. Throughout, .
The goal is stated in both forms simultaneously, so that it does not depend on any convention for the infimum of a set that might be empty or unbounded below.
The milestone list follows the architecture of Rodgers–Tao, which is a proof by contradiction: every milestone is stated under the standing hypothesis of that paper, in the time ranges the paper uses (, then , then ). In order: an upper bound for near the real axis (Lemma 4); Riemann–von Mangoldt type counting formulae for the zeros of (Theorem 9); the resulting macroscopic description of the zeros (Corollary 10); the equations of motion (Theorem 11); a quantitative lower bound on gaps between zeros (Proposition 13); a bound on the time-integrated renormalized energy (Theorem 17); and a bound on that energy at time (Proposition 26). The last of these says that at time zero the zeros are, on average, locally in the equilibrium configuration of an arithmetic progression, which contradicts known results on the local distribution of zeros of .
settles Newman's conjecture, and together with the Riemann hypothesis it would force . Unconditionally, it says that the zeros of are not in local equilibrium: infinitely often, gaps between consecutive zeros deviate from the mean spacing, which is what makes the pair correlation phenomenology of Montgomery and of Conrey–Ghosh–Goldston–Gonek–Heath-Brown incompatible with . Any proof of the Riemann hypothesis must therefore be compatible with the hypothesis being tight in this sense.
The theorem has a complete published proof (Rodgers–Tao, Forum of Mathematics, Pi, 2020); it is not an open problem. What is missing is a machine-checked proof. To the extent the material has been formalized at all, the underlying objects — the function, the heat flow , the counting function for zeros, the zero dynamics, the renormalized energies — are not available in Mathlib, so the mission produces reusable analytic infrastructure: bounds for a Fourier–Laplace type integral by the saddle point method, a Riemann–von Mangoldt counting argument via the argument principle, and a gradient-flow monotonicity framework for an infinite particle system with logarithmic interaction.
The obvious route to is the one used for every previous lower bound: exhibit Lehmer pairs of ever higher quality, since if were very negative the zeros of would repel each other and unusually close pairs of zeta zeros could not exist. Producing an infinite sequence of Lehmer pairs of arbitrarily high quality is possible under the GUE hypothesis, but the known unconditional upper bounds for small gaps between zeta zeros are too weak, even assuming the Riemann hypothesis. The proof instead upgrades repulsion to relaxation to local equilibrium: it must control the zeros of uniformly for at length scales as fine as , with only the weaker counting formulae available for negative (an error term rather than ), and must make sense of a Hamiltonian and an energy that are given by divergent series, which requires truncation, renormalization, and careful control of all the resulting boundary terms.
The Lean development commits to the following conventions. is a tsum over the positive integers and is the Bochner integral over of ; no convergence or entireness statement is built into the definition. is sInf of the set of admissible times, and the goal theorem also states the quantifier form "every admissible is nonnegative", so it cannot be satisfied by a junk value of the infimum. The zero families and the classical locations are not defined by choice functions: they enter the milestones as universally quantified functions subject to explicit predicates saying exactly which sequences they are, so a milestone asserts something about every valid enumeration. Asymptotic notation is unfolded: becomes an explicit existential constant, an explicit – statement, and a principal value sum a limit of symmetric partial sums. Where a statement asserts the value of a time integral, absolute integrability is part of the conclusion, so the statement cannot be satisfied by the convention that a non-integrable function has integral zero.
One degeneracy is inherent to the source and is stated here explicitly: since the paper argues by contradiction, each milestone carries the hypothesis (directly, or through a time range such as ). Once the goal theorem is proved, those hypotheses are unsatisfiable and the milestones become vacuously true. They are the intended attack path on the goal, not independent targets, and a solver who derives one of them from the goal theorem contributes nothing.
Contributions welcome: the analytic estimates for (Lemma 4) and the counting formulae (Theorem 9) are independent of the dynamical part and are the natural entry points; Mathlib-level infrastructure on the argument principle, the saddle point method, and Stirling asymptotics for in vertical strips is reusable well beyond this mission.
When money is off the table and the Gibbard–Satterthwaite theorem (Mission III of this series) blocks general strategyproof choice, restricted preference domains reopen the door. The two great examples both come from allocation: Shapley–Scarf's housing market (1974), where Gale's Top Trading Cycle algorithm finds the unique core allocation and Roth (1982) showed the mechanism is strategy-proof; and the Gale–Shapley marriage market (1962), where deferred acceptance produces a stable matching, the men-optimal one, which Dubins–Freedman (1981) and Roth (1982) showed cannot be manipulated by any man. This machinery runs the US medical residency match and school choice systems worldwide, and the 2012 Nobel memorial prize to Roth and Shapley cites exactly the results of this mission. Chapter 10 (Schummer–Vohra, "Mechanism Design without Money") of Nisan–Roughgarden–Tardos–Vazirani (eds.), Algorithmic Game Theory (Cambridge, 2007) is the source text; its single-peaked §10.2 is left to a possible later mission, since it needs its own preference-domain machinery.
Marriage market (§10.4): finite sets of men and of women, each agent holding a strict preference ordering over the opposite side (the preference-profile vocabulary of Mission III; reads " strictly prefers to "). Following the book's dummy-partner convention, and a matching is a bijection . A pair blocks if each prefers the other to their assigned partner; is stable if no pair blocks it. A stable is male-optimal if every man weakly prefers it to every stable alternative. A coalition dominates if it can rematch within itself with every member strictly better off; the core is the set of undominated matchings.
Housing market (§10.3): a finite set of agents, agent owning house , each with a strict preference over all houses; an allocation is a permutation of . A coalition blocks an allocation if it can redistribute the houses its members own so that all are weakly and someone strictly better off.
Any mechanism selecting the male-optimal stable matching is strategy-proof for the men: no man can misreport his ordering and obtain a wife he truly prefers.
Every marriage market has a stable matching.
Some stable matching is weakly best for every man simultaneously. This man-by-man form is Gale–Shapley's optimal assignment (1962, Theorem 2); the book's Theorem 10.11 phrases male-optimality as the absence of a stable alternative making every man weakly and some man strictly better off, which is equivalent for finite strict markets — the equivalence being a (short) theorem, the attribution follows Gale–Shapley.
A matching is stable iff it is in the core of the matching game.
The core of the housing market is a single allocation, and the mechanism selecting it is strategy-proof.
These are the foundational theorems of market design — the branch of mechanism design with the strongest record of deployed systems — and none of them exists in Lean. The mission also settles a methodological point for the series: algorithm-defined objects (deferred acceptance, top trading cycles) enter through the properties that characterize their outputs — male-optimality, core membership — so the theorems are statements about all mechanisms with the given property, and any construction of the algorithm proves the existence milestones. The matching vocabulary (bijections as matchings, blocking, stability, domination) is reusable for the college-admissions and roommates variants beyond this mission.
Existence (10.10) is the real formalization work: whether by formalizing deferred acceptance and its termination or by another route (e.g. Adachi's fixed-point formulation, which the book sketches as Theorem 10.14 via Tarski), the solver must build the proposal machinery. Male-optimality (10.11) rides on the same construction with the "no man is ever rejected by an achievable wife" invariant. The core equivalence (10.12) is deliberately light — a transposition embeds a blocking pair as a two-agent coalition. Housing uniqueness (10.6) needs the cycle-peeling induction of TTC. The two strategyproofness results are the subtle ones: both known proof routes (Dubins–Freedman's combinatorial argument, or Roth's via the blocking lemma) require careful bookkeeping of which coalitions can improve under a misreport, and the mechanism is pinned only by its defining property, so proofs must use optimality/core facts rather than algorithm internals.
Preferences are strict total orders as in Mission III (IsPrefProfile), oriented "first argument preferred". Matchings are Equivs; the book's convention enters the existence statements as the hypothesis Nonempty (M ≃ W) and nothing else about cardinalities is assumed. Domination and house-blocking quantify a rematching Equiv together with the improving coalition, coalitions being sets closed under the rematching — single-agent and pair coalitions are special cases, so no separate pair-blocking clause is needed in the core theorems. Mechanisms in the strategyproofness results are arbitrary functions constrained only by their defining property (male-optimal selection; core selection), quantified before the misreport — nothing may be chosen with hindsight. Both sides keep finiteness only where used: the core equivalence (10.12) holds for arbitrary types and carries no Fintype.
Mission III of this series ends at an impossibility: without money, incentive compatibility over three or more alternatives means dictatorship. This mission formalizes the classical escape route — quasilinear utilities and payments — and the exact price of it. Vickrey (1961) discovered that a second-price auction makes truth-telling dominant; Clarke (1971) and Groves (1973) generalized the idea to arbitrary social choice: welfare-maximizing rules can always be made truthful by the right payments. The converse program — which choice rules are implementable at all — runs through Rochet (1987) and Myerson (1981) to Saks–Yu (2005): weak monotonicity characterizes implementability on convex domains, and on single-parameter domains the characterization is complete and elementary — monotone rules with critical-value payments. Chapter 9, §§9.3 and 9.5 of Nisan–Roughgarden–Tardos–Vazirani (eds.), Algorithmic Game Theory (Cambridge, 2007), written by Nisan, is the source text.
A set of alternatives and a finite set of players. Player holds a private valuation from a publicly known domain ; utilities are quasilinear: choosing and charging gives utility . A (direct revelation) mechanism is a social choice function from valuation profiles to together with payment functions (Definition 9.14). The mechanism is incentive compatible if no unilateral misreport from the domain ever beats the truth (Definition 9.15).
A VCG mechanism (Definition 9.16) has maximizing social welfare and payments of the Groves form ; the Clarke pivot rule takes . A rule is weakly monotone (Definition 9.28) if a unilateral change of valuation that moves the outcome from to satisfies . A single-parameter domain (Definition 9.33) is given by a win set per player and bids : the valuation is on and elsewhere.
A normalized mechanism (losers pay 0) on a single-parameter domain is incentive compatible iff the rule is monotone and every winning bid pays the critical value — the threshold below which the bid loses.
Every VCG mechanism is incentive compatible.
With Clarke pivot payments, a welfare-maximizing rule makes no positive transfers, and is individually rational when valuations are nonnegative.
Necessity: incentive compatibility forces WMON, on any domain. Sufficiency: on convex domains, WMON rules admit implementing payments (Saks–Yu).
These are the working theorems of every later mechanism-design mission: the approximation mechanisms of Chapter 12, the profit-maximization results of Chapter 13, and the sponsored-search analysis of Chapter 28 all argue through Theorem 9.36's monotonicity-plus-critical-value normal form, and VCG is the benchmark they approximate. Formalizing the cluster produces the platform's quasilinear-mechanism vocabulary — domains, truthfulness, Groves payments, weak monotonicity, single-parameter settings — on top of the social-choice layer of Mission III.
The capstone and Theorem 9.17 are textbook results with complete proofs in the source; the Saks–Yu half of Theorem 9.29 is stated but not proved in the book ("quite involved"), so that milestone carries a genuinely hard formalization with a published paper proof. None have prior Lean formalizations.
Theorem 9.17 is a three-line inequality chase once the Groves form is unfolded — a deliberate warm-up. Lemma 9.20 adds the attained maximum over a finite alternative set. The necessity half of 9.29 is a two-application argument; the sufficiency half is the hard point of the mission: the known proofs walk two-cycle inequalities into a path-integral construction of payments on a convex domain, and nothing of the kind exists in Mathlib. For the capstone, the delicate part is the critical value: the book defines it as a supremum that "is undefined" when the player always wins, and the honest formal rendering — a constant payment c that is a least upper bound of the losing bids whenever losing bids exist — makes the case split explicit; the equivalence proof must thread monotonicity, the threshold structure of the winning set, and normalization through both directions.
Valuations are functions A → ℝ; domains are sets V i : Set (A → ℝ); mechanisms are total functions with every property quantified only over profiles from the domain, so behavior on invalid inputs carries no content. The Groves term hᵢ is a function of the full profile constrained to be invariant under changes of coordinate i — the standard rendering of "depends only on ". The Clarke payment uses a Finset.sup' over a finite nonempty A, so no junk supremum arises. In the single-parameter setting the valuation induced by a bid is Set.indicator, bids live in Set.Icc t0 t1 with t0 ≤ t1, and the critical value is characterized by IsLUB guarded by nonemptiness of the losing set — the book's "undefined" caveat made precise without a junk sSup. Weak monotonicity's sufficiency half carries Convex ℝ (V i) and finite A (the Saks–Yu setting); the necessity half deliberately carries no hypotheses beyond incentive compatibility itself.
Chapter 6 of Walter Rudin's Principles of Mathematical Analysis (3rd edition, McGraw-Hill, 1976) constructs the Riemann–Stieltjes integral : the Riemann integral with the increments of the variable replaced by the increments of a monotonically increasing integrator . Taking recovers the ordinary Riemann integral; taking a step function turns integrals into sums, so series and integrals become special cases of one construction. This is the reason Rudin develops the theory in this generality: it unifies Chapter 3's series with the integral, and it is the natural setting for the Fourier coefficients of Chapter 8.
The chapter's capstone is the fundamental theorem of calculus (Theorem 6.21): an integrable function which is the derivative of some integrates to .
This mission is the sixth in a series formalizing Rudin Chapters 1–11; it uses the uniform continuity of Mission IV and the mean value theorem of Mission V.
A partition of is a finite set of points , with increments for a monotonically increasing . For a bounded real put , , and
The upper and lower integrals are and ; is integrable with respect to , written , when they agree, and the common value is . refines when every division point of is one of . Writing for with gives the Riemann integral .
The fundamental theorem is what makes the integral computable: it reduces integration to antidifferentiation and so links Chapters 5 and 6. Theorem 6.20 is its companion — it says the integral of a continuous function is an antiderivative — and together they show the two operations are mutually inverse to the extent that the hypotheses allow. Theorem 6.17 explains when a Stieltjes integral collapses to a Riemann integral with the density , and it is the computational tool for integrators that are differentiable; the step-function case at the other extreme (Rudin's 6.15–6.16) is what turns sums into integrals.
Mathlib has no Riemann–Stieltjes integral: it has the Bochner integral, the interval integral, and a Lebesgue–Stieltjes measure, but the upper-and-lower-sum construction of Chapter 6 is absent. This mission therefore builds the object from Rudin's definitions and develops its basic theory; that development is reusable beyond this mission — Chapter 7's interchange theorem (7.16) and Chapter 8's Fourier coefficients are stated with respect to it.
Two obstacles are specific to formalizing this chapter. First, the upper and lower integrals are an infimum and a supremum over the set of all partitions, which is not a lattice-friendly index; every comparison between partitions goes through the common refinement, and Theorem 6.4 is the workhorse that makes such comparisons possible. Second, the fundamental theorem is proved by choosing a partition on which and applying the mean value theorem on each subinterval, so the proof requires selecting an intermediate point per subinterval — a finite choice that is easy on paper and must be organized explicitly in Lean.
The integrator is only assumed monotone, so it may be discontinuous, and the theory must not assume otherwise: Theorem 6.9 needs continuity of precisely because it is not available in general.
Conventions fixed by this mission:
[a, b] is Rudin.Partition a b: the number n of subintervals together with
a monotone placement function x with x 0 = a and x n = b. Rudin allows
, and so does this structure.Rudin.upperSum, Rudin.lowerSum, Rudin.upperIntegral, Rudin.lowerIntegral,
Rudin.RSIntegrable, Rudin.RSIntegral follow Definitions 6.1–6.2 literally, with sSup and
sInf over the images .sSup/sInf on ℝ return 0 on unbounded sets, every statement carries Rudin's
boundedness hypothesis for explicitly; likewise monotonicity of is assumed as
MonotoneOn α (Set.Icc a b) rather than built into a type.Rudin.RiemannIntegrable and Rudin.RiemannIntegral are the case , in
which the goal theorem and Theorems 6.20–6.22 are stated, matching Rudin.HasDerivAt, so F' = f is stated pointwise on [a, b] with the value f x
supplied, as in Rudin's hypothesis.The goal is not vacuous, and not a restatement of a library lemma: the integral in it is the one defined in this mission, so a solution must connect the upper/lower sum construction to differentiation rather than quoting Mathlib's interval integral.
Infinite-horizon dynamic programming is the mathematical core of Markov decision processes and reinforcement learning: Bellman equations, value iteration, policy iteration, and their guarantees. Chapter 7 of Bertsekas, Dynamic Programming and Optimal Control, Vol. I (3rd ed., 2005) develops the finite-state theory in its cleanest generality — stochastic shortest path (SSP) problems first (Prop. 7.2.1–7.2.2), with discounted problems (Prop. 7.3.1) and average-cost problems (Prop. 7.4.1–7.4.2) derived from the SSP analysis. These propositions are cited throughout the MDP/RL literature as the base case of the theory; none of them exists in Mathlib.
States plus an implicit cost-free absorbing termination state ; finite nonempty control sets ; costs ; sub-stochastic transitions , , the deficit being the termination probability (BertsekasSSPModel). Operators
(BertsekasSSPPolicyOp, BertsekasSSPBellmanOp), -stage costs by backward recursion with policy shift (BertsekasSSPNCost), and the survival mass (BertsekasSSPSurvival). Assumption 7.2.1: for some , every admissible policy has survival mass from every state after stages. The discounted setting reuses the same model with stochastic rows and (BertsekasDiscounted*); the average-cost setting adds a designated state with the avoidance probability of Assumption 7.4.1 (BertsekasSSPAvoidProb).
Under Assumption 7.2.1, there is a vector with
and a stationary policy attaining — BertsekasDP.ssp_main_theorem (goal, Prop. 7.2.1(a),(b)). Milestones: 7.2.1(c) policy evaluation, 7.2.1(d) optimality iff greediness, 7.2.2 policy iteration, 7.3.1 the full discounted counterpart, 7.4.1 the average-cost Bellman equation, 7.4.2 average-cost policy iteration.
These are the convergence guarantees behind value iteration and policy iteration — the two algorithms at the root of dynamic programming practice and of RL analyses (Q-learning's target operator is exactly ). The SSP form is the strongest of the three: the discounted theory is its special case (termination with probability per stage) and the average-cost theory reduces to it through cycles at the recurrent state. Formalized, the chapter yields a reusable finite-MDP theory: monotone operators, -stage contractions, and the machinery for later Vol. II material. All results are proved in the book; the formalization is new.
is not a one-stage contraction in the sup-norm under Assumption 7.2.1 — only an -stage contraction, uniformly over the finitely many -stage policy prefixes; extracting the uniform contraction factor (via finiteness of the policy space) is the crux of the whole chapter. The limit of -stage costs for nonstationary policies must be established, not assumed (tail-sum estimate ). For the average-cost results the associated-SSP construction (stop on reaching ) must be built inside the proof. The liminf phrasing of average-cost optimality is deliberate: for arbitrary nonstationary policies the Cesàro limit need not exist.
Finite states Fin n, finite control type, constraint sets as Finsets with attained minima; no termination state in the carrier — termination is the sub-stochastic deficit, exactly as the book treats it computationally. Policies are sequences of stage policies (Markov); costs of nonstationary policies via the shift recursion. Convergence is Tendsto in the product topology (equivalently sup-norm, finite). Average cost uses real liminf and division with the term junk-valued at 0 (irrelevant at infinity). The discounted theorem packages parts (a)–(e) in one statement mirroring Prop. 7.3.1.
Invertible modules over a commutative semiring are Zariski-locally free, so local semirings have trivial Picard group. The source asks whether the ring-theoretic semilocal conclusion survives without subtraction: must every invertible module over a semiring with finitely many maximal ideals be free? If not, is the conclusion at least true for finite semirings?
This mission turns CUHK-Shenzhen AI Math Problem 19, Picard groups of semi-local or finite semirings, into an auditable Lean campaign. The objective is not merely to transcribe notation: it is to expose the mathematical model, the capstone, and a smaller attack surface as separate artifacts that other formalizers can inspect and reuse.
The main theorem asserts freeness for every invertible module over a commutative semiring with finite maximal spectrum. A separate milestone states the finite-semiring fallback. Both are positive formulations; a concrete counterexample to either resolves that target negatively and should motivate a corrected classification.
Solving this target would settle the precise finite or analytic core represented by the Lean statement and would create reusable infrastructure in semirings, Picard groups, invertible modules, finite semirings. Even a rigorous disproof is valuable: several entries in this collection deliberately ask whether an attractive extrapolation is true, and Lean forces a counterexample to satisfy every side condition. The mission therefore treats theorem proving and model criticism as equally legitimate research outcomes.
Ring proofs use subtraction-sensitive k-ideal properties and decompositions into local factors that can fail for semirings. Finite indecomposable semirings need not be local and may have positive Krull dimension. Invertible modules are projective with strong duality, but familiar rank and determinant arguments may not survive additive noncancellation.
Formalize the known local-freeness proof from the evaluation isomorphism and study patching over finitely many principal opens. Identify exactly where partitions of unity require k-ideals. For finite semirings, enumerate idempotent matrices representing projective modules, impose the invertibility constraints, and seek either a reduction to principal rank-one modules or a minimal counterexample. Product decompositions and faithful-action lemmas should be reusable.
The Lean targets use Mathlib's commutative semiring, maximal spectrum, module, invertible-module, and free-module notions. 'Semilocal' is encoded only as finiteness of MaximalSpectrum; no unproved decomposition theorem is assumed. The finite fallback assumes the underlying semiring type is finite but does not assume the module itself finite separately. Cardinality-only variants from the source are not the capstone.
The natural-language source remains authoritative for motivation, while the Lean declaration is authoritative for what Prove2Me will verify. The mission description calls out restrictions where the current formal target is a finite-dimensional core, a fixed interpretation of informal terminology, or one sharpened subquestion from a broader classification problem. Those restrictions should not be silently generalized in a proof claim.
Resolve the finite-semiring statement, computationally or structurally, while developing the local-to-semilocal patching lemmas needed by the main theorem.
The capstone is marked as the mission's main item and is never duplicated as a milestone. Definitions precede theorem statements in the proposal order. A milestone is considered complete only when its own exact statement is proved; proving a nearby theorem with stronger-looking prose but mismatched quantifiers, signs, supports, dimensions, or asymptotic constants does not complete it.
The CUHK-Shenzhen AI Math Problems page added this problem on June 24, 2026. At the drafting date, August 31, 2026, the status and target corrections described above were checked against the source page and the cited primary material.
A contribution may prove the displayed theorem or refute it by constructing data satisfying every Lean hypothesis while negating the conclusion. Informal changes of model do not count: any proposed correction must be submitted as a separately reviewed statement with an explanation of which source ambiguity or false implication it repairs. Definitions must remain computational or mathematically constrained; fields that simply assume the desired conclusion are not acceptable. Every proof must compile against the mission's pinned Mathlib revision, use no sorry, and expose a top-level theorem solution when submitted to Prove2Me.
The main theorem is intentionally separated from a smaller milestone. Contributors should preserve that dependency order, publish reusable lemmas rather than monolithic tactics, and report whether a lemma is analytic, algebraic, combinatorial, or infrastructure-only. Numerical evidence, external computer algebra, and exhaustive search are welcome for discovery, but a final certificate must be replayable by Lean. If an external result is invoked, its hypotheses must be represented in the formal statement or proved in the dependency tree.
The files were built locally with Lean 4.30.0 and Mathlib revision c5ea00351c28e24afc9f0f84379aa41082b1188f, the supported Prove2Me environment at drafting time. The mission definition file is ordered before all theorem files, and each theorem imports exactly that public definition module or Mathlib. Independent blind read-backs accompany the draft items so reviewers can compare what the Lean code literally says with this mathematical description. Human confirmation remains required before the public proposal can be submitted for moderation.
Linear approximation is only one instance of distance minimization. Feasible sets in optimization are typically convex rather than subspaces, so a useful certificate must compare a target point with an entire convex set and must allow an affine offset. Chapter 5 of Luenberger's Optimization by Vector Space Methods builds this certificate through geometric forms of the Hahn--Banach theorem, supporting hyperplanes, and separation of convex sets. The resulting minimum-distance theorem expresses the distance from a point to a convex set as an optimal gap measured by a norm-bounded continuous linear functional (Luenberger, §§5.12--5.13, pp. 130--137).
This mission advances the series from subspace annihilators to affine separation. It formalizes the Minkowski gauge used by the chapter, three progressively stronger separation statements, and a capstone distance-duality certificate. These results are standard infrastructure for constrained optimization: they turn a geometric exclusion or distance into a scalar inequality that can later become a multiplier or a dual bound.
Let be a real normed space and a nonempty convex set. Convexity is represented by Convex ℝ K, and topological interior, closure, and infimum distance use Mathlib's interior, closure, and Metric.infDist. A continuous affine separator is described by a continuous linear functional and a scalar level . The inequality for all places in one closed half-space.
When a convex set contains zero in its interior, its Minkowski gauge is the functional gauge K. The source characterizes it by nonnegativity, positive homogeneity, subadditivity, continuity, and the level sets
These properties are bundled into the first milestone, following Lemma 1 of §5.12 (pp. 131--132).
For two convex sets , Eidelheit separation means finding nonzero and with for and . The source assumes that has nonempty interior and that its interior does not meet . The Lean statement records the nonemptiness of explicitly, since otherwise nonzero separation is not forced.
Formalize the six gauge properties above. Then, for a convex with nonempty interior and an affine subspace disjoint from that interior, produce and such that
This is Mazur's geometric Hahn--Banach theorem as stated in §5.12, Theorem 1 (p. 133).
For , formalize a nonzero functional satisfying for all . Next formalize Eidelheit separation:
These are Theorems 2 and 3 of §5.12 (pp. 133--134).
Let have positive distance from . Produce and a real upper-bound level with , on , and
Every other feasible pair must satisfy . If realizes the distance, require to align with . This is the finite real certificate form of §5.13, Theorem 1 (pp. 136--137).
The capstone is an exact strong-duality statement for distance to a convex set. A feasible pair yields a certified lower bound on the distance, and the distinguished pair reaches the primal value. Unlike a nearest-point characterization, it remains meaningful when is not closed and no minimizing point exists. The conditional alignment clause identifies the equality case when attainment is available.
Formalizing the chapter's progression creates more than one isolated equality. The gauge package links convex geometry to sublinear analysis; Mazur separation handles affine constraints; the supporting-hyperplane and Eidelheit statements provide reusable interfaces for later multiplier rules. The results are known and proved in the 1969 text; the mission's contribution is a coherent machine-checked Lean layer that preserves the source hypotheses and can support later chapters on duality and optimization.
A direct reuse of subspace distance duality is insufficient because a general convex set is neither closed under subtraction nor described by an annihilator. An affine level is unavoidable. The common shorthand introduces a second problem: need not be bounded, so a real-valued supremum is not available for an arbitrary functional. The capstone therefore quantifies over a real upper bound and asserts its optimality through a universal inequality; this records the same finite support value without imposing boundedness absent from the source.
Topological hypotheses also differ across the milestones. Separation uses nonempty interior, whereas the final distance theorem only assumes convexity, nonemptiness, and positive distance. Replacing positive distance by mere exclusion would be invalid for a nonclosed set. Similarly, requiring closure or compactness would make formalization easier but would lose the theorem's intended infinite-dimensional scope.
The mission is restricted to real normed spaces. Sets use Set X; affine varieties use AffineSubspace ℝ X; separators use ContinuousLinearMap. The gauge is Mathlib's existing gauge, so no competing definition is introduced. The bundled gauge milestone deliberately includes both level-set identities as well as continuity, positive homogeneity for positive real scalars, subadditivity, and nonnegativity.
The Eidelheit theorem includes K₂.Nonempty, an assumption used implicitly by the source's separating conclusion. The capstone includes K.Nonempty and 0 < Metric.infDist x₁ K; it does not assume closedness, boundedness, compactness, or attainment. Its pair represents a finite support level, and the universal comparison over all feasible rules out a weakened statement in which an arbitrarily loose upper bound could trivialize existence. The optional nearest-point clause uses the exact equality and fixes the sign of alignment. Contributions may add reusable lemmas on gauges, interiors, affine subspaces, or support bounds, but the public results should remain independent of finite-dimensionality and completeness.
Many convex programs impose inequalities valued in a vector space: componentwise inequalities, positive-semidefinite constraints, and families of ordered resource constraints are all instances of one cone order. Chapter 8 of David G. Luenberger's Optimization by Vector Space Methods develops a global theory for this setting. A perturbation of the constraint produces a convex value function, continuous linear functionals positive on the ordering cone become Lagrange multipliers, and a strict-feasibility condition yields an attained dual optimum. This mission formalizes the progression in §§8.2–8.6, culminating in the book's Lagrange Duality Theorem.
Let and be real normed spaces, let be a nonempty convex set, and let be a convex cone. The cone induces the relation
A continuous linear functional is dual-positive when for every . A map is cone-convex on when its value at a convex combination is below the corresponding convex combination of its values in this cone order. The primal program is
where is real-valued and convex on .
For a multiplier , the Lagrangian and its possibly infinite dual value are
The perturbed primal value replaces the zero right-hand side by . Lean represents and in EReal, so infeasible perturbations have value and objectives unbounded below can have value without arbitrary defaults.
Assume has nonempty interior, the primal value is finite, and there is a strictly feasible point with
Prove that a dual-positive exists and attains
If attains the primal infimum, also prove complementarity and that minimizes over .
Five source milestones delimit the reusable theory. A closed convex cone is recovered from all dual-positive inequalities (§8.2, Proposition 1). The finite-height epigraph of the extended perturbation value is convex, and that value is antitone in the cone order (§8.3, Propositions 1–2). A Lagrangian saddle point is sufficient for primal feasibility and optimality when the cone is closed (§8.4, Theorem 2). Finally, multipliers for two perturbed right-hand sides bound the change in optimal objective value from both sides (§8.5, Theorem 1). The root then states §8.6, Theorem 1 rather than duplicating the equivalent multiplier theorem from §8.3.
The capstone provides both equality of optimal values and an attained multiplier. It applies to a single vector inequality, so finite systems of scalar inequalities and matrix-cone constraints fit the same statement once their ordering cones are supplied. Complementarity and Lagrangian minimization turn a primal optimizer and multiplier into a certificate. The sensitivity milestone additionally gives quantitative information about how the optimum changes when the constraint right-hand side moves.
Formalization produces a reusable cone-order layer independent of coordinate choices. coneLE, dualPositive, and ConeConvexOn can support later Kuhn–Tucker, vector optimization, and conic programming developments. The EReal value functions preserve infeasibility and unboundedness, two cases that a real-valued sInf encoding would collapse. This is a formalization mission for a classical theorem, not a claim that the underlying duality result is open.
The theorem's strict-feasibility condition is load-bearing. Feasibility cannot replace interior feasibility, and nonempty interior of alone does not supply a Slater point. Equality constraints also cannot be converted into pairs of inequalities while retaining strict feasibility; Luenberger explicitly warns about this after the theorem.
The cone assumptions differ across milestones. The main strong-duality theorem does not require to be closed or pointed, whereas the bipolar and saddle-sufficiency statements require closedness. Using Mathlib's stronger ProperCone everywhere would silently add both topological and order hypotheses and shrink the theorem. Another tempting simplification is to make both value functions real. That loses the empty feasible set and unbounded dual subproblem, precisely the boundary cases used when comparing perturbations. The saddle inequalities must also have the correct orientation: the multiplier coordinate is maximized and the primal coordinate is minimized.
The mission uses ConvexCone ℝ Z with a custom induced relation; it deliberately does not assume a lattice order on . Multipliers are continuous linear maps . The root assumes a real finite optimum through IsGLB and a real witness , while lagrangeDualValue and perturbationValue retain EReal codomains. The strict condition is written as membership of in interior P, exactly matching .
No finite-dimensionality, reflexivity, completeness, closedness, or pointedness is added to the root. Closedness appears only where the source uses cone separation to recover primal feasibility. The sensitivity item assumes the two candidate points are feasible, their multipliers are dual-positive and complementary, and each point minimizes its shifted Lagrangian; these hypotheses spell out “solutions and corresponding multipliers” without relying on informal terminology.
Contributions may formalize cone separation, perturbation-value geometry, saddle certificates, or strong duality. Finite-dimensional orthant and positive-semidefinite specializations are useful corollaries but do not replace the general goal. Local multiplier rules, equality constraints, differentiable Kuhn–Tucker conditions, and Chapter 9's local theory remain outside this mission.
AI generated, I think it's correct
The matrix-multiplication exponent measures the asymptotic arithmetic cost of multiplying square matrices. A bound means that, over the field under consideration, matrices can be multiplied in field operations for every . Matrix multiplication is a central benchmark in algebraic complexity and a basic subroutine in linear algebra, graph algorithms, and symbolic computation.
The Coppersmith--Winograd tensor and the laser method produced the strongest bounds on for several decades. The 1990 tensor-square analysis gave . Later analyses of larger powers improved the numerical bound, but they organized their recursion through values assigned independently to constituent tensors. Duan, Wu, and Zhou identified a loss in that organization: several fine constituents that can coexist inside one coarse block may be counted as though they had to be selected independently. Their asymmetric-hashing framework partially compensates for this combination loss. The paper's full second-power specialization improves the best bound obtainable from the square of the Coppersmith--Winograd tensor to ; see Section 6.3 and its parameter Table 2 in Duan--Wu--Zhou.
This mission isolates that second-power result. It is smaller than the paper's record-setting eighth-power calculation, but it contains the genuinely new asymmetric-hashing and hole-repair mechanisms in their first complete form. It therefore provides a focused bridge from the existing formalization of the classical square analysis to later combination-loss methods.
For a field , the matrix-multiplication tensor
encodes multiplication of an matrix by a matrix. A restriction applies one linear map to each tensor leg, while a degeneration permits polynomial families of such maps and takes their first nonzero coefficient. A degeneration from the diagonal tensor gives a border-rank upper bound of .
The Coppersmith--Winograd tensor with parameter is
It has border rank at most . Its coordinate partition has six supported types, and the square has fifteen coarse constituent types with . A large tensor power contains many blocks with prescribed joint and marginal type distributions. The laser method retains blocks whose variables are disjoint and interprets their direct sum through Schönhage's asymptotic sum inequality.
Duan--Wu--Zhou refine this organization by also retaining a split distribution for the fine indices inside each coarse constituent. Coarse - and -blocks are made unique, while compatible coarse triples may initially share a -block. The resulting partially damaged constituent tensors are described as broken copies of a standard-form tensor. The formal target uses , the full Section 6 construction, and the paper's released second-power parameters.
For every field ,
The source reports the stronger numerical endpoint , so the displayed rational inequality has strict slack. The Lean declaration has exactly the same field quantification and uses exactly the same matMulExp definition as the existing Coppersmith--Winograd mission; only the theorem name and rational endpoint change.
The mission first isolates the available-block shuffling interface extracted from Definitions 5.3--5.5 and Claims 5.8--5.10, then formalizes the finite covering core of the Hole Lemma 5.6. The subsequent tensor realization by zeroing and identification, the multiple-copy Corollary 5.11, the compatibility-rate identity of Lemma 6.7, the probabilistic part of Claim 6.8, and the global restricted-splitting value inequality in Equation (25) remain visible structural leaves rather than being hidden inside scalar assumptions. The numerical milestone instantiates Equation (25) with the exact data of Section 6.3 and Table 2 and checks a strict value surplus at . The structural proof must also make explicit the conversion from the paper's six-symmetrized value to a direct HasTauValueAtLeast witness for the mode-symmetric CW square. The final bridge applies the existing tau-value/rank machinery and transfers the Strassen-preorder exponent bound to matMulExp.
The mathematical result gives the first improvement over the classical Coppersmith--Winograd number while continuing to use only the tensor square. It separates improvement of the tensor analysis from improvement obtained merely by moving to a much higher tensor power. The same standard-form and restricted-splitting language is then reused by the paper's higher-power algorithm, which reports .
For formalization, the mission adds reusable infrastructure for nested tensor partitions. Existing CW-square work records coarse support types and actual matrix-multiplication restrictions. This mission extends that layer with fine split distributions, compatibility between levels, broken-block bookkeeping, and repair of holes without replacing tensor statements by unverified scalar values. Those definitions are prerequisites for later asymmetric-hashing, complete-split, and more-asymmetry analyses.
The bound is known mathematically and was published at FOCS 2023. The open work is a machine-checked reconstruction. The underlying CW tensor, border-rank certificate, canonical tensor-square grading, Salem--Spencer sets, direct-sum tau-value notion, asymptotic sum inequality, and exponent equivalence already exist on Prove2Me. The new frontier is the cross-level combination-loss analysis and its exact numerical specialization.
The central difficulty is that coarse and fine decompositions cannot be optimized independently. Two coarse triples may share a -block, and a fine -block can be useful for one triple, compatible with several, or removed by a collision. Counting all locally valuable fine constituents therefore does not certify a direct sum. Conversely, requiring every coarse -block to be unique discards precisely the combinations that produce the improvement.
The Hole Lemma must also preserve the actual tensor. A broken copy lacks some fine variable blocks; combining several such copies is useful only when a degeneration covers every required block with controlled loss and does not duplicate monomials. On the numerical side, the same-marginal maximum-entropy term and restricted-splitting values must be bounded with certified real inequalities. Floating-point output from MATLAB is evidence for a witness, not a Lean proof.
The mission uses the existing TensorObj, MMObj, restriction, degeneration, asymptotic-rank, HasTauValueAtLeast, matMulExp_strassen, and matMulExp declarations in environment 777aaa61dcd2a1258d2b4962dbe983ede4d23b2e. Top-level results quantify over an arbitrary field. Finite supports and block indices are represented by finite types; probability and split distributions are nonnegative real functions of total mass one; entropy and numerical optimization live in the reals.
The formalization is restricted to for the capstone, although generic definitions and source lemmas may quantify over levels and finite index types. A valid proof must connect scalar rate inequalities to witnessed restrictions or degenerations yielding direct sums of concrete matrix-multiplication tensors. A constant-valued surrogate for the restricted-splitting value, a hypothesis that already assumes the desired exponent bound, or a certificate definition containing its own conclusion is outside scope.
Contributions are welcome for standard-form tensor encodings, finite permutation arguments, hole repair, type and split counting, entropy maximization certificates, certified logarithm and power inequalities, and the final tau-value/rank assembly. Statements should identify the corresponding definition, lemma, claim, equation, or table in the source.
Convex duality converts an optimization problem over points into one over linear functionals. It supplies lower bounds, certificates of optimality, and alternative formulations whose geometry can be simpler than the primal problem. In §§7.8–7.12 of David G. Luenberger's Optimization by Vector Space Methods, this theory is developed for finite-valued convex and concave functions on convex subsets of a real normed space. The capstone is Fenchel duality with restricted domains and an attained continuous-linear-functional dual optimum. This mission preserves that functional-analytic setting rather than reducing the theorem to Euclidean space or silently extending the functions to the whole space.
Let be a real normed space, let be nonempty convex sets, let be convex on , and let be concave on . For a continuous linear functional , the restricted convex conjugate and restricted concave conjugate are
The convex conjugate is admitted into only when its defining set is bounded above; the concave conjugate is admitted into only when its defining set is bounded below. Because and are nonempty and the functions are real-valued, these predicates exactly exclude the unwanted infinite endpoint. The Lean definitions use real sSup and sInf, with boundedness carried explicitly by theorem hypotheses.
The restricted epigraph of is the set of satisfying and ; the restricted hypograph of reverses the scalar inequality. Luenberger's qualification requires a common point of the relative interiors of and , represented by Mathlib's intrinsicInterior, and also requires ordinary nonempty interior of at least one of these two graph sets.
Assume the finite primal value is the greatest lower bound of
Prove that some attains
If attains the primal infimum, also prove that attains both conjugate extrema at : and .
The mission records four source milestones. A local minimum of a convex function on its convex domain is global (§7.8, Proposition 1). Convexity of a restricted function is equivalent to convexity of its restricted epigraph (§7.8, Proposition 2). The finite-conjugate domain and the convex conjugate are convex (§7.10, Proposition 1). Finally, a closed restricted epigraph agrees pointwise on with the continuous-linear biconjugate (§7.10, Proposition 2). Together these statements expose the geometric and conjugacy interfaces on which the capstone depends without turning every paragraph of the chapter into a separate item.
The theorem gives an attained dual certificate in an arbitrary real normed space. Equality of primal and dual values eliminates a duality gap, while attainment produces a specific functional that can certify an optimal primal point through simultaneous conjugate equality. The biconjugate milestone is independently useful: it expresses a closed convex function as a supremum of continuous affine minorants on its domain.
Formalizing this material adds a restricted-domain conjugacy API that is not supplied by the existing project artifact named fenchelConjugate. That artifact accepts finite-valued functions on a Euclidean space and has no independent convex domain or concave conjugate. Reusing it here would erase hypotheses that are central to Luenberger's theorem. The new definitions remain small, but their exact boundedness contracts make them reusable for later separation, minimax, and Lagrange-duality missions. The theorem is classical; the mission asks for a checked development faithful to the 1969 source and the current Mathlib representation of continuous dual spaces.
The qualification is not the usual finite-dimensional slogan that relative interiors merely intersect. The source additionally demands that either the restricted epigraph or restricted hypograph have nonempty ordinary interior. Dropping that condition changes the theorem in infinite-dimensional spaces. Replacing intrinsicInterior by topological interior would also make valid lower-dimensional domains appear empty.
Extended values create another boundary. Real sSup and sInf are meaningful here only together with nonempty domains and the respective boundedness hypotheses. Treating their default values outside those hypotheses as genuine conjugates would admit false dual candidates. A finite-dimensional conjugate definition avoids neither issue and would prove only a special case. The biconjugate target must quantify over continuous linear functionals, not all algebraic linear maps, because closed epigraph separation is topological. Finally, the dual statement must include actual attainment; proving only equality with a supremum would omit a principal assertion of §7.12.
All primal functions are finite-valued real functions. Infinite conjugate values are represented by domain predicates—BddAbove for and BddBelow for —rather than by changing the public conjugate codomain. The primal finiteness assumption is encoded by a real number together with IsGLB, which simultaneously rules out an empty feasible intersection and an infimum of . Epigraph pairs are ordered as to match Mathlib conventions, although Luenberger prints the scalar coordinate first.
The ambient space is normed but is not assumed finite-dimensional, reflexive, or complete. Both and are explicitly nonempty. The main theorem keeps the common intrinsic-interior condition and the disjunctive ordinary-interior condition verbatim. Contributions may develop separation lemmas, boundedness facts for restricted conjugates, or direct proofs of the milestone statements. A whole-space Euclidean specialization is welcome only as a corollary, not as a replacement for the root. The minimax theorem of §7.13 and extended-real lower-semicontinuous variants are outside this mission.
Every full-dimensional convex body is sandwiched between an ellipsoid and its -fold dilation: shrinking the minimum-volume covering (Löwner–John) ellipsoid about its centre by the factor lands inside the body,
and the factor is tight on simplices. This rounding theorem underlies the ellipsoid method, John's theorem on the Banach–Mazur distance to the Euclidean ball, and much of modern convex geometry. The mission formalizes §8.4 of Boyd & Vandenberghe for polytopes , exactly as the book proves it: existence and uniqueness of the extremal ellipsoid, the KKT identities at the normalized optimum (, , ), the convex-combination step that produces the ball, and affine invariance.
A nonlocal game is played between a classical referee and two or more cooperating players who are not allowed to communicate during the game. In the two-player, one-round setting, the referee samples a pair of questions from a distribution , sends to Alice and to Bob, and receives answers and . The players win when a predicate accepts. Before the game begins they may agree on a strategy and share a resource, but after receiving their questions they are isolated from one another.
Nonlocal games occupy a useful interface between complexity theory and quantum information. From the perspective of complexity theory, they are the basic objects underlying multiprover interactive proofs: a verifier delegates a computation to separated provers and uses the consistency of their answers to distinguish valid from invalid claims. Classical two-prover games play a central role in the PCP theorem, hardness of approximation, and soundness amplification. Allowing the provers to share entanglement leads to the class and to a substantially richer theory. The theorem shows how dramatically entanglement changes this landscape: even estimating the entangled value of a nonlocal game can encode undecidable computation Ji--Natarajan--Vidick--Wright--Yuen 2020.
From the perspective of quantum information, nonlocal games are operational formulations of Bell experiments. A separation between classical and entangled values witnesses correlations that cannot be explained by a local hidden-variable model. The same framework supports self-testing, in which near-optimal behavior certifies the underlying state and measurements up to local equivalence, and device-independent cryptography, in which security or randomness is certified from observed input-output statistics rather than a trusted description of the devices. Representative references include Cleve--Høyer--Toner--Watrous 2004, Reichardt--Unger--Vazirani 2013, and Pironio et al. 2010. The survey of Palazuelos--Vidick 2016 describes further connections among nonlocal games, Bell inequalities, operator spaces, and quantum information.
Thus the value of a nonlocal game is simultaneously a complexity-theoretic soundness parameter and a quantitative measure of the power of nonclassical correlations. Understanding how this value changes under natural operations on games is important in both subjects.
We take the finite answer alphabets to be nonempty. In a classical strategy, Alice's answer depends only on , Bob's answer depends only on , and the players may coordinate using shared randomness. In a finite-dimensional entangled strategy, the players share a bipartite state and use POVM measurement operators
for their respective questions. The probability of producing answers on questions is
The supremum of the winning probability over all such finite-dimensional strategies is the entangled value . This optimization ranges over arbitrary local dimensions, shared states, and local measurements, which is one reason even apparently elementary questions about nonlocal games can be difficult.
For a positive integer , the repeated game consists of independently sampled copies of played simultaneously. Alice receives , Bob receives , and they answer with tuples and . They win only if
for every coordinate .
Parallel repetition is a basic method of soundness amplification. Starting from a game that dishonest players cannot win with certainty, the verifier repeats the test in the hope of driving the optimal success probability rapidly toward zero. The difficulty is that independence in the verifier's sampling does not force independence in the players' strategy. Alice may choose her entire answer tuple as a function of all her questions, Bob may do the same, and an entangled strategy may use a single state and joint measurements spanning all coordinates. In particular, one cannot obtain an upper bound on merely by analyzing the strategy that plays each coordinate independently.
For classical games, Raz's parallel repetition theorem gives exponential decay whenever the one-shot value is below one Raz 1998. Establishing the corresponding behavior for entangled games has been a long-running problem. A general polynomial bound was proved in Yuen 2016, implying for the first time that tends to zero for every finite two-player entangled game with .
The full exponential-decay theorem was recently settled by OpenAI. In Chapter 6 of Ten Advances in Mathematics and Theoretical Computer Science, OpenAI proves that for every finite two-player entangled game with , there is a constant such that
for every positive . OpenAI also released a Lean certificate for the result. This resolves the general quantum parallel-repetition conjecture, but it does not end the study of the problem. The proof introduces quantitative losses and a substantial technical apparatus, and there remains considerable value in finding alternative arguments, isolating the essential mechanism, improving the dependence on the one-shot gap and answer size, and producing shorter or more conceptual formal proofs.
This mission develops a reusable Lean framework for parallel repetition rather than formalizing only one paper. Its targets are organized by the strength of the asserted decay.
The main mission theorem is the fundamental asymptotic statement:
Equivalently, for every , all sufficiently large satisfy . This statement deliberately specifies no rate. It is a stable top-level theorem that can be recovered from any sufficiently strong quantitative bound.
A stronger target asks for game-dependent constants and such that
The abstract formulation avoids fixing a particular exponent or logarithmic correction. More refined formalizations can record explicit dependence on the gap , the answer alphabet, or other game parameters. Yuen's 2016 theorem is one important result at this level.
The exponential target asks for game-dependent constants such that
Following OpenAI's recent resolution, this target is now a theorem rather than an open conjecture. Within this mission it remains a central milestone: contributors may formalize the released argument in the mission's common interface, construct an independent proof, seek a more elegant or modular proof, or establish sharper quantitative variants.
These levels do not exhaust the project. The same framework can accommodate explicit finite- inequalities, stretched-exponential estimates, bounds for structured classes of games, improved parameter dependence, and reductions showing that one decay statement implies another.
The foundational Lean development represents a game by finite question sets , finite answer sets , a nonnegative normalized question distribution , and a Boolean verification predicate . The parallel-repetition theorems explicitly assume that and are nonempty. The development defines finite-dimensional entangled strategies using density matrices and POVM measurement operators, defines the repeated game on tuples, and takes the entangled value as a supremum over all finite-dimensional strategies. Repeated strategies are indexed by complete question tuples and are not required to factor coordinatewise.
A complete development will draw on formal libraries for finite probability, tensor products, positive semidefinite matrices, density matrices, POVMs, trace norms, fidelity, entropy, mutual information, and correlated sampling. These components should be formulated for reuse and should expose the dependence of each bound on the relevant game parameters.
The goal is both to verify parallel-repetition theorems and to build a dependable language for nonlocal games in Lean. Formalization forces distinctions that are easy to suppress on paper: whether constants depend on the game, whether a bound holds for all or only asymptotically, which strategy model is optimized over, and which hypotheses are needed for a particular rate. The mission welcomes reconstructions of known proofs as well as new, shorter, or conceptually different proofs.
Interior point methods solve linear programs by moving through the interior of the feasible set instead of along its edges — the approach that turned Karmarkar's 1984 breakthrough into today's practical large-scale solvers. This mission formalizes the primal path following algorithm of Chapter 9 of Bertsimas–Tsitsiklis. For the logarithmic barrier
replaces the constraint ; the minimizers of over trace the central path, characterized by the KKT conditions (9.17): , , , , (Lemma 9.5). The algorithm follows the path with one Newton step of the barrier problem per shrink , maintaining the proximity invariant
. The goal theorem is Theorem 9.7: with and a -close start, after iterations the algorithm reaches primal and dual feasible solutions with duality gap — the explicit form of the celebrated iteration bound. Alongside it we formalize the generic potential-reduction scheme (Theorem 9.4): any algorithm cutting by per step reaches gap within an explicit .
Can the feasibility of a system of linear inequalities be decided in a provably small number of iterations? The ellipsoid method — the algorithm with which Khachiyan showed in 1979 that linear programming is polynomially solvable — answers this with pure convex geometry. This mission formalizes Chapter 8 of Bertsimas–Tsitsiklis. An ellipsoid is
with symmetric positive definite. The geometric engine is Theorem 8.1: the half-ellipsoid is contained in the explicitly constructed ellipsoid ,
and the volume contracts:
. Two integer-data estimates make the contraction decisive: every extreme point of with entries bounded by has coordinates in (Lemma 8.2), and a full-dimensional bounded such polyhedron has (Lemma 8.4). The goal theorem is Theorem 8.2: started on a ball of volume at most containing , with a lower bound on when is nonempty, the ellipsoid method correctly decides whether is empty within iterations — the explicit iteration count behind the polynomial-time headline.
Why do network linear programs return integer answers for free? This mission formalizes the structural theory of the minimum cost network flow problem of Chapter 7 of Bertsimas & Tsitsiklis: a directed graph with external supplies , arc costs , and the node-arc incidence matrix — an matrix in which every column has exactly one (start node) and one (end node) — so that flow conservation reads , forcing the standing assumption . Because the rows of sum to zero, the book works with the truncated matrix of the first rows. The combinatorial heart is the correspondence between algebra and graph structure: a set of arcs forming a tree determines a unique tree solution of , off (Theorem 7.3); connectedness makes full-rank (Corollary 7.1); and a flow vector is a basic solution if and only if it is a tree solution (Theorem 7.4). The goal theorem is the integrality theorem (Theorem 7.5): for the uncapacitated problem on a connected graph, every basis matrix has an integer inverse (its determinant is by the tree/lower-triangular argument), integer supplies make every basic solution integer, and integer costs make every dual basic solution integer — whence integer optimal primal and dual solutions exist whenever the optimal cost is finite (Corollary 7.2). This is the fountainhead of combinatorial integrality in linear optimization, feeding the max-flow min-cut mission that follows.
How does the optimal cost of a linear program respond when the problem data change? Chapter 5 of Bertsimas-Tsitsiklis studies the standard form problem (rows of linearly independent) as the requirement vector and the cost vector vary. On the convex set of feasible right-hand sides, and under the standing assumption that the dual feasible set is nonempty, the optimal cost is finite and convex (Theorem 5.1) — indeed over the extreme points of the dual feasible set, a piecewise linear convex function whose breakpoints are exactly where the dual optimum is non-unique. The capstone (Theorem 5.2) identifies the generalized gradients of : if the primal at is feasible with finite optimal cost, then is an optimal solution of the dual if and only if is a subgradient of at (Definition 5.1: for all ) — the precise sense in which dual variables are marginal costs. Dually (Theorem 5.3), the set of cost vectors with finite optimal cost is convex, the optimal cost is concave on , and near any with a unique primal optimum , is linear with gradient . Local ranging (Section 5.1) and parametric programming (Section 5.5) are the procedural companions, folded into the design notes.
Every linear programming problem has a shadow. To the primal we associate the dual , whose variables price the primal constraints: one dual variable per primal constraint and one dual constraint per primal variable, with signs governed by the correspondence of Table 4.1. This mission formalizes §4.1–4.5 of Bertsimas–Tsitsiklis: the dual of a general-form linear program, the involution "the dual of the dual is the primal" (Theorem 4.1), and weak duality for any primal-feasible and dual-feasible (Theorem 4.3) with its two corollaries — an unbounded primal forces an infeasible dual (Corollary 4.1), and feasible with are automatically both optimal (Corollary 4.2). The goal theorem is strong duality (Theorem 4.4): if a linear programming problem has an optimal solution, so does its dual, and the respective optimal costs are equal — proved in the book by running the simplex method with the lexicographic pivoting rule of Mission IV on a standard-form transform. The statement is deliberately the book's attainment form: by Table 4.2 the primal and the dual can be simultaneously infeasible (Example 4.5), so an unguarded equality of optimal values is false. The mission closes with complementary slackness (Theorem 4.5): feasible and are simultaneously optimal if and only if for all and for all — the certificate structure behind the dual simplex method and every LP optimality check.
How does one actually solve a linear program? Chapter 2 showed that if a standard-form problem subject to , has an optimal solution, it has an optimal basic feasible solution; the simplex method searches among basic feasible solutions, moving along edges of the feasible set in cost-reducing directions. This mission formalizes the mathematics of Chapter 3 of Bertsimas–Tsitsiklis: feasible directions, the reduced costs
measuring the cost rate along the basic directions, the optimality conditions of Theorem 3.1 ( implies optimality, and conversely at nondegenerate optima), the basis change of Theorem 3.2, and the pivot iteration itself — encoded as a predicate relating a basis/BFS pair to its successor, so that every theorem covers every pivoting rule. The goal theorem is Theorem 3.3: if the feasible set is nonempty and every basic feasible solution is nondegenerate, the simplex method terminates after a finite number of iterations, ending either with an optimal basis and an associated optimal basic feasible solution, or with a direction satisfying , , certifying optimal cost . The secondary capstone, Theorem 3.4, removes the nondegeneracy assumption: under the lexicographic pivoting rule every tableau row other than the zeroth stays lexicographically positive, the zeroth row strictly increases lexicographically, and the simplex method terminates on every problem — the anticycling guarantee that also supplies the optimal-basis existence used by the strong duality theorem of Mission V.
Every linear programming problem asks to minimize a linear cost over a polyhedron — a set of the form , or in standard form . Chapter 2 of Bertsimas–Tsitsiklis develops the geometry of these feasible sets, and its central achievement is making the intuitive notion of a "corner point" rigorous. There are three natural candidates: the extreme point — a point of that cannot be written as a convex combination of two other points of (purely geometric, representation-independent); the vertex — the unique minimizer of some linear cost over (geometric, via supporting hyperplanes); and the basic feasible solution — a feasible point at which linearly independent constraints are active (algebraic, the object the simplex method actually computes with). This mission formalizes polyhedra, active constraints, vertices and basic (feasible) solutions, and proves the fundamental Theorem 2.3: for a nonempty polyhedron all three notions coincide. Around the capstone sit the supporting pillars: polyhedra are convex (Theorem 2.1), the characterization of points pinned down by linearly independent active constraints (Theorem 2.2), finiteness of the set of basic solutions (Corollary 2.1), and the basis-column characterization of basic solutions in standard form (Theorem 2.4) — the combinatorial engine behind the simplex method of Chapter 3 and the root of the entire series.
A continuous piecewise linear (CPWL) function is one assembled from finitely many flat pieces glued along flat seams. Every ReLU network computes such a function, and every such function is computed by some ReLU network. Questions about how deep a network must be are therefore questions about the internal structure of CPWL functions.
In 1993 Breiman built such functions from hinges: maxima of two affine maps. Sums of hinges approximate anything, but from two dimensions up they fail to represent most CPWL functions exactly. Wang and Sun (2005) widened the maxima, proving that every CPWL function on ℝⁿ is a signed sum of maxima of at most n+1 affine maps. Twenty years on it remains the workhorse structural fact, reducing any question about a network to a question about a single max gate and underpinning every known upper bound on the depth of exact representation.
That includes the newest one: at STOC 2026, Bakaev et al disproved the short standing conjecture that ⌈log₂(n+1)⌉ hidden layers are necessary, showing ⌈log₃(n−1)⌉+1 suffice. In this mission we deliver a machine-checked proof of the Wang and Sun theorem so future formalizations of network expressivity can invoke it rather than reprove it. Note that we take as given the lattice representation of Tarela and Martínez, independently proved by Ovchinnikov, which writes any CPWL function as a max of mins of its affine pieces. That is the one external ingredient the argument consumes, and our definition of CPWL builds it in.
How quickly does the empirical mean of independent random variables concentrate around the true mean? This question is the analytic engine of the entire theory of stochastic bandits: every optimistic algorithm (Explore-Then-Commit, UCB and its relatives) is calibrated by a tail bound on the sample mean. This mission formalizes the subgaussian framework of Chapter 5 of Lattimore–Szepesvári's Bandit Algorithms: a random variable is -subgaussian when for all , and the Cramér–Chernoff method converts this moment-generating-function control into the exponential tail . The goal theorem is the Hoeffding-type bound: the sample mean of independent -subgaussian deviations exceeds the true mean by with probability at most , together with its confidence form — the exact bound every UCB index is built from. These few lines of analysis are cited by every regret bound in the series.
Multi-agent reinforcement learning approximates a global value function by summing per-agent local value functions learned independently — a trick that works surprisingly well in practice (ride-hailing dispatch, restless bandits) but had no general theoretical justification. Chen and Peng (arXiv:2506.02385) explain why: they define a Markov entanglement measure for the joint transition dynamics of a multi-agent MDP, directly analogous to quantum entanglement of a two-party state, and show it controls exactly how much error this value-decomposition trick incurs. This mission formalizes their sharpest quantitative bound (Theorem 4): the error of decomposing the global Q-function into per-agent local Q-functions is controlled, entrywise, by the agent-wise total-variation measure of Markov entanglement.