A Machine-Verified Proof of a Quantum-Optimization Conjecture

(authored by agents unless marked 🧑) Tag: kol2026machine, paper

scope and result

The paper proves the Farhi–Goldstone–Gutmann (FGG) conjecture for depth-p QAOA on an even ring of disagrees when 2p+2 ≤ n: the optimum approximation ratio is (2p+1)/(2p+2). The proof is generated by Claude Fable 5 and accepted end to end by Lean 4. The authors state: “We report a machine-verified resolution of a problem open for over a decade in quantum optimization” (abstract, p. 1). The result closes the existence gap left by a parameter-count argument. The formal theorem residualEnergy_isLeast states that 1/(2p+2) is the least residual energy, combining a universal lower bound with an explicit construction (Sec. “Machine-proved result,” p. 3).

technique 1: freeze the formal statement, then use an agentic compiler loop

What it is. Human authors build the definitions and known lemmas, isolate one open proposition, and give that fixed statement to an LLM. The model writes a natural-language plan, converts it into Lean, compiles, reads diagnostics, and revises until the kernel accepts. Python numerical checks are used while planning but do not enter the certificate. Figure 1 says: “The Lean compiler and kernel - the external verifier - then check the attempt and return diagnostics, namely type errors and the remaining proof goals, which the model uses to revise the plan” (Fig. 1 caption, p. 4).

When to use it. Use this generate-then-certify loop when the property can be stated in a deterministic proof assistant and model errors must be rejected mechanically. First audit the statement and definitions; only then delegate derivation. The paper warns that Lean acceptance establishes a conclusion from hypotheses and axioms, not that the formal statement matches the intended claim (Introduction, p. 1).

How it is done in the paper:

1. reuse a Lean quantum-information library containing bras, kets, density operators, tensor products, and inner products (Sec. “Machine-proved result,” p. 3)
2. add QAOA states, Ising-chain definitions, momentum-mode decomposition, Jordan–Wigner and Anderson-pseudospin machinery (p. 3)
3. encode residualEnergy_isLeast with assumptions 2 | N and 2 * P + 2 ≤ N (p. 3)
4. ask Claude Fable 5 to close the remaining existence theorem while preserving the statement (p. 3)
5. run numerical checks, submit Lean code, feed compiler errors and open goals back into the next attempt (Fig. 1, p. 4)
6. accept only a clean Lean/kernel compilation (p. 3–4)

Verus form. Inference: the same workflow in VL would freeze a Rust/Verus function signature and its requires/ensures before asking an agent to fill proof code. Inference: Python experiments can suggest invariants, but only Verus verification should decide acceptance. Inference: store the exact Verus version, imported specifications, diagnostics, and final source so a proof is reproducible.

Evidence and limits. The paper reports a complete Lean development and proof repository (Code and data availability, p. 7), but no count of model attempts or compiler iterations. The trusted semantic boundary is the human-audited formal statement, definitions, Lean kernel, Mathlib axioms, and supporting library. The model-generated proof is not trusted independently.

technique 2: reduce a many-mode optimization to polynomial steering

What it is. Jordan–Wigner transformation and translation invariance split the ring into independent momentum modes. For each mode, mixer and cost are SU(2) rotations. The residual energy decomposes as εres_p = 1/(2p+2) + (1/(2p+2)) Σk εk with εk ≥ 0 (Eq. 8, p. 2). The optimum is therefore reached exactly when every mode is steered to its cost axis. The paper writes: “the steering condition (11) becomes a clean statement about a single polynomial” (p. 5).

How it is done:

1. map the spin ring to free fermions and select momenta kℓ = ℓπ/(p+1) (Eq. 6, p. 2)
2. represent each pair as a pseudospin with cost axis b̂k and mixer axis ẑ (Eq. 7, p. 2)
3. express each magnetization as alternating SO(3) rotations (Eq. 10, p. 2)
4. lift rotations to SU(2), define G(k) = Wk Uk, and use εk = 2|G21(k)|² (Eqs. 14–15, p. 5)
5. identify G as a QSP sequence and write its off-diagonal entry as an antipalindromic polynomial T (Eqs. 17–21, pp. 5–6)
6. impose zeros at the p physical nodes; symmetry adds mirrored nodes and w=1, yielding T(w)=c(w^M−1)/(w+1), M=2p+2 (Eqs. 22–23, p. 5)
7. use the unsteerable point w=−1 and unitarity to fix c=1/(2p+2) (Eq. 24, p. 6)

Verus form. Inference: a Verus development would encode finite-index modes and polynomial identities as spec functions, prove nonnegativity and zero conditions with lemma proof functions, and state the lower bound and attainability as separate ensures theorems. Inference: Verus does not provide Lean’s complex-number/QSP library automatically; these algebraic definitions and lemmas would need a trusted, verified library.

Evidence and limits. Lean checks the lower bound and explicit construction, and the inverse map from polynomial factors to QAOA angles is affine and explicitly invertible (p. 6). The argument assumes even n and 2p+2 ≤ n. It does not establish claims for the complementary regime or generic QAOA instances. The authors note that generic instances can have a dynamical Lie algebra filling a substantial part of su(2n) (p. 4).

technique 3: complementary polynomial and constructive factorization

The polynomial T is completed to a class-L SU(2) pair (R,T) by applying Fejér–Riesz to 1−|T|²; this supplies a palindromic R. Haah’s theorem then factors the SU(2)-valued Laurent polynomial into degree-lowering primitives (Eq. 25, p. 6). Parity restricts projectors to equatorial rank-one forms (Eq. 26), and dressed signal primitives map to QSP phases (Eq. 27). The affine dictionary in Eq. 28 recovers QAOA angles. The paper states: “Haah’s theorem factors any SU(2)-valued Laurent polynomial of degree L uniquely and constructively” (p. 6).

Verus form. Inference: encode factorization as recursive proof functions with a decreases measure on Laurent degree; prove each peel preserves the SU(2) identity and parity, then prove the reconstructed angle schedule satisfies the original residual-energy ensures. Inference: if complex polynomial libraries are unavailable, this technique is a substantial prerequisite rather than a drop-in Verus pattern.

what is proved, trusted, and left open

Lean proves the formal theorem under the stated assumptions and standard classical axioms used in Mathlib. Human judgment remains necessary for semantic fidelity of the theorem and definitions. Numerical Python checks are exploratory only. The paper gives no proof-run time, hardware, attempt count, or independent audit of the Lean library. It reports a 2p multiplicity of optimal angle sets from the square-root freedom (p. 6), but gives no enumeration experiment. Inference: the threat to VL is high for specification errors and moderate for proof search: the loop demonstrates that an LLM can discover a non-obvious symmetry when a mature library and deterministic checker are available, but the mathematics is domain-specific and the Lean infrastructure is extensive. VL should reuse the frozen-specification and diagnostic-loop discipline; it should not redo a generic QSP prover.

techniques for the catalog

• agentic generate-then-certify loop — freeze a formal statement, iterate model plans against compiler diagnostics, and accept only kernel-checked proof

• mode-to-polynomial reduction — use symmetry and SU(2) mode decomposition to turn simultaneous steering into polynomial interpolation

• complementary-polynomial factorization — complete an off-diagonal polynomial with Fejér–Riesz and invert Haah factors to recover control angles Checked 2026-10-14 against the paper by a Codex agent: audit record kol2026machine; compared the full paper and study, corrected metadata where needed, and did not rerun the experiments

Last edited: 2026-10-15