A Machine-Verified Proof of a Quantum-Optimization Conjecture

TL;DR: A team formalized a decade-old conjecture about the exact power of QAOA on a canonical benchmark — the "ring of disagrees" — and then handed the one remaining open gap to an LLM equipped with a Lean 4 toolchain. The model found a genuinely new proof route: it recognized that each momentum mode's dynamics is a Quantum Signal Processing sequence, converting a hard existence question about 2p transcendental equations into an explicit polynomial construction, with the mysterious constant 1/(2p+2) falling out as the normalization of a unique polynomial. Lean's kernel certified every step, so the only thing humans had to check is that the theorem statement means what it should. This is one of the cleanest existing demonstrations of an LLM producing new mathematical structure — not a rediscovery, not a search over known tactics — under a verification regime where hallucination is structurally impossible to smuggle through.

The conjecture: what exactly can depth-p QAOA do?

QAOA is the workhorse ansatz of near-term quantum optimization. You encode a combinatorial cost function into a Hamiltonian H_C, pick a simple "mixer" B = \sum_j \sigma^x_j, and alternate p rounds of evolution under each:

|\bm{\gamma},\bm{\beta}\rangle = e^{-i\beta_p B}e^{-i\gamma_p H_C}\cdots e^{-i\beta_1 B}e^{-i\gamma_1 H_C}\,|+\rangle^{\otimes n},

then classically optimize the 2p angles (\bm{\gamma},\bm{\beta}) to maximize the expected cost. The figure of merit is the approximation ratio r_p: the achieved cost divided by the true optimum.

In their original 2014 paper, Farhi, Goldstone, and Gutmann analyzed the cleanest possible benchmark: MaxCut on a cycle of n spins ("ring of disagrees" — maximize the number of adjacent spins that disagree; physically, a 1D antiferromagnetic Ising chain). From numerics they conjectured that for even n with 2p+2 \le n, the optimal ratio is exactly

r_p^* = \frac{2p+1}{2p+2}.

That's 3/4 at depth 1, 5/6 at depth 2, approaching 1 as 1/p. They proved p=1; Wang et al. later proved p=2 by an exact fermionic calculation; numerics confirmed the pattern out to p=128. But the general statement stayed open for over a decade — despite this being arguably the single most-studied QAOA instance.

Why it was stuck: a square system with no theorem behind it

The hard direction was already reduced substantially by prior work. Because the Ising ring is a free-fermion model, a Jordan–Wigner transformation plus translational invariance splits the whole 2^n-dimensional evolution into p independent momentum modes at k_\ell = \ell\pi/(p+1). Each mode is a single effective spin-½ (an Anderson pseudospin) whose Bloch vector \bm{m}_k starts at \hat{\bm{z}} and gets rotated by the QAOA layers — alternating \mathrm{SO}(3) rotations about \hat{\bm{z}} (mixer) and about a tilted cost axis \hat{\bm{b}}_k = (-\sin k, 0, \cos k). Mbeng, Fazio, and Santoro showed the residual energy (the shortfall from optimal) decomposes as

\varepsilon^{\mathrm{res}}_p = \frac{1}{2p+2} + \frac{1}{2p+2}\sum_k \varepsilon_k, \qquad \varepsilon_k = \tfrac{1}{2}\|\bm{m}_k - \hat{\bm{b}}_k\|^2 \ge 0.

Since each \varepsilon_k \ge 0, the lower bound \varepsilon^{\mathrm{res}}_p \ge 1/(2p+2) — equivalently r_p^* \le (2p+1)/(2p+2) — was already known. The conjecture is that the bound is saturated: there exist angles that simultaneously steer every mode's Bloch vector exactly onto its cost axis.

Count parameters: each condition \bm{m}_k = \hat{\bm{b}}_k pins a unit vector, which is two real constraints; p modes give 2p equations in 2p angles. A square system. If it were linear you'd be done. But the equations are transcendental in the angles through products of rotations, and square transcendental systems can have zero, one, or many real solutions. Everyone believed the answer from the parameter count and the numerics — but "the dimensions match" is not a proof, and nobody had a construction. This existence statement was the gap.

The pipeline: generate, then certify

The methodology is a tight loop between an LLM (which the paper calls Claude Fable 5) and the Lean 4 proof assistant.

The generate-then-certify loop (paper's Fig. 1). The model drafts proof plans in natural language, tests candidate claims numerically in Python before investing in formalization, writes Lean, and revises based on compiler diagnostics until the kernel accepts. Hallucinated steps cannot survive compilation.

Three details of the setup matter. First, the humans did substantial groundwork: building on a Lean quantum-information library from parallel work on quantum cryptography, they formalized QAOA itself, the Ising ring, and — importantly — all the known components of the problem, including the Jordan–Wigner reduction and the per-mode decomposition. Second, they isolated the open gap as a single formal existence statement, fixed before the model saw it, and the model never modified it. Third, the model's Python numerical checks are purely internal scratchwork; only Lean acceptance counts.

The final theorem, residualEnergy_isLeast, states that 1/(2p+2) is the least attainable residual energy — combining the known lower bound and the new attainability construction, both fully kernel-checked with only Mathlib's standard classical axioms.

The proof the model found: steering becomes polynomial interpolation

Here is where it gets genuinely interesting. The model's route runs through Quantum Signal Processing (QSP) — the \mathrm{SU}(2) polynomial machinery that underlies modern quantum algorithms (QSVT, Hamiltonian simulation). No prior paper on this conjecture used QSP.

The lift. Rotations of a Bloch vector are the adjoint action of \mathrm{SU}(2). Lift the per-mode \mathrm{SO}(3) dynamics to two \mathrm{SU}(2) elements: the depth-p propagator U_k and a fixed frame rotation W_k = e^{-ik\tau^y_k/2} that maps \hat{\bm{z}} to the cost axis. Why is \mathrm{SU}(2) available at all? Not because it's a symmetry of the Hamiltonian — it isn't. It's a dynamical symmetry: the mixer and cost generators for each mode close into a three-dimensional Lie algebra \mathfrak{su}(2), so the dynamical Lie algebra of the whole circuit is \bigoplus_k \mathfrak{su}(2)_k — dimension O(p) instead of the generic O(4^n). The free-fermion structure is exactly what makes single-qubit machinery like QSP the right tool.

The keystone. Define the lifted propagator G(k) := W_k U_k \in \mathrm{SU}(2). Because the adjoint action preserves dot products, the per-mode residual collapses to one matrix entry:

\varepsilon_k = 2\,|G_{21}(k)|^2.

Steering mode k perfectly means G(k) is diagonal. The whole 2p-equation transcendental system becomes: make one off-diagonal function vanish at p points.

QSP structure. Rewriting each cost layer as a conjugated z-rotation, G takes the standard QSP form — an alternating product of the fixed signal W_k and k-independent phases \psi_j, affinely related to the QAOA angles. In the variable z = e^{ik/2}, W_k is linear in z^{\pm 1}, so G is an \mathrm{SU}(2)-valued Laurent polynomial of degree L = 2p+1. Its off-diagonal entry, after a parity reduction to w = z^2, is a polynomial T(w) of degree \le L that is antipalindromic: w^L T(1/w) = -T(w). Unitarity gives |R|^2 + |T|^2 = 1 on the unit circle, with R the palindromic diagonal partner.

Now watch the constant appear. The steering condition says T must vanish at the p nodes w_\ell = e^{ik_\ell}, which are (2p+2)-th roots of unity. Antipalindromy forces a root at w=1 and drags in each node's complex-conjugate mirror. Count: p nodes + p mirrors + the root at 1 = 2p+1 = L roots — the polynomial is completely determined up to a constant. The roots are exactly all M := 2p+2 roots of unity except w = -1:

T(w) = c\,\frac{w^M - 1}{w + 1}.

The steering polynomial $T$ for depth $p=4$ ($M=10$). The $p$ required zeros (top), their mirrors (bottom), and the parity-forced root at $w=1$ account for all $2p+1$ roots: $T$ is the unique node polynomial up to scale. The excluded point $w=-1$ corresponds to $k=\pi$, where cost and mixer axes are antiparallel and steering is impossible — and unitarity at exactly that point pins $|T(-1)|=1$, fixing $c = 1/(2p+2)$.

The excluded root w=-1 is the mode k = \pi, whose cost and mixer axes are antiparallel — geometrically unsteerable. Palindromy forces R(-1) = 0, so unitarity demands |T(-1)| = 1, and since T(-1) = -cM, the scale is c = 1/M = 1/(2p+2). The FGG constant, seen only in numerics for a decade, is the normalization of the unique node polynomial, fixed by unitarity at the one mode that cannot be steered. That is a structural explanation, not just a proof.

Closing the loop. Existence of the palindromic partner R with |R|^2 = 1 - |T|^2 \ge 0 follows from the Fejér–Riesz theorem (spectral factorization of nonnegative trigonometric polynomials) — with 2^p choices of square root, explaining a 2^p-fold degeneracy of optimal angles that had also been observed numerically. Finally, Haah's constructive factorization of \mathrm{SU}(2)-valued Laurent polynomials peels G into primitives; the parity constraint forces each primitive to be equatorial, one phase \varphi_j each, and an explicit affine dictionary converts the \varphi_j back into QAOA angles (\gamma_\ell, \beta_\ell). The hard existence problem ends as an explicit construction.

How strong is this evidence, and what to be skeptical about

The trust model here is unusually clean, and worth spelling out. Lean's kernel guarantees the conclusion follows from the hypotheses and Mathlib's classical axioms. What it cannot guarantee is that the formal statement means the FGG conjecture — the "semantic gap." The authors confined human verification to exactly that: the theorem statement, residualEnergy, ringQAOA, and their transitive definitions. They state the statement was frozen before the model saw the gap and never modified. The full Lean development is public, so this is auditable — and auditing the statement is precisely what an interested reader should do, since misformalization is the one remaining failure mode. (This is much less far-fetched than it sounds; encoding "residual energy of depth-p QAOA on the ring" involves many definitional choices — normalizations, boundary conditions, the parity sector of the Jordan–Wigner transformation — where an error would make the theorem true but about the wrong object.)

Some honest deflation of the headline. The model did not resolve "a decade-old open problem" from a cold start: humans (and their autoformalization agents) formalized the entire known reduction — Jordan–Wigner, pseudospins, the per-mode decomposition, the lower bound — and served the model a single, sharply-posed existence statement. That statement was the genuinely open part, and the community had failed to close it, so the contribution is real; but the framing "LLM proves open conjecture" compresses a lot of human problem-shaping. Relatedly, the paper gives no data on the process: how many iterations of the loop, how much compute, how many dead-end proof plans, whether the QSP idea came out in the first attempt or the hundredth. Without that, we can't tell if this is a repeatable methodology or a one-off success on a problem that happened to have hidden low-dimensional structure. "Claude Fable 5" is not a publicly documented model, which adds to the opacity.

On novelty of the idea itself: the paper is candid that the nearest prior result — transverse-field Ising dynamics are QSP sequences (their ref [2]) — existed in the literature, just never aimed at QAOA optimization. So the model's move is best described as recognizing that a known bridge applies, then executing a nontrivial construction across it (the parity analysis, node polynomial, Fejér–Riesz completion, Haah inversion). That's a realistic picture of what current LLMs can do at their best: creative recombination at research grade, verified so we don't have to take it on faith. A note added mentions independent concurrent work on the same problem, so the result may not be unique to this pipeline.

Finally, scope: the result pins the expressive power of QAOA on one free-fermion benchmark. It generalizes, as the authors note, to any translation-invariant free-fermion QAOA whose per-mode dynamics close into \mathfrak{su}(2) — but the whole proof strategy lives and dies on the dynamical Lie algebra collapsing from O(4^n) to O(p) dimensions. Generic QAOA instances have no such collapse, so don't expect this to crack MaxCut on general graphs.

What changes if this holds up

Two things. For quantum optimization: a canonical benchmark now has an exact, explicit performance guarantee with constructive optimal angles, and a new QSP-based lens on free-fermion QAOA that others will likely reuse. For AI-for-math: this is a concrete template for the division of labor that actually works today — humans audit a compact formal statement, the model does unbounded creative search inside it, and a deterministic kernel filters hallucination at zero marginal trust cost. The paper's closing observation is the right one: formal problems are the natural first domain for autonomous discovery because they are closed — the verifier is a complete in-loop oracle, so a wrong step is discarded rather than propagated.

What to read: Section IV is the payoff — the proof itself, especially IV.2 (the keystone identity \varepsilon_k = 2|G_{21}|^2) and IV.5, where the constant 1/(2p+2) emerges from unitarity at the unsteerable mode. If you care about the methodology more than the math, Section III plus a browse of the public Lean repository — checking that ringQAOA and residualEnergy encode what you think they do — is the best use of an hour.