A Machine-Verified Proof of a Quantum-Optimization Conjecture

The Farhi, Goldstone, and Gutmann (FGG) conjecture has been a significant open problem in quantum optimization for over a decade. It posits that for a depth-p QAOA circuit applied to the ring of disagrees (a one-dimensional antiferromagnetic Ising model), the optimal approximation ratio is exactly (2p+1)/(2p+2). While numerical evidence supported this for years, a formal analytical proof remained elusive. The authors of this paper utilized an agentic AI workflow, employing the large language model Claude Fable 5, to generate a proof that was then rigorously verified by the Lean 4 proof assistant.

The researchers formalized the QAOA components, the Ising chain, and the necessary quantum information definitions within Lean 4. By leveraging a Jordan-Wigner transformation and translational invariance, they reduced the problem to a set of decoupled momentum modes. The AI was tasked with closing the gap in the proof by constructing a formal argument that the steering condition—the requirement that these modes be driven onto their respective cost axes—could be satisfied for all p. The system utilized a feedback loop where the model proposed proof steps, and the Lean kernel provided deterministic verification, ensuring that every inference was logically sound.

The proof reveals that the per-mode dynamics of the QAOA circuit can be mapped to Quantum Signal Processing (QSP) sequences. By identifying a hidden dynamical symmetry, the authors demonstrated that the steering condition is equivalent to a polynomial interpolation problem. The optimal approximation ratio emerges naturally from the normalization of the unique node polynomial required by the unitarity of the SU(2) evolution. This construction not only confirms the FGG conjecture but also provides a general framework for resolving similar optimization problems in translation-invariant free-fermion systems.