Oct 6, 2026
Lean formalization in OpenAI math repository (Result 274)
Model / AI: OpenAI (unreleased)
machine-checked (formal proof)self-reported (formal proof)
OpenAI's internal frontier model proved and formalized in Lean the main result of 'Product-projection localization and the QAC⁰ parity lower bound'. We prove that constant-depth quantum circuits with arbitrary one-qubit and unbounded-arity Toffoli gates cannot compute parity with any fixed positive worst-case advantage using polynomially many qubits. Ancillas start in zero, only one output qubit is measured, and all final garbage is unrestricted. This resolves Moore's parity conjecture in the measured-output model.
Source read 2026-10-08. Cataloged from OpenAI's formalization.yaml (Family 274). The Lean development was not rebuilt locally.