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.
Bandit Algorithms III: Asymptotic and Minimax Optimality of UCBTextbook
The basic UCB regret bound of Mission II is logarithmic but not tight: its leading constant $16/\Delta_i$ is eight times the information-theoretic limit, and its worst-case rate carries a spurious $\sqrt{\log n}$. Chapters 8–9 of Lattimore–Szepesvári close both gaps. A refined confidence schedule $f(t) = 1 + t\log^2 t$ yields the asymptotically optimal $\limsup_{n\to\infty} R_n/\log n \le \sum_{i:\Delta_i>0} 2/\Delta_i$ — exactly matching the instance-dependent lower bound of Mission VII for Gaussian noise. The MOSS index $\hat\mu_i + \sqrt{\tfrac{4}{T_i}\log^+\!\big(\tfrac{n}{k T_i}\big)}$ achieves minimax regret $R_n \le 39\sqrt{kn} + \sum_i \Delta_i$, matching the $\Omega(\sqrt{kn})$ lower bound up to a constant. These two theorems are the gold standard for finite-armed stochastic bandits.
Bandit Algorithms II: Stochastic Bandits and the UCB AlgorithmTextbook
A learner repeatedly chooses one of $k$ slot machines, observes only the reward of the chosen arm, and wants to earn almost as much as the best arm in hindsight. This is the stochastic multi-armed bandit, the canonical model of the exploration–exploitation dilemma. This mission formalizes the model (environments, policies, regret, and the regret decomposition $R_n = \sum_i \Delta_i\,\mathbb{E}[T_i(n)]$) and the two classical algorithms of Chapters 6–7 of Lattimore–Szepesvári: Explore-Then-Commit and the Upper Confidence Bound algorithm built on the optimism principle. The goal theorem is the instance-dependent UCB regret bound $R_n \le 3\sum_i \Delta_i + \sum_{i:\Delta_i>0} 16\log(n)/\Delta_i$ — logarithmic regret with explicit constants, the single most cited result of bandit theory — together with its distribution-free companion $R_n \le 8\sqrt{nk\log n} + 3\sum_i \Delta_i$.
Bandit Algorithms V: Adversarial Bandits and Exp3Textbook
What if the rewards are not random at all, but chosen by an adversary who knows your algorithm? Remarkably, a randomized learner can still compete with the best fixed arm in hindsight. Chapters 11–12 of Lattimore–Szepesvári develop the adversarial $k$-armed bandit: rewards $x_{ti} \in [0,1]$ are an arbitrary fixed matrix, the learner samples $A_t \sim P_t$, and regret is measured against $\max_i \sum_t x_{ti}$. The exponential-weights algorithm Exp3, fed by importance-weighted loss estimates $\hat X_{ti} = 1 - \mathbb{1}\{A_t = i\}(1 - X_t)/P_{ti}$, achieves $R_n \le \sqrt{2nk\log k}$ — the goal theorem. The companion Exp3-IX, which deliberately biases its estimator, upgrades this to a bound holding with high probability rather than only in expectation. These results are the foundation of all adversarial online learning with partial feedback.
Convex Optimization VI: Self-Concordance and the Barrier MethodTextbook
Why do interior-point methods solve convex programs in $O(\sqrt{m}\log(1/\varepsilon))$ Newton steps? Nesterov and Nemirovskii's answer is **self-concordance**: a convex function whose third derivative is controlled by its second, $|\varphi'''(t)| \le 2\,\varphi''(t)^{3/2}$ along every line, admits a Newton analysis with *absolute* constants and no condition number — and the logarithmic barrier is self-concordant. This mission formalizes §9.6 and Chapter 11 of Boyd & Vandenberghe: the self-concordance calculus, the Newton-decrement analysis, the duality gap $m/t$ along the central path, the per-centering work bound $m(\mu - 1 - \log\mu)/\gamma + c$, and the crown result — with the aggressive schedule $\mu = 1 + 1/\sqrt{m}$ the barrier method reaches duality gap $\varepsilon$ after
$$\Bigl\lceil \sqrt{m}\,\log_2\bigl(m/(t^{(0)}\varepsilon)\bigr)\Bigr\rceil$$
centering steps, each of uniformly bounded Newton cost.
Convex Optimization III: Conic Duality and the S-procedureTextbook
Two quadratic functions can be compared losslessly. The **S-procedure** says that, when the constraint is strictly feasible, the implication
$$q_1(x) \le 0 \;\Longrightarrow\; q_2(x) \le 0, \qquad q_k(x) = x^{T}F_k x + 2g_k^{T}x + h_k,$$
holds if and only if a single nonnegative multiplier certifies it as a matrix inequality, $\lambda \begin{bmatrix} F_1 & g_1 \\ g_1^{T} & h_1\end{bmatrix} \succeq \begin{bmatrix} F_2 & g_2 \\ g_2^{T} & h_2\end{bmatrix}$ for some $\lambda \ge 0$. It is a cornerstone of control theory, trust-region methods and robust optimization, and a rare case in which a nonconvex problem has zero duality gap. The route runs through the theory this mission builds from Boyd & Vandenberghe §5.8–5.9 and Appendix B: strong alternatives for convex inequality systems, cone-program strong duality under a generalized Slater condition, semidefinite programming duality, the LMI theorems of alternatives, and the hidden convexity of the joint range of two quadratic forms.
Log-concave functions are the meeting point of convex analysis and probability: densities of Gaussian, exponential, uniform and Wishart distributions are all log-concave, and countless facts of applied probability flow from one structural theorem — integrating out variables preserves log-concavity. This mission builds the convex-analysis spine of Boyd & Vandenberghe's *Convex Optimization* (Chapters 2–3) — separation and supporting hyperplanes, dual cones, the first- and second-order differential characterizations of convexity, Fenchel conjugacy — and climbs to Prékopa's theorem via the Prékopa–Leindler inequality, a landmark of Brunn–Minkowski theory absent from Mathlib.
Bandit Algorithms XIV: Bayesian Bandits, the Gittins Index and Thompson SamplingTextbook
The oldest bandit algorithm (Thompson, 1933) is also the most modern: sample a parameter from the posterior and act greedily. Chapters 34–36 of Lattimore–Szepesvári develop the Bayesian view in two crowning results. The Gittins index theorem: for infinite-horizon discounted Markov bandits, the seemingly intractable dynamic program is solved *exactly* by an index policy — each arm gets a retirement-value index computable arm-by-arm, and playing the largest index is Bayesian optimal. And the frequentist analysis of Thompson sampling — the goal theorem: with Gaussian posteriors, Thompson sampling on 1-subgaussian bandits achieves $\lim_{n\to\infty} R_n/\log n = \sum_{i:\Delta_i>0} 2/\Delta_i$, exactly asymptotically optimal, alongside the minimax-grade $R_n \le C\sqrt{kn\log n}$. Together they explain why posterior sampling is both principled and practically dominant.
Bandit Algorithms VII: Lower Bounds for Finite-Armed BanditsTextbook
How well can any algorithm possibly do? Chapters 13–17 of Lattimore–Szepesvári answer with three matching impossibility results. The divergence decomposition identifies the information a policy collects: $D(\mathbb{P}_{\nu\pi}, \mathbb{P}_{\nu'\pi}) = \sum_i \mathbb{E}[T_i(n)] D(P_i, P_i')$. Feeding it into the Bretagnolle–Huber inequality of Mission VI yields the goal theorem — the minimax lower bound $R_n \ge \frac{1}{27}\sqrt{(k-1)n}$ over Gaussian bandits, showing MOSS (Mission III) is optimal up to a constant. The same machinery gives the instance-dependent bound of Lai–Robbins type: every consistent policy suffers $\liminf_n R_n/\log n \ge \sum_{i:\Delta_i>0} \Delta_i / d_{\inf}(P_i, \mu^*, \mathcal{M}_i)$, certifying the asymptotic optimality of the UCB of Mission III and KL-UCB of Mission IV, and a high-probability lower bound showing the Exp3-IX guarantees of Mission V cannot be improved.
Every lower bound in bandit theory rests on one question: how hard is it to tell two probability measures apart from a sample? The answer is quantified by the relative entropy $D(P,Q)$, and the sharpest elementary tool is the Bretagnolle–Huber inequality: for any event $A$, $P(A) + Q(A^c) \ge \frac{1}{2}\exp(-D(P,Q))$ — no test can distinguish $P$ from $Q$ with total error probability below $\frac{1}{2}e^{-D(P,Q)}$. This mission formalizes Chapter 14 of Lattimore–Szepesvári: the Bretagnolle–Huber inequality (the goal theorem, proved via Le Cam's inequality $\int p \wedge q \ge \frac{1}{2}(\int\sqrt{pq})^2$), Pinsker's inequality $\delta(P,Q) \le \sqrt{D(P,Q)/2}$, and the closed-form divergences between Gaussians and Bernoullis. These half-page inequalities power every impossibility result in Missions VII, XI and beyond.
The classical convergence theory of smooth convex minimization. For a function that is $m$-strongly convex and $M$-smooth ($mI \preceq \nabla^2 f(x) \preceq MI$), gradient descent converges linearly, while Newton's method exhibits its famous two phases: a *damped* phase in which every backtracking step decreases the objective by a fixed amount $\gamma$, and a *quadratically convergent* phase in which the scaled gradient norm squares at each step, $\tfrac{L}{2m^2}\lVert \nabla f(x^{+})\rVert_2 \le \bigl(\tfrac{L}{2m^2}\lVert \nabla f(x)\rVert_2\bigr)^2$. Together they give the iteration count of B&V (9.36),
$$\#\text{iterations} \;\le\; \frac{f(x^{(0)}) - p^{\star}}{\gamma} \;+\; \log_2\log_2(\varepsilon_0/\varepsilon), \qquad \gamma = \frac{\alpha\beta\eta^2 m}{M^2}, \quad \varepsilon_0 = \frac{2m^3}{L^2},$$
with $L$ the Lipschitz constant of the Hessian and $\alpha,\beta$ the backtracking parameters. This mission formalizes Chapters 9–10 of Boyd & Vandenberghe with every constant exactly as printed — a quantitative theory entirely absent from Mathlib.
The Karush–Kuhn–Tucker conditions are the central result of convex optimization: for a convex differentiable problem satisfying Slater's condition, a point is optimal exactly when primal feasibility, dual feasibility, complementary slackness and Lagrangian stationarity hold. This mission formalizes Chapters 4–5 of Boyd & Vandenberghe end to end — the first-order optimality criterion, concavity of the Lagrange dual, weak duality, Slater's strong-duality theorem with dual attainment (via the separating-hyperplane argument of §5.3.2), the saddle-point characterization, sensitivity bounds and Pareto scalarization — culminating in the full KKT characterization.
Excursion Coupling for the Monge Problem on the Line (Juillet 2019)Research Paper
The Monge optimal transport problem on the real line with the classical distance cost $|x-y|$ famously fails to have a unique solution. Juillet (2019) restored uniqueness by considering the strictly concave power costs $|x-y|^p$ with $p<1$ and letting $p\to 1^-$: the limit selects a distinguished optimal plan, the *excursion coupling*, built from the level sets of the difference $F_\sigma=F_\mu-F_\nu$ of the cumulative distribution functions. This mission formalizes the completed-graph construction, the generalized Banach indicatrix identities of Bertoin-Yor, the alternating crossing structure of almost every level, and the marginal identities for the crossing counting measures. It culminates in Propositions 3.5-3.6: every monotone transport plan is concentrated on the paired routes, and the marginals uniquely determine the coupling carried by those routes, including in the presence of atoms.
This mission formalizes the key implication 3=>4 in Juillet's Main Theorem.
Introduction to Linear Optimization X: Max-Flow Min-CutTextbook
How much flow can be sent from a source $s$ to a sink $t$ through a network with arc capacities $u_{ij}\in(0,\infty]$ — and what certifies that no more is possible? This mission formalizes §7.4-7.5 of Bertsimas & Tsitsiklis. The circulation calculus of §7.4 supplies the two structural tools: the flow decomposition theorem (Lemma 7.1 — every nonzero nonnegative circulation is a positive combination $\mathbf{f}=\sum_i a_i\mathbf{f}^i$ of simple circulations with only forward arcs, with integer $a_i$ when $\mathbf{f}$ is integer) and the optimality criterion for the minimum cost network flow problem (Theorem 7.6 — a feasible flow is optimal if and only if there is no unsaturated cycle with negative cost). Section 7.5 then formulates the maximum flow problem ($\max b_s$ s.t. $\mathbf{A}\mathbf{f}=\mathbf{b}$, $b_t=-b_s$, $b_i=0$ for $i\ne s,t$, $0\le\mathbf{f}\le\mathbf{u}$), defines augmenting paths (Definition 7.2: $f_{ij}<u_{ij}$ on forward arcs, $f_{ij}>0$ on backward arcs) and the Ford–Fulkerson algorithm, and proves integer invariance and finite termination for integer capacities (Theorem 7.8). The goal is Theorem 7.10:
(a) if the Ford–Fulkerson algorithm terminates because no augmenting path can be found, the current flow is optimal;
(b) the value of the maximum flow equals the minimum cut capacity $$C(S)=\sum_{\{(i,j)\in\mathcal{A}\mid i\in S,\,j\notin S\}}u_{ij}$$ — the archetypal combinatorial min-max theorem, which the book notes can also be read as LP duality (pp. 311-312).
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$.
Bandit Algorithms XIII: Pure Exploration and Best-Arm IdentificationTextbook
Sometimes reward during learning is irrelevant — a pharmaceutical company running phase-II trials only cares about identifying the best treatment, as quickly and as reliably as possible. Chapter 33 of Lattimore–Szepesvári formalizes fixed-confidence best-arm identification: a policy together with a stopping time $\tau$ and a recommendation must be *sound* (wrong with probability at most $\delta$) while minimizing $\mathbb{E}[\tau]$. The information-theoretic complexity is $c^*(\nu)^{-1} = \sup_{\alpha\in\mathcal{P}_{k-1}} \inf_{\nu'\in\mathcal{E}_{alt}(\nu)} \sum_i \alpha_i D(\nu_i, \nu_i')$: every sound strategy needs $\mathbb{E}[\tau] \ge c^*(\nu)\log\frac{1}{4\delta}$, and the Track-and-Stop algorithm — the goal theorem — achieves $\lim_{\delta\to 0} \mathbb{E}[\tau]/\log(1/\delta) = c^*(\nu)$ exactly. The mission also covers the fixed-budget counterpart, sequential halving.
Every full-dimensional convex body is sandwiched between an ellipsoid and its $n$-fold dilation: shrinking the minimum-volume covering (Löwner–John) ellipsoid $\mathcal{E}$ about its centre $x_0$ by the factor $1/n$ lands inside the body,
$$x_0 + \tfrac{1}{n}\,(\mathcal{E} - x_0) \;\subseteq\; C \;\subseteq\; \mathcal{E},$$
and the factor $n$ is tight on simplices. This rounding theorem underlies the ellipsoid method, John's theorem on the Banach–Mazur distance to the Euclidean ball, and much of modern convex geometry. The mission formalizes §8.4 of Boyd & Vandenberghe for polytopes $C = \operatorname{conv}\{x_1,\dots,x_m\}$, exactly as the book proves it: existence and uniqueness of the extremal ellipsoid, the KKT identities at the normalized optimum ($\sum_i \lambda_i x_i x_i^{T} = I$, $\sum_i \lambda_i x_i = 0$, $\sum_i \lambda_i = n$), the convex-combination step that produces the $1/n$ ball, and affine invariance.
Introduction to Linear Optimization XIII: Lagrangean Duality and Integer ProgrammingTextbook
Linear programming has a complete duality theory; integer programming does not — and the Lagrangean dual measures exactly how far duality reaches. This mission formalizes the duality theory of integer programming from Section 11.4 of Bertsimas–Tsitsiklis, built on the general linear programming duality of Section 4.10. For the integer program $$Z_{IP} = \min\{c'x : Ax \ge b,\ Dx \ge d,\ x \text{ integer}\}$$ with integer data, the complicating constraints $Ax \ge b$ are dualized with multipliers $p \ge 0$ over the tractable set $X = \{x \text{ integer} \mid Dx \ge d\}$: the dual function is $$Z(p) = \min_{x \in X}\big(c'x + p'(b - Ax)\big)$$ and the Lagrangean dual is $Z_D = \max_{p \ge 0} Z(p)$. Weak duality $Z_D \le Z_{IP}$ (Theorem 11.2) always holds, but strong duality can fail. The convex hull $CH(X)$ of the integer points of a polyhedron with integer data is itself a polyhedron (Theorem 11.3, Meyer's theorem), and the capstone — Theorem 11.4, the central result of Section 11.4 — identifies the Lagrangean dual exactly: $Z_D$ equals the optimal cost of the linear program $$\min\{c'x : Ax \ge b,\ x \in CH(X)\}$$. This is the geometric explanation of the strength of Lagrangean relaxation, yields the bound ordering $Z_{LP} \le Z_D \le Z_{IP}$, and Corollary 11.1 characterizes exactly when the bounds collapse. The polyhedral engine is the general weak/strong duality pair (Theorems 4.17/4.18) over a primal $\min c'x$ s.t. $Ax \ge b$, $x \in P = \{x \mid Dx \ge d\}$, and the formulation-strength comparison $P_{sub} \subseteq P_{cut}$ of Theorem 10.1 supplies the motivating principle that tighter relaxations of the same integer set give sharper bounds.
Parallel repetition for quantum gamesResearch Paper
# Parallel repetition for quantum games
## Nonlocal games
A **nonlocal game** is played between a classical referee and two or more cooperating players who are not allowed to communicate during the game. In the two-player, one-round setting, the referee samples a pair of questions $(x,y)$ from a distribution $\mu$, sends $x$ to Alice and $y$ to Bob, and receives answers $a$ and $b$. The players win when a predicate $V(x,y,a,b)$ accepts. Before the game begins they may agree on a strategy and share a resource, but after receiving their questions they are isolated from one another.
Nonlocal games occupy a useful interface between complexity theory and quantum information. From the perspective of complexity theory, they are the basic objects underlying multiprover interactive proofs: a verifier delegates a computation to separated provers and uses the consistency of their answers to distinguish valid from invalid claims. Classical two-prover games play a central role in the PCP theorem, hardness of approximation, and soundness amplification. Allowing the provers to share entanglement leads to the class $\mathrm{MIP}^*$ and to a substantially richer theory. The theorem $\mathrm{MIP}^*=\mathrm{RE}$ shows how dramatically entanglement changes this landscape: even estimating the entangled value of a nonlocal game can encode undecidable computation [Ji--Natarajan--Vidick--Wright--Yuen 2020](https://arxiv.org/abs/2001.04383).
From the perspective of quantum information, nonlocal games are operational formulations of Bell experiments. A separation between classical and entangled values witnesses correlations that cannot be explained by a local hidden-variable model. The same framework supports **self-testing**, in which near-optimal behavior certifies the underlying state and measurements up to local equivalence, and **device-independent cryptography**, in which security or randomness is certified from observed input-output statistics rather than a trusted description of the devices. Representative references include [Cleve--Høyer--Toner--Watrous 2004](https://arxiv.org/abs/quant-ph/0404076), [Reichardt--Unger--Vazirani 2013](https://doi.org/10.1038/nature12035), and [Pironio et al. 2010](https://doi.org/10.1038/nature09008). The survey of [Palazuelos--Vidick 2016](https://arxiv.org/abs/1512.00419) describes further connections among nonlocal games, Bell inequalities, operator spaces, and quantum information.
Thus the value of a nonlocal game is simultaneously a complexity-theoretic soundness parameter and a quantitative measure of the power of nonclassical correlations. Understanding how this value changes under natural operations on games is important in both subjects.
## Entangled strategies and value
We take the finite answer alphabets to be nonempty. In a classical strategy, Alice's answer depends only on $x$, Bob's answer depends only on $y$, and the players may coordinate using shared randomness. In a finite-dimensional entangled strategy, the players share a bipartite state $\rho$ and use POVM measurement operators
$$
\{A_a^x\}_{a\in A}
\qquad\text{and}\qquad
\{B_b^y\}_{b\in B}
$$
for their respective questions. The probability of producing answers $(a,b)$ on questions $(x,y)$ is
$$
\operatorname{Re}\operatorname{Tr}\!\left(\rho\,(A_a^x\otimes B_b^y)\right).
$$
The supremum of the winning probability over all such finite-dimensional strategies is the **entangled value** $\omega^*(G)$. This optimization ranges over arbitrary local dimensions, shared states, and local measurements, which is one reason even apparently elementary questions about nonlocal games can be difficult.
## Parallel repetition
For a positive integer $n$, the repeated game $G^n$ consists of $n$ independently sampled copies of $G$ played simultaneously. Alice receives $(x_1,\ldots,x_n)$, Bob receives $(y_1,\ldots,y_n)$, and they answer with tuples $(a_1,\ldots,a_n)$ and $(b_1,\ldots,b_n)$. They win only if
$$
V(x_i,y_i,a_i,b_i)=1
$$
for every coordinate $i$.
Parallel repetition is a basic method of **soundness amplification**. Starting from a game that dishonest players cannot win with certainty, the verifier repeats the test in the hope of driving the optimal success probability rapidly toward zero. The difficulty is that independence in the verifier's sampling does not force independence in the players' strategy. Alice may choose her entire answer tuple as a function of all her questions, Bob may do the same, and an entangled strategy may use a single state and joint measurements spanning all coordinates. In particular, one cannot obtain an upper bound on $\omega^*(G^n)$ merely by analyzing the strategy that plays each coordinate independently.
For classical games, Raz's parallel repetition theorem gives exponential decay whenever the one-shot value is below one [Raz 1998](https://doi.org/10.1137/S0097539795280895). Establishing the corresponding behavior for entangled games has been a long-running problem. A general polynomial bound was proved in [Yuen 2016](https://arxiv.org/abs/1604.04340), implying for the first time that $\omega^*(G^n)$ tends to zero for every finite two-player entangled game with $\omega^*(G)<1$.
The full exponential-decay theorem was recently settled by OpenAI. In Chapter 6 of [*Ten Advances in Mathematics and Theoretical Computer Science*](https://cdn.openai.com/pdf/ten-proofs-oai.pdf), OpenAI proves that for every finite two-player entangled game $G$ with $\omega^*(G)<1$, there is a constant $c_G>0$ such that
$$
\omega^*(G^n)\le e^{-c_G n}
$$
for every positive $n$. OpenAI also released a [Lean certificate](https://github.com/openai/ten-proofs/blob/main/QuantumParallelRepetition.lean) for the result. This resolves the general quantum parallel-repetition conjecture, but it does not end the study of the problem. The proof introduces quantitative losses and a substantial technical apparatus, and there remains considerable value in finding alternative arguments, isolating the essential mechanism, improving the dependence on the one-shot gap and answer size, and producing shorter or more conceptual formal proofs.
## A hierarchy of formalization targets
This mission develops a reusable Lean framework for parallel repetition rather than formalizing only one paper. Its targets are organized by the strength of the asserted decay.
### Qualitative decay
The main mission theorem is the fundamental asymptotic statement:
$$
\omega^*(G)<1
\quad\Longrightarrow\quad
\lim_{n\to\infty}\omega^*(G^n)=0.
$$
Equivalently, for every $\delta>0$, all sufficiently large $n$ satisfy $\omega^*(G^n)<\delta$. This statement deliberately specifies no rate. It is a stable top-level theorem that can be recovered from any sufficiently strong quantitative bound.
### Polynomial decay
A stronger target asks for game-dependent constants $C>0$ and $\alpha>0$ such that
$$
\omega^*(G^n)\le Cn^{-\alpha}.
$$
The abstract formulation avoids fixing a particular exponent or logarithmic correction. More refined formalizations can record explicit dependence on the gap $1-\omega^*(G)$, the answer alphabet, or other game parameters. Yuen's 2016 theorem is one important result at this level.
### Exponential decay
The exponential target asks for game-dependent constants $C,c>0$ such that
$$
\omega^*(G^n)\le C e^{-cn}.
$$
Following OpenAI's recent resolution, this target is now a theorem rather than an open conjecture. Within this mission it remains a central milestone: contributors may formalize the released argument in the mission's common interface, construct an independent proof, seek a more elegant or modular proof, or establish sharper quantitative variants.
These levels do not exhaust the project. The same framework can accommodate explicit finite-$n$ inequalities, stretched-exponential estimates, bounds for structured classes of games, improved parameter dependence, and reductions showing that one decay statement implies another.
## Formalization scope
The foundational Lean development represents a game by finite question sets $X,Y$, finite answer sets $A,B$, a nonnegative normalized question distribution $\mu(x,y)$, and a Boolean verification predicate $V(x,y,a,b)$. The parallel-repetition theorems explicitly assume that $A$ and $B$ are nonempty. The development defines finite-dimensional entangled strategies using density matrices and POVM measurement operators, defines the repeated game on tuples, and takes the entangled value as a supremum over all finite-dimensional strategies. Repeated strategies are indexed by complete question tuples and are not required to factor coordinatewise.
A complete development will draw on formal libraries for finite probability, tensor products, positive semidefinite matrices, density matrices, POVMs, trace norms, fidelity, entropy, mutual information, and correlated sampling. These components should be formulated for reuse and should expose the dependence of each bound on the relevant game parameters.
The goal is both to verify parallel-repetition theorems and to build a dependable language for nonlocal games in Lean. Formalization forces distinctions that are easy to suppress on paper: whether constants depend on the game, whether a bound holds for all $n$ or only asymptotically, which strategy model is optimized over, and which hypotheses are needed for a particular rate. The mission welcomes reconstructions of known proofs as well as new, shorter, or conceptually different proofs.
## Selected references
- R. Cleve, P. Høyer, B. Toner, and J. Watrous, [*Consequences and limits of nonlocal strategies*](https://arxiv.org/abs/quant-ph/0404076), CCC 2004.
- R. Raz, [*A parallel repetition theorem*](https://doi.org/10.1137/S0097539795280895), SIAM Journal on Computing 27(3), 1998.
- H. Yuen, [*A parallel repetition theorem for all entangled games*](https://arxiv.org/abs/1604.04340), ICALP 2016.
- Z. Ji, A. Natarajan, T. Vidick, J. Wright, and H. Yuen, [$\mathrm{MIP}^*=\mathrm{RE}$](https://arxiv.org/abs/2001.04383), Communications of the ACM 64(11), 2021.
- OpenAI, [*Ten Advances in Mathematics and Theoretical Computer Science*](https://cdn.openai.com/pdf/ten-proofs-oai.pdf), Chapter 6, 2026; accompanying [Lean formalization](https://github.com/openai/ten-proofs/blob/main/QuantumParallelRepetition.lean).
Markov Entanglement: Value Decomposition Error in Multi-agent MDPsResearch Paper
Value decomposition — approximating the value of a joint state by a sum of per-agent local values — is a staple of multi-agent dynamic programming and reinforcement learning, from index policies for restless bandits to modern MARL architectures, yet it is normally used without justification. Chen and Peng (arXiv:2506.02385) supply one. They show a multi-agent MDP admits an exact value decomposition precisely when its transition matrix is not *entangled* — a notion built in direct analogy with quantum entanglement — and then turn that qualitative characterisation into a quantitative one: a measure of Markov entanglement bounds the decomposition error in general. This mission formalizes that core theory. The goal is Theorem 6, the general N-agent bound in the occupancy-weighted norm; the milestones are the equivalence between separability and exact decomposition, the perturbation machinery that carries a one-step transition error into a value-function error, and the extensions to shared global state and shared rewards. The paper's restless-bandit application, which needs mean-field machinery of its own, is left to a second mission in the series.
Introduction to Linear Optimization XII: Interior Point Methods and Path FollowingTextbook
Interior point methods solve linear programs by moving through the interior of the feasible set instead of along its edges — the approach that turned Karmarkar's 1984 breakthrough into today's practical large-scale solvers. This mission formalizes the primal path following algorithm of Chapter 9 of Bertsimas–Tsitsiklis. For $\mu > 0$ the logarithmic barrier $$B_\mu(\mathbf{x}) = \mathbf{c}'\mathbf{x} - \mu\sum_{j=1}^n \log x_j$$ replaces the constraint $\mathbf{x} \ge \mathbf{0}$; the minimizers $\mathbf{x}(\mu)$ of $B_\mu$ over $\{A\mathbf{x} = \mathbf{b}\}$ trace the central path, characterized by the KKT conditions (9.17): $A\mathbf{x} = \mathbf{b}$, $\mathbf{x} \ge \mathbf{0}$, $A'\mathbf{p} + \mathbf{s} = \mathbf{c}$, $\mathbf{s} \ge \mathbf{0}$, $XS\mathbf{e} = \mu\mathbf{e}$ (Lemma 9.5). The algorithm follows the path with one Newton step of the barrier problem per shrink $\mu^{k+1} = \alpha\mu^k$, maintaining the proximity invariant $$\|\frac{1}{\mu}XS\mathbf{e} - \mathbf{e}\| \le \beta$$. The goal theorem is Theorem 9.7: with $\alpha = 1 - \frac{\sqrt{\beta}-\beta}{\sqrt{\beta}+\sqrt{n}}$ and a $\beta$-close start, after $K = \Big\lceil \frac{\sqrt{\beta}+\sqrt{n}}{\sqrt{\beta}-\beta}\,\log\frac{(\mathbf{s}^0)'\mathbf{x}^0(1+\beta)}{\varepsilon(1-\beta)} \Big\rceil$ iterations the algorithm reaches primal and dual feasible solutions with duality gap $(\mathbf{s}^K)'\mathbf{x}^K \le \varepsilon$ — the explicit form of the celebrated $O(\sqrt{n}\log(1/\varepsilon))$ iteration bound. Alongside it we formalize the generic potential-reduction scheme (Theorem 9.4): any algorithm cutting $G(\mathbf{x},\mathbf{s}) = q\log\mathbf{s}'\mathbf{x} - \sum_j \log x_j - \sum_j \log s_j$ by $\delta$ per step reaches gap $\varepsilon$ within an explicit $K$.
Introduction to Linear Optimization XI: The Ellipsoid MethodTextbook
Can the feasibility of a system of linear inequalities be decided in a provably small number of iterations? The ellipsoid method — the algorithm with which Khachiyan showed in 1979 that linear programming is polynomially solvable — answers this with pure convex geometry. This mission formalizes Chapter 8 of Bertsimas–Tsitsiklis. An ellipsoid is $$E(\mathbf{z}, D) = \{\mathbf{x} \in \mathbb{R}^n \mid (\mathbf{x}-\mathbf{z})'D^{-1}(\mathbf{x}-\mathbf{z}) \le 1\}$$ with $D$ symmetric positive definite. The geometric engine is Theorem 8.1: the half-ellipsoid $E \cap \{\mathbf{x} \mid \mathbf{a}'\mathbf{x} \ge \mathbf{a}'\mathbf{z}\}$ is contained in the explicitly constructed ellipsoid $E' = E(\bar{\mathbf{z}}, \bar{D})$, $$\bar{\mathbf{z}} = \mathbf{z} + \frac{1}{n+1}\frac{D\mathbf{a}}{\sqrt{\mathbf{a}'D\mathbf{a}}},$$ $$\bar{D} = \frac{n^2}{n^2-1}\big(D - \frac{2}{n+1}\frac{D\mathbf{a}\mathbf{a}'D}{\mathbf{a}'D\mathbf{a}}\big),$$ and the volume contracts: $$\mathrm{Vol}(E') < e^{-1/(2(n+1))}\,\mathrm{Vol}(E)$$. Two integer-data estimates make the contraction decisive: every extreme point of $P = \{\mathbf{x} \mid A\mathbf{x} \ge \mathbf{b}\}$ with entries bounded by $U$ has coordinates in $[-(nU)^n, (nU)^n]$ (Lemma 8.2), and a full-dimensional bounded such polyhedron has $\mathrm{Vol}(P) > n^{-n}(nU)^{-n^2(n+1)}$ (Lemma 8.4). The goal theorem is Theorem 8.2: started on a ball $E(\mathbf{x}_0, r^2 I)$ of volume at most $V$ containing $P$, with $v$ a lower bound on $\mathrm{Vol}(P)$ when $P$ is nonempty, the ellipsoid method correctly decides whether $P$ is empty within $t^* = \lceil 2(n+1)\log(V/v) \rceil$ iterations — the explicit iteration count behind the polynomial-time headline.
Introduction to Linear Optimization IX: Network Flow IntegralityTextbook
Why do network linear programs return integer answers for free? This mission formalizes the structural theory of the minimum cost network flow problem of Chapter 7 of Bertsimas & Tsitsiklis: a directed graph $G=(\mathcal{N},\mathcal{A})$ with external supplies $b_i$, arc costs $c_{ij}$, and the node-arc incidence matrix $\mathbf{A}$ — an $n\times m$ matrix in which every column has exactly one $+1$ (start node) and one $-1$ (end node) — so that flow conservation reads $\mathbf{A}\mathbf{f}=\mathbf{b}$, forcing the standing assumption $\sum_{i\in\mathcal{N}} b_i=0$. Because the rows of $\mathbf{A}$ sum to zero, the book works with the truncated matrix $\tilde{\mathbf{A}}$ of the first $n-1$ rows. The combinatorial heart is the correspondence between algebra and graph structure: a set $T$ of $n-1$ arcs forming a tree determines a unique tree solution of $\tilde{\mathbf{A}}\mathbf{f}=\tilde{\mathbf{b}}$, $f_{ij}=0$ off $T$ (Theorem 7.3); connectedness makes $\tilde{\mathbf{A}}$ full-rank (Corollary 7.1); and a flow vector is a basic solution if and only if it is a tree solution (Theorem 7.4). The goal theorem is the integrality theorem (Theorem 7.5): for the uncapacitated problem on a connected graph, every basis matrix $\mathbf{B}$ has an integer inverse $\mathbf{B}^{-1}$ (its determinant is $\pm 1$ by the tree/lower-triangular argument), integer supplies make every basic solution integer, and integer costs make every dual basic solution integer — whence integer optimal primal and dual solutions exist whenever the optimal cost is finite (Corollary 7.2). This is the fountainhead of combinatorial integrality in linear optimization, feeding the max-flow min-cut mission that follows.
Introduction to Linear Optimization VIII: Sensitivity Analysis and Subgradients of the Optimal CostTextbook
How does the optimal cost of a linear program respond when the problem data change? Chapter 5 of Bertsimas-Tsitsiklis studies the standard form problem $\min\{c'x \mid Ax = b,\ x \ge 0\}$ (rows of $A$ linearly independent) as the requirement vector $b$ and the cost vector $c$ vary. On the convex set $S = \{b \mid P(b) \neq \emptyset\}$ of feasible right-hand sides, and under the standing assumption that the dual feasible set is nonempty, the optimal cost $F(b)$ is finite and convex (Theorem 5.1) — indeed $F(b) = \max_{i} (p^i)'b$ over the extreme points $p^1, \dots, p^N$ of the dual feasible set, a piecewise linear convex function whose breakpoints are exactly where the dual optimum is non-unique. The capstone (Theorem 5.2) identifies the generalized gradients of $F$: if the primal at $b^*$ is feasible with finite optimal cost, then $p$ is an optimal solution of the dual if and only if $p$ is a subgradient of $F$ at $b^*$ (Definition 5.1: $F(b^*) + p'(b - b^*) \le F(b)$ for all $b \in S$) — the precise sense in which dual variables are marginal costs. Dually (Theorem 5.3), the set $T$ of cost vectors with finite optimal cost is convex, the optimal cost $G(c)$ is concave on $T$, and near any $c$ with a unique primal optimum $x^*$, $G$ is linear with gradient $x^*$. Local ranging (Section 5.1) and parametric programming (Section 5.5) are the procedural companions, folded into the design notes.
Introduction to Linear Optimization VII: Cones, Extreme Rays, and the Resolution TheoremTextbook
How can an unbounded polyhedron be described by finitely many geometric objects? Sections 4.8-4.9 of Bertsimas-Tsitsiklis build the cone machinery: recession cones $\{d \mid Ad \ge 0\}$ and their rays, extreme rays (defined, like basic solutions, by $n-1$ linearly independent active constraints), the pointedness criterion (Theorem 4.12: $0$ is an extreme point of a polyhedral cone iff the cone contains no line iff $n$ of the constraint vectors are linearly independent), and the characterization of unbounded linear programs (Theorems 4.13-4.14: over a pointed polyhedral cone, and then over any polyhedron with an extreme point, the optimal cost is $-\infty$ iff some extreme ray $d$ has $c'd < 0$). The capstone is the resolution theorem (Theorem 4.15): a nonempty polyhedron $P$ with at least one extreme point equals $Q = \{\sum_i \lambda_i x^i + \sum_j \theta_j w^j \mid \lambda_i \ge 0, \theta_j \ge 0, \sum_i \lambda_i = 1\}$ — the convex hull of its extreme points plus the cone generated by a complete set of its extreme rays. It specializes to Theorem 2.9 / Corollary 4.4 (a nonempty bounded polyhedron is the convex hull of its extreme points) and Corollary 4.5 (a pointed polyhedral cone is generated by its extreme rays). The converse, Theorem 4.16, states that every finitely generated set is a polyhedron — in particular the convex hull of finitely many vectors is a polyhedron. Together these form the Minkowski-Weyl equivalence of the two representations of polyhedra, verified absent from Mathlib and the genuine content of this mission.