A Machine-Verified Proof of a Quantum-Optimization Conjecture
Uri Kol, Maor Ben-Shahar, Kfir Sulimany, Dirk Englund
quant-ph
Jun 29, 2026 · v1
cs.AI cs.LG cs.LO math.OC
TL;DR
Proves the FGG conjecture on QAOA approximation ratio using Claude Fable 5 with end-to-end Lean 4 verification.
Abstract
We report a machine-verified resolution of a problem open for over a decade in quantum optimization: the Farhi, Goldstone and Gutmann (FGG) conjecture that depth-$p$ Quantum Approximate Optimization Algorithm (QAOA) on the ring of disagrees attains approximation ratio $(2p+1)/(2p+2)$ exactly. We found the proof using a large language model, Claude Fable 5, and verified its correctness end-to-end by the Lean 4 proof assistant. Our methodology includes several ingredients: building on a substantial Lean library of quantum information, we formalized the QAOA components and the known parts of the problem, and reduced the conjecture to a single open mathematical statement. The model was then handed the library and our agentic toolkit, and tasked with closing that gap by constructing a proof in Lean. The resulting process is a feedback loop between the model's natural-language reasoning and Lean's mechanical verification, which converged to a machine-verified proof. Human verification is required only for the structural scaffolding - that the formal statement faithfully encodes the intended claim - while the proof itself is supplied by the model and certified mechanically by Lean. The proof is nevertheless striking - the model uncovered a hidden dynamical symmetry of the problem and exploited it, borrowing tools and machinery from an adjacent field to turn a hard existence problem into an explicit construction. This work paves the way for resolving open conjectures in quantum information science and beyond.
Problem
The Farhi-Goldstone-Gutmann (FGG) conjecture, open for over a decade, states that depth-p QAOA on the ring of disagrees attains approximation ratio (2p+1)/(2p+2) exactly. No proof existed.
Approach
The authors built a Lean 4 library of quantum information and formalized QAOA components, reducing the conjecture to a single open mathematical statement. Claude Fable 5 was given this library and an agentic toolkit, then tasked with constructing the closing proof in Lean via a generate-then-verify feedback loop. The model discovered a hidden dynamical symmetry linking per-mode QAOA propagators to Quantum Signal Processing (QSP) sequences, turning the existence problem into an explicit polynomial construction.
Results
The LLM produced a machine-verified Lean 4 proof of the full FGG conjecture. The proof introduces a novel QSP-based technique not previously applied to QAOA analysis. The complete Lean library and proof are publicly released.
