Lean formalization in OpenAI math repository (Result 277)
Model / AI: OpenAI (unreleased)
OpenAI's internal frontier model proved and formalized in Lean the main result of 'Threshold parallel repetition for finite-dimensional entangled games'. 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 δ.
Source read 2026-10-08. Cataloged from OpenAI's formalization.yaml (Family 277). The Lean development was not rebuilt locally.