## Motivation
The $k$-server problem was introduced by Manasse, McGeoch, and Sleator ([STOC 1988 / J. Algorithms 1990](https://doi.org/10.1016/0196-6774(90)90003-W)) 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](https://doi.org/10.1016/0196-6774(90)90003-W)) 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](https://doi.org/10.1109/FSCS.1990.89566)) 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.](https://doi.org/10.1137/0404017)) prove the conjecture on the real line via **Double Coverage**; Chrobak and Larmore ([SIAM J. Comput.](https://doi.org/10.1137/0220008)) extend it to all tree metrics.
- **1995.** Koutsoupias and Papadimitriou ([J. ACM](https://doi.org/10.1145/210118.210128)) 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](https://arxiv.org/abs/2102.10474)) give a unifying potential for all known WFA analyses and push the frontier to the circle.
- **2023.** Bubeck, Coester, and Rabani ([STOC](https://arxiv.org/abs/2211.05753)) 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.
## 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](https://doi.org/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](https://doi.org/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](https://doi.org/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](https://doi.org/10.1137/0220008)
- E. Koutsoupias, C. Papadimitriou, *On the k-server conjecture*, J. ACM 42 (1995). [doi:10.1145/210118.210128](https://doi.org/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](https://arxiv.org/abs/2102.10474)
- S. Bubeck, C. Coester, Y. Rabani, *The randomized k-server conjecture is false!*, STOC 2023. [arXiv:2211.05753](https://arxiv.org/abs/2211.05753)
- E. Koutsoupias, *The k-server problem* (survey), Computer Science Review 3 (2009). [doi:10.1016/j.cosrev.2009.04.002](https://doi.org/10.1016/j.cosrev.2009.04.002)
Vector Space Methods IV: Hahn–Banach and Minimum Norm DualityTextbook
## Motivation
Chapter 5 of Luenberger's *Optimization by Vector Space Methods* (Wiley, 1969) carries the minimum norm theory of Chapter 3 (Mission I of this series) from Hilbert space to arbitrary real normed spaces. The inner product is gone, so orthogonal projection is no longer available; its role is taken over by the **Hahn–Banach theorem**, in two classical forms. The extension form generalizes the projection theorem and yields a duality principle equating a minimum norm problem in a space $X$ with a maximization problem in its dual $X^*$; the geometric form (separating hyperplanes) extends that duality from subspaces to convex sets. These duality theorems are the backbone of the optimization theory in the remainder of the book — conjugate functionals (Ch. 7) and Lagrange duality (Ch. 8) both trace back to them.
## Setting
Throughout, $X$ is a **real normed linear space**. A linear functional $f$ on $X$ is **bounded** if $|f(x)| \le M\|x\|$ for some constant $M$ and all $x$; the least such $M$ is the norm $\|f\|$. The **(normed) dual** $X^*$ is the space of bounded (equivalently, continuous) linear functionals with this norm; $\langle x, x^*\rangle$ denotes $x^*(x)$. A functional $p : X \to \mathbb{R}$ is **sublinear** when $p(x+y) \le p(x) + p(y)$ and $p(\alpha x) = \alpha\, p(x)$ for $\alpha > 0$. Vectors $x \in X$ and $x^* \in X^*$ are **aligned** when $\langle x, x^*\rangle = \|x^*\|\,\|x\|$, and **orthogonal** when $\langle x, x^*\rangle = 0$; for $S \subseteq X$, the complement $S^\perp \subseteq X^*$ consists of the functionals vanishing on $S$, and for $U \subseteq X^*$, ${}^\perp U \subseteq X$ consists of the vectors annihilated by every member of $U$. A **hyperplane** is a maximal proper linear variety; closed hyperplanes are the level sets $\{x : \langle x, x^*\rangle = c\}$ of nonzero bounded functionals. The **support functional** of a convex set $K$ is $h(x^*) = \sup_{k \in K}\, \langle k, x^*\rangle$.
## Formalization targets
The goal is §5.13 Theorem 1 (**Minimum Norm Duality**): if $x_1 \in X$ has distance $d > 0$ from a convex set $K$ with support functional $h$, then
$$d \;=\; \inf_{x \in K} \|x - x_1\| \;=\; \max_{\|x^*\| \le 1}\ \big[\langle x_1, x^*\rangle - h(x^*)\big],$$
the maximum on the right being achieved by some $x_0^*$; and if the infimum is achieved by $x_0 \in K$, then $-x_0^*$ is aligned with $x_0 - x_1$.
The milestones trace the chapter's route there: boundedness $\Leftrightarrow$ continuity (§5.2); the Hahn–Banach theorem in sublinear form (§5.4 Theorem 1) with its norm-preserving extension and norming-functional corollaries; the annihilator identity ${}^\perp(M^\perp) = M$ for closed subspaces (§5.7 Theorem 1); the two subspace duality theorems and the alignment characterization of best approximations (§5.8 — the chapter's principal results); and the geometric form: Mazur's separation theorem, the support theorem, and Eidelheit's separation theorem (§5.12).
## Significance
The §5.8 duality theorems are the exact normed-space analogue of the projection theorem: existence transfers to the dual problem (minimum norm problems should be *formulated in a dual space* to guarantee solutions — the chapter's methodological moral), orthogonality becomes alignment, and infinite-dimensional problems with finitely many constraints reduce to finite-dimensional dual problems. The geometric form underpins all of convex duality.
All results are classical and proved in the source. Mathlib contains the Hahn–Banach extension theorem and point/convex separation theorems, so several milestones are exercises in connecting Luenberger's formulations to existing library lemmas; the two §5.8 duality theorems, the alignment corollary, and the §5.13 convex duality theorem have no direct Mathlib counterpart and are the mission's genuinely new content.
## Difficulty
Degenerate cases are the trap throughout. In §5.8 Corollary 1 the "only if" direction fails literally when $M$ is dense and $x \in M$ (then $M^\perp = \{0\}$ and no nonzero aligned functional exists); the formalization therefore carries the hypothesis $x \notin \overline{M}$. In the separation theorems the strict inequality holds only on the *interior* of the convex set — on the set itself only $\le$ survives — and nonemptiness hypotheses (of the interior, of $K_2$, of the variety) are what make the "nonzero functional" claims true; dropping any of them creates false statements in trivial spaces. In §5.13 the support functional may take the value $+\infty$, so the dual maximum is formalized by two quantified inequalities (the witness achieves $d$; no admissible functional exceeds $d$) rather than by a real-valued supremum. The infimum in the primal problems need not be attained — attainment appears only as a hypothesis in the alignment clauses.
## Formalization scope
Real scalars throughout. The dual space is represented concretely as continuous linear maps `X →L[ℝ] ℝ`, and annihilators are written as explicit quantified conditions rather than named subspaces. Five notions the chapter needs and Mathlib lacks are published as **definitions** and used by the statements rather than inlined: **alignment** ($\langle x, x^*\rangle = \|x^*\|\,\|x\|$), the **support functional** ($h(x^*) = \sup_{k \in K} \langle k, x^*\rangle$, valued in the extended reals since it may be infinite), the **total variation** of a function on an interval, the normalized space **$NBV[a,b]$**, and the **Riemann–Stieltjes integral** (defined relationally, so that no existence claim is built into the definition). The Minkowski functional needed for Mazur's theorem is Mathlib's `gauge`. Minimum distances are infima `⨅` over coerced sets or submodules; in §5.8 Theorem 2 the dual-side supremum is a real `sSup` over $\{\langle x, x^*\rangle : x \in M,\ \|x\| \le 1\}$, which is nonempty and bounded. Sublinearity in §5.4 is hypothesized exactly as in the source (subadditivity plus positive homogeneity plus continuity). Linear varieties are parametrized as $x_0 + M$ with $M$ a `Submodule ℝ X`. No completeness of $X$ is assumed anywhere — the chapter's results are genuinely about normed spaces, and Hahn–Banach needs no completeness. The concrete dual of $C[a,b]$ (§5.5) **is** in scope, and carries most of the mission's new infrastructure: Mathlib has the *property* of bounded variation (`eVariationOn`) but no total-variation norm, no normalized space $NBV[a,b]$, and no Riemann–Stieltjes integral — its `StieltjesFunction` is the different object of a monotone right-continuous function inducing a Borel measure, and its Riesz–Markov–Kakutani development represents positive functionals on $C_c(X)$ by measures, not bounded functionals on $C[a,b]$ by functions of bounded variation. This mission therefore publishes those notions as definitions and states the representation theorem in both directions. §5.3 (the Riesz–Fréchet theorem, i.e. self-duality of Hilbert space) is the one omission: Mathlib's `InnerProductSpace.toDual` already provides it. §5.6 (second dual, reflexivity) is definitional and likewise present in Mathlib.
## Selected references
- David G. Luenberger, *Optimization by Vector Space Methods*, John Wiley & Sons, 1969. Chapter 5, pp. 103–142. ISBN 0-471-55359-X.
- H. Hahn, *Über lineare Gleichungssysteme in linearen Räumen*, J. Reine Angew. Math. 157 (1927), 214–229; S. Banach, *Sur les fonctionnelles linéaires II*, Studia Math. 1 (1929), 223–239.
- S. Mazur, *Über konvexe Mengen in linearen normierten Räumen*, Studia Math. 4 (1933), 70–84.
## 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](https://doi.org/10.1007/BFb0120913)) 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](https://doi.org/10.1016/0020-0190(90)90028-V)) rediscover this via a monotonicity property.
- **1995.** Goemans ([Math. Programming 69](https://doi.org/10.1007/BF01585563)) 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](https://arxiv.org/abs/1201.1870)) 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](https://arxiv.org/abs/2007.01409)) and then an integrality-gap bound $\gamma \le 3/2 - \varepsilon$ with $\varepsilon > 10^{-36}$ ([FOCS 2022](https://arxiv.org/abs/2105.10043)), 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](https://doi.org/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](https://doi.org/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](https://doi.org/10.1007/BF01585563)
- A. Sebő, J. Vygen, *Shorter tours by nicer ears*, Combinatorica 34 (2014). [arXiv:1201.1870](https://arxiv.org/abs/1201.1870)
- A. Karlin, N. Klein, S. Oveis Gharan, *A (slightly) improved approximation algorithm for metric TSP*, STOC 2021. [arXiv:2007.01409](https://arxiv.org/abs/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](https://arxiv.org/abs/2105.10043)
- V. Traub, J. Vygen, *Approximation Algorithms for Traveling Salesman Problems*, Cambridge University Press, 2024. [book page](https://www.or.uni-bonn.de/tspbook/book.pdf)
Vector Space Methods II: Gauss–Markov EstimationTextbook
## Motivation
Chapter 4 of Luenberger's *Optimization by Vector Space Methods* (Wiley, 1969) develops linear least-squares estimation as an application of the Hilbert space projection theorem formalized in Mission I of this series. The chapter's centerpiece is the classical **Gauss–Markov theorem**: among all linear unbiased estimators of an unknown parameter vector from noisy linear measurements, the estimator $(W^\top Q^{-1} W)^{-1} W^\top Q^{-1} y$ has minimum variance — componentwise, not merely in trace. This result is foundational for statistics and econometrics, and its Hilbert-space derivation is the cleanest known.
## Setting
Measurements are modeled as $y = W\beta + \varepsilon$, where $y$ is an $m$-dimensional data vector, $W$ a known $m \times n$ matrix ($n < m$) with linearly independent columns, $\beta$ an unknown $n$-dimensional parameter vector, and $\varepsilon$ a random $m$-vector of measurement errors with $E\varepsilon = 0$ and covariance $E[\varepsilon\varepsilon^\top] = Q$, positive definite. A **linear estimate** is $\hat\beta = Ky$ for a constant $n \times m$ matrix $K$; it is **unbiased** when $E\hat\beta = \beta$ for every $\beta$, which holds iff $KW = I$. The optimality criterion is the error second moment $E\|\hat\beta - \beta\|^2$, and the book's key observation (p. 85) is that the problem splits into $n$ independent minimum norm problems, one per component, each solvable by the dual approximation theorem of Mission I.
Formally, randomness is carried by an abstract probability space: a measure space $(\Omega, \mu)$ with $\mu$ a probability measure, random vectors as functions $\Omega \to \mathbb{R}^m$ with explicit integrability hypotheses for all first and second moments, and $E[\cdot] = \int \cdot \, d\mu$.
## Formalization targets
The goal is §4.4 Theorem 1 (Gauss–Markov): with $K_0 = (W^\top Q^{-1} W)^{-1} W^\top Q^{-1}$,
$$K_0 W = I, \qquad E\big[(K_0 y - \beta)_i^2\big] \le E\big[(K y - \beta)_i^2\big] \quad \text{for every } i \text{ and every } K \text{ with } KW = I,$$
with error covariance
$$E\big[(K_0 y - \beta)(K_0 y - \beta)^\top\big] = (W^\top Q^{-1} W)^{-1}.$$
Milestones: the deterministic least-squares estimate $\hat\beta = (W^\top W)^{-1} W^\top y$ (§4.3 Theorem 1); the book's deterministic reduction — minimize the diagonal entries of $KQK^\top$ subject to $KW = I$ (p. 85); the minimum-variance estimate $\hat\beta = E[\beta y^\top] (E[y y^\top])^{-1} y$ for random $\beta$ (§4.5 Theorem 1); and the information-form identities $RW^\top(WRW^\top + Q)^{-1} = (W^\top Q^{-1}W + R^{-1})^{-1}W^\top Q^{-1}$ and $R - RW^\top(WRW^\top+Q)^{-1}WR = (W^\top Q^{-1}W + R^{-1})^{-1}$ (§4.5 Corollary 2).
## Significance
The Gauss–Markov theorem justifies weighted least squares as the optimal linear unbiased procedure and is the standard benchmark against which biased and nonlinear estimators are measured. The minimum-variance estimate of §4.5 is the Bayesian counterpart with prior covariance $R$; the information-form identities connect the two and exhibit Gauss–Markov as the limit $R^{-1} \to 0$. Mission III builds the recursive (Kalman) estimator directly on these results.
All results are classical and proved in the source. Mathlib has mature measure-theoretic integration but, to date, no Gauss–Markov theorem and no linear estimation theory; the matrix milestones (trace reduction, information form) are also absent as stated. The probabilistic statements here are deliberately phrased with elementary integrals of products of real-valued components — no Bochner integration of vector-valued maps — so they are approachable with `MeasureTheory.integral` alone.
## Difficulty
The subtlety is bookkeeping, not depth. Unbiasedness must be encoded as the algebraic constraint $KW = I$ (the book proves the equivalence with $E\hat\beta = \beta$ for all $\beta$); the componentwise variance claim is strictly stronger than the trace claim and requires the per-component minimum norm argument, not a single matrix inequality. Positive definiteness of $Q$ enters through invertibility of $W^\top Q^{-1} W$, which itself needs the linear independence of the columns of $W$ — dropping either hypothesis makes the goal false. In the probabilistic statements every integral needs an integrability hypothesis; the drafts supply integrability of all pairwise products of components, from which integrability of every derived expression follows.
## Formalization scope
Random vectors are plain functions `Ω → Fin m → ℝ` on a `MeasurableSpace Ω` with a probability measure `μ`; second moments are hypotheses of the form `∫ ω, ε ω i * ε ω j ∂μ = Q i j` with explicit `Integrable` assumptions; no independence, Gaussianity, or distributional assumptions are used anywhere. Matrices are `Matrix (Fin m) (Fin n) ℝ` with Mathlib's `Matrix.PosDef`, nonconstructive inverse `⁻¹`, and `mulVec`. Norms on parameter space are written as explicit finite sums of squares, avoiding any ambiguity between Euclidean and supremum norms on pi types. The estimators under comparison are strictly linear ($\hat\beta = Ky$, no affine offset), exactly as in the source; §4.5's affine extension (its Problem 6) is out of scope.
## Selected references
- David G. Luenberger, *Optimization by Vector Space Methods*, John Wiley & Sons, 1969. Chapter 4, pp. 78–102. ISBN 0-471-55359-X.
- A. C. Aitken, *On least squares and linear combination of observations*, Proc. Roy. Soc. Edinburgh 55 (1935), 42–48 (the weighted-least-squares form of Gauss–Markov).
Vector Space Methods I: Minimum Norm Problems in Hilbert SpaceTextbook
## Motivation
Luenberger's *Optimization by Vector Space Methods* (Wiley, 1969) organizes a large part of optimization theory around a single geometric idea: minimum norm problems in inner product spaces, solved by orthogonal projection. Chapter 3 is the technical heart of that program. Its projection theorem and normal equations underlie least-squares data fitting, Fourier approximation, minimum-energy control, and the whole statistical estimation theory of Chapter 4 — which Missions II and III of this series formalize on top of the present one.
## Setting
Throughout, spaces are **real**. A **pre-Hilbert space** is a real vector space $X$ with an inner product $\langle\cdot,\cdot\rangle$ inducing the norm $\|x\| = \langle x,x\rangle^{1/2}$; a **Hilbert space** $H$ is a complete pre-Hilbert space. Vectors $x, y$ are **orthogonal** when $\langle x, y\rangle = 0$; for a subset $S$, the **orthogonal complement** $S^\perp$ is the set of vectors orthogonal to every element of $S$. Given $y_1,\dots,y_n \in H$, their **Gram matrix** is $G(y_1,\dots,y_n)_{ij} = \langle y_i, y_j\rangle$ and its determinant $g(y_1,\dots,y_n)$ is the **Gram determinant**. A **linear variety** is a translate $x + M$ of a subspace $M$.
## Formalization targets
The goal is §3.10 Theorem 2, the **dual approximation problem**: for linearly independent $y_1,\dots,y_n \in H$ and constants $c_1,\dots,c_n$, among all $x \in H$ satisfying the constraints
$$\langle x, y_i\rangle = c_i, \qquad i = 1,\dots,n,$$
there is a unique vector of minimum norm, and it has the form
$$x_0 = \sum_{i=1}^n \beta_i\, y_i, \qquad \text{where} \qquad \sum_{j=1}^n \beta_j \langle y_j, y_i\rangle = c_i .$$
The milestone list follows the chapter's own development: the projection theorem in its pre-Hilbert form (§3.3 Theorem 1) and classical form (§3.3 Theorem 2), the orthogonal decomposition $H = M \oplus M^\perp$ with $M^{\perp\perp} = M$ (§3.4 Theorem 1), the normal equations and Gram matrices (§3.6), the Gram determinant formula $\delta^2 = g(y_1,\dots,y_n,x)/g(y_1,\dots,y_n)$ for the minimum distance (§3.6 Theorem 1), best approximation by Fourier sums over orthonormal families (§3.7, §3.9), minimum norm over a linear variety (§3.10 Theorem 1), and the extension from subspaces to closed convex sets with its variational inequality characterization (§3.12 Theorem 1).
## Significance
The dual approximation theorem converts an infinite-dimensional constrained minimum norm problem into an $n \times n$ linear system — the book's model example of finite reduction, applied there to minimum-energy control of a motor (§3.11) and, in Chapter 4, to every linear estimation problem: least squares, Gauss–Markov, and recursive (Kalman) estimation are all instances of these results in a Hilbert space of random variables.
All results here are classical and proved in the source; the mission's product is a faithful machine-checked development with reusable statements. Mathlib already contains close relatives of several milestones (orthogonal projection onto complete subspaces, `Submodule.orthogonal`), so part of the work is connecting the book's formulations to that library; the Gram determinant distance formula and the dual approximation theorem itself have no direct Mathlib counterpart.
## Difficulty
The individual milestones are standard Hilbert space theory. The care is in the statements, not tricks: the pre-Hilbert version of the projection theorem asserts uniqueness and the orthogonality characterization *without* existence, while existence requires completeness and closedness — conflating the two versions produces unprovable or vacuous statements. The Gram determinant formula requires the $(n+1) \times (n+1)$ Gram matrix of the extended family $(y_1,\dots,y_n,x)$, where index bookkeeping (`Fin.snoc`) is easy to get wrong. In §3.12 the variational inequality $\langle x - k_0, k - k_0\rangle \le 0$ replaces the equality characterization valid for subspaces; the inequality direction is a known trap.
## Formalization scope
The development commits to: real scalars (the book allows complex; this series does not), an abstract space `H : Type` with `[NormedAddCommGroup H] [InnerProductSpace ℝ H]` and `[CompleteSpace H]` exactly where the source assumes a Hilbert space; subspaces as `Submodule ℝ H` with explicit `IsClosed` hypotheses; finite families as `Fin n → H`; Gram matrices as `Matrix (Fin n) (Fin n) ℝ` via `Matrix.of`; minimum distances as infima (`⨅`) over coerced submodules. Best approximation statements are phrased as explicit inequalities `‖x - m₀‖ ≤ ‖x - m‖` rather than through any projection operator, so they are usable without choosing Mathlib's `orthogonalProjection` API. Statements deliberately carry no more hypotheses than the source: §3.3 Theorem 1 and the normal equations hold in any real inner product space; completeness appears only where existence is claimed.
Proofs are expected to lean on Mathlib's inner product space library; contributions of reusable bridging lemmas (e.g. between `⨅`-formulations and `orthogonalProjection`) are welcome as child lemmas via proof sketches.
## Selected references
- David G. Luenberger, *Optimization by Vector Space Methods*, John Wiley & Sons, 1969. Chapter 3, pp. 46–77. ISBN 0-471-55359-X.
Erdős Problem 146: Failure of the 2-Degenerate Extremal BoundResearch Paper
A graph $H$ is **$r$-degenerate** if every nonempty subgraph of $H$ has a vertex of degree at most $r$. Erdős conjectured — this is Erdős problem #146 — that every fixed bipartite $r$-degenerate graph $H$ satisfies
$$\mathrm{ex}(n, H) = O\!\left(n^{2-1/r}\right).$$
The conjecture was known in several cases: when one bipartition class has maximum degree at most $r$, for $r$-degenerate blow-ups of trees, and, for $r = 2$, for grids and certain critical 2-degenerate graphs. The best general bound was the weaker $\mathrm{ex}(n,H) = O(n^{2-1/(4r)})$ of Alon, Krivelevich and Sudakov.
This mission carries a complete Lean 4 formalisation **refuting** it at $r = 2$.
**Theorem.** There exist a fixed connected bipartite 2-degenerate graph $H$ and constants $c, \varepsilon > 0$ such that
$$\mathrm{ex}(n, H) \ \ge\ c\,n^{3/2 + \varepsilon}$$
for all sufficiently large $n$. Since the conjectured bound at $r = 2$ is $O(n^{3/2})$, the excess is polynomial rather than constant, so the conjecture fails outright. A related conjecture of Erdős (problem #113) asserts that a bipartite graph is 2-degenerate if and only if $\mathrm{ex}(n,H) = O(n^{3/2})$; Janzer had already disproved the reverse implication, and this result refutes the forward one.
**The construction.** The counterexample $H$ is built in layers: starting from a layer $V_0$ of size $L_0$, each subsequent layer is $V_i = \binom{V_{i-1}}{2}$, and every vertex $\{a,b\} \in V_i$ is joined to its two parents $a, b \in V_{i-1}$. The result is connected, bipartite and 2-degenerate by construction, and is related to the complete degenerate graphs of Grzesik, Janzer and Nagy.
The lower bound comes from a **sampled Hamming-ball graph**. With $U = \{0,1\}^m$, two disjoint copies $U_L, U_R$ are joined whenever their Hamming distance is at most $k = \lfloor \tau m\rfloor$, and each vertex is retained independently with probability $p = 2^{-\beta m}$. The two parameters are governed by the thresholds
$$A(\tau) = \kappa + \tau\log_2 3, \qquad C(\tau) = 2h(\tau) - 1,$$
and the construction needs a sampling exponent with $A(\tau) < \beta < C(\tau)$. The lower threshold controls exclusion of the layered graph; the upper one controls whether the sampled host has more than $n^{3/2}$ edges.
Exclusion runs on a conditional-entropy functional $E(u,z) = \frac{1}{m}\sum_j H(Z_j \mid X_j, Y_j)$ over parent and child arrays. An array of conditional entropy $E$ has at most $2^{mME + O(m\log_2 M)}$ realisations, while requiring its $M = \binom{L}{2}$ children to survive sampling costs $2^{-\beta mM}$ — which dominates the $2^{mL}$ possible parent arrays whenever $E < \beta$. An embedding of $H$ would therefore have to raise a bounded entropy potential by a fixed amount at each layer, which is impossible after enough layers. A second-moment argument shows the sampled graph still has $\Omega(n^{3/2+\varepsilon})$ edges, and padding extends the construction to every sufficiently large order.
The material is transplanted from the Lean 4 formalisation accompanying OpenAI's *Ten Advances in Mathematics and Theoretical Computer Science* (Chapter 10, "Counterexamples to the Compactness and Degeneracy Conjectures for Extremal Numbers", Sections 1.2 and 5–8), and re-verified in this environment: every node is proved from `[propext, Classical.choice, Quot.sound]` alone, and each staged statement's elaborated type was checked to be identical to the original declaration's. The mission is offered as a curated, closed campaign whose definitions and lemmas — binary entropy and the pair kernel, the layered construction, the Hamming-ball host and its retention measure — are reusable foundations for further work in extremal graph theory.
This is the companion result to Erdős problem #180, the Erdős–Simonovits compactness conjecture, which is formalised in the same source chapter and published as a separate mission.
Erdős Problem 180: the Erdős–Simonovits Compactness ConjectureResearch Paper
Erdős and Simonovits conjectured that forbidding a finite family of graphs cannot reduce the extremal number by more than a constant factor compared with forbidding one of its members: for every finite nonempty family $\mathcal{F}$ whose members all contain a cycle, there should be some $F \in \mathcal{F}$ and $C>0$ with $\mathrm{ex}(n,F) \le C\,\mathrm{ex}(n,\mathcal{F})$ for all large $n$. The cycle hypothesis is essential — the folklore family $\{K_{1,2}, 2K_2\}$ already defeats the original formulation — and the corrected conjecture is Erdős problem #180.
This mission carries a complete Lean 4 formalisation refuting it, and refuting it quantitatively: there is a finite family $\mathcal{F}$ of **connected bipartite** graphs, each containing a cycle, with
$$\mathrm{ex}(n,\mathcal{F}) = O\!\left(n^{4/3-1/48}\right) \qquad\text{while}\qquad \mathrm{ex}(n,F) = \Omega\!\left(n^{4/3}\right) \ \ (F \in \mathcal{F}).$$
The two bounds are separated by a polynomial factor $n^{1/48}$, so no member can dominate the family up to any constant. The family is $\mathcal{F} = \{C_4, C_6\} \cup \mathcal{J} \cup \mathcal{K}$, where $\mathcal{J}$ and $\mathcal{K}$ are the admissible quotients of two properly $2$-coloured templates built from the subdivisions of $K_{3,2}$ and $K_{3,3}$. The upper bound comes from counting short paths in an $\mathcal{F}$-free graph: excluding $\mathcal{J}$ bounds the number of vertices that fail to be centres of a subdivided $K_{3,3}$, and excluding $\mathcal{K}$ forces those vertices to form a vertex cover. The lower bound comes from incidence graphs of symplectic generalized quadrangles $W(q)$, with the characteristic of the underlying field chosen to suit the forbidden member — even $q$ for $\mathcal{J}$, odd $q$ for $\mathcal{K}$ — which is exactly the freedom a family bound does not have.
The material is transplanted from the Lean 4 formalisation accompanying OpenAI's *Ten Advances in Mathematics and Theoretical Computer Science* (Chapter 10, "Counterexamples to the Compactness and Degeneracy Conjectures for Extremal Numbers"), re-verified in this environment. Every node is proved; the mission is offered as a curated, closed campaign whose definitions and lemmas are reusable foundations for further work in extremal graph theory.
Erdős Problem 183: Multicolour Triangle Ramsey NumbersResearch Paper
How fast do multicolour Ramsey numbers grow? Write $R_k$ for the least $n$ such that every colouring of the edges of $K_n$ with $k$ colours contains a monochromatic triangle. The classical bounds, essentially unimproved for decades, place $R_k$ between $c^k$ and $e\cdot k!$, and Erdős asked repeatedly whether the truth is closer to the exponential lower end — his Problem 183 asks whether $R_k^{1/k}\to\infty$, i.e. whether the growth is genuinely superexponential.
This mission carries a complete Lean 4 formalisation resolving that question in the affirmative, with an explicit bound: $R_k \ge \left(\tfrac{1}{6e^{38}}\,k^{1/3}/\log k\right)^{k}$ for all sufficiently large $k$, from which $R_k^{1/k}\to\infty$ follows, together with the matching two-sided estimate $\log R_k = \Theta(k\log k)$ pinning the sharp coefficients. The argument is constructive: it builds triangle-free colourings by a recursive palette construction whose colour count grows fast enough to beat every exponential.
The material is transplanted from the Lean 4 formalisation accompanying OpenAI's *Ten Advances in Mathematics and Theoretical Computer Science*, re-verified in this environment. Every node is proved — the mission is offered as a curated, closed campaign whose milestones map the attack path and whose lemmas are reusable foundations for further work on multicolour Ramsey theory.
Erdős Problem 788: Exponent One-Half and Explicit BoundsResearch Paper
Erdős Problem 788 asks how large a set can always be retained when prescribed distinct pair-sums are forbidden. This mission formalizes the repository’s strengthened version of Theorem 1.1: an explicit lower bound valid for every $n\ge 3$, an eventual quantitative upper bound, the conclusion $f(n)=n^{1/2+o(1)}$, and the exact affirmative answer to the original upper-bound question.
Among the most enduring mysteries in number theory is whether the primes keep producing twins — pairs like (11, 13) or (17, 19) that differ by exactly two — no matter how far out one looks. The general form was set down by Alphonse de Polignac in 1849, and the first deep theorem came from Viggo Brun in 1915, who proved that the reciprocals of the twin primes converge to a finite value, now called Brun's constant; in doing so he invented modern sieve theory and showed that twins must thin out even if there are infinitely many. Hardy and Littlewood went further, conjecturing a precise density of about 2C₂·x/(ln x)² for the count of twins below x. For nearly a century the infinitude itself stood untouched, until Yitang Zhang's stunning announcement on 17 April 2013 that some gap below 70 million recurs infinitely often — the first finite bound ever proved. A Polymath collaboration led by Terence Tao, together with James Maynard's independent multidimensional sieve, soon drove that bound down to 246, where it still stands. Closing the gap all the way to 2 — the twin prime conjecture itself — remains open. This mission states it cleanly: the set of primes p for which p + 2 is also prime is infinite.
Congruent Numbers — Tunnell's Criterion (Even Case)Open Problem
Which whole numbers are the area of a right triangle with rational sides? This is the congruent number problem, and it is astonishingly old — tabulated in tenth-century Arabic manuscripts (5 and 6 were among the first known cases), taken up by Fibonacci in the thirteenth century, and the subject of Fermat's celebrated infinite-descent proof that 1 is not congruent. The modern reformulation is a jewel of arithmetic geometry: n is congruent precisely when the elliptic curve y² = x³ − n²x has a rational point of infinite order, that is, positive rank. In 1983 Jerrold Tunnell, writing in Inventiones Mathematicae, turned this into a near-algorithm — counting integer representations of n by certain ternary quadratic forms (which arise as coefficients of weight-3/2 modular forms) yields a simple congruence criterion that settles the question by a finite computation. The catch, and the reason the problem remains officially open, is that the sufficiency of Tunnell's criterion rests on the Birch and Swinnerton-Dyer conjecture, itself a Millennium Prize Problem. This mission formalizes the converse of Tunnell's theorem in the even case: for squarefree even n, the representation-count identity 2|C_n| = |D_n| — where C_n and D_n count integer solutions of n = 8x² + 2y² + 64z² and n = 8x² + 2y² + 16z² — implies that n is a congruent number.
Congruent Numbers — Tunnell's Criterion (Odd Case)Open Problem
Which whole numbers are the area of a right triangle with rational sides? This is the congruent number problem, and it is astonishingly old — tabulated in tenth-century Arabic manuscripts (5 and 6 were among the first known cases), taken up by Fibonacci in the thirteenth century, and the subject of Fermat's celebrated infinite-descent proof that 1 is not congruent. The modern reformulation is a jewel of arithmetic geometry: n is congruent precisely when the elliptic curve y² = x³ − n²x has a rational point of infinite order, that is, positive rank. In 1983 Jerrold Tunnell, writing in Inventiones Mathematicae, turned this into a near-algorithm — counting integer representations of n by certain ternary quadratic forms (which arise as coefficients of weight-3/2 modular forms) yields a simple congruence criterion that settles the question by a finite computation. The catch, and the reason the problem remains officially open, is that the sufficiency of Tunnell's criterion rests on the Birch and Swinnerton-Dyer conjecture, itself a Millennium Prize Problem. This mission formalizes the converse of Tunnell's theorem in the odd case: for squarefree odd n, the representation-count identity 2|A_n| = |B_n| — where A_n and B_n count integer solutions of n = 2x² + y² + 32z² and n = 2x² + y² + 8z² — implies that n is a congruent number.
That the prime numbers, thinning out as they climb yet never quite vanishing, should nonetheless contain arithmetic progressions of every finite length is one of the most celebrated discoveries of twenty-first-century mathematics. Ben Green and Terence Tao proved it in 2004 (published in the Annals of Mathematics in 2008), resolving a question whose roots reach back to Lagrange and Waring around 1770 and which had crystallized in the Erdős–Turán conjecture. The primes have density zero, so Szemerédi's theorem — which guarantees long progressions only in positive-density sets — does not apply directly; the genius of the proof was a transference principle extending Szemerédi's theorem to sets sitting densely inside a 'pseudorandom' host, built from the sieve ideas of Goldston, Pintz, and Yıldırım. The result was a centerpiece of the citation for Tao's 2006 Fields Medal and opened a whole industry, including the Tao–Ziegler extension to polynomial progressions. Unusually for a headline problem, this theorem is already proved — which makes it an ideal flagship formalization mission: a deep, decomposable argument whose pieces, from Szemerédi's theorem to the transference principle, the community can rebuild and verify in Lean.
In a 1999 Vienna doctoral thesis, Gerhard Zauner conjectured that in every finite dimension d one can find d² unit vectors in complex d-space that are mutually as spread out as possible — any two sharing the same squared overlap 1/(d+1). Such a configuration, a symmetric informationally complete positive operator-valued measure (SIC-POVM), is the optimal minimal measurement for reconstructing an unknown quantum state, which is why the idea was rediscovered and named by Renes, Blume-Kohout, Scott, and Caves in 2004 and became central to quantum tomography, quantum cryptography, and the QBist reading of quantum mechanics. Geometrically these are maximal sets of complex equiangular lines; physically they are the most efficient quantum measurements; and, remarkably, they appear to be governed by deep number theory — recent work by Appleby, Flammia, Kopp, and others ties exact SICs to Stark units and Hilbert's twelfth problem on explicit class field theory. Exact solutions have been hand-built in scores of dimensions and numerical ones found in every dimension checked, yet a general existence proof remains out of reach. Formalizing Zauner's conjecture gives this problem — straddling quantum information, geometry, and algebraic number theory — a precise shared target.
A Hadamard matrix is a square array of +1s and −1s whose rows are mutually orthogonal — equivalently, one whose determinant attains the absolute maximum that Jacques Hadamard proved in 1893 any ±1 matrix can reach. The story opens earlier, with James Joseph Sylvester's 1867 doubling construction producing such matrices in every power-of-two order; Hadamard himself added orders 12 and 20. The conjecture bearing his name asserts that a Hadamard matrix exists for every order divisible by four. Raymond Paley's 1933 construction from finite fields settled vast new families, and computer searches filled stubborn gaps — beginning with order 92 at JPL in 1962 and reaching order 428 only in 2005, after which 668 became the smallest order whose existence is still unknown. Far from a curiosity, these matrices are workhorses of applied mathematics, underpinning error-correcting codes (the Reed–Muller code that sharpened Mariner spacecraft imagery), spread-spectrum and CDMA signal design, optimal statistical designs of experiments, and coded-aperture spectroscopy. Settling the conjecture would close a 130-year-old gap where combinatorics, number theory, and design theory meet.
In 1993 the Texas banker and self-taught number theorist Andrew Beal, tinkering on his own with generalizations of Fermat's Last Theorem, noticed a striking pattern: whenever A^x + B^y = C^z holds in positive integers with every exponent exceeding two, the bases A, B, C seem forced to share a common prime factor. Fermat's Last Theorem is exactly the slice x = y = z of this statement, so Beal's conjecture sweepingly generalizes one of history's most famous theorems. Beal backed his question with money, raising the prize from $5,000 in 1997 to $1,000,000, now held in trust by the American Mathematical Society. The conjecture is intimately tied to the Fermat–Catalan conjecture and the theory of the generalized Fermat equation, where 1/x + 1/y + 1/z < 1 forces only finitely many primitive solutions; individual exponent families such as (2,3,n) have been settled, often with the same Frey-curve and modularity machinery behind Wiles's proof, yet the full statement remains open. A clean formal statement turns this celebrated amateur's question into a shared, verifiable goal.
Formulated in 1985 by Joseph Oesterlé and David Masser as an arithmetic distillation of Szpiro's conjecture on elliptic curves, the abc conjecture makes a deceptively simple claim about coprime triples with a + b = c: the three numbers cannot all be built from many repeated small primes at once, so c can only rarely exceed rad(abc)^(1+ε). Dorian Goldfeld called it 'the most important unsolved problem in Diophantine analysis,' and for good reason — a single proof would cascade through number theory, delivering Fermat's Last Theorem for all large exponents almost for free, along with Roth's theorem, the Mordell–Faltings theorem, the Fermat–Catalan conjecture, infinitely many non-Wieferich primes, and all but finitely many counterexamples to Beal's conjecture. Since 2012 Shinichi Mochizuki has claimed a proof via inter-universal Teichmüller theory, published in 2021, but the community has not accepted it: in 2018 Peter Scholze and Jakob Stix identified a gap they regarded as fatal. A precise formal statement gives everyone a shared, machine-checkable target around which to organize verified progress.
A complete formal proof of Fermats Last Theorem for exponent 5: for all positive natural numbers a,b,c, a^5 + b^5 != c^5. The proof follows the classical Legendre-Dirichlet approach (1825-1830): Case 1 (5 does not divide a,b,c) is dispatched by congruences, and Case 2 (5 divides one of them) uses infinite descent through the ring Z[zeta_5]. The open hard leaf is the Z[zeta_5] PID step (flt5_zeta5_ring_witnesses).