Threshold repetition for entangled games

1 paperLean

Proves exponential threshold repetition for every finite two-player one-round game: if its entangled value is v < 1, the probability of winning at least a fraction \(v+\delta\) of k independent repetitions decays exponentially in k, for \(0\lt \delta\lt 1-v\). Arbitrary joint finite-dimensional entangled strategies and correlated question distributions are allowed.

Watch

▶Introduction: the problem and why it mattersin preparation

▶The presented solutionin preparation

Papers 1

Threshold parallel repetition for finite-dimensional entangled games

OpenAI · September 25, 2026

For every finite two-player game with entangled value v < 1, we prove exponential decay for the probability of winning at least a \(v+\delta\) fraction of k independent repetitions, uniformly over all finite-dimensional joint strategies. The result allows arbitrary correlated question distributions and holds for every \(0\lt \delta\lt 1-v\) and k ≥ 1. Its universal rate is proportional to \(\delta^5/(1+\log(|\mathcal A||\mathcal B|))\), where \(\mathcal A,\mathcal B\) are the answer alphabets. For each fixed question distribution, we also obtain an explicit cubic rate in δ.

Read PDF Download Source

Cite

@misc{OAI:Threshold-parallel-repetition-for-finite-dimensional-entangled-games-September-25-2026,
  author = {{OpenAI}},
  title = {{Threshold parallel repetition for finite-dimensional entangled games}},
  howpublished = {OpenAI Math Release preprint
                  \href{https://github.com/openai/math/blob/main/preprints/Threshold-parallel-repetition-for-finite-dimensional-entangled-games-September-25-2026/paper.pdf}{OAI:Threshold-parallel-repetition-for-finite-dimensional-entangled-games-September-25-2026}},
  year = {2026}
}

What was formalized in Lean

The following describes the scope of the Lean formalization related to the following accompanying paper(s):

Threshold parallel repetition for finite-dimensional entangled games

Scope

The formalization gives exponential threshold parallel repetition for every finite two-player game with arbitrary correlated questions. If its finite-dimensional entangled value is \(v<1\), its answer sets are \(A,B\), and \(0<\delta<1-v\), then the probability of winning at least the fraction \(v+\delta\) of \(k\) repetitions is at most \(\exp(-\kappa\delta^{13}k/(1+\log(|A||B|)))\) for one universal \(\kappa>0\). The bound applies to every joint finite-dimensional strategy and to their supremum, without assuming attainment. The separate distribution-dependent cubic bound is outside this scope.

Comparator links

Result	Comparator statement
Threshold parallel repetition for entangled games	EntangledGames.lean

Scope note on GitHub →