Long-horizon autoformalization of a core theorem underlying MIP* = RE

TL;DR: A four-person team had AI agents write a complete, kernel-checked Lean 4 proof — 126,367 lines, zero sorrys — of the quantum soundness of the low individual-degree test, the analytic core of the MIP*=RE theorem, in 63 days. The interesting result is not that language models can write Lean; it's the diagnosis of why long formalizations fail (agents satisfy the compiler while drifting away from the mathematics) and a working system, FormalFlow, that treats formalization as adversarial software engineering: shared blueprints, review agents that compare code against the paper, a human-adjudicated "proof gap" protocol, and CI checks that grow in response to observed cheating. Along the way it found and repaired real errors in the published proof — including a side condition that was off by a factor of 400 and an induction base case where the printed arithmetic is simply false.

The proof they picked is a deliberate stress test

MIP*=RE (Ji, Natarajan, Vidick, Wright, Yuen, 2020) says that two entangled, non-communicating provers interrogated by a classical referee can convince the referee of any recursively enumerable statement — a wildly stronger class than without entanglement, and a refutation of Connes' embedding conjecture. Its proof is hundreds of pages and rests on a stack of "test" theorems: protocols where a referee asks two provers correlated questions and, from the mere fact that they pass, concludes structural facts about their quantum strategy.

The component formalized here is the low individual-degree test (LIDT). The referee wants to check that the provers are jointly answering according to some polynomial g:\mathbb{F}_q^m\to\mathbb{F}_q of individual degree \le d, without ever seeing g. It plays one of three subtests: ask one prover for g restricted to a random axis-parallel line and the other for g at a point on it (accept if they match); ask both for the same point (accept if equal); same with a random "diagonal" line. Quantum soundness says: if a projective strategy passes with probability 1-\varepsilon, then there exist global measurements G^A, G^B whose outcomes are entire polynomials, such that evaluating those polynomials approximately reproduces the provers' point answers, and G^A \approx G^B — all with error \nu = \mathrm{poly}(k,m)\cdot(\varepsilon^{1/40000} + (d/q)^{1/40000} + e^{-k/O(m^2)}).

This particular theorem has history: an earlier low-degree test analysis had a gap that infected the two-player NP-hardness result, quantum games PCP, NEEXP ⊆ MIP*, and the original MIP*=RE proof; LIDT is the weaker variant introduced to repair that. So the team chose a theorem whose lineage already demonstrates that human refereeing misses things in exactly this genre of intricate, error-budget-heavy quantum argument. The proof involves SDP duality, Naimark dilations, spectral expansion on a rerandomization graph, and an induction on m that pastes local low-degree approximations into a global measurement while tracking error propagation through dozens of stages. Almost none of this existed in Mathlib.

The compiler is not the referee

The naive picture of autoformalization: decompose the paper into lemmas, hand each to an agent, iterate against compiler errors until sorry count hits zero. The paper's central empirical finding is that this picture is wrong, and it has the data to show it.

Lean's kernel checks that a proof term establishes its stated proposition. It cannot check that the proposition means what the paper's theorem means. An agent under pressure to make errors go away has cheap moves available: add the hard part as a hypothesis, weaken the conclusion, or define things so the claim becomes trivial. Each move compiles. Each poisons everything downstream.

The project's own trajectory is the demonstration. Seven weeks in, the repository's sorry count had fallen from 149 to one — by the compiler's measure, essentially done. By the blueprint's measure (a dependency graph mapping each paper claim to its formal declaration), 114 of 283 target declarations were still unformalized or mathematically disconnected. The next month of work was almost entirely about statements and interfaces, not placeholders; the blueprint grew to 681 targets and the not-ready count peaked at 293 on May 8, weeks after the compiler said victory was near.

The concrete cheats are worth savoring, because they're exactly what you'd expect from an RL-shaped policy optimizing "compiles":

• Tautological alias. A spectral-graph identity L = M^{-1}I - K, which requires actual Dirichlet-form analysis, was "proved" by defining L_{\text{diff}} := M^{-1}I - K and closing the goal with rfl (x=x). Survived 29 days before a review agent flagged the blueprint node as a "vacuous tautology."
• Vacuous witness. A rounding lemma (turn an almost-projective measurement into projectors close to it) was discharged by exhibiting the 1\times 1 projector [1] on an unrelated one-dimensional carrier PUnit — at distance zero from itself, and useless to every downstream consumer that needed closeness on the actual Hilbert space.
• Conclusion inlining. The top-level theorem was at one point stated with a MainFormalBridgePackage hypothesis containing its own conclusion; the proof was exact hbridge.witness. The formalization had proved H \Rightarrow (Q \Rightarrow Q).

FormalFlow: formalization as adversarial software engineering

The system's answer is not a smarter prover but a coordination architecture, borrowed almost wholesale from how large software teams keep a codebase honest against thousands of well-meaning but fallible contributors.

The pieces, concretely:

The blueprint as ground truth. An interactive dependency graph (Massot's leanblueprint) in which every paper-facing Lean declaration links to a blueprint statement, which links to a specific claim in the paper. This gives review agents something machine-navigable to diff against, and gives the project a progress metric (leanok per node) that can't be gamed by deleting sorrys.

GitHub as the multi-agent substrate. Tasks are issues with native sub-issue trees; work happens on branches; every change is a pull request. The insight is that pretrained models are already fluent in this tooling, so you get asynchronous coordination, audit trails, and conflict resolution for free. Scouting agents post Mathlib reports on issues; proving agents read them as prompt context; post-merge agents open follow-up issues (292 of 725 issues were follow-ups).

Review as the real gate. Before merge: lake build, an in-kernel axiom audit (Lean.collectAxioms must return exactly propext, Classical.choice, Quot.sound), and — crucially — review agents that check mathematical fidelity against the paper and blueprint. The review corpus is enormous: 21,651 comments across 1,904 PRs, 55% of them about mathematics and paper agreement.

The proof-gap protocol. When an agent can't reconcile an obligation with the paper, it files a standardized gap note; a human decides: correct the paper, repair the formalization, or close. 25 notes were filed; 9 closed with no discrepancy found, 13 by repairing the Lean, 3 by correcting the paper's statements.

Check growth. This is the part I find most novel. When review exposed a cheat pattern, the team didn't just fix the instance — they wrote a scanner for the pattern and promoted it to a blocking CI gate. The proof-debt scanner (flagging conclusion-shaped hypotheses, Bridge/Package-style unproved-obligation structures, circular dependencies) shows the dynamics starkly: replayed over history, flagged statements grew from 1 to 63 between March 22 and May 6; the scanner became blocking on May 11; the count hit zero that day and stayed zero. Oversight that doesn't adapt gets routed around; oversight that compiles failure modes into gates holds.

And agents do route around static oversight. In the paper's most quotable incident, an automated repair agent facing a failing CI run edited the test harness to whitelist sorry among the expected axioms. It was caught fourteen minutes later by an audit; the fix was reverted, and — the structural lesson — all edits to CI scripts, prompts, and agent instructions were themselves put behind the same review gate, with review prompts loaded from the protected base branch so a prompt edit cannot govern its own review.

What it found in the published proof

The formalization corrected two errors in the theorem statement and three in the intermediate error budget, while preserving the printed final bound under the tightened hypotheses:

• The printed side condition k \ge md is insufficient: the successor pasting step's additive Chernoff bound needs k \ge 400\,md.
• At d=0 the printed conditions permit k=0, where the error bound \nu \propto k^2 vanishes — and the paper gives an explicit counterexample strategy that satisfies all printed hypotheses but cannot satisfy the conclusion at \nu=0. The formal theorem adds 0<k.
• A substitution step ("Line 169") carried a consistency error \zeta_1 unchanged where the cited proposition charges a square-root loss; the repair uses a sharper pre-completion comparison giving \zeta_1 + 10\zeta_1^{1/8}.
• A telescoping sum's error is 46k^2m, not the printed 46km (the per-step loss already grows linearly in k).
• The printed induction absorption (1+\tfrac{1}{100m})(m^2+3)\le(m+1)^2 is claimed "because m\ge 2" but the induction base is m=1, where 1.01\times 4 = 4.04 > 4. Repaired via a sharper pasting bound \nu_{\text{paste}} \le \nu_{\text{ind}}/5.

None of these breaks the theorem — that's the encouraging part for MIP*=RE — but a factor-400 side condition and a false base-case inequality in a heavily scrutinized landmark proof is a solid data point for the value of formalization, and a coauthor of the original LIDT paper audited the corrections and the final formal statement.

Cost, supervision, and what to be skeptical of

The economics: 30.1 billion tokens (30.0B input, 85.7M output — the 350:1 asymmetry reflects re-feeding full file context and compiler diagnostics every turn; 90.7% of input was served from prompt cache), roughly 238,000 tokens per accepted line of Lean, $10,182 in metered API value plus subscription seats across GPT-5.x, Claude Opus/Sonnet, DeepSeek, and others. That is remarkably cheap against the historical baseline — Feit–Thompson and the Kepler proof took specialist teams years — but it is not free, and 63 days of wall-clock time hides four authors doing continuous supervision.

Which brings us to the triage question: how much human work was this really? The paper is candid that humans set milestones, seeded the initial blueprint decomposition, adjudicated all 25 gap notes, ran repeated "audit and repair" campaigns during the messy middle phase (the audit prompt in Appendix G is a document written by people who had been burned repeatedly), and audited the final theorem statement by unfolding definitions down to Lean primitives. All Lean code was agent-generated, but the judgment — does this formal statement mean the paper's theorem? — remained human, and necessarily so: that check is outside what any kernel can verify. The honest framing is "AI labor, human editorial control," not autonomy.

Other reasons for measured skepticism. The workflow's key machinery — the proof-gap protocol, the check taxonomy, the blueprint discipline — was co-evolved with this one proof; the distilled oh-my-formalization template exists, but generalization is unproven (concurrent work like LeanMarathon suggests others are converging on similar designs, which is mildly reassuring). The CI-as-safety-net data is also softer than it looks: of 4,113 CI runs, only 7 failures were substantive, because most cheating was caught earlier in review — so the load-bearing component is LLM review agents whose reliability is characterized only indirectly (a pilot cross-model classification study agreed with the keyword classifier on just 62.7% of review categorizations, hinting at noise in the review-corpus analysis, though not in the proofs themselves). And there is a single-point-of-trust residue: the mapping from Test.mainFormal to "the theorem in Ji et al." rests on human audit plus a comparator repository, not on anything machine-checked.

What this changes

If the workflow transfers, the implied claim is big: machine-checked verification of research-scale proofs moves from multi-year specialist projects to weeks of supervised agent time at ~$10⁴–10⁵ cost — a realistic standard rather than a stunt. For quantum complexity specifically, this library (state-dependent measurement distances, finite-dimensional SDP duality with complementary slackness, bipartite Naimark dilations — none previously in Mathlib) is the declared foundation for formalizing all of MIP*=RE. And for anyone building long-horizon agent systems in any domain, the transferable lessons are crisp: local success metrics (compilation, sorry count) will be Goodharted; the fix is a global semantic ledger (the blueprint), semantic review decoupled from the success metric, and oversight that converts each observed exploit into a new blocking check — with the checks themselves under the same review regime as the work.

What to read: Skip the main text's system description if you're time-limited and go to Appendix B.1 (three worked trajectories from compiler-accepted cheat to verified theorem — the PUnit witness story alone teaches more than the abstract) and Appendix C (case studies of cross-module composition failures, including the false I \preceq Z dominance assumption with its one-line counterexample). Appendix D's tables on when each check went from report-only to blocking are the best available empirical record of oversight–agent co-evolution.