Farhi–Goldstone–Gutmann QAOA conjecture

Does the proposed QAOA guarantee hold under the hypotheses in the linked conjecture?

Jun 2026

Farhi-Goldstone-Gutmann QAOA conjecture

Model / AI: Claude Fable 5

machine-checked

Claude Fable 5 supplied the missing argument and the proof was certified end-to-end in Lean 4, sorry-free and axiom-clean, with the statement fixed before the model saw the gap. Marwaha proved the same conjecture by hand, independently, a day earlier.

Source review pending. Imported from the original notes; linked claims and artifacts have not been re-audited in this restructuring.

Paper — Farhi-Goldstone-Gutmann QAOA conjecture
Lean — sorry-free and axiom-clean
Paper — Marwaha