What was already known
Farhi, Goldstone and Gutmann conjectured the formula and proved p=1. Wang and collaborators proved p=2. Mbeng, Fazio and Santoro reduced the general case to simultaneous mode steering and checked numerically through p=128, but the existence proof remained open. Kunal Marwaha posted an independent proof on 28 June 2026, one day before the AI-proof paper, using quantum signal processing and Laurent polynomials.
AI involvement
The paper credits Claude Fable 5 with the decisive quantum-signal-processing proof, after the human authors built the formal statement and supporting library.
Importance
Supplies a separate machine-verified, AI-generated constructive proof of the exact depth-p QAOA performance on this benchmark.
Limitations
The human authors supplied the formal problem, quantum definitions, supporting library and known reductions; Claude Fable 5 supplied the decisive argument. Marwaha’s earlier independent proof establishes the theorem separately, not the correctness of this model-generated argument.
Technical verification
The paper reports that the final `residualEnergy_isLeast` theorem, lower bound and attainment are compiled in Lean 4 using standard Mathlib classical axioms. The authors reviewed the formal statement and definitions against the intended QAOA claim. This is source-reported; AIProofWatch did not reproduce the check.
Formal checking
The paper reports that `residualEnergy_isLeast`, its lower bound and attainment subtheorems compile in Lean 4 with standard Mathlib classical axioms; the authors checked correspondence between formal definitions and the stated ring conjecture.
- Checker
- Lean 4 kernel, as reported by Kol and collaborators
- Scope
- For every depth p and even ring size N with 2p+2≤N, the optimal QAOA approximation ratio for MaxCut on the ring of disagrees is exactly (2p+1)/(2p+2).
- Basis
- Reported by the linked checker
Checking a formal statement does not establish that it matches the original problem.
Human understanding
Uri Kol and collaborators explain the model-generated dynamical-symmetry and quantum-signal-processing construction in Section IV.
Correction and publication history
Primary paper, contribution attribution, prior baseline and checking scope reviewed for non-notifying local inclusion.
Read this published revision