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).