# A Machine-Verified Proof of a Quantum-Optimization Conjecture

arXiv: https://arxiv.org/abs/2606.29687 · HTML: https://mlsanity.com/paper/2606.29687/

## Key facts

- Cited by 3 papers in the map (data through 14 Oct 2026).
- Builds on 2 of its 11 references that are in the map.
- First posted on arXiv 29 Jun 2026.

## Builds on (most cited first, 2 of 2)

- [DeepSeek-Prover-V2: Advancing Formal Mathematical Reasoning via Reinforcement Learning for Subgoal Decomposition](https://mlsanity.com/paper/2504.21801/) (2025)
- [Ax-Prover: A Deep Reasoning Agentic Framework for Theorem Proving in Mathematics and Quantum Physics](https://mlsanity.com/paper/2510.12787/) (2025)

## Built on by (most cited first, 3 of 3)

- [Lean-QIT: Towards a Formal Infrastructure for Quantum Information Theory](https://mlsanity.com/paper/2607.09632/) (2026)
- [AxQM: A Textbook-Scale Benchmark for Formal Proof Synthesis in a Library of Finite-Dimensional Quantum Mechanics](https://mlsanity.com/paper/2609.05157/) (2026)
- [QuantumNovelty: A Skill-Orchestrating Language Agent for Referee-Style Review and Patentability Screening of Quantum Papers and Patents](https://mlsanity.com/paper/2608.16900/) (2026)

## Abstract (arXiv)

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.