Bandit Algorithms XI: Lower Bounds for Stochastic Linear BanditsTextbook
Is the $d\sqrt{n}$ regret of LinUCB (Mission X) an artifact of the algorithm or a law of nature? Chapters 24–25 of Lattimore–Szepesvári prove it is essentially unimprovable. On the unit ball there is a parameter $\theta$ with $\|\theta\|_2^2 = d^2/(48n)$ forcing $R_n \ge \frac{d\sqrt{n}}{16\sqrt{3}}$ — the goal theorem — and the hypercube gives the same $\Omega(d\sqrt{n})$ rate. The asymptotic chapter is more striking still: for fixed finite action sets, the instance-optimal constant $c(\mathcal{A},\theta)$ is characterized by an allocation program, and *optimism itself is provably suboptimal* — LinUCB and Thompson sampling cannot achieve it, because exploration must sometimes deliberately play actions optimism would never touch. These lower bounds define the targets for the entire linear-bandit literature.
Bandit Algorithms X: Stochastic Linear Bandits and LinUCBTextbook
When actions are feature vectors and the mean reward is linear — $X_t = \langle \theta_*, A_t\rangle + \eta_t$ — a bandit can generalize across arms: pulling one arm reveals information about all of them. Chapter 19 of Lattimore–Szepesvári carries the optimism principle into this setting: LinUCB (a.k.a. OFUL) plays the action maximizing $\max_{\theta\in\mathcal{C}_t}\langle\theta, a\rangle$ over the confidence ellipsoid $\mathcal{C}_t$ of Mission IX. The goal theorem: with probability $1-\delta$, $\hat R_n \le \sqrt{8n\beta_n \log\frac{\det V_n}{\det V_0}} \le \sqrt{8dn\beta_n\log\frac{d\lambda + nL^2}{d\lambda}}$ — regret $\tilde O(d\sqrt{n})$ independent of the number of actions. The combinatorial engine is the elliptical potential lemma, bounding how many times adaptively chosen directions can be surprising. Chapter 22's phased elimination with G-optimal design (Mission IX) sharpens this to $\tilde O(\sqrt{dn\log k})$ for finite action sets.
Bandit Algorithms IX: Self-Normalized Concentration and Optimal DesignTextbook
Least-squares estimation from *adaptively* collected data is the statistical heart of linear bandits: the actions $A_t$ depend on past noise, so classical fixed-design theory does not apply. Chapter 20 of Lattimore–Szepesvári resolves this with the method of mixtures: the process $M_t(x) = \exp(\langle x, S_t\rangle - \frac{1}{2}\|x\|^2_{V_t(\lambda)})$ is a supermartingale, and integrating over a Gaussian mixture yields the self-normalized bound — the goal theorem — $\mathbb{P}\big(\exists t : \|S_t\|^2_{V_t(\lambda)^{-1}} \ge 2\log\frac{1}{\delta} + \log\frac{\det V_t(\lambda)}{\lambda^d}\big) \le \delta$, valid uniformly over all times. The resulting confidence ellipsoids for the regularized least-squares estimator (Abbasi-Yadkori et al.) calibrate every algorithm of Mission X. The mission also formalizes the Kiefer–Wolfowitz theorem of Chapter 21: G-optimal and D-optimal experimental designs coincide, with optimal value exactly $d$ — the classical equivalence theorem of optimal design theory.
Bandit Algorithms VIII: Contextual Bandits and Exp4Textbook
Real decisions come with context: a news site chooses an article *for a particular user*. Competing with the single best arm is then meaningless; the right benchmark is the best mapping from contexts to arms, or more generally the best of $M$ expert policies. Chapter 18 of Lattimore–Szepesvári formalizes this via Exp4 — exponential weighting over experts, fed by the importance-weighted estimator of Mission V. The goal theorem: with learning rate $\eta = \sqrt{2\log(M)/(nk)}$, Exp4 satisfies $R_n \le \sqrt{2nk\log M}$ against the best of $M$ experts. Since $M$ enters only logarithmically, the learner can compete with exponentially large policy classes — the conceptual gateway from bandits to reinforcement learning with function approximation.
Single-Server Queueing Convergence via Forward CouplingTextbook
Formalize sample-path stability for a continuous-time, unit-rate, infinite-buffer single-server queue. Starting from cumulative arriving service work, define the reflected transient workload, the workload constructed from the infinite past, long-run offered load, and two-time stationarity. Prove that subcritical load forces finite-time coupling and consequently that every finite initial workload converges in its two-time finite-dimensional distributions to the stationary workload law.
Formalize sample-path Little's Law for deterministic continuous-time queueing trajectories, decomposed into area, sojourn, arrival-rate, boundary, and squeeze lemmas.
First raised for two variables by Ludwig Kraus in 1884 and stated in full generality by Ott-Heinrich Keller in 1939, the Jacobian conjecture asks something that sounds almost like freshman calculus: if a polynomial map from complex n-space to itself has a Jacobian determinant equal to a nonzero constant, must it be invertible by another polynomial map? That constant-Jacobian condition is precisely the algebraic shadow of the inverse function theorem, yet producing a polynomial — not merely analytic — inverse has resisted every attack for over eighty years. Shreeram Abhyankar championed the problem because it can be stated 'using little beyond a knowledge of calculus,' and Stephen Smale placed it sixteenth on his 1998 list of problems for the new century. Its notoriety is sharpened by a graveyard of published 'proofs' that later collapsed. Deep reductions exist — Bass, Connell, and Wright showed in 1982 that the general case reduces to maps of degree three — and the problem is equivalent, through work of Tsuchimoto, Belov-Kanel, and Kontsevich, to the Dixmier conjecture on the Weyl algebra. A formal statement anchors this famously slippery problem so that progress can be verified rather than merely believed.
The Hardy-Littlewood Method I: Weyl's InequalityTextbook
## Motivation
The Hardy--Littlewood circle method is the principal analytic tool for counting solutions to additive equations in integers. Introduced by Hardy and Ramanujan for the partition function and developed by Hardy and Littlewood in their *Partitio Numerorum* series (1920--1928), it produces asymptotic formulae for the number of representations of a large integer $n$ as a sum of $s$ terms drawn from a prescribed set — $k$-th powers, primes, values of a polynomial.
Its engine is an estimate for **exponential sums**. If a sum $\sum_{x<N} e(\alpha x^k)$, where $e(\theta)=\exp(2\pi i\theta)$, exhibits cancellation for every $\alpha$ not well approximable by a rational with small denominator, the method delivers an asymptotic formula; if it does not, the method stalls. Weyl's inequality (Weyl 1916) was the first such estimate and remains the standard one for moderate $k$.
A short timeline of the estimate this mission targets. Weyl (1916) proved the inequality below with the exponent $2^{1-k}$, in the course of his work on uniform distribution. Hardy and Littlewood (1920--1928) built the circle method on it, obtaining $G(k)\le (k-2)2^{k-1}+5$ for Waring's problem. Vinogradov (1935) replaced Weyl differencing by his mean value theorem, superior for large $k$, reducing the bound to $O(k\log k)$; Wooley's efficient congruencing (2012) and the Bourgain--Demeter--Guth decoupling theorem (2016) settled the main conjecture of Vinogradov's mean value theorem. For small $k$ — and as the entry point to the subject — Weyl's inequality is still the right tool, and it is the natural first capstone for a formalization of the method.
## Setting
For a real number $\theta$ write
$$e(\theta) \;=\; \exp(2\pi i \theta),$$
the standard additive character of $\mathbb{R}/\mathbb{Z}$: it satisfies $e(x+y)=e(x)e(y)$, $|e(x)|=1$, and $e(x)=1$ exactly when $x\in\mathbb{Z}$.
For a real number $\theta$ write $\|\theta\|$ for the distance from $\theta$ to the nearest integer. It is periodic with period $1$, vanishes exactly on $\mathbb{Z}$, satisfies the triangle inequality, and is at most $\tfrac12$.
Given a finite set $A\subseteq\mathbb{Z}$, its generating function is $f_A(\theta)=\sum_{a\in A}e(a\theta)$. The basic identity of the subject is
$$\int_0^1 f_A(\theta)^s\,e(-n\theta)\,d\theta \;=\; \#\{(a_1,\dots,a_s)\in A^s : a_1+\cdots+a_s=n\},$$
a consequence of the orthogonality relation $\int_0^1 e(m\theta)\,d\theta=[\,m=0\,]$.
A **Weyl sum** of degree $k$ is $\sum_{0\le x<N} e(\alpha x^k)$. The whole difficulty is to bound it for $\alpha$ in the *minor arcs* — those $\alpha$ admitting no rational approximation $a/q$ with $q$ small.
## Target
Fix $k\ge 2$. For every $\varepsilon>0$ there is a constant $C=C(k,\varepsilon)$ such that whenever $(a,q)=1$, $q\ge 1$, and $\left|\alpha-\frac{a}{q}\right|\le \frac{1}{q^2}$,
$$\left|\sum_{0\le x<N} e(\alpha x^{k})\right| \;\le\; C\,N^{1+\varepsilon}\left(\frac{1}{q}+\frac{1}{N}+\frac{q}{N^{k}}\right)^{2^{1-k}}.$$
The intermediate targets, weakest first, are the milestone list: the counting identity, the Weyl differencing (squaring) step, the Farey covering with coprime numerator, the divisor bound $d(n)\ll_\varepsilon n^\varepsilon$, Hua's fourth-moment inequality for $k=2$, and the degree-two case of the inequality itself.
## Significance
*The result itself.* Weyl's inequality is what makes the minor arcs negligible. Applied with $q$ in the range $N^{\delta}\le q\le N^{k-\delta}$ it gives a power saving over the trivial bound $N$, and integrating that saving over the minor arcs shows their contribution is smaller than the main term produced by the major arcs. Every classical application of the circle method — the asymptotic formula in Waring's problem, Vinogradov's three primes theorem, the Birch--Davenport theory of forms in many variables — passes through an estimate of this shape. Without it the method produces an identity, not a theorem.
*Formalizing it.* Mathlib currently contains the analytic prerequisites — Fourier characters on `AddCircle`, Dirichlet's approximation theorem, Abel summation, Gauss sums — but no circle-method apparatus whatsoever: no Weyl sums, no arc dissection, no singular series, no mean value estimates. This mission supplies the first layer. The foundational tier is already machine-checked: **53 theorems** covering the character $e$, the norm $\|\cdot\|$, the geometric sum bound $\left|\sum_{x<N}e(x\theta)\right|\le\min\!\left(N,\frac{1}{2\|\theta\|}\right)$, both orthogonality relations, both forms of Dirichlet's theorem, and the basic theory of $f_A$, are published on the platform with verified proofs and may be imported freely. What remains open is the combinatorial and analytic core listed in the milestones. None of the milestone statements is currently formalized anywhere, to the best of our knowledge.
## Difficulty
The obvious approach fails immediately. One would like to sum $\left|\sum_{x<N}e(\alpha x^k)\right|$ by comparing it to the linear case, where the geometric series gives $\min(N,\frac{1}{2\|\alpha\|})$ outright. But for $k\ge2$ the summand is not a geometric progression and there is no closed form.
Weyl's device is to square and difference: $\left|\sum_x e(\phi(x))\right|^2=\sum_{x,y}e(\phi(x)-\phi(y))$, and the substitution $y=x+h$ turns the inner polynomial into one of degree $k-1$ in $x$. Iterating $k-1$ times reduces to a linear sum, at the cost of raising the estimate to the power $2^{1-k}$ — which is why the saving is so weak for large $k$, and why Vinogradov's method eventually supersedes it.
The genuine obstacles in a formalization are: (i) bookkeeping the shifted ranges produced by each differencing step, which are not $[0,N)$ and must be handled uniformly; (ii) the divisor bound $d(n)\ll_\varepsilon n^\varepsilon$, needed to count the $h$ for which the resulting linear coefficient is close to an integer, and which is not currently in Mathlib in this form; (iii) tracking the $\varepsilon$-dependent constants through $k-1$ iterations without the informal $\ll$ notation.
## Formalization scope
Statements are given over the Prove2Me default environment (Lean `v4.30.0`, Mathlib `c5ea003`), in the shared namespace `CircleMethod`, and build on two published definitions: `CircleMethod_char` (the character `e` and the norm `nrm`) and `CircleMethod_genfun` (the generating function `f`).
Conventions this mission commits to:
- $\|\theta\|$ is `nrm θ = |θ - round θ|`. Mathlib's `round` breaks ties upwards, so `round` is *not* an odd function; the characterisation to use is minimality, `nrm θ ≤ |θ - n|` for every integer `n`, which is published as `CircleMethod.nrm_le`.
- Sums run over `Finset.range N`, that is $0\le x<N$, and $N$ is a natural number. Hypotheses `0 < N` and `0 < q` are stated explicitly rather than left implicit.
- Asymptotic notation is eliminated in favour of explicit existential constants: $X\ll_\varepsilon Y$ is rendered as `∀ ε > 0, ∃ C > 0, ∀ …, X ≤ C * Y`, with the constant quantified *outside* the parameters it may depend on and *inside* nothing else. Solvers should not weaken this by allowing $C$ to depend on $N$, $q$ or $\alpha$.
- Exponents such as $N^{1+\varepsilon}$ and $2^{1-k}$ are real powers (`Real.rpow`), not natural powers.
- Coprimality is `Nat.Coprime a.natAbs q`, which is the correct notion for a possibly negative numerator.
One trivialising formalization to rule out: the goal must not be read with $C$ permitted to depend on $N$, since then $C=N$ makes it vacuous. The quantifier order in the Lean statement already forbids this, and solvers should preserve it exactly.
Contributions welcome on any milestone independently; the divisor bound and the Farey covering are self-contained and need no other milestone. Both are reusable well beyond this mission.
## Selected references
- H. Weyl, *Über die Gleichverteilung von Zahlen mod. Eins*, Mathematische Annalen 77 (1916), 313--352. [DOI:10.1007/BF01475864](https://doi.org/10.1007/BF01475864)
- G. H. Hardy and J. E. Littlewood, *Some problems of 'Partitio Numerorum' I--VI*, 1920--1928.
- R. C. Vaughan, *The Hardy--Littlewood Method*, 2nd ed., Cambridge Tracts in Mathematics 125, Cambridge University Press, 1997. (Weyl's inequality is Lemma 2.4; the geometric sum bound is Lemma 2.1.)
- I. M. Vinogradov, *New estimates for Weyl sums*, Doklady Akademii Nauk SSSR 8 (1935), 195--198.
- T. D. Wooley, *Vinogradov's mean value theorem via efficient congruencing*, Annals of Mathematics 175 (2012), 1575--1627. [DOI:10.4007/annals.2012.175.3.12](https://doi.org/10.4007/annals.2012.175.3.12)
- J. Bourgain, C. Demeter and L. Guth, *Proof of the main conjecture in Vinogradov's mean value theorem for degrees higher than three*, Annals of Mathematics 184 (2016), 633--682. [DOI:10.4007/annals.2016.184.2.7](https://doi.org/10.4007/annals.2016.184.2.7)
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.
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.
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).