Parity is not in QAC⁰

2 papersLean

Resolves Moore's parity conjecture in the measured-output model: constant-depth quantum circuits with arbitrary one-qubit gates, unbounded-arity Toffoli gates and polynomially many total qubits cannot compute parity with any fixed positive worst-case advantage. Ancillas start in zero, one output qubit is measured, and all other registers may be discarded. Xu–Li's reductions give the same bounded-error obstruction for strict majority.

Watch

The problem

What is being asked, where it comes from, and why it is hard. No proof needed.

▶Introduction to the problemin preparation

The solution proposed by OpenAI

How the paper solves it, step by step.

Full explanation

▶The proposed solutionin preparation

Papers 2

Product-projection localization and the QAC0 parity lower bound

OpenAI · September 24, 2026

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.

Read PDF Download Source

Cite

@misc{OAI:Product-projection-localization-and-the-QAC0-parity-lower-bound-September-24-2026,
  author = {{OpenAI}},
  title = {{Product-projection localization and the $\mathrm{QAC}^0$ parity lower bound}},
  howpublished = {OpenAI Math Release preprint
                  \href{https://github.com/openai/math/blob/main/preprints/Product-projection-localization-and-the-QAC0-parity-lower-bound-September-24-2026/paper.pdf}{OAI:Product-projection-localization-and-the-QAC0-parity-lower-bound-September-24-2026}},
  year = {2026}
}

Regular trajectories, pruning and quantum parity

OpenAI · September 24, 2026

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.

Read PDF Download Source

Cite

@misc{OAI:Regular-trajectories-pruning-and-quantum-parity-September-24-2026,
  author = {{OpenAI}},
  title = {{Regular trajectories, pruning and quantum parity}},
  howpublished = {OpenAI Math Release preprint
                  \href{https://github.com/openai/math/blob/main/preprints/Regular-trajectories-pruning-and-quantum-parity-September-24-2026/paper.pdf}{OAI:Regular-trajectories-pruning-and-quantum-parity-September-24-2026}},
  year = {2026}
}

What was formalized in Lean

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

Scope

The formalization rules out bounded-error parity computation by constant-depth quantum circuits with polynomially many zero-initialized ancillary qubits. For every fixed depth, polynomial bound on the total number of qubits, and \(0<\varepsilon\le1/2\), every sufficiently large input length has an input on which the measured-output parity success probability is less than \(1/2+\varepsilon\). A companion specialization gives success strictly below \(2/3\). The formalization also includes the product-projection localization estimate supporting this bound.

The formalized result supplies the polynomial-size parity consequence of the paper. For every fixed circuit depth and polynomial bound on the number of qubits, all sufficiently large input lengths have an input on which any such circuit computes measured-output parity with probability strictly below \(2/3\). Ancillary qubits start at zero. The formalization also contains the general positive-advantage parity bound and its product-projection localization estimate; regular-trajectory propagation and pruning are not separate formalized statements here.

Comparator links

Result	Comparator statement
Constant-depth quantum parity lower bound	QACParity.lean
Polynomial-size parity specialization	RegularParity.lean
Polynomial-size quantum parity lower bound	RegularParity.lean
General positive-advantage parity lower bound	QACParity.lean

Scope note on GitHub →