The OR Formalization Drive

Motivation

The traveling salesman problem — visit $n$ cities by the cheapest round trip — is the most widely known problem in combinatorial optimization, and its central open question concerns a linear program. The subtour-elimination relaxation (the Held–Karp bound) replaces tours by fractional edge weights, and both in theory and in practice (it powers the lower bounds inside the Concorde solver) it is remarkably close to the true optimum. How close, in the worst case, is the integrality gap of the relaxation: the supremum of $\mathrm{OPT}/\mathrm{LP}$ over metric instances. Explicit instance families push the gap up to $4/3$; the best proven upper bound sits just barely below $3/2$. The 4/3 conjecture — the gap is exactly $4/3$ — has been the benchmark question of approximation algorithms for four decades.

Timeline

• 1954. Dantzig, Fulkerson, and Johnson solve a 49-city instance by hand with the cutting planes that become the subtour-elimination LP.
• 1970–1971. Held and Karp introduce the 1-tree/Lagrangian bound and show it equals the subtour LP value — since then, "the Held–Karp bound".
• 1976/1978. Christofides, and independently Serdyukov, give the $3/2$-approximation: minimum spanning tree plus a matching on odd-degree vertices.
• 1980. Wolsey (Math. Prog. Study 13) shows Christofides' analysis goes through against the LP: $\mathrm{OPT} \le \frac{3}{2}\,\mathrm{LP}$, so the integrality gap is at most $3/2$. Shmoys and Williamson (IPL 1990) rediscover this via a monotonicity property.
• 1995. Goemans (Math. Programming 69) analyzes the worst-case ratios of TSP relaxations and states the $4/3$ conjecture explicitly; the $4/3$ lower-bound families (three parallel paths) are by then folklore.
• 2011–2014. For graph metrics (shortest-path metrics of unweighted graphs) the barrier breaks: Oveis Gharan–Saberi–Singh and Mömke–Svensson beat $3/2$, and Sebő–Vygen (Combinatorica 2014) reach $7/5$ — the conjectured-optimal shape of progress, but only for a special class.
• 2020–2022. Karlin, Klein, and Oveis Gharan prove a $3/2 - \varepsilon$ approximation for general metric TSP (STOC 2021) and then an integrality-gap bound $\gamma \le 3/2 - \varepsilon$ with $\varepsilon > 10^{-36}$ (FOCS 2022), via max-entropy sampling of spanning trees and strongly Rayleigh distributions — the first general improvement over Wolsey in forty years, by an astronomically small margin.
• Today. The gap between the $4/3$ lower bound and the $3/2 - 10^{-36}$ upper bound is the conjecture. For half-integral LP solutions — where the conjectured extremal instances live — the bound has been pushed to $1.4983$ (Gupta, Lee, Li, Mucha, Newman, and Sarkar, via matroid-based rounding).

Setting

An instance on $n \ge 3$ cities is a cost function $c$ assigning to each ordered pair of cities $u, v$ a real cost $c(u,v)$, required to be a metric cost: symmetric ($c(u,v) = c(v,u)$), zero on the diagonal ($c(v,v) = 0$), and satisfying the triangle inequality $c(u,w) \le c(u,v) + c(v,w)$. Nonnegativity follows; distinct cities at distance zero are allowed, as usual for metric TSP.

A tour visits every city exactly once and returns to its start. Formally a tour is given by an ordering: a permutation $\pi$ of the cities, traversed as $\pi(0), \pi(1), \dots, \pi(n-1)$ and back to $\pi(0)$; its cost $\mathrm{tourCost}(c, \pi)$ is the sum of the costs of consecutive steps, and $\mathrm{OPT}(c)$ — written tspOpt c — is the minimum over all orderings.

The subtour-elimination (Held–Karp) relaxation replaces the tour by a fractional edge weight $x(u,v)$ for each pair of cities. A weight vector $x$ is feasible (IsHeldKarp x) when it is symmetric with zero diagonal, has entries in $[0,1]$, gives every city fractional degree two ($\sum_u x(v,u) = 2$), and crosses every nontrivial cut at least twice: for every set $S$ of cities other than $\emptyset$ and all cities, $\sum_{u \in S} \sum_{v \notin S} x(u,v) \ge 2$. The Held–Karp bound hkValue c is the infimum of $\frac{1}{2}\sum_u \sum_v c(u,v)\,x(u,v)$ over feasible $x$ (the double sum counts each edge twice, hence the $\frac12$). The incidence vector of any tour is feasible, so $\mathrm{LP} \le \mathrm{OPT}$ always.

Formalization targets

Goal — the 4/3 conjecture

$$\mathrm{OPT}(c) \;\le\; \tfrac{4}{3}\,\mathrm{LP}(c) \qquad \text{for every } n \ge 3 \text{ and every metric cost } c.$$

Together with the known lower-bound families this says the integrality gap is exactly $4/3$. The goal carries no algorithm and no constant to improve: it is the terminal statement of the ladder, open in both directions (a proof or a counterexample instance would each settle it).

Milestones — the known ladder

Five results over the same definitions: the relaxation is valid ($\mathrm{LP} \le \mathrm{OPT}$); instance families force the gap arbitrarily close to $4/3$; tree doubling gives $\mathrm{OPT} \le 2\,\mathrm{LP}$; Wolsey's theorem gives $\mathrm{OPT} \le \frac{3}{2}\,\mathrm{LP}$, the classical upper bound; and the Karlin–Klein–Oveis Gharan record $\mathrm{OPT} \le (\frac{3}{2} - \varepsilon)\,\mathrm{LP}$ for some $\varepsilon > 10^{-36}$ (FOCS 2022). The last milestone is a statement-level target: its known proof (max-entropy sampling, strongly Rayleigh polynomials) is far beyond current formalization practice, so the mission's usable proving frontier remains Wolsey — the milestone records the state of the art as a formal statement.

Significance

The 4/3 conjecture is the reference open problem of approximation algorithms: the quality of the subtour LP calibrates every algorithmic advance on TSP, and the conjectured extremal instances guide the search for better rounding schemes. The bound is also what practical solvers actually compute — branch-and-cut on this LP solves instances with tens of thousands of cities — so the conjecture is a statement about the observed tightness of the world's most-used combinatorial lower bound.

Nothing in this circle exists in any proof assistant: Mathlib has no TSP, no LP relaxations, no polyhedral combinatorics of tours. The mission's milestones force the base layer into existence — tours over Equiv.Perm, cut constraints over Finset, and, for the upper bounds, the parity and tree arguments (spanning trees against the LP, T-joins for the $3/2$ bound) whose infrastructure is reusable for matching theory and network design far beyond TSP.

Difficulty

The naive plan — round the LP solution to a tour — has no known analysis losing less than $3/2$ in general, and the half-integral extremal instances show the hard cases are structured and simple-looking at once. Christofides' matching argument is provably stuck at $3/2$ against the LP; forty years of work moved the constant by $10^{-36}$, and that advance needed an entirely new probabilistic toolkit. On the other side, no instance family with ratio above $4/3$ has ever been found despite extensive computational search over small instances (Benoit–Boyd and successors). Both directions of the goal are genuinely open territory.

Formalization scope

The Lean model commits to: cities Fin n; costs c : Fin n → Fin n → ℝ with IsMetricCost (symmetry, zero diagonal, triangle inequality — nonnegativity is derived, and semimetrics are included as in the standard statement of the conjecture); tours as orderings π : Equiv.Perm (Fin n) traversed cyclically via finRotate, so every permutation denotes a Hamiltonian cycle and every Hamiltonian cycle is denoted; both optimal values as sInf over nonempty, bounded-below sets of reals, so they are genuine minima for n ≥ 3. The hypothesis 3 ≤ n is load-bearing: for n ≤ 2 the degree-2 constraints are infeasible, sInf ∅ = 0 by convention, and the bounds would be false — every theorem therefore carries it.

Welcome contributions: the milestones in any order — held_karp_le_opt is the natural entry point (the tour's incidence vector crosses every cut at least twice); integrality_gap_lower_bound needs the three-path instance family and a case analysis on its tours; tree_doubling_bound needs spanning trees against the LP; wolsey_bound adds the T-join/parity argument and is the summit. Reusable infrastructure — spanning tree polytopes, T-joins, Eulerian traversals, cut lemmas — is welcome as platform theorems. Graph-TSP ($7/5$), path TSP, and asymmetric TSP are deliberately left to future missions; the Karlin–Klein–Oveis Gharan bound is stated as a milestone, but its sampling machinery is expected to arrive, if ever, as shared infrastructure built over many contributions.

Selected references

• G. Dantzig, R. Fulkerson, S. Johnson, Solution of a large-scale traveling-salesman problem, Oper. Res. 2 (1954).
• M. Held, R. Karp, The traveling-salesman problem and minimum spanning trees, Oper. Res. 18 (1970); Part II, Math. Programming 1 (1971).
• N. Christofides, Worst-case analysis of a new heuristic for the travelling salesman problem, CMU report (1976); A. Serdyukov, Upravlyaemye Sistemy 17 (1978).
• L. Wolsey, Heuristic analysis, linear programming and branch and bound, Math. Prog. Study 13 (1980). doi:10.1007/BFb0120913
• D. Shmoys, D. Williamson, Analyzing the Held-Karp TSP bound: a monotonicity property with application, Inf. Process. Lett. 35 (1990). doi:10.1016/0020-0190(90)90028-V
• M. Goemans, Worst-case comparison of valid inequalities for the TSP, Math. Programming 69 (1995). doi:10.1007/BF01585563
• A. Sebő, J. Vygen, Shorter tours by nicer ears, Combinatorica 34 (2014). arXiv:1201.1870
• A. Karlin, N. Klein, S. Oveis Gharan, A (slightly) improved approximation algorithm for metric TSP, STOC 2021. arXiv:2007.01409
• A. Karlin, N. Klein, S. Oveis Gharan, A (slightly) improved bound on the integrality gap of the subtour LP for TSP, FOCS 2022. arXiv:2105.10043
• V. Traub, J. Vygen, Approximation Algorithms for Traveling Salesman Problems, Cambridge University Press, 2024. book page

Motivation

The $k$-server problem was introduced by Manasse, McGeoch, and Sleator (STOC 1988 / J. Algorithms 1990) as a common generalization of paging, weighted caching, and related sequential decision problems, and their $k$-server conjecture has since become the central open question of competitive analysis. The conjecture asserts that a single ratio — exactly $k$ — governs deterministic online server management on every metric space.

Timeline

• 1985. Sleator and Tarjan introduce competitive analysis — an online algorithm judged against the offline optimum on every input — for list update and paging, and ask for a theory of such guarantees.
• 1988–1990. Manasse, McGeoch, and Sleator introduce the $k$-server problem (STOC 1988; J. Algorithms 1990) and settle its extremes: no deterministic algorithm beats ratio $k$ on any space with more than $k$ points (Corollary 7), two servers admit a $2$-competitive algorithm (Theorem 5, algorithm RES), and $k$ servers on $k+1$ points admit a $k$-competitive one (Theorem 4, algorithm BAL). Section 8 poses the $k$-server conjecture, in the symmetric finite setting of the paper.
• 1990. Fiat, Rabani, and Ravid (FOCS 1990) give the first competitive ratio depending on $k$ alone — exponential in $k$, but finite on every metric space.
• 1991. Chrobak, Karloff, Payne, and Vishwanathan (SIAM J. Discrete Math.) prove the conjecture on the real line via Double Coverage; Chrobak and Larmore (SIAM J. Comput.) extend it to all tree metrics.
• 1995. Koutsoupias and Papadimitriou (J. ACM) prove the Work Function Algorithm is $(2k-1)$-competitive on every metric space — the breakthrough, and still the best general bound. Their Conjecture 1.1 fixes the conjecture's modern form: for every metric space there is an online algorithm with competitive ratio $k$.
• 1996. The same authors verify the conjecture on spaces of $k+2$ points via the dual 2-evader problem (Inf. Process. Lett. 57).
• 2004. Bartal and Koutsoupias prove the WFA itself is $k$-competitive on the line, weighted stars, and all spaces of $k+2$ points.
• 2021. Coester and Koutsoupias (ICALP) give a unifying potential for all known WFA analyses and push the frontier to the circle.
• 2023. Bubeck, Coester, and Rabani (STOC) refute the randomized analogue: no $o(\log^2 k)$-competitive randomized algorithm exists in general. The deterministic conjecture — this mission's goal — survives as the central open question, with the gap between $k$ and $2k-1$ unmoved since 1995.
• 2026. Coester, Koutsoupias, and Zbysiński post The $k$-server conjecture is true (arXiv:2609.15979), a claimed proof of the full conjecture: the Work Function Algorithm itself is $k$-competitive on every metric space, via a matrix representation of work functions and a potential function built on it. The preprint is not yet peer-reviewed; this mission's goal stays open until a machine-checked proof exists.

Setting

Fix a metric space $M$ with distance function $d$, and a number of servers $k \ge 1$. A configuration records where the $k$ servers stand: it is a function $C$ assigning to each server $i \in \{1, \dots, k\}$ a point $C(i) \in M$. Moving the servers from configuration $C$ to configuration $C'$ means server $i$ travels from $C(i)$ to $C'(i)$; the movement cost is the total distance traveled,

$$\mathrm{moveCost}(C, C') \;=\; \sum_{i=1}^{k} d\bigl(C(i),\, C'(i)\bigr).$$

A request sequence is a finite list $\sigma = (r_1, \dots, r_n)$ of points of $M$, presented one at a time; write $\sigma_{\le j} = (r_1, \dots, r_j)$ for the list of the first $j$ requests (so $\sigma_{\le 0}$ is the empty list).

A deterministic online algorithm $A$ is a rule that, for every finite request sequence $\ell$, specifies a configuration $A(\ell)$ — where the servers stand after serving the requests of $\ell$ in order. In particular $A(\text{empty list})$ is the initial configuration, before any request arrives. Two points about this way of modeling an algorithm:

• Online and deterministic, by construction. The configuration after $j$ requests is $A(\sigma_{\le j})$, a function of those first $j$ requests only — the algorithm cannot see the future, and makes no random choices.
• The service constraint. Whenever a request sequence ends with a request $r$, some server must stand at $r$ immediately after: for every list $\ell$ and every point $r$, the configuration reached after serving $\ell$ followed by $r$ places at least one server at the point $r$.

Running $A$ on $\sigma = (r_1, \dots, r_n)$ produces the configurations $A(\sigma_{\le 0}),\, A(\sigma_{\le 1}),\, \dots,\, A(\sigma_{\le n})$, and its cost is the total movement along this trajectory:

$$\mathrm{cost}_A(\sigma) \;=\; \sum_{j=1}^{n} \mathrm{moveCost}\bigl(A(\sigma_{\le j-1}),\, A(\sigma_{\le j})\bigr).$$

For comparison, an offline schedule for $\sigma$ starting at a configuration $C_0$ is any sequence of configurations $S_0 = C_0, S_1, \dots, S_n$ in which $S_j$ places a server at the request $r_j$, for each $j$ — chosen with the whole of $\sigma$ known in advance. The optimal offline cost $\mathrm{OPT}(C_0, \sigma)$ is the infimum, over all such schedules, of the total movement $\sum_{j=1}^{n} \mathrm{moveCost}(S_{j-1}, S_j)$.

Finally, $A$ is $c$-competitive if there is a constant $a$ — depending on the algorithm, hence possibly on the metric space and the initial configuration, but never on the request sequence — with

$$\mathrm{cost}_A(\sigma) \;\le\; c \cdot \mathrm{OPT}\bigl(A(\text{empty list}),\, \sigma\bigr) + a \qquad \text{for every request sequence } \sigma.$$

Formalization targets

Goal — the $k$-server conjecture

$$\text{For every } k \ge 1,\ \text{every metric space } M,\ \text{and every initial configuration } C_0:\ \exists\, A \text{ starting at } C_0 \text{ that is } k\text{-competitive.}$$

The goal fixes no algorithm: any $k$-competitive construction settles it. This is the weakest stable form of the conjecture — it survives every improvement in constants or techniques short of a disproof.

Milestones — the known ladder

The milestones are the classical results between the trivial and the conjectured, each an existence or impossibility statement over the same definitions: the lower bound $c \ge k$ on any space with at least $k+1$ points; the conjecture for $k = 2$; for spaces of exactly $k+1$ points; for the real line; the $(2k-1)$ upper bound of the Work Function Algorithm on every space; the conjecture for spaces of exactly $k+2$ points; the conjecture for three servers in the Manhattan plane $(\mathbb{R}^2, \ell^1)$ — the one settled case over a genuinely two-dimensional continuum (Bein–Chrobak–Larmore 2002; reproved by the unifying potential of Coester–Koutsoupias 2021); Coester–Koutsoupias's 2021 result that the Work Function Algorithm itself — not just some algorithm — is $3$-competitive for three servers on trees, stated over an explicit formalization of the WFA; and the 2023 Bubeck–Coester–Rabani refutation of the randomized analogue: there are $(k+1)$-point spaces on which every randomized algorithm is $\Omega(\log^2 k)$-competitive, stated over a mixed-strategy model of randomized online algorithms.

Significance

A proof of the conjecture would close the founding problem of competitive analysis and pin down the exact power of determinism in online optimization over arbitrary metrics; a disproof would separate general metric spaces from every special class where the ratio $k$ is known tight. Either outcome recalibrates the field's standard model of adversarial request sequences.

None of these results — not even the lower bound — has a machine-checked proof, and online algorithms as a subject are absent from Mathlib. This mission builds the base layer: a faithful model of online service systems (configurations, online algorithms as prefix functions, offline schedules, competitiveness), the classical possibility and impossibility results over it, and, at the top, the Koutsoupias–Papadimitriou bound, whose potential-function argument is self-contained but delicate. The model is reusable for paging, weighted caching, metrical task systems, and the randomized $k$-server problem.

Difficulty

The obvious first idea — the greedy algorithm, moving the nearest server to each request — is not competitive for any constant, already on three points of the line: two nearby points can ping-pong one server forever while a server parked slightly farther away never moves. Every known competitive algorithm must sometimes move a server other than the nearest one, and the whole difficulty of the conjecture is quantifying exactly how much such foresight-free hedging can achieve. The Work Function Algorithm's analysis via a potential over offline work functions loses a factor of two for reasons nobody has been able to remove; on the lower-bound side, no metric space is known where the deterministic ratio exceeds $k$.

Formalization scope

The Lean model commits to: configurations as functions Fin k → M (labeled servers — equivalent in cost to the unlabeled multiset model, since offline can permute labels for free); algorithms as total functions List M → (Fin k → M) with the service constraint, so a step may move several servers (the standard laziness reduction makes this equivalent to one-move-per-request); costs in ℝ via Metric.dist; the offline optimum as an sInf over schedules, which agrees with the attained minimum on finite spaces; and the additive-constant form of competitiveness, quantified as ∃ a, ∀ σ.

Two conventions guard against trivialization. The additive constant is quantified before the request sequence — allowing it to depend on $\sigma$ would make every algorithm $1$-competitive. And the lower-bound milestone requires $k+1$ distinct points (Finset.card = k + 1); on spaces with at most $k$ points the conjecture is trivially true and the lower bound false.

Three further definitional layers extend the model. The work function workFunction C₀ σ C is the sInf of (schedule cost + final move to C) over schedules serving σ from C₀, and the Work Function Algorithm WFA is defined on finite spaces with k ≥ 1 servers: after each request it moves to a configuration containing the request minimizing (movement cost) + (work function of the history including the request), a minimizer existing by finiteness and ties broken by a fixed arbitrary choice — matching the standard definition with its "ties broken arbitrarily" (our fixed choice is one admissible instance). A tree is a finite metric space carrying a tree graph whose weighted path lengths realize the metric — exactly "the set of vertices of a tree" of the sources. A randomized algorithm is a mixed strategy: a probability measure over an index type together with a deterministic algorithm per outcome and measurable per-sequence cost; its expected cost is a lower Lebesgue integral in $[0,\infty]$, and $c$-competitiveness from $C_0$ demands every outcome start at $C_0$ and one additive constant work for all request sequences.

Welcome contributions: proofs of any milestone in any order (the lower bound and the $(k+1)$-point case are the natural entry points); alternative algorithms for milestones already closed; and infrastructure lemmas about moveCost, schedules, and work functions published as reusable platform theorems.

Selected references

• M. Manasse, L. McGeoch, D. Sleator, Competitive algorithms for server problems, J. Algorithms 11 (1990). doi:10.1016/0196-6774(90)90003-W
• A. Fiat, Y. Rabani, Y. Ravid, Competitive k-server algorithms, FOCS 1990. doi:10.1109/FSCS.1990.89566
• M. Chrobak, H. Karloff, T. Payne, S. Vishwanathan, New results on server problems, SIAM J. Discrete Math. 4 (1991). doi:10.1137/0404017
• M. Chrobak, L. Larmore, An optimal on-line algorithm for k servers on trees, SIAM J. Comput. 20 (1991). doi:10.1137/0220008
• E. Koutsoupias, C. Papadimitriou, On the k-server conjecture, J. ACM 42 (1995). doi:10.1145/210118.210128
• E. Koutsoupias, C. Papadimitriou, The 2-evader problem, Inf. Process. Lett. 57(5) (1996), 249–252.
• C. Coester, E. Koutsoupias, Towards the k-server conjecture: a unifying potential, pushing the frontier to the circle, ICALP 2021. arXiv:2102.10474
• S. Bubeck, C. Coester, Y. Rabani, The randomized k-server conjecture is false!, STOC 2023. arXiv:2211.05753
• E. Koutsoupias, The k-server problem (survey), Computer Science Review 3 (2009). doi:10.1016/j.cosrev.2009.04.002

Motivation

Discrepancy theory asks how evenly a collection of objects can be split into two parts. Its central open question is a conjecture of Komlós, first circulated in the 1980s: any finite family of vectors of Euclidean length at most one can be signed $\pm 1$ so that the signed sum is bounded in every coordinate by a universal constant — independent of how many vectors there are and of the dimension they live in.

Timeline

• 1963. Steinitz-type vector balancing questions circulate; Bárány and Grinberg later (1981) show any norm admits a dimension-dependent bound $2d$, setting the theme: how much of the dependence on dimension is real?
• 1981. Beck and Fiala (Discrete Appl. Math.) prove degree-$t$ set systems have discrepancy at most $2t - 1$, by the floating-colors argument, and conjecture $O(\sqrt{t})$.
• 1980s. Komlós poses the vector form — unit $\ell^2$-norm columns, constant $\ell^\infty$ discrepancy — which implies the Beck–Fiala conjecture; it circulates through Spencer's Ten Lectures (1987) as the central open problem of the area.
• 1985. Spencer (Trans. AMS) proves "six standard deviations suffice": discrepancy $6\sqrt{n}$ for $n$ sets on $n$ points, beating random signing via the partial-coloring method.
• 1998. Banaszczyk (Random Struct. Algorithms) proves the Komlós bound $O(\sqrt{\log n})$ by a recursive Gaussian-measure argument over convex bodies.
• 2010–2016. The constructive era: Bansal (2010) makes Spencer algorithmic by SDP random walks, Lovett and Meka (2012) simplify, and Bansal, Dadush, and Garg (STOC 2016) give a polynomial-time algorithm matching Banaszczyk's bound.
• 2023. Kunisky (SIAM J. Discrete Math.) constructs instances from unsatisfiable formulas with discrepancy approaching $1+\sqrt{2}$ — the strongest lower bound on the conjectured constant.
• 2025. Bansal and Jiang (arXiv:2508.03961) break the Banaszczyk barrier: $\tilde{O}((\log n)^{1/4})$ for Komlós, and the Beck–Fiala conjecture resolved for $t \ge \log^2 n$ — the first movement in nearly thirty years. The gap between $2.414\ldots$ and $\tilde{O}((\log n)^{1/4})$ is the conjecture.

Setting

Fix $n$ vectors $v_1, \dots, v_n \in \mathbb{R}^m$ with Euclidean norm $\lVert v_i \rVert_2 \le 1$. A sign vector is an $\varepsilon \in \{-1, +1\}^n$: one sign $\varepsilon_i \in \{\pm 1\}$ per vector. Writing $v_{ij}$ for the $j$-th coordinate of the vector $v_i$, the discrepancy of the family under $\varepsilon$ is the largest coordinate, in absolute value, of the signed sum $\sum_i \varepsilon_i v_i$ — that is, $\max_{j \le m} \lvert \sum_{i \le n} \varepsilon_i v_{ij} \rvert$, the $\ell^\infty$ norm of the signed sum. The Komlós property at constant $K$ — KomlosBound K — says that every such family, in every $n$ and every $m$, admits a sign vector with every coordinate of the signed sum at most $K$ in absolute value.

Set systems embed as the special case of $0/1$-incidence matrices: if $A$ is an $m \times n$ matrix of $0$s and $1$s in which every column has at most $t$ ones (every element lies in at most $t$ sets), the columns scaled by $1/\sqrt{t}$ have norm at most one, so the Komlós property gives discrepancy $K\sqrt{t}$ — the Beck–Fiala conjecture.

Formalization targets

Goal — the Komlós conjecture

$$\exists\, K \in \mathbb{R}: \quad \text{every } v_1, \dots, v_n \in \mathbb{R}^m \text{ with } \lVert v_i\rVert_2 \le 1 \text{ admits } \varepsilon \in \{\pm 1\}^n \text{ with } \max_j \Big|\sum_i \varepsilon_i v_{ij}\Big| \le K.$$

The goal fixes no value of $K$: any finite universal constant settles it, so the statement survives every improvement in the constant.

Milestones — the known ladder

Eight results over the same definitions: Beck–Fiala's $2t - 1$ for degree-$t$ set systems; Spencer's $6\sqrt{n}$ for $n$ sets on $n$ points; Banaszczyk's $O(\sqrt{\log n})$ for the Komlós setting; its corollary $O(\sqrt{t \log n})$ for set systems; the reduction "Komlós at $K$ implies Beck–Fiala at $K\sqrt{t}$"; Kunisky's lower bound $K \ge 1 + \sqrt{2}$; and the two 2025 Bansal–Jiang breakthroughs — $\tilde{O}((\log n)^{1/4})$ for the Komlós setting, and the Beck–Fiala conjecture's bound $O(\sqrt{t})$ in the regime $t = \Omega(\log^2 n)$.

Significance

The conjecture is the meeting point of the two main techniques of discrepancy theory — partial coloring and the Gaussian/convex-geometric method — and each further improvement has forced a new technique into existence. A proof would resolve the Beck–Fiala conjecture in full and sharpen the hereditary-discrepancy landscape; a disproof would break the widely-shared expectation that vector balancing is dimension-free. The problem is also a benchmark for algorithmic discrepancy: every known bound now has a polynomial-time counterpart, and the constructive tools built for it (random-walk roundings, spectral partial colorings) are used across approximation algorithms and ranging into differential privacy.

None of this literature is formalized anywhere; Mathlib has no discrepancy theory at all. The definitions here are elementary — finite sums, absolute values, one norm hypothesis — so the mission's entry cost is unusually low for an open-problem mission: the Beck–Fiala theorem and the scaling reduction are self-contained finite combinatorics, while Spencer and Banaszczyk each force a genuinely new proof technique (pigeonhole partial coloring; Gaussian measure on convex bodies) into Lean.

Difficulty

Random signs lose: they give $\Theta(\sqrt{n})$, not a constant, so the naive probabilistic argument is ruled out from the start. The Beck–Fiala argument caps discrepancy by degree, not by norm, and provably cannot be pushed below $2t - O(1)$ by its own bookkeeping. Partial coloring alone loses a logarithm through its iteration, and Banaszczyk's method is blocked at $\sqrt{\log n}$ by the Gaussian measure of the cube. The 2025 advance decouples the two methods but still pays iterated polylogarithmic factors. Nothing currently known contracts the remaining gap to a constant, and the lower bound says the constant, if it exists, is at least $1 + \sqrt{2}$ — so any proof must handle instances strictly harder than the set-system case.

Formalization scope

The Lean model commits to: vectors as EuclideanSpace ℝ (Fin m), whose norm is the $\ell^2$ norm (the hypothesis $\lVert v_i \rVert \le 1$ reads ‖v i‖ ≤ 1); the $\ell^\infty$ conclusion written coordinatewise as ∀ j, |∑ i, ε i * v i j| ≤ K, avoiding any auxiliary sup-norm structure; sign vectors as real vectors with ε i = 1 ∨ ε i = -1; and set systems as matrices A : Fin m → Fin n → ℝ with an entrywise $0/1$ hypothesis and column-degree counted by Set.ncard. Quantifier order matters everywhere: in KomlosBound K the constant is fixed before $n$ and $m$ — a $K$ depending on $n$ would make the statement the trivial $\sqrt{n}$ bound. In beck_fiala the hypothesis $t \ge 1$ is required (the degree-$0$ system has discrepancy $0 > 2t-1$ otherwise); the Banaszczyk-form bounds use $\log(n+2)$ so that the bound is positive already at $n \le 1$. In the Bansal–Jiang milestones the asymptotic $\tilde{O}$ and $\Omega$ are rendered by existential constants quantified before all instances: the hidden $\mathrm{poly}(\log\log n)$ factor becomes $(\log\log(n+8))^{\gamma}$ for some fixed $\gamma > 0$ (the inner shift $+8$ keeps the iterated logarithm positive), and the threshold $t = \Omega(\log^2 n)$ becomes $C_0 \log^2(n+2) \le t$ for some fixed $C_0 > 0$.

Welcome contributions: any milestone in any order — beck_fiala and komlos_implies_beck_fiala are self-contained finite arguments and the natural entry points; spencer_six_deviations and banaszczyk_bound each import a major technique; komlos_lower_bound needs an explicit construction and a case analysis over all sign vectors. Reusable infrastructure — partial colorings, Gaussian measure bounds for convex bodies, hereditary discrepancy — is welcome as platform theorems. The matrix Spencer conjecture, prefix discrepancy, and the Steinitz problem are related but deliberately left to future missions.

Selected references

• J. Beck, T. Fiala, "Integer-making" theorems, Discrete Applied Mathematics 3 (1981). doi:10.1016/0166-218X(81)90022-6
• J. Spencer, Six standard deviations suffice, Trans. Amer. Math. Soc. 289 (1985). doi:10.1090/S0002-9947-1985-0784009-0
• W. Banaszczyk, Balancing vectors and Gaussian measures of n-dimensional convex bodies, Random Structures & Algorithms 12 (1998). doi link
• N. Bansal, D. Dadush, S. Garg, An algorithm for Komlós conjecture matching Banaszczyk's bound, FOCS 2016 / SIAM J. Comput. arXiv:1605.02882
• N. Bansal, H. Jiang, Decoupling via affine spectral-independence: Beck–Fiala and Komlós bounds beyond Banaszczyk, 2025. arXiv:2508.03961
• D. Kunisky, The discrepancy of unsatisfiable matrices and a lower bound for the Komlós conjecture constant, SIAM J. Discrete Math. 37 (2023). arXiv:2111.02974
• B. Chazelle, The Discrepancy Method, Cambridge University Press, 2000. author's page

The problem of solving linear inequalities

The linear feasibility problem takes a matrix $A \in \mathbb{R}^{m\times n}$ and a vector $b \in \mathbb{R}^m$ and asks whether the system of $m$ linear inequalities in $n$ real unknowns

$$\{\,x \in \mathbb{R}^n \mid Ax \ge b\,\} \;\ne\; \emptyset$$

has a solution. By linear programming duality, optimizing a linear objective over such a set reduces to feasibility, so this decision problem carries the whole complexity of linear programming.

What "polynomial time" means here depends on the machine. In the bit model the input is a list of rational numbers, its size $L$ counts the bits of all numerators and denominators, and an algorithm is polynomial if it runs in time $\mathrm{poly}(m, n, L)$. In the real-number model the input is a list of $mn + m$ exact real numbers, each arithmetic operation ($+, -, \times, \div$), comparison, or memory move costs one unit, and a running time may only depend on $m$ and $n$. An algorithm polynomial in this second sense is what Smale asks for; the closely related bit-model notion — $\mathrm{poly}(m,n)$ arithmetic operations and polynomially bounded intermediate bit sizes — is called strongly polynomial. This mission fixes the real-number model precisely as a Blum–Shub–Smale (BSS) machine (Blum–Shub–Smale 1989): a finite program of instructions acting on a bi-infinite tape $\mathbb{Z} \to \mathbb{R}$ of real registers — loads of arbitrary real machine constants, exact field arithmetic at fixed addresses, two-sided tape shifts, a sign-test branch, and accept/reject — with cost equal to the number of executed instructions. The convention that costs something: the program must be uniform, one finite instruction list serving every $m$, $n$, and every real instance. Uniformity is exactly what separates the question from point-location tricks available to non-uniform families of decision trees.

Why it matters

For optimization, the question is the last gap in the complexity of its central problem. Linear programs with combinatorial structure already admit strongly polynomial algorithms — Tardos (1986) solved every LP whose running time may depend on the entries of $A$ but not on $b$ or $c$, covering network flows and all $\{0,\pm1\}$-constraint problems — and a positive answer for general LP would extend that unification to the whole class, while explaining why simplex-type methods behave so well in practice (Spielman–Teng 2004).

For the theory of computation over the reals, the problem is a benchmark for what unit-cost exact arithmetic can do: it is Problem 9 on Smale's list of mathematical problems for the twenty-first century (Smale 1998), posed in the BSS model as the real-number analogue of the P-versus-NP style questions of that program, and it interacts with polyhedral combinatorics through the polynomial Hirsch conjecture: a polynomial bound on polytope diameters is a necessary condition for any polynomial pivot rule. A problem that calibrates both the practice of optimization and the foundations of real computation is a subject, not a special case.

The question and what is known

$$\textbf{Question (Smale's 9th).}\quad \text{Is there a uniform BSS program deciding } \{x \mid Ax \ge b\} \ne \emptyset \text{ in } \mathrm{poly}(m,n) \text{ steps?}$$

The timeline splits into a negative branch (lower bounds against algorithm classes) and a positive branch (polynomial algorithms in weaker senses).

Lower bounds. Klee–Minty (1972) constructed a deformed cube on which Dantzig's largest-coefficient simplex rule visits all $2^n$ vertices; analogous exponential examples were later found for essentially every deterministic pivot rule, and randomized rules were driven to subexponential lower bounds by Friedmann–Hansen–Zwick (2011) — against upper bounds of $\exp(O(\sqrt{n \log n}))$ from Kalai (1992) and Matoušek–Sharir–Welzl (1996). On the interior-point side, Allamigeon–Benchimol–Gaubert–Joswig (2018) showed by tropical methods that log-barrier path following is not strongly polynomial, and Allamigeon–Gaubert–Vandame (2022) extended this to every self-concordant barrier: no interior-point method of that class can settle the question positively.

Polynomial algorithms in weaker senses. Khachiyan (1979/80) proved LP feasibility is polynomial in the bit model via the ellipsoid method; Karmarkar (1984) and then Renegar (1988) brought interior-point methods to $O(\sqrt{n}\,L)$ iterations. Megiddo (1984) solved LP in linear time for every fixed dimension; Tardos (1986) gave the combinatorial strongly polynomial class; Vavasis–Ye (1996) and Dadush–Huiberts–Natura–Végh (2020) replaced the bit size by condition measures of $A$ alone; Ye (2011) proved policy iteration strongly polynomial for fixed-discount Markov decision processes.

The central difficulty is visible in every positive result: each known iteration count is controlled by a scale-dependent quantity — bit length, condition number, barrier curvature — that is unbounded over the real instances with $m, n$ fixed. The naive plan, "run the ellipsoid method and round", fails at its first step in the real model: the number of iterations needed to separate a feasible system from an infeasible one grows with the thinness of the feasible set, which is not a function of $(m, n)$; no data-independent perturbation $\varepsilon$ exists when the data are arbitrary reals. All results above are proved on paper only; none has a machine-checked proof in the literature. What is already formalized, on this platform, is the substrate this mission builds on: the simplex iteration (mission Introduction to Linear Optimization IV), the ellipsoid method with its volume-halving correctness theorem (XI), interior-point path following (XII), and self-concordance with the barrier method (Convex Optimization VI).

A hierarchy of formalization targets

The mission's milestone list realizes this hierarchy in order; each level states what it deliberately leaves open.

Level 0 — the model works. A uniform BSS program decides one-variable feasibility in linear time:

$$\exists\,P,\,C\ \ \forall m,\ \forall (a,b) \in \mathbb{R}^m \times \mathbb{R}^m:\ P \text{ decides } \{x \in \mathbb{R} \mid a_i x \ge b_i\ \forall i\} \ne \emptyset \text{ within } C(m{+}1) \text{ steps}.$$

It fixes nothing about $n \ge 2$; its role is to certify that the machine model and cost semantics of the goal are non-vacuous.

Level 1 — the classical method is exponential. On the Klee–Minty cube, Dantzig's rule admits a run of

$$2^n - 1 \text{ pivots}$$

from the all-slack basis to the optimum. It leaves open all other pivot rules — extensions to further rules are welcome as strengthenings.

Level 2 — the bit model succeeds. Through the Cramer–Hadamard solution bound $|x_j| \le n!\,U^n$ and the perturbation estimates, Khachiyan's theorem: for integer data bounded by $U$, every admissible ellipsoid run decides feasibility within

$$t^* \le 10^6\,(n{+}2)^4(\log_2 U + n + 2) \text{ iterations}.$$

The generous constants are deliberate — only the polynomial order is load-bearing. This level leaves open exactly the dependence on $\log U$.

Level 3 — the goal (open). A uniform program with data-independent polynomial cost:

$$\exists\,P,\,C,\,d\ \ \forall m, n, A, b:\ P \text{ decides } \{x \mid Ax \ge b\} \ne \emptyset \text{ within } C\,(mn + m + 2)^d \text{ steps}.$$

The statement asserts only the shape of the truth — no hard-coded degree or constant — so it is stable under every future quantitative improvement. These levels do not exhaust the project: Tardos' combinatorial LP theorem, Ye's fixed-discount MDP result, and impossibility statements for restricted program classes in the style of Allamigeon–Gaubert–Vandame are natural later milestones.

Formalization scope

Polyhedra, simplex states, pivots, and ellipsoid runs are the platform's existing LinearOptimization development over Matrix (Fin m) (Fin n) ℝ, with $\{x \mid Ax \ge b\}$ as polyhedron A b; algorithms with data-dependent iteration counts are formalized as run predicates, as in the parent missions. The new SmaleNinth definitions supply what the goal genuinely needs and the run-predicate style cannot express: a concrete inductive type of BSS programs with operational semantics and unit-cost accounting, the Klee–Minty data with Dantzig's rule, and the explicit Khachiyan constants. One convention closes the degenerate escape hatch: the goal quantifies over finite BSSProgram terms under the fixed encodeLP input convention — formalizing "algorithm" as an arbitrary function $\mathbb{R}^{mn+m} \to \mathrm{Bool}$ would make the statement trivially true and is not the theorem. Division is totalized as $x/0 = 0$ and the branch test is $x_i \le 0$; both are benign for the class of programs quantified over.

The machine module is infrastructure beyond this mission — any real-number complexity statement (other Smale problems, sums-of-square-roots, BSS-completeness) can reuse it, as can any pivot-rule lower bound reuse the Klee–Minty module. Formalization forces distinctions the literature leaves informal: which machine variant carries the unit-cost claim, how ties in Dantzig's rule are resolved, and which of the interchangeable Khachiyan constants each estimate actually needs. Welcome contributions include proofs of any milestone, alternative exponential instances for other pivot rules, sharper constants in the Khachiyan module, and ports of the known strongly polynomial special cases.

Selected references

• L. Blum, M. Shub, S. Smale, On a theory of computation and complexity over the real numbers, Bull. AMS 21(1):1–46, 1989. DOI
• S. Smale, Mathematical problems for the next century, Math. Intelligencer 20(2):7–15, 1998. DOI
• V. Klee, G. J. Minty, How good is the simplex algorithm?, in Inequalities III, Academic Press, 1972, pp. 159–175.
• L. G. Khachiyan, Polynomial algorithms in linear programming, USSR Comput. Math. Math. Phys. 20:53–72, 1980. DOI
• N. Karmarkar, A new polynomial-time algorithm for linear programming, Combinatorica 4:373–395, 1984. DOI
• J. Renegar, A polynomial-time algorithm, based on Newton's method, for linear programming, Math. Programming 40:59–93, 1988. DOI
• É. Tardos, A strongly polynomial algorithm to solve combinatorial linear programs, Oper. Res. 34(2):250–256, 1986. DOI
• N. Megiddo, Linear programming in linear time when the dimension is fixed, J. ACM 31(1):114–127, 1984. DOI
• G. Kalai, A subexponential randomized simplex algorithm, STOC 1992. DOI
• O. Friedmann, T. D. Hansen, U. Zwick, Subexponential lower bounds for randomized pivoting rules for the simplex algorithm, STOC 2011. DOI
• D. A. Spielman, S.-H. Teng, Smoothed analysis of algorithms: why the simplex algorithm usually takes polynomial time, J. ACM 51(3):385–463, 2004. DOI
• S. A. Vavasis, Y. Ye, A primal-dual interior point method whose running time depends only on the constraint matrix, Math. Programming 74:79–120, 1996. DOI
• Y. Ye, The simplex and policy-iteration methods are strongly polynomial for the Markov decision problem with a fixed discount rate, Math. Oper. Res. 36(4):593–603, 2011. DOI
• X. Allamigeon, P. Benchimol, S. Gaubert, M. Joswig, Log-barrier interior point methods are not strongly polynomial, SIAM J. Appl. Algebra Geom. 2(1):140–178, 2018. DOI
• X. Allamigeon, S. Gaubert, N. Vandame, No self-concordant barrier interior point method is strongly polynomial, STOC 2022. arXiv
• D. Dadush, S. Huiberts, B. Natura, L. A. Végh, A scaling-invariant algorithm for linear programming whose running time depends only on the constraint matrix, STOC 2020. arXiv
• D. Bertsimas, J. N. Tsitsiklis, Introduction to Linear Optimization, Athena Scientific, 1997 (Chapters 3, 8, 9 — formalized in the Introduction to Linear Optimization mission series).
• B. Korte, J. Vygen, Combinatorial Optimization: Theory and Algorithms, 6th ed., Springer, 2018, §4.1–4.5.

Motivation

A robust counterpart draws a hard line. Inside the uncertainty set the constraint must hold; outside it, nothing is promised — and in a real problem the perturbation does sometimes land outside. Chapter 3 answered this for linear problems with the globalized robust counterpart: keep the constraint exactly on the normal range $\mathcal{Z}$, and let it degrade at a controlled rate outside, proportionally to the distance from $\mathcal{Z}$. That mission published Proposition 3.2.1, which says the GRC of an uncertain linear inequality is equivalent to two ordinary robust counterparts.

Chapter 11 of Ben-Tal, El Ghaoui and Nemirovski, Robust Optimization (Princeton, 2009) does the same for conic constraints, and the move is not routine. The left hand side of a conic constraint is a vector, not a scalar, so "the constraint is violated by at most $\alpha \,\mathrm{dist}(\zeta, \mathcal{Z})$" has no direct meaning. What replaces it is the observation that a scalar inequality $a^Ty - b \le 0$ is the inclusion $a^Ty - b \in \mathbf{Q} \equiv \mathcal{R}_-$, and that the violation is the distance from the left hand side to $\mathbf{Q}$. In that form the notion lifts verbatim, and the whole chapter follows.

Setting

Definition 11.1.2. Consider an uncertain convex constraint

$$\Bigl[P^0 + \sum_{\ell=1}^L \zeta_\ell P^\ell\Bigr]y - \Bigl[p^0 + \sum_{\ell=1}^L \zeta_\ell p^\ell\Bigr] \ \in\ \mathbf{Q}, \tag{11.1.4}$$

with $\mathbf{Q} \subseteq \mathcal{R}^k$ nonempty, closed and convex. Let the perturbation space split as $\mathcal{R}^L = \mathcal{R}^{L_1}\times\cdots\times\mathcal{R}^{L_S}$, each factor carrying a normal range $\mathcal{Z}^s$, a closed convex cone $\mathcal{L}^s$ and a norm $\|\cdot\|_s$, and let $\|\cdot\|_{\mathbf{Q}}$ be a norm on $\mathcal{R}^k$. A candidate $y$ is robust feasible with global sensitivities $\alpha_s$ if

$$\mathrm{dist}\bigl(P(y,\zeta), \mathbf{Q}\bigr) \ \le\ \sum_{s=1}^S \alpha_s\, \mathrm{dist}(\zeta^s, \mathcal{Z}^s|\mathcal{L}^s) \qquad \forall\, \zeta \in \mathcal{Z} + \mathcal{L}, \tag{11.1.6}$$

where $\mathrm{dist}(u,\mathbf{Q}) = \min_{v\in\mathbf{Q}}\|u - v\|_{\mathbf{Q}}$ and $\mathrm{dist}(\zeta^s,\mathcal{Z}^s|\mathcal{L}^s) = \min\{\|\zeta^s - v\|_s : v \in \mathcal{Z}^s,\ \zeta^s - v \in \mathcal{L}^s\}$.

The object that makes the analysis work is the recessive cone of $\mathbf{Q}$ (Definition 11.3.1): for any $\bar x \in \mathbf{Q}$,

$$\mathrm{Rec}(\mathbf{Q}) = \{h : \bar x + th \in \mathbf{Q}\ \ \forall t \ge 0\},$$

which does not depend on $\bar x$ and is a nonempty closed convex cone.

Formalization targets

Goal — Proposition 11.3.3, the decomposition of the conic GRC

A candidate $y$ is feasible for the GRC (11.1.6) if and only if it satisfies the system

$$\text{(a)}\quad \Bigl[P^0 + \sum_\ell \zeta_\ell P^\ell\Bigr]y - \Bigl[p^0 + \sum_\ell \zeta_\ell p^\ell\Bigr] \in \mathbf{Q} \qquad \forall \zeta \in \mathcal{Z} = \mathcal{Z}^1\times \cdots\times\mathcal{Z}^S,$$ $$\text{(b}_s)\quad \mathrm{dist}\Bigl(\sum_{\ell} [P^\ell y - p^\ell](E_s\zeta^s)_\ell,\ \mathrm{Rec}(\mathbf{Q})\Bigr) \ \le\ \alpha_s \qquad \forall \zeta^s \in \mathcal{L}^s \text{ with } \|\zeta^s\|_s \le 1, \quad s = 1,\ldots,S .$$

Line (a) is the ordinary robust counterpart over the normal range. Each line (b$_s$) is a bounded semi-infinite constraint — the perturbation ranges over the unit ball of a cone, not over an unbounded set — measuring the distance to the recessive cone rather than to $\mathbf{Q}$ itself.

Supporting targets

$$\text{(Def 11.3.1)}\quad \mathrm{Rec}(\mathbf{Q}) \text{ is independent of the base point and is a nonempty closed convex cone},$$ $$\text{(Ex 11.3.2)}\quad \mathbf{Q} \text{ bounded} \Rightarrow \mathrm{Rec}(\mathbf{Q}) = \{0\}; \quad \mathbf{Q} \text{ a cone} \Rightarrow \mathrm{Rec}(\mathbf{Q}) = \mathbf{Q}; \quad \mathrm{Rec}\{u : Au - b \in \mathbf{K}\} = \{h : Ah \in \mathbf{K}\},$$ $$\text{(Prop 11.4.1)}\quad \Psi_\Xi(\mathcal{M}) = \Psi_{\Xi_*}(\mathcal{M}^*), \qquad \Psi(\mathcal{M}) = \max\{\mathrm{dist}_{\|\cdot\|_F}(\mathcal{M}e, \mathbf{K}^F) : e \in \mathbf{K}^E,\ \|e\|_E \le 1\} .$$

Significance

The goal is the chapter's structural result and it does exactly what Proposition 3.2.1 did one level down: it converts a single semi-infinite constraint over an unbounded perturbation set into a robust counterpart over the bounded normal range plus finitely many constraints over unit balls. That matters because every tractability result of Chapters 6 to 9 is about bounded uncertainty sets; without the decomposition none of them applies to a GRC.

The two halves of the decomposition are genuinely different objects. Line (a) is familiar. Lines (b$_s$) are not: they measure the distance from a linear image of a ball to the recessive cone, and that is the function

$$\Psi(\mathcal{M}) = \max\bigl\{\mathrm{dist}(\mathcal{M}e, \mathbf{K}^F) : e \in \mathbf{K}^E,\ \|e\|_E \le 1\bigr\}$$

of §11.4, which is almost a norm on linear maps — nonnegative, positively homogeneous, subadditive, but neither symmetric nor strictly positive. Proposition 11.4.1 says this function is self-dual in the precise sense that $\Psi$ of a map with respect to a setup equals $\Psi$ of the adjoint map with respect to the dual setup: dual norms, dual cones, source and destination exchanged. That single identity is what lets every bound on $\Psi$ be computed on whichever side of the duality is tractable, and it is the engine of §11.4's tractability results.

The recessive cone results are the vocabulary. The one that earns its place is $\mathrm{Rec}\{u : Au - b \in \mathbf{K}\} = \{h : Ah \in \mathbf{K}\}$: the conic sets of this book are all of that form, so it says the recessive cone of every constraint in sight is computed by deleting the constant term.

Difficulty

The goal is an equivalence and the two directions are asymmetric.

Forward — GRC implies the system — is where the recessive cone is discovered rather than used. Fix $\bar\zeta \in \mathcal{Z}$ and $\zeta^s$ in the unit ball of $\mathcal{L}^s$, and run $\zeta_i = \bar\zeta + i\,\zeta^s$ out along the cone. The GRC bounds the distance to $\mathbf{Q}$ by $\alpha_s i$, so there are $q_i \in \mathbf{Q}$ with $\|P(y,\bar\zeta) + i\Phi(y)E_s\zeta^s - q_i\|_{\mathbf{Q}} \le \alpha_s i$; the rescaled points $q_i/i$ stay bounded, and a limit point of them lies in $\mathrm{Rec}(\mathbf{Q})$ by the limit characterization of the recessive cone. This is a genuine compactness argument, and it is why the recessive cone — not $\mathbf{Q}$ — is what appears in lines (b$_s$).

Backward is a decomposition-and-assemble: split each $\zeta^s = \bar\zeta^s + \delta^s$ with $\bar\zeta^s \in \mathcal{Z}^s$, $\delta^s \in \mathcal{L}^s$ realizing the distance, get a point of $\mathbf{Q}$ from line (a) and a recession direction from each line (b$_s$), and add them — using that $\mathbf{Q} + \mathrm{Rec}(\mathbf{Q}) \subseteq \mathbf{Q}$.

Proposition 11.4.1 is a chain of polarity identities: the polar of $X + K$ is $X^o \cap (-K_*)$ for compact convex $X$ containing the origin, the polar of a norm ball of radius $\alpha$ is the dual-norm ball of radius $1/\alpha$, and bipolarity. Each step is standard and the composition is not.

Formalization scope

Built on the module published by the third mission of this series, which carries the linear-case globalized robust counterpart and the dual cone. New here: norms as functions with their defining properties, dual norms, the two distances, the recessive cone, the conic GRC, and the function $\Psi$.

Conventions committed to:

• Norms are functions carrying an explicit predicate, not typeclass instances. Chapter 11 quantifies over arbitrary norms $\|\cdot\|_{\mathbf{Q}}$ and $\|\cdot\|_s$ on fixed coordinate spaces, and a statement must be able to range over them; a typeclass instance would fix one norm per type. IsNormOn bundles definiteness, absolute homogeneity and the triangle inequality, and nonnegativity follows from them.
• The dual norm is a predicate, not a construction. $\|f\|^* = \sup\{f^Te : \|e\| \le 1\}$ is asserted as a least upper bound of the set of values, so no supremum is taken on faith.
• Distances are infima, not minima. The source writes $\min$, which is correct because the sets are closed; writing $\inf$ avoids carrying an attainment proof into every statement, and agrees with the minimum whenever the source's own hypotheses hold.
• The recessive cone is indexed by a base point. Definition 11.3.1 defines it at an arbitrary $\bar x \in \mathbf{Q}$ and then asserts independence of the choice; that assertion is one of the published items, so the definition cannot presuppose it.
• The perturbation is carried as a family of blocks, $\zeta = (\zeta^1,\ldots,\zeta^S)$ with $\zeta^s \in \mathcal{R}^{L_s}$, rather than as a single vector in $\mathcal{R}^L$ together with the embeddings $E_s$. This is the same data and removes the index bookkeeping of $E_s$ from every statement.
• $\Psi$ is a predicate on a real number, as for the dual norm and for the same reason.
• §11.2 and §11.5 are out of scope: the definition of a tight safe approximation of a GRC and the worked analysis of nonexpansive dynamical systems. The first is a definition the chapter uses only to phrase §11.4's programme, the second an application.

Selected references

• A. Ben-Tal, L. El Ghaoui and A. Nemirovski, Robust Optimization, Princeton University Press, 2009. Chapter 11, §§11.1, 11.3-11.4, pp. 281-294; Chapter 3 for the linear case. https://doi.org/10.1515/9781400831050
• A. Ben-Tal, S. Boyd and A. Nemirovski, Extending scope of robust optimization: comprehensive robust counterparts of uncertain problems, Mathematical Programming 107 (2006), 63-89. https://doi.org/10.1007/s10107-005-0679-z
• R. T. Rockafellar, Convex Analysis, Princeton University Press, 1970. https://doi.org/10.1515/9781400873173

Motivation

Sequential planning problems — inventory replenishment, hydro-thermal power scheduling, asset-liability management — routinely span more than two decision epochs, with information about the future revealed gradually as each period unfolds. A two-stage recourse model (decide now, observe once, recourse once) is too coarse for these: it either collapses the whole horizon into a single "wait and see" observation or forces an ad-hoc rolling-horizon heuristic with no optimality guarantee. The multistage stochastic program is the natural model that keeps the full sequence of decisions and observations, and Benders (L-shaped) decomposition is the workhorse algorithm the field has used to solve it since Van Slyke and Wets [1969] introduced it for the two-stage case. Ho and Manne [1974] and Glassey [1973] first proposed nested decomposition for deterministic multistage models; Louveaux [1980] extended it to multistage quadratic stochastic programs, and Birge [1985] gave the linear multistage generalization this mission formalizes, later implemented at scale by Pereira and Pinto [1985] and Gassmann [1990] and still the basis of production stochastic-programming solvers today.

Setting

A multistage stochastic linear program unfolds over $H$ stages $t = 1,\dots,H$. At each stage, uncertainty resolves into one of finitely many realizations, so the whole process of realizations forms a scenario tree: a single scenario at $t=1$ (the root), branching into finitely many scenarios at $t=2$, each of those again branching at $t=3$, and so on. Write $k$ for a scenario (a tree node) and $a(k)$ for its ancestor, the scenario at stage $t-1$ that $k$ descends from; $D^{t+1}(j)$ is the set of scenario $j$'s descendants at the next stage. Each scenario $k$ at stage $t$ carries its own decision vector $x^t_k \ge 0$, bounded above ($x^t_k \le u^t_k$, coordinatewise), subject to the linear constraint

$$W^t x^t_k = h^t_k - T^{t-1}_k x^{t-1}_{a(k)},$$

where the recourse matrix $W^t$ depends only on the stage (fixed recourse) while the transition matrix $T^{t-1}_k$ and right-hand side $h^t_k$ may vary scenario by scenario. Stacking every scenario's constraint over the whole tree gives the deterministic equivalent linear program, minimizing the probability-weighted total cost $\sum_k p_k (c^t_k)^\top x^t_k$ over this feasible region — problem (3.4.1) in the source.

The nested L-shaped method solves (3.4.1) by decomposition rather than forming this (typically enormous) single LP directly. Each scenario $k$ owns a small subproblem, $\mathrm{NLDS}(t,k)$, that looks exactly like a two-stage L-shaped subproblem: it has $k$'s own constraint and bound, plus a running set of feasibility cuts and optimality cuts accumulated so far, plus, if $k$ has descendants, an approximation variable $\theta^t_k$ standing in for the (unknown, convex, piecewise-linear) future cost $Q^{t+1}_k$ of everything downstream of $k$. Solving $\mathrm{NLDS}(t,k)$ either finds it infeasible — in which case a feasibility cut is derived from the infeasibility certificate and sent up to $k$'s parent — or finds an optimal dual solution, whose aggregate over all of $j$'s children (weighted by conditional probability) becomes a candidate optimality cut for $j = a(k)$. The method sweeps forward and backward across the tree, feasibility and optimality cuts accumulating at every internal node, until no node's subproblem produces a fresh cut.

Formalization targets

Goal (Chapter 6, Theorem 1)

$$\text{if every }\Xi_t\text{ is finite and every }x_t\text{ has a finite upper bound, then the nested L-shaped method}$$ $$\text{converges finitely to an optimal solution of the deterministic equivalent (3.4.1), or correctly certifies its infeasibility.}$$

This is the chapter's only numbered result and the weakest faithful statement of "the method works": it makes no claim about the number of iterations beyond finiteness, and none about which sequencing protocol (forward-forward-back, or any other) is used to choose which subproblem to solve next.

Significance

Finite convergence is what separates an algorithm from a heuristic: without it, nothing rules out an infinite sequence of ever-finer cuts that never certifies optimality or infeasibility. Birge's 1985 result is the reason nested Benders decomposition can be used as an exact method rather than an approximation, and every later refinement (bunching, sifting, multicuts, parallel implementations, all mentioned in the source text) modifies how cuts are generated or which subproblem is solved next without touching this finiteness guarantee — they are all still instances of the same cut-generation mechanism this mission formalizes. The two-stage case (Chapter 5, Theorem 2) is the $H=2$ special case of this theorem; the mission's tree-indexed state and transition relation are written to specialize to the two-stage development directly when the tree has one branching level, though the two developments are not connected by an import (see Formalization scope). No machine-checked proof of either the two-stage or multistage case appears to exist prior to this series; formalizing it here produces the first Lean statement of the mechanism nested Benders decomposition rests on.

Difficulty

The obvious first idea — prove finiteness by bounding the total number of cuts a node can ever receive, the way a flat scenario set bounds the two-stage method's cut count by its number of LP bases — fails because a node's own subproblem is not a fixed-size LP: every cut recorded at node $k$ becomes a new row of $k$'s own constraint set, so the "number of possible bases" at $k$ keeps changing as the algorithm runs, and the bound at $k$ depends recursively on how many cuts $k$'s own children could ever produce. The book's actual argument (p. 290) is a genuine induction on the stage index, from the last stage backward: assume the bound holds for every node at stage $t+1$, then combinatorially bound the finite number of extended bases at stage $t$ that this permits, then take the finite union over every possible extension size. This mission's Lean development commits to a scope that keeps a node's basis a fixed-size object (see below) rather than re-deriving that combinatorial bound.

Formalization scope

Every stage shares one decision dimension $n$ and one constraint dimension $m$ (Fin n, Fin m); the book allows these to vary by stage but nothing in Theorem 1's statement needs that generality. Scenario probabilities p are the unconditional probability of reaching a node, required strictly positive and summing to $1$ within each stage (Instance.hp_pos, Instance.hp_sum); the aggregation formulas use only the ratio $p_k/p_j$ for $k$ a child of $j$, which reads the same whether p is unconditional or conditional, so this is a normalization choice, not a substantive restriction. The upper bound ub is ℝ-valued rather than extended-real-valued, which is Theorem 1's own hypothesis ("finite upper bounds"), not an added convention.

The one deliberate scope-narrowing choice, flagged here and in MODERATION_NOTES.md, and strengthened in this revision after moderator review (2026-09-19, CHANGES_REQUESTED.md #2): a node $k$'s dual witness (Basis, FeasBasis) is read off $k$'s original constraint (1.2) alone — the fixed-size recourse matrix $W^{\mathrm{stage}(k)}$ — never off the extended constraint set (1.2)-(1.4). The gap this leaves is broader than "accumulated cuts are ignored": $k$'s own continuation variable $\theta_k$ — present in (1.1)'s objective, and fixed to $0$ from Step 0 onward, not merely absent until cuts accumulate — has no representation at all in Basis, multiplier, basisValue, or the optimality-cut coefficients optCutCoeffs computes for a parent $j$ of $k$. Consequently, whenever a child $k$ used in an optimality cut is itself an interior node ($k$ has children of its own, i.e. $\mathrm{stage}(k) < H-1$, which happens for every $H \geq 3$ tree), the mechanized cut coefficients are not the book's $(E^{t-1}_j, e^{t-1}_j)$ of Eq. (1.1) and are not the printed algorithm's mechanism at that node — they are the dual of $k$'s plain sub-LP alone, omitting $k$'s own contribution to the recourse value entirely, not only the portion contributed by $k$'s accumulated cuts. This gap is inert exactly when every child aggregated in a cut is a last-stage node ($H \le 2$, where the mechanism coincides with the already-published two-stage sibling 05-two-stage-methods) and active for every deeper cut, which is most of what a general Tree H actually exercises. Concretely: as mechanized, the optimality-cut half of Step (Bases.optCutCoeffs, Step.opt) is faithful to the printed nested L-shaped method's cut-generation step only when every child it aggregates over is a last-stage node; for an interior child it computes a value that omits that child's own $\theta$ term rather than the book's recursive one. The feasibility-cut half (Bases.feasCutCoeffs, Step.feas) has no such gap — feasibility does not involve $\theta$ at any stage — and the tree/instance layer (Tree, Instance) and the goal theorem's own outer shape are unaffected: thm1_finite_convergence's statement (existence of a finite, Step-reachable state that is infeasible-certified or globally optimal) is not weakened, but the reader should treat the mechanized Step relation itself, for H ≥ 3, as a documented variant of Steps 1-2 rather than a literal transcription of them at every node — see STATUS.md's Revision section for the moderator exchange this responds to. Reworking cut generation to consume each child's own current $(x_k, \theta_k)$ witness directly, so that an interior child's continuation value is no longer dropped, is left to a future revision; it is a materially larger change (the child's local optimum is then piecewise-linear rather than linear in its own parent's decision, so the duality argument needs a genuinely different — not merely extended — basis notion) than this session's time budget allows. This keeps every basis type a fixed-size Fin m → Fin n object, exactly as in the two-stage method, and keeps the algorithm's finite-step bound an explicit, provable cardinality (|Node × FeasBasis| + |Node → Basis|) rather than the book's own implicit, recursively-defined one. The trivializing formalization this scope choice must not fall into — declaring victory by proving the plain two-stage case is what convergence "reduces to" without ever quantifying over the tree — is avoided because every definition and the goal statement itself are stated for a general Tree H with unrestricted branching, not merely $H = 2$; what is disclosed above is a gap in how faithfully Step models the book's own cut-generation mechanism at depth, not a restriction of the statement to $H = 2$.

Reusable beyond this mission: Def_StochasticProg_Multistage_Tree (the finite scenario tree) is a natural building block for 07-integer-programs (an integer restriction of the same two-stage subproblem) and 10-multistage-approximations (multistage Jensen bounds, which need the same tree). Contributions welcome: a faithful account of the extended-basis induction sketched above, and a formalization of Chapter 6, Theorem 3 (finite termination of the quadratic nested decomposition of Section 6.2), which this mission omits for time (see STATUS.md).

Selected references

• J.R. Birge, "Decomposition and Partitioning Methods for Multistage Stochastic Linear Programs", Operations Research 33(5), 1985.
• R.M. Van Slyke, R. Wets, "L-Shaped Linear Programs with Applications to Optimal Control and Stochastic Programming", SIAM Journal on Applied Mathematics 17(4), 1969. https://doi.org/10.1137/0117061
• H.I. Gassmann, "MSLiP: A Computer Code for the Multistage Stochastic Linear Programming Problem", Mathematical Programming 47, 1990. https://doi.org/10.1007/BF01580858
• M.V.F. Pereira, L.M.V.G. Pinto, "Stochastic Optimization of a Multireservoir Hydroelectric System: A Decomposition Approach", Water Resources Research 21(6), 1985. https://doi.org/10.1029/WR021i006p00779
• J.R. Birge, F. Louveaux, Introduction to Stochastic Programming, 2nd ed., Springer Series in Operations Research and Financial Engineering, 2011. https://doi.org/10.1007/978-1-4614-0237-4

Motivation

Most stochastic programs cannot be solved exactly: the expectation defining the objective is an integral over a continuous or high-dimensional random parameter, and evaluating it exactly is as hard as the optimization itself. The standard remedy is Monte Carlo: draw a sample of size ν from the random parameter, replace the true expectation by the sample average, and solve the resulting finite-dimensional "sample average approximation" (SAA) instead. This only helps if the SAA's optimal value and optimal solution actually converge to the true problem's as ν → ∞, and if that convergence is fast enough to be useful with a sample size one can actually draw and solve. Birge & Louveaux's Chapter 9, §9.5, states the two central asymptotic results that justify this approach for a general (not necessarily linear, not necessarily two-stage) stochastic program: a central limit theorem describing the SAA optimal value's fluctuations around the truth (Theorem 6, after Shapiro [1991]), and an exponential-rate large-deviation bound on how quickly both the SAA value and the SAA solution concentrate near their true counterparts as the sample grows (Theorem 7, after Dai, Chen & Birge [2000]). This mission formalizes both statements.

Setting

Fix a feasible set X ⊆ ℝⁿ of first-stage decisions and an outcome space Ξ carrying a σ-algebra. The book considers the general stochastic program

z* = inf_{x ∈ X} ∫_Ξ g(x,ξ) P(dξ),                                                        (5.1)

with g : ℝⁿ × Ξ → ℝ an abstract integrand — no longer specialized to the two-stage recourse cost Q(x,ξ) of Chapters 3–7, matching the book's own level of generality at this point in §9.5 — and ξ a random element of (Ξ, 𝓑, P). Given an i.i.d. sample ξ₁, ξ₂, … from P, the sample average approximation of size ν is

zν = inf_{x ∈ X} (1/ν) Σᵢ₌₁^ν g(x,ξᵢ) .                                                    (5.2)

Both z* and zν are attained (an optimal solution x* of (5.1); a random optimal solution xν(ω) of (5.2) at each sample outcome ω). The two chapter results describe, in different regimes, how (zν, xν) relates to (z*, x*) as ν → ∞.

Formalized in this mission: X sits in EuclideanSpace ℝ (Fin n); the sample is a sequence ξ : ℕ → Ω → Ξ on an ambient probability space (Ω, P), independent and identically distributed (Mathlib's iIndepFun/IdentDistrib); z*, x*, zν, xν are given as hypotheses that pin them down as the optimal value and an optimal point of (5.1)/(5.2) (a lower bound over X plus attainment at the named point), rather than computed via sInf/sSup of an image set — Real's extended-real infimum returns the junk value 0 on an unbounded-below or empty set, which would silently misstate the theorems if X, g are only assumed as loosely as the book states them.

Formalization targets

Goal — Chapter 9, Theorem 7 (p. 412)

∀ ε>0, ∃ α>0, ∃ β>0,
  (∀ ν>0, P[|zν − z*| ≥ ε] ≤ α·e^{−βν})
  ∧ (x* the unique optimal solution of (5.1) → ∀ ν≥1, P[‖xν − x*‖ ≥ ε] ≤ α·e^{−βν})

under the moment hypothesis: there exist a>0, θ₀>0, η : Ξ → ℝ with |g(x,ξ)| ≤ a·η(ξ) for all x ∈ X, and E[e^{θ·η(ξ)}] < ∞ for every θ ∈ [0,θ₀]. This is the mission's goal because it is a clean, self-contained existential-constants statement — no algorithm to define, unlike most of the chapter's other convergence results — and because, like Chunk 03's Theorem 6(a), the book's own proof cites an external paper (Dai, Chen & Birge [2000], Theorems 3.1–3.2) and gives no in-text derivation: the statement itself, not a derivation from a preceding numbered result of this book, is the mission's content.

Milestone — Chapter 9, Theorem 6 (p. 411)

X compact, g(x,·) measurable ∀x∈X, g Lipschitz in x with an L²(μ) envelope a,
x0 the unique minimizer of x ↦ E g(x) over X
  ⟹ √ν·[zν − E g(x0)] converges in distribution to N(0, Var g(x0))

Included as a milestone (not used in Theorem 7's proof, which the book does not give — see above) because it is the chapter's other general SAA convergence result, standing on the same setup (5.1)–(5.2), and because Mathlib's MeasureTheory.Function.ConvergenceInDistribution (the TendstoInDistribution predicate) plus Probability.Distributions.Gaussian.Real (gaussianReal) and Mathlib's own i.i.d. central limit theorem (ProbabilityTheory.tendstoInDistribution_inv_sqrt_mul_sum_sub) supply exactly the vocabulary needed to state — not prove — a faithful weak-convergence-to-Gaussian conclusion. Chunk 09's BRIEF.md flagged this as a milestone to attempt "only if your workspace has enough of a weak-convergence/CLT toolkit in Mathlib to state it faithfully"; the toolkit is present (verified directly, not assumed from substrate.md, which predates this rev's addition of ConvergenceInDistribution.lean), so it is included.

Significance

Every practical Monte Carlo solution method for stochastic programming — every discretization, every scenario-reduction heuristic, every "solve on a sample and hope" approach used throughout the rest of the book and the wider literature — rests on exactly these two results: that the SAA converges at all (Theorem 6's CLT gives the asymptotic distribution of the error) and that it converges fast enough to bound the error at a finite, computable sample size (Theorem 7's exponential rate). Formalizing them gives Prove2Me a first foothold in convergence-rate theory for stochastic optimization under sampling, a genre distinct from the concentration-of-measure results already reachable via Mathlib's sub-Gaussian machinery (Probability/Moments/SubGaussian.lean): sub-Gaussian concentration bounds a fixed-size sample's deviation from its own mean, not the rate-in-ν convergence of a nested sequence of optimization problems' values and solutions to a limiting problem's — the object Theorem 7 is actually about.

Difficulty

Theorem 6 needs a functional/uniform argument over the whole feasible set X (not the plain i.i.d. CLT at the single point x0) to control the interaction between sampling noise and the optimization over x; the book states it without proof, citing Shapiro [1991]. Theorem 7's constants α, β are produced by a large-deviation argument specific to the exponential-moment condition, again cited rather than derived in the book. Both are left as sorry; the value of this mission is the faithful statement, matching the difficulty pattern already established for Chunk 03's Theorem 6(a) (a result the book itself only cites).

Formalization scope

• Existential constants left abstract, never sharpened or weakened. Theorem 7's α, β are ∃-bound exactly as the book leaves them (trap 8 of reference/FAITHFULNESS_TRAPS.md: the existentials sit outside every quantifier they must be uniform over — in particular outside the ∀ ν). No closed form for α, β in terms of a, θ0, ε is invented.
• The book's own typo is corrected, and the correction is flagged. The printed (5.8) reads P[E[zν − z*)] ≥ ε] ≤ αe^{−βν} — an unmatched parenthesis and a stray E[·] around a quantity that is already deterministic. milestones.yaml/MODERATION_NOTES.md quote the typo verbatim; the Lean and natural_language_statement use the unambiguous P[|zν − z*| ≥ ε] the surrounding prose (and every other occurrence of this quantity in the section) plainly intends.
• g is left fully abstract, not specialized to the two-stage recourse cost Q(x,ξ) of Chunks 03–07, matching §9.5's own generality and keeping this mission independent of every other chunk's namespace (no cross-chunk import, per missions/README.md's "Prior art" column for this chunk: "none expected").
• z*, x*, zν, xν are hypothesis-characterized, not sInf/sSup-defined, to avoid the real extended-value junk-value trap (trap 5) discussed under Setting above.
• Measurability of zν, xν is an added hypothesis (hzSAA_meas/hxSAA_meas/hzSAA_meas in Theorem 6), not derivable from the other hypotheses since g is abstract; the book is silent on this technical point, standard for an applied convergence theorem, but Lean's P {ω | …} needs it for the displayed probability to be the actual measure of the event rather than an outer-measure value on a possibly non-measurable set.
• Convergence in distribution (Theorem 6) is formalized via Mathlib's TendstoInDistribution, with the limiting Gaussian supplied as an explicit random variable Y on a separate probability space with HasLaw Y (gaussianReal 0 σ²) P' — the same pattern Mathlib's own CLT (tendstoInDistribution_inv_sqrt_mul_sum_sub) uses for its own conclusion.
• Trivialization risk (this chapter's own, beyond paper.md's book-wide list item 5). A formalization that quantifies α, β universally, or with an invented closed form, would assert something the book's proof (cited, not given) does not establish; a formalization of Theorem 7 that used a computable sInf-defined zν on a set that is not shown bounded below would let the conclusion hold vacuously via the junk value 0, independent of the genuine large-deviation content — both are excluded by the choices above.

Selected references

• Birge, J.R., Louveaux, F. Introduction to Stochastic Programming, 2nd ed., Springer 2011, Chapter 9, §9.5 (pp. 409–412).
• Shapiro, A. "Asymptotic properties of statistical estimators in stochastic programming." Annals of Statistics 19 (1991), 1463–1466 — proof of Theorem 6 (their Theorem 3.3).
• Dai, L., Chen, C.-H., Birge, J.R. "Convergence properties of two-stage stochastic programming." Journal of Optimization Theory and Applications 106 (2000), 489–509 — proof of Theorem 7 (their Theorems 3.1–3.2).
• King, A.J., Rockafellar, R.T. "Asymptotic theory for solutions in statistical estimation and stochastic programming." Mathematics of Operations Research 18 (1993), 148–162 — the general theory of §9.5's opening (Theorem 5), the chapter's third general result, not formalized here (see STATUS.md for why it is out of scope).

Motivation

Gradient descent's convergence rate for a general smooth convex problem is $O(1/k)$ in the function-value gap; Nemirovski and Yudin (1983) proved that no first-order method can do better than $O(1/k^2)$ is achievable, and Nesterov (1983, 1988, 2004) constructed the first method attaining it — the accelerated (or "fast") gradient method. For thirty years this was the standard route to $O(1/k^2)$-rate solvers in convex optimization, and the technique underlies essentially every modern accelerated first-order method used at scale in machine learning (accelerated SGD, momentum methods, Nesterov-style extensions of Adam). The two building blocks this mission formalizes on the way there — subgradient descent (Polyak, 1960s) and mirror descent (Nemirovski & Yudin, 1983) — are themselves the default tools whenever the objective is nonsmooth or the constraint set's natural geometry is not Euclidean (e.g. the probability simplex, where mirror descent with the entropic distance-generating function beats projected subgradient descent by a $\sqrt{n/\ln n}$ factor).

Setting

Fix a nonempty closed convex set $X$ (in Lean: a normed real vector space $E$, X : Set E) and a convex $f : X \to \mathbb{R}$; write $f^* := \min_{x\in X} f(x)$ and $x^*$ for an arbitrary minimizer. The projected-subgradient update is $x_{t+1} := \arg\min_{x\in X}\gamma_t\langle g(x_t),x\rangle + \tfrac12\|x-x_t\|_2^2$ for a subgradient $g(x_t)\in\partial f(x_t)$ and stepsize $\gamma_t>0$. Its generalization, mirror descent, replaces the Euclidean proximal term with a Bregman divergence $V(x,z) := \nu(z) - \nu(x) - \langle\nabla\nu(x),z-x\rangle$ built from a 1-strongly-convex distance-generating function $\nu$ with respect to a general norm $\|\cdot\|$ (dual norm $\|\cdot\|_*$): $x_{t+1} := \arg\min_{x\in X}\gamma_t g_t(x) + V(x_t,x)$, where $g_t$ is now a continuous linear functional (a subgradient in the dual space, since the norm need not come from an inner product). Choosing $\nu(x)=\|x\|_2^2/2$ recovers $V(x,z) = \|z-x\|_2^2/2$ and the plain subgradient update as a special case.

The accelerated gradient method additionally assumes $f$ has $L$-Lipschitz gradient ($f(y)-f(x)-\langle f'(x),y-x\rangle \le \tfrac{L}{2}\|y-x\|^2$) and is $\mu$-generalized-strongly-convex w.r.t. $V$ ($f(x)+\langle f'(x),y-x\rangle+\mu V(x,y)\le f(y)$ for $\mu\ge0$), and tracks three coupled sequences from $(x_0,\bar x_0)\in X\times X$:

$$\tilde x_t = (1-q_t)\bar x_{t-1}+q_tx_{t-1},\quad x_t = \arg\min_{x\in X}\{\gamma_t[\langle f'(\tilde x_t),x\rangle+\mu V(\tilde x_t,x)]+V(x_{t-1},x)\},\quad \bar x_t = (1-\alpha_t)\bar x_{t-1}+\alpha_tx_t.$$

Formalization targets

Goal — Theorem 3.6, closed-form rate

With $q_t=\alpha_t=\tfrac{2}{t+1}$, $\gamma_t=\tfrac{t}{2L}$ and $\mu=0$:

$$f(\bar x_k) - f(x^*) \le \frac{4L}{k(k+1)}V(x_0,x^*).$$

Supporting milestones, in attack order

• Lemma 3.1 / Theorem 3.1 (Euclidean case): the three-point inequality for the plain projected-subgradient step, and the resulting $\sum_t \gamma_t[f(x_t)-f(x)] \le \tfrac12(\|x-x_s\|_2^2 + M^2\sum_t\gamma_t^2)$ bound under $M$-Lipschitz $f$.
• Lemma 3.4 / Theorem 3.5 (general-norm mirror descent): the same two results with the squared Euclidean distance replaced by $V$ and the Euclidean norm by a general dual pair $\|\cdot\|,\|\cdot\|_*$.
• Proposition 3.1: the one-step accelerated-method recursion $f(\bar x_t)-f(x)+\alpha_t(\mu+ 1/\gamma_t)V(x_t,x) \le (1-\alpha_t)[f(\bar x_{t-1})-f(x)]+(\alpha_t/\gamma_t)V(x_{t-1},x)$.
• Theorem 3.6, general form: Proposition 3.1's recursion telescoped across $t=1,\dots,k$ (with $\mu=0$) into a single two-term bound relating step $k$ to step $0$.

Every constant here is exactly the book's; no milestone hides an $O(\cdot)$ behind an unspecified absolute constant.

Significance

The chain culminates in an explicit, non-asymptotic $O(1/k^2)$ certificate for accelerated gradient descent — the theoretically optimal rate for smooth convex minimization by a first-order method (matching the Nemirovski–Yudin lower bound, not re-derived here). Formalizing it forces every implicit convention in a standard optimization-course derivation to become explicit: which of the three sequences $x_t,\tilde x_t,\bar x_t$ a given quantity refers to, exactly which inequality (3.3.7)-(3.3.9) each specific stepsize schedule needs to satisfy, and the precise index range over which the chapter's own stated hypotheses actually get used in its own proof (see Difficulty below).

None of these six results (or their strongly-convex counterpart, Theorem 3.7, left for future work — see Formalization scope) has a machine-checked proof on Prove2Me. The one theorem with the same name as this mission's subject, BanditAlgorithm.mirror_descent_regret_bound (Lattimore & Szepesvári, Theorem 28.4), is a different object: an online, adversarial regret bound against a changing sequence of loss vectors $y_t$, not an offline function-value gap for a single fixed $f$; not reused. Likewise OnlineConvexOpt.FirstOrder.online_gradient_descent_regret (Hazan) and OnlineConvexOpt.ConvexBasics.constrained_gd_well_conditioned_convergence are, respectively, an online-regret bound and a plain-gradient-descent (non-accelerated) linear-rate result — checked and confirmed not reusable per the mission brief.

Difficulty

The three-point inequalities (Lemmas 3.1/3.4) are routine consequences of a strongly-convex minimizer's optimality condition. The real difficulty is bookkeeping across three coupled sequences in the accelerated method: a formalization using only $x_t$ and $\bar x_t$ (dropping $\tilde x_t$, the point at which the gradient is actually evaluated) is not Lan's algorithm and proves either a false or a different bound — $\tilde x_t$ is what lets the method use a gradient computed at a point between $x_{t-1}$ and $\bar x_{t-1}$, which is exactly the extrapolation step that makes acceleration work.

A second, subtler difficulty is that Theorem 3.6's own stated hypothesis — "(3.3.15) for any $t=1,\dots,k$" — is not quite what its proof uses. Telescoping Proposition 3.1's per-step bound via (3.3.15) requires the previous step's constants $\gamma_{t-1},\alpha_{t-1}$; at $t=1$ these would be $\gamma_0,\alpha_0$, values the recursion (3.3.4)-(3.3.6) never defines (it only ever uses $q_t,\gamma_t,\alpha_t$ for $t\ge1$). The book's own proof, read closely, invokes (3.3.15) only for $t=2,\dots,k$, with $t=1$ handled directly by Proposition 3.1's conclusion connecting $\bar x_1,x_1$ to the given base data $\bar x_0,x_0$. Formalizing the literal hypothesis range would either be unstatable (no $\gamma_0,\alpha_0$ exist) or vacuous (adding unused ghost parameters); this mission states the range the proof actually needs.

Formalization scope

Chapter 3's own §3.1/§3.2 split (Euclidean vs. general norm) is preserved rather than collapsed: subgradient_iterate_three_point/subgradient_descent_bound are stated over a real inner product space with the vector subgradient $g(x_t)\in E$ and the Euclidean norm, exactly matching §3.1; mirror_iterate_three_point/mirror_descent_bound and the two accelerated-method milestones are stated over a general real normed space [NormedAddCommGroup E] [NormedSpace ℝ E], with subgradients as continuous linear functionals E →L[ℝ] ℝ (whose Mathlib operator norm is already the dual norm $\|\cdot\|_*$, needing no separate definition) and the Bregman divergence $V : E \to E \to \mathbb{R}$ left as a free two-point function — but, following a 2026-09-19 revision, no longer a totally free function. V is now required to satisfy the two facts (3.2.2)/(3.2.3)/(3.2.6) actually establish and every downstream proof (Lemma 3.4, Theorem 3.5, Proposition 3.1, Theorem 3.6) uses: nonnegativity ($V(x,z)\ge 0$ for $x,z\in X$) and the three-point/cosine identity $V(x,z) = V(x,y) + \langle\nabla V(x,\cdot)(y), z-y\rangle + V(y,z)$, the latter made explicit via an added parameter dV : E → E → (E →L[ℝ] ℝ) read as "the gradient of $V(x,\cdot)$ at $y$." Without these two hypotheses the five items that use an abstract V (mirror_iterate_three_point, mirror_descent_bound, accelerated_one_step_recursion, accelerated_gradient_recursion_bound, accelerated_gradient_rate) are false as stated — a constant V satisfies the bare pointwise-minimality hypotheses while violating the conclusion, as two worked counterexamples confirmed. This mission does not derive V/dV from an explicit distance-generating function $\nu$ (the heavier, fully book-literal route (3.2.1)-(3.2.2) would); it takes the two facts the proofs actually consume as hypotheses directly, which is lighter and sufficient. Satisfiability is witnessed by the Euclidean case already in §3.1: $\nu(x)=\|x\|^2/2$, $V(x,z)=\|z-x\|_2^2/2$, $dV\,x\,y = \langle y-x,\cdot\rangle$, exactly how subgradient_iterate_three_point/subgradient_descent_bound already handle the Euclidean special case. A trivializing formalization this mission rules out: specializing $V$ to the Euclidean squared distance in mirror_iterate_three_point/mirror_descent_bound would make those two milestones restatements of the §3.1 Euclidean results rather than genuine generalizations, exactly the pitfall the chapter brief flags.

Every argmin-defined iterate ($x_{t+1}$ in each of the three update rules) is represented by its defining pointwise-minimality property rather than by an IsMinOn/argmin term, so no existence or uniqueness lemma for the underlying minimization problem is needed anywhere in this mission — matching how the book's own proofs use these updates (via their first-order optimality condition, never via an explicit formula for the minimizer).

Left out of scope, for time: Theorem 3.7 (the strongly-convex, $\mu>0$ linear-rate companion to Theorem 3.6, sharing Proposition 3.1 as its own base lemma) and Corollary 3.5 (the composite-objective extension $f=\hat f+F$). Both are natural continuations reusing this mission's accelerated_one_step_recursion; a later mission or an amendment to this one could add them as additional milestones/goals without touching what is here.

Selected references

• G. Lan, First-Order and Stochastic Optimization Methods for Machine Learning, Springer Series in the Data Sciences, Springer 2020, Chapter 3. https://doi.org/10.1007/978-3-030-39568-1
• Y. Nesterov, "A method for solving the convex programming problem with convergence rate $O(1/k^2)$," Doklady AN SSSR, 269, 1983, pp. 543–547.
• Y. Nesterov, Introductory Lectures on Convex Optimization, Springer, 2004.
• A. Nemirovski and D. Yudin, Problem Complexity and Method Efficiency in Optimization, Wiley, 1983 (source of the mirror-descent method and the $O(1/k^2)$ lower bound for smooth convex optimization).

Motivation

Machine learning's canonical training objective — minimize an expected or empirical risk over a data distribution — is almost never observed exactly: at each step an algorithm sees only a noisy gradient sample (a minibatch gradient, a single-example gradient, a simulation draw). Stochastic mirror descent (Nemirovski, Juditsky, Lan & Shapiro 2009) is the modern, general-norm answer to "what happens to first-order convergence guarantees when the gradient itself is a random variable": it takes the deterministic mirror-descent scheme of the previous chapter and replaces the exact subgradient with an unbiased stochastic estimate, and asks for both an expected convergence rate and, when the noise is well-behaved, an explicit probability-of-large-deviation guarantee. This is the theoretical backbone of stochastic gradient descent as used in practice.

Setting

Fix a nonempty closed convex set $X$ in a real normed space $E$, and a convex $f:X\to\mathbb R$ with $f^*:=\min_{x\in X}f(x)$ and $x^*$ an arbitrary minimizer, exactly as in Chapter 3. A stochastic oracle $G(x,\xi)$, queried at a point $x$ with a fresh random sample $\xi$, returns an estimate of a subgradient $g(x)\in\partial f(x)$: $\mathbb E[G(x,\xi)] = g(x)$ (unbiasedness), $\|g(x)\|_*\le M$ (a dual-norm Lipschitz bound, Eq. (4.1.7)), and $\mathbb E[\|G(x,\xi)-g(x)\|_*^2]\le\sigma^2$ (a second-moment/variance bound). The stochastic mirror-descent update is exactly Chapter 3's mirror-descent update with $G_t := G(x_t,\xi_t)$ in place of the deterministic $g_t$: $x_{t+1} := \arg\min_{x\in X}\gamma_t\langle G_t,x\rangle + V(x_t,x)$ (Eq. (4.1.6)), where $V$ is the Bregman divergence of a fixed distance-generating function $\nu$.

Formalization targets

Goal — Theorem 4.1

$$\mathbb E[f(\bar x^k_s)] - f^* \le \Big(\sum_{t=s}^k\gamma_t\Big)^{-1}\Big(\mathbb E[V(x_s,x^*)] + (M^2+\sigma^2)\sum_{t=s}^k\gamma_t^2\Big).$$

Supporting milestones, in attack order

• Lemma 3.4, invoked for the stochastic update: the same three-point inequality as the deterministic mirror-descent update, restated with the stochastic gradient functional $G_t$ in place of $g_t$ — the book's own remark ("It can be easily seen that the result in Lemma 3.4 holds with $g_t$ replaced by $G_t$") is exactly what licenses treating this as the same algebraic fact for a fixed sample path.
• Lemma 4.1: the martingale-difference deviation bound, a Chernoff-type concentration inequality for a conditionally sub-Gaussian martingale-difference sequence — the chapter's general-purpose probabilistic tool, proved independently of the optimization setting.

Every constant is exactly the book's; $M^2+\sigma^2$ (not a generic $O(\cdot)$) is the goal's own noise-dependent constant, taken verbatim.

Significance

This is the first mission in the series to leave the purely deterministic, real-analytic setting of Chapters 2-3 and formalize a genuinely probabilistic convergence guarantee: an expectation taken over an entire random algorithm trajectory $\xi_1,\dots,\xi_k$, not merely over a single random variable. Getting the goal theorem's statement right requires being explicit about exactly which quantities are random (the iterates $x_t$, hence $f(\bar x_s^k)$ and $V(x_s,x^*)$) and which are deterministic constants fixed in advance ($M,\sigma,\gamma_t$), and about the precise mathematical content of "the stochastic gradient's bias vanishes after conditioning on the past" — Lemma 4.1 is included specifically because it is the general machine that makes that vanishing rigorous, independent of the optimization application.

No result matching stochastic mirror descent, Assumption 4's sub-Gaussian/light-tail condition, or this martingale-difference concentration lemma exists on the platform as of 2026-09-18 (q= stochastic gradient, q=stochastic mirror descent, q=martingale, q=sub-Gaussian — see Prior art below for what these queries actually returned).

Difficulty

The central difficulty is disentangling which facts in the chapter's proof genuinely need measure theory and which do not. The per-step algorithmic relations — $x_{t+1}$'s minimality, $f$'s subgradient inequality at $x_t$, the dual-norm bound on $g$ — hold for every sample path individually and are formalized pointwise in $\omega$, exactly as chunk 03-deterministic formalizes its deterministic analogues; only the second-moment bound and the final expectation inequality are genuine integrals. The one place this pointwise treatment cannot simply mirror the deterministic case is the noise cross-term $\mathbb E[\gamma_t\langle\delta_t,x_t-x^*\rangle]=0$: in the book's proof this vanishes because $\delta_t=G_t-g(x_t)$ is conditionally mean-zero given the past and $x_t$ is a function of the past (the martingale-difference property, via the tower property of conditional expectation) — a genuinely non-pointwise fact. Rather than thread an explicit filtration through the goal theorem's own statement (which Lemma 4.1 already does, as the chapter's dedicated home for that machinery), the goal theorem takes this post-tower-property consequence directly as a named hypothesis (hcross); see Formalization scope.

Formalization scope

stochastic_mirror_iterate_three_point and stochastic_mirror_descent_bound are stated over a general real normed space [NormedAddCommGroup E] [NormedSpace ℝ E], matching chunk 03-deterministic's general-norm milestones (mirror_iterate_three_point/mirror_descent_bound) rather than the Euclidean/inner-product specialization of that chunk's §3.1 items — Chapter 4's own stochastic mirror descent is presented directly in the general-norm framework of §3.2, with no Euclidean-only warm-up. $V$ is left a free two-point function (never hard-coded to a squared Euclidean distance), and the stochastic gradient $G_t$ and the subgradient selector $g$ are continuous linear functionals E →L[ℝ] ℝ, whose Mathlib operator norm supplies the dual norm $\|\cdot\|_*$ with no separate definition needed — the same trivializing formalization chunk 03-deterministic rules out (specializing $V$ to the Euclidean case) applies here and is ruled out the same way.

martingale_difference_deviation_bound (Lemma 4.1) is a standalone probabilistic result, formalized with Mathlib's MeasureTheory.Filtration and condExp machinery: the sequence $\xi_{[t]}$'s generated filtration, $\zeta_t$'s $\mathcal F_t$-measurability, and the two conditional-expectation hypotheses (conditional mean zero, conditional sub-Gaussian tail) are all literal translations of the book's own E|ξ[t-1] notation.

Left out of scope, for time: Assumption 4 (the light-tail/sub-Gaussian oracle assumption), Proposition 4.1 (the large-deviation bound under Assumption 4, which chains Lemma 4.1's concentration bound with the constant stepsize policy (4.1.11) and a second Markov-inequality argument on $\sum\gamma_t^2\|\delta_t\|_*^2$), Lemma 4.2 and Theorem 4.2 (the smooth-$f$ case, §4.1.2, requiring a separate recursion and averaging convention $x_t^{av}$). All four are natural continuations reusing this mission's stochastic_mirror_iterate_three_point and/or martingale_difference_deviation_bound; a later mission or an amendment to this one could add them without touching what is here. Per Hard Rule 7 (faithfulness over coverage), a genuinely faithful formalization of Proposition 4.1 in particular — which needs Assumption 4's own conditional-MGF hypothesis threaded consistently with Lemma 4.1's, plus the constant-stepsize substitution and a second concentration argument — was judged to need more time than this session's budget allowed to do without shortcuts; it is named here rather than approximated.

Selected references

• G. Lan, First-Order and Stochastic Optimization Methods for Machine Learning, Springer Series in the Data Sciences, Springer 2020, Chapter 4, §4.1. https://doi.org/10.1007/978-3-030-39568-1
• A. Nemirovski, A. Juditsky, G. Lan, A. Shapiro, "Robust stochastic approximation approach to stochastic programming," SIAM Journal on Optimization, 19(4), 2009, pp. 1574-1609.
• H. Robbins, S. Monro, "A stochastic approximation method," Annals of Mathematical Statistics, 22(3), 1951, pp. 400-407 (origin of stochastic approximation).