pith. sign in

arxiv: 2606.29687 · v1 · pith:K3K3D2ITnew · submitted 2026-06-29 · 🪐 quant-ph · cs.AI· cs.LG· cs.LO· math.OC

A Machine-Verified Proof of a Quantum-Optimization Conjecture

Uri Kol , Maor Ben-Shahar , Kfir Sulimany , Dirk Englund This is my paper

Pith reviewed 2026-06-30 06:37 UTC · model grok-4.3

classification 🪐 quant-ph cs.AIcs.LGcs.LOmath.OC
keywords QAOAFGG conjectureapproximation ratiomachine-verified proofring of disagreesquantum optimizationdynamical symmetryLean
0
0 comments X

The pith

A machine has produced a verified proof of the Farhi-Goldstone-Gutmann conjecture on QAOA ratios.

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The paper establishes that depth-p QAOA on the ring of disagrees attains an approximation ratio of exactly (2p+1)/(2p+2). This settles a conjecture that remained open for more than a decade in quantum optimization. The proof was generated by a large language model and then certified end-to-end by the Lean 4 proof assistant after the problem was reduced to one remaining mathematical statement. The model identified a hidden dynamical symmetry that converted an existence question into an explicit construction. A sympathetic reader would care because the result confirms the performance bound for this family of quantum algorithms and demonstrates a workable route for closing other long-standing conjectures with automated assistance.

Core claim

The Farhi-Goldstone-Gutmann conjecture is true: for every positive integer depth p the Quantum Approximate Optimization Algorithm applied to the ring of disagrees problem achieves an approximation ratio of precisely (2p+1)/(2p+2). The proof was located by an LLM that uncovered a hidden dynamical symmetry of the evolution and used it, together with tools from an adjacent field, to replace a non-constructive argument with an explicit construction; the entire argument was then mechanically verified by Lean.

What carries the argument

The hidden dynamical symmetry of the QAOA evolution on the ring of disagrees, which converts the conjecture from an existence claim into an explicit construction.

If this is right

  • The stated approximation ratio is achieved exactly for every depth p.
  • The performance of QAOA on this problem is now known with formal certainty rather than numerical evidence.
  • The same reduction-plus-explicit-construction strategy can be applied to other open statements in quantum optimization.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

  • The symmetry identified in the proof may appear in QAOA instances defined on other regular graphs.
  • The LLM-Lean feedback loop could be tested on conjectures whose statements are already present in existing formal libraries.
  • Explicit constructions derived this way might yield new classical algorithms that match the proven quantum ratio.

Load-bearing premise

The formal statement supplied to the proof assistant accurately encodes the original mathematical claim made by Farhi, Goldstone and Gutmann.

What would settle it

A direct calculation for any fixed small p, such as p=1, showing that the highest achievable approximation ratio on the ring of disagrees is strictly less than the conjectured value (2p+1)/(2p+2).

Figures

Figures reproduced from arXiv: 2606.29687 by Dirk Englund, Kfir Sulimany, Maor Ben-Shahar, Uri Kol.

Figure 1
Figure 1. Figure 1: FIG. 1 [PITH_FULL_IMAGE:figures/full_fig_p004_1.png] view at source ↗
read the original 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.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Referee Report

1 major / 0 minor

Summary. The paper claims a machine-verified resolution of the decade-old Farhi-Goldstone-Gutmann conjecture: that depth-p QAOA on the ring-of-disagrees graph attains approximation ratio exactly (2p+1)/(2p+2). An LLM (Claude Fable 5) is used to close a single reduced mathematical gap after the authors formalize the QAOA components and known results in Lean 4 on top of an existing quantum-information library; the resulting proof is mechanically checked end-to-end by Lean. Human effort is stated to be required only to confirm that the formalized statement matches the original conjecture.

Significance. If the formalized statement is faithful to the original FGG claim, the work supplies the first machine-checked proof of an open conjecture in quantum optimization. The explicit credit given to the Lean library, the reduction to a single gap, and the model's discovery of a hidden dynamical symmetry constitute concrete strengths. The result illustrates a viable workflow for AI-assisted resolution of existence-type problems in quantum information.

major comments (1)
  1. [Abstract] Abstract and §1 (structural scaffolding paragraph): the central claim that the work resolves the FGG conjecture is load-bearing on the unshown equivalence between the Lean statement and the original definitions (ring-of-disagrees graph, QAOA unitary, expectation-value expression, and optimization over variational parameters). No explicit matching or reference to Farhi et al. (2014) is supplied, so the mechanical verification applies only to the reduced statement.

Simulated Author's Rebuttal

1 responses · 0 unresolved

We thank the referee for the positive assessment and the constructive comment on the structural scaffolding. We address the point below and will revise the manuscript accordingly.

read point-by-point responses

  1. Referee: [Abstract] Abstract and §1 (structural scaffolding paragraph): the central claim that the work resolves the FGG conjecture is load-bearing on the unshown equivalence between the Lean statement and the original definitions (ring-of-disagrees graph, QAOA unitary, expectation-value expression, and optimization over variational parameters). No explicit matching or reference to Farhi et al. (2014) is supplied, so the mechanical verification applies only to the reduced statement.

    Authors: We agree that an explicit side-by-side mapping strengthens the central claim. In the revised manuscript we will add a new subsection (or short appendix) that directly references Farhi et al. (2014) and provides a component-wise correspondence: the ring-of-disagrees graph (Definition 1 in the paper vs. the cycle graph with alternating signs in FGG), the QAOA unitary (the product of cost and mixer unitaries with the standard parameterization), the expectation-value expression, and the optimization over variational parameters. This will include verbatim quotations from the original paper and a table confirming that the Lean statement is a faithful formalization of the conjecture. With this addition the mechanical verification applies to the original claim. revision: yes

Circularity Check

0 steps flagged

No circularity: machine-verified Lean proof is independent of inputs

full rationale

The paper reduces the FGG conjecture to a single open statement, supplies it to an LLM, and obtains a Lean-certified proof against an external quantum-information library. The proof itself is mechanically verified and does not reduce to any fitted parameter, self-definition, or self-citation chain. The acknowledged human step (confirming the formal statement matches the original conjecture) lies outside the derivation and is not part of the proof construction. No load-bearing step matches any of the enumerated circularity patterns.

Axiom & Free-Parameter Ledger

0 free parameters · 2 axioms · 0 invented entities

The claim rests on the correctness of the existing Lean quantum-information library, standard axioms of linear algebra and quantum mechanics, and the assumption that the formalized QAOA operators match the original definition. No free parameters or new postulated entities appear.

axioms (2)
  • domain assumption Standard properties of QAOA unitaries, Pauli operators, and approximation ratios as encoded in the prior Lean quantum-information library.
    The paper states it builds on a substantial Lean library of quantum information to formalize QAOA components.
  • domain assumption The reduced single open mathematical statement is equivalent to the original FGG conjecture once the structural scaffolding is accepted.
    The methodology reduces the conjecture to one statement that the model then proves.

pith-pipeline@v0.9.1-grok · 5808 in / 1494 out tokens · 34585 ms · 2026-06-30T06:37:59.332680+00:00 · methodology

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.

Reference graph

Works this paper leans on

47 extracted references · 18 canonical work pages · 5 internal anchors

  1. [1]

    A Quantum Approximate Optimization Algorithm

    E. Farhi, J. Goldstone, and S. Gutmann, A Quantum Approximate Optimization Algorithm (2014), arXiv:1411.4028 [quant-ph]

    work page internal anchor Pith review Pith/arXiv arXiv 2014

  2. [2]

    de Moura and S

    L. de Moura and S. Ullrich, inInternational Conference on Automated Deduction(Springer, 2021) pp. 625–643

    2021

  3. [3]

    The mathlib Community, inProceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs(2020)

    2020

  4. [4]

    T. H. Trinh, Y. Wu, Q. V. Le, H. He, and T. Luong, Nature625, 476 (2024)

    2024

  5. [5]

    Hubertet al., Nature651, 607 (2025)

    T. Hubertet al., Nature651, 607 (2025)

    2025

  6. [6]

    Romera-Paredeset al., Nature625, 468 (2024)

    B. Romera-Paredeset al., Nature625, 468 (2024)

    2024

  7. [7]

    Y. Wu, A. Q. Jiang, W. Li, M. N. Rabe, C. Staats, M. Jamnik, and C. Szegedy, inAdvances in Neural Information Processing Systems (NeurIPS)(2022) arXiv:2205.12615

    work page arXiv 2022

  8. [8]

    K. Yang, A. M. Swope, A. Gu, R. Chalamala, P. Song, S. Yu, S. Godil, R. Prenger, and A. Anandkumar, inAdvances in Neural Information Processing Systems (NeurIPS), Datasets and Benchmarks Track(2023) arXiv:2306.15626

    work page arXiv 2023

  9. [9]

    Z. Z. Renet al., DeepSeek-Prover-V2: Advancing Formal Mathematical Reasoning via Reinforcement Learning for Subgoal Decomposition (2025), arXiv:2504.21801 [cs.CL]

    work page internal anchor Pith review Pith/arXiv arXiv 2025

  10. [10]

    A. Q. Jiang, S. Welleck, J. P. Zhou, W. Li, J. Liu, M. Jamnik, T. Lacroix, Y. Wu, and G. Lample, in International Conference on Learning Representations (ICLR)(2023) arXiv:2210.12283

    work page arXiv 2023

  11. [11]

    Ax-Prover: A Deep Reasoning Agentic Framework for Theorem Proving in Mathematics and Quantum Physics

    B. Breen, M. Del Tredici, J. McCarran, J. Aspuru Mijares, W. W. Yin, K. Sulimany, J. M. Taylor, F. H. L. Koppens, and D. Englund, Ax-Prover: A Deep Reasoning Agentic Framework for Theorem Proving in Mathematics and Quantum Physics (2025), arXiv:2510.12787 [cs.AI]

    work page internal anchor Pith review Pith/arXiv arXiv 2025

  12. [12]

    Wurtz and P

    J. Wurtz and P. Love, Phys. Rev. A103, 042612 (2021)

    2021

  13. [13]

    M. P. Harriganet al., Nature Physics17, 332 (2021)

    2021

  14. [14]

    Quantum Optimization for Maximum Independent Set Using Rydberg Atom Arrays

    H. Pichler, S.-T. Wang, L. Zhou, S. Choi, and M. D. Lukin, Quantum Optimization for Maximum Independent Set Using Rydberg Atom Arrays (2018), arXiv:1808.10816 [quant-ph]

    work page internal anchor Pith review Pith/arXiv arXiv 2018

  15. [15]

    Ebadiet al., Science376, 1209 (2022)

    S. Ebadiet al., Science376, 1209 (2022)

    2022

  16. [16]

    Nguyenet al., PRX Quantum4, 010316 (2023)

    M.-T. Nguyenet al., PRX Quantum4, 010316 (2023)

    2023

  17. [17]

    Bernienet al., Nature551, 579 (2017)

    H. Bernienet al., Nature551, 579 (2017)

    2017

  18. [18]

    Keeslinget al., Nature568, 207 (2019)

    A. Keeslinget al., Nature568, 207 (2019)

    2019

  19. [19]

    U. Kol, M. Ben-Shahar, K. Sulimany, and D. Englund, QuantumOptimization: a Lean 4 / Mathlib library of machine-verified quantum-optimization results,https: //github.com/urikol/QuantumOptimization(2026)

    2026

  20. [20]

    Z. Wang, S. Hadfield, Z. Jiang, and E. G. Rieffel, Phys. Rev. A97, 022304 (2018), arXiv:1706.02998 [quant-ph]

    work page arXiv 2018

  21. [21]

    G. B. Mbeng, R. Fazio, and G. E. Santoro, Optimal quantum control with digitized Quantum Annealing (2019), arXiv:1911.12259 [quant-ph]

    work page arXiv 2019

  22. [22]

    E. Lieb, T. Schultz, and D. Mattis, Ann. Phys.16, 407 (1961)

    1961

  23. [23]

    Jordan and E

    P. Jordan and E. Wigner, Z. Phys.47, 631 (1928)

    1928

  24. [24]

    P. W. Anderson, Phys. Rev.112, 1900 (1958)

    1900

  25. [25]

    G. B. Mbeng, R. Fazio, and G. Santoro, Quantum Annealing: a journey through Digitalization, Control, and hybrid Quantum Variational schemes (2019), arXiv:1906.08948 [quant-ph]

    work page arXiv 2019

  26. [26]

    W. W. Ho and T. H. Hsieh, SciPost Phys.6, 029 (2019)

    2019

  27. [27]

    Thequantumapproximateoptimizationalgorithm needs to see the whole graph

    E. Farhi, D. Gamarnik, and S. Gutmann, The Quantum Approximate Optimization Algorithm Needs to See the Whole Graph: A Typical Case (2020), arXiv:2004.09002 [quant-ph]

    work page arXiv 2020

  28. [28]

    Bravyi, A

    S. Bravyi, A. Kliesch, R. Koenig, and E. Tang, Phys. Rev. Lett.125, 260505 (2020), arXiv:1910.08980 [quant-ph]

    work page arXiv 2020

  29. [29]

    Ben Shahar, J

    M. Ben Shahar, J. Morag, D. Englund, and K. Sulimany (2026), in preparation

    2026

  30. [30]

    LeanScriber: an agentic toolkit for Lean 4 formalization, https://github.com/urikol/leanscriber(2026)

    2026

  31. [31]

    Larocca, P

    M. Larocca, P. Czarnik, K. Sharma, G. Muraleedharan, P. J. Coles, and M. Cerezo, Quantum6, 824 (2022), arXiv:2105.14377 [quant-ph]

    work page arXiv 2022

  32. [32]

    Matos, C

    G. Matos, C. N. Self, Z. Papi´ c, K. Meichanetzidis, and H. Dreyer, Quantum7, 966 (2023), arXiv:2206.06400 [quant-ph]

    work page arXiv 2023

  33. [33]

    Wiersema, E

    R. Wiersema, E. K¨ okc¨ u, A. F. Kemper, and B. N. Bakalov, npj Quantum Information10, 110 (2024)

    2024

  34. [34]

    G. H. Low and I. L. Chuang, Phys. Rev. Lett.118, 010501 (2017), arXiv:1606.02685 [quant-ph]

    work page internal anchor Pith review Pith/arXiv arXiv 2017

  35. [35]

    Gily´ en, Y

    A. Gily´ en, Y. Su, G. H. Low, and N. Wiebe, in 51st Annual ACM SIGACT Symposium on Theory of Computing(2018) arXiv:1806.01838 [quant-ph]

    work page arXiv 2018

  36. [36]

    G. H. Low, T. J. Yoder, and I. L. Chuang, Phys. Rev. X 6, 041067 (2016)

    2016

  37. [37]

    Fej´ er, J

    L. Fej´ er, J. Reine Angew. Math.146, 53 (1916)

    1916

  38. [38]

    Riesz, J

    F. Riesz, J. Reine Angew. Math.146, 83 (1916)

    1916

  39. [39]

    Haah, Quantum3, 190 (2019)

    J. Haah, Quantum3, 190 (2019)

    2019

  40. [40]

    J. M. Martyn, Z. M. Rossi, A. K. Tan, and I. L. Chuang, PRX Quantum2, 040203 (2021), arXiv:2105.02859 [quant-ph]

    work page arXiv 2021

  41. [41]

    V. M. Bastidas, S. Zeytino˘ glu, Z. M. Rossi, I. L. Chuang, and W. J. Munro, Phys. Rev. B109, 014306 (2024)

    2024

  42. [42]

    Chapman and S

    A. Chapman and S. T. Flammia, Quantum4, 278 (2020)

    2020

  43. [43]

    Chapman, S

    A. Chapman, S. J. Elman, and R. L. Mann, A Unified Graph-Theoretic Framework for Free-Fermion Solvability (2023), arXiv:2305.15625

    work page arXiv 2023

  44. [44]

    Preskill, Quantum2, 79 (2018)

    J. Preskill, Quantum2, 79 (2018)

    2018

  45. [45]

    Pirandola, U

    S. Pirandola, U. L. Andersen, L. Banchi, M. Berta, D. Bunandar, R. Colbeck, D. Englund, T. Gehring, C. Lupo, C. Ottaviani, J. Pereira, M. Razavi, J. S. Shaari, M. Tomamichel, V. C. Usenko, G. Vallone, P. Villoresi, and P. Wallden, Adv. Opt. Photon.12, 1012 (2020)

    2020

  46. [46]

    Sulimany, S

    K. Sulimany, S. K. Vadlamani, R. Hamerly, P. Iyengar, and D. Englund, Phys. Rev. X15, 041056 (2025)

    2025

  47. [47]

    Marwaha (2026), to appear

    K. Marwaha (2026), to appear

    2026