Parallel repetition for quantum games

Parallel repetition for quantum games

Model / AI: OpenAI (unreleased)

OpenAI reports a resolution with an accompanying Lean artifact. Sienicki and Sienicki later identified a success-versus-failure polarity error in the printed proof of a preliminary conditioning lemma, gave a counterexample to the printed procedure and proved a corrected version with the same statement and parameters. They explicitly do not claim to verify the main theorem.

Source read 2026-09-08. Read the OpenAI source and the independent August 2026 audit. The audit verifies and repairs one preliminary lemma but does not assess the remainder of the proof; no local rebuild was performed.

• Lean — OpenAI's ten advances
• Lean — Result-specific Lean file
• Paper — Independent audit and correction