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 'Regular trajectories, pruning and quantum parity'. We prove that constant-depth quantum circuits with arbitrary one-qubit gates and unbounded-arity Toffoli gates cannot compute parity with any fixed positive worst-case advantage using polynomially many total qubits. Ancillary qubits are initialized to |0\rangle, one output qubit is measured, and all other final registers may be discarded without restriction. 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.