The mathematical discipline of drawing inferences from data under uncertainty: estimation, hypothesis testing, prediction, and the quantification of confidence. Grounded in probability, it spans classical and Bayesian inference, experimental design, and modern high-dimensional and nonparametric theory, asking what data can reveal and with what guarantees.
Missions
🏆Completed
Captain: Shuze Chen
Exact Matrix CompletionResearch Paper
Every time a streaming service guesses what you would rate a film you have never seen, it is solving a matrix completion problem: fill in the missing entries of a vast user-by-item table from the few that are observed. The question became famous during the Netflix Prize (2006-2009), and it looks hopeless - infinitely many matrices fit the observed entries - until one assumes the structure that makes recommendation possible: the table is essentially low rank, because tastes are governed by a few latent factors. In their landmark 2009 paper 'Exact Matrix Completion via Convex Optimization' (Foundations of Computational Mathematics), Emmanuel Candes and Benjamin Recht proved that an n-by-n matrix of rank r can be recovered exactly, with high probability, from only about n^1.2 * r * log n randomly observed entries - not by the NP-hard route of minimizing rank, but by minimizing the nuclear norm, a convex surrogate (the sum of the singular values) solvable efficiently. The proof, in the lineage of Candes-Romberg-Tao compressed sensing, turns on two ideas: an incoherence condition ensuring the singular vectors are spread out rather than spiky, and a dual certificate witnessing optimality, whose existence rests on delicate random-matrix concentration. It transformed a practical engineering puzzle into rigorous theory and seeded a decade of work across machine learning, signal processing, computer vision, and sensor localization. This mission formalizes the Candes-Recht exact-recovery theorem in Lean, decomposed into its dual-certificate construction and the probabilistic concentration reductions at its core.
594 thms9 active usersReviewed
Captain: Shuze Chen
The Markov Chain Central Limit TheoremResearch Paper
Markov chain Monte Carlo turns hard integration problems into long simulations: to estimate an expectation $E_\pi f$ one runs a Markov chain with stationary distribution $\pi$ and reports the sample average $\bar f_n$. The ergodic theorem guarantees $\bar f_n \to E_\pi f$, but honest error bars require more: a central limit theorem $$\sqrt{n}(\bar f_n - E_\pi f) \to_d N(0, \sigma_f^2).$$ On general state spaces this is famously delicate - a merely ergodic chain with a square-integrable functional can fail the CLT, so the classical theory trades convergence rates (drift, minorization, geometric or polynomial total-variation rates) and mixing conditions ($\alpha$-, $\rho$-, $\varphi$-mixing) against moment conditions on $f$. This mission formalizes G. L. Jones's survey "On the Markov chain central limit theorem" (Probability Surveys, 2004): the drift-condition CLTs of Meyn-Tweedie and Jarner-Roberts, the classical mixing CLTs of Ibragimov-Linnik, Doukhan-Massart-Rio and Billingsley, the characterizations via uniform integrability and boundedness in probability, and their assembly into the summary theorem: six practically checkable regimes - from polynomial ergodicity with bounded functionals to uniform ergodicity with second moments - each of which guarantees the CLT for every initial distribution. The stationarity, total-variation and mixing infrastructure is general state space and reusable well beyond this mission.
96 thms5 active usersReviewed
🏆Completed
Captain: Shuze Chen
Matrix Completion has No Spurious Local MinimumResearch Paper
Matrix completion — recovering a low-rank matrix $M = ZZ^\top$ from a small random subset of its entries — powers recommender systems and collaborative filtering. In practice it is solved by running (stochastic) gradient descent on the non-convex objective $$f(X)=\min_X\frac12\|P_\Omega(M-XX^\top)\|_F^2+\lambda R(X)$$
where $\Omega=\{(i,j)|M_{i,j} \text{ is observed}\}$ and $R(X)$ is a certain regularizer. from a random starting point, and it just works.
Ge, Lee and Ma (NeurIPS 2016 Best student paper award) explained why: the regularized objective has *no spurious local minima* — every local minimum is global and exactly recovers $M$. This mission formalizes that landmark theorem in Lean 4, in its strongest known form and along its simplest known proof: the unified landscape analysis of Ge–Jin–Zheng (ICML 2017) and an improved sampling bound in Chen–Li (JMLR 2019). Conditional on an explicit good-sample predicate (which holds with high probability under Bernoulli sampling), every local minimum $X$ of $f$ satisfies $XX^\top = ZZ^\top$.
14 thms4 active users
🏆Completed
Captain: Shuze Chen
Vector Space Methods III: Recursive EstimationTextbook
## Motivation
The final sections of Chapter 4 of Luenberger's *Optimization by Vector Space Methods* (Wiley, 1969) derive the **discrete-time Kalman filter** (§4.7 Theorem 1, attributed to Kalman 1960) purely from Hilbert space geometry: the optimal estimate of a linearly evolving random state is an orthogonal projection onto the span of past measurements, and the projection updates recursively as measurements arrive. This derivation — no Gaussian assumptions, no density calculations — is a canonical application of the projection theorem formalized in Mission I and the estimation theory of Mission II.
## Setting
Following §4.2 and §4.7 of the source, all random variables have zero mean and finite second moments, and are treated as elements of a **Hilbert space of random variables**: an abstract real inner product space $H$ in which the inner product of two random variables is their correlation, $\langle a, b\rangle = E[ab]$. Random $n$-vectors are families $\mathrm{Fin}\ n \to H$; two random variables are **uncorrelated** iff they are orthogonal in $H$; the **covariance matrix** of a zero-mean random vector $x$ is the Gram matrix $\langle x_i, x_j\rangle$. A **white** process $u$ satisfies $E[u(k)u(l)^\top] = Q(k)\,\delta_{kl}$.
The **dynamic model** (§4.7) consists of a state process and measurements
$$x(k+1) = \Phi(k)\,x(k) + u(k), \qquad v(k) = M(k)\,x(k) + w(k), \qquad k = 0, 1, 2, \dots$$
with known matrices $\Phi(k) \in \mathbb{R}^{n\times n}$, $M(k) \in \mathbb{R}^{m\times n}$, white noises $u, w$ with covariances $Q(k)$, $R(k)$ ($R(k)$ positive definite), mutually uncorrelated and uncorrelated with the initial state $x(0)$. The estimate $\hat x(k+1 \mid k)$ is the projection of each component of $x(k+1)$ onto the subspace spanned by the components of $v(0), \dots, v(k)$.
## Formalization targets
The goal is §4.7 Theorem 1: the estimates generated by the recursion
$$\hat x(k+1 \mid k) = \Phi(k) P(k) M^\top(k)\big[M(k)P(k)M^\top(k) + R(k)\big]^{-1}\big(v(k) - M(k)\hat x(k \mid k-1)\big) + \Phi(k)\, \hat x(k \mid k-1)$$
$$P(k+1) = \Phi(k) P(k)\big\{I - M^\top(k)[M(k)P(k)M^\top(k) + R(k)]^{-1} M(k) P(k)\big\}\Phi^\top(k) + Q(k),$$
started from $\hat x(0 \mid -1) = 0$ and $P(0) = \operatorname{cov} x(0)$, are the linear minimum-variance estimates: each $\hat x(k \mid k-1)$ lies in the span of past measurement components, its error is orthogonal to all past measurements, and its error covariance is $P(k)$.
Milestones: orthogonality of the **innovation** $v(k) - M(k)\hat x(k\mid k-1)$ to the past-data subspace, and the single-step **updating formula** (§4.6 Example 1) — given a prior projection with error covariance $R$ and new data $y = W\beta + \varepsilon$, the updated projection is $\hat\beta + RW^\top(WRW^\top + Q)^{-1}(y - W\hat\beta)$ with error covariance $R - RW^\top(WRW^\top+Q)^{-1}WR$.
## Significance
The Kalman filter is among the most used algorithms in engineering — navigation, tracking, control, time-series analysis — and this mission gives it a machine-checked correctness statement at the natural level of generality: linear minimum-variance optimality over arbitrary zero-mean second-order processes, with no Gaussian hypothesis. Mathlib currently has no Kalman filter and no linear filtering theory. The abstract Hilbert-space formulation also makes the development directly reusable: the update milestone is a general two-stage projection lemma independent of the dynamic model.
## Difficulty
The recursion couples two invariants that must be established simultaneously by induction: the geometric one (the error is orthogonal to the growing measurement subspace, and the estimate lies in it) and the algebraic one (the error Gram matrix equals $P(k)$). Whiteness enters precisely through the index inequalities — $u(k)$ and $w(k)$ are orthogonal to everything generated by $x(0), u(0..k{-}1), w(0..k{-}1)$ — and an off-by-one in these ranges silently breaks the induction. Invertibility of $M(k)P(k)M^\top(k) + R(k)$ must be derived, not assumed: $P(k)$ is positive semidefinite as a Gram matrix and $R(k)$ is positive definite. The naive approach of expanding all projections over a concrete probability space adds measure-theoretic overhead the abstract formulation avoids entirely.
## Formalization scope
The Hilbert space of random variables is an abstract `H : Type` with `[NormedAddCommGroup H] [InnerProductSpace ℝ H]`; **zero means are implicit** in this representation (§4.7 assumes all variables zero-mean), so expectations never appear — only inner products. Matrix-vector actions on random vectors are written componentwise as `∑ j, A i j • x j`. Processes are indexed by `ℕ`, with `x̂(0 | -1)` rendered as `xh 0 = 0` and covariances as explicit Gram identities. Whiteness and uncorrelatedness are hypotheses on inner products with `if k = l then _ else 0`. The span of past data at time $k$ is `Submodule.span ℝ {a | ∃ l < k, ∃ j, a = v l j}`. The recursion defining `xh` and `P` is supplied as hypotheses, so the goal asserts exactly the optimality and covariance claims of the source theorem. Statements deliberately avoid Mathlib's `orthogonalProjection`; the projection property is asserted by membership plus orthogonality, which characterizes it uniquely.
## Selected references
- David G. Luenberger, *Optimization by Vector Space Methods*, John Wiley & Sons, 1969. §4.6–4.7, pp. 90–97. ISBN 0-471-55359-X.
- R. E. Kalman, *A new approach to linear filtering and prediction problems*, J. Basic Eng. 82 (1960), 35–45. https://doi.org/10.1115/1.3662552
4 thms2 active usersReviewed
🏆Completed
Captain: Shuze Chen
Treatment Locality in A/B TestingResearch Paper
Modern A/B tests must infer *lifetime* treatment effects — e.g. customer lifetime value under a new feature — from short-horizon experiment data. Chen, Simchi-Levi and Wang (arXiv:2407.19618) model the experiment as a Markov decision process and exploit a structural fact of many practical interventions: the treatment is *local*, modifying the system at a single crucial state only. This mission formalizes the core asymptotic theory of the paper: for **any** differentiable estimator built from the experiment's transition and reward statistics, *information sharing* — pooling across test arms the samples collected away from the treated state — keeps the estimator asymptotically normal with the same asymptotic bias and never increases its asymptotic variance (Theorem 9), and is asymptotically efficient among unbiased estimators (Theorem 5). The route runs through a Markov chain central limit theorem with the asymptotic variance identified as the autocovariance series, and the linearization/delta method for functionals of chain statistics.
42 thms2 active users
🏆Completed
Captain: Shuze Chen
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).