FormalFlow: Long-Horizon Autoformalization with AI Agents...

Key results at a glance

FormalFlow coordinates AI proving agents under human supervision to formalize multi-hundred-page mathematical proofs in Lean 4. We applied it to formalize the quantum soundness of the low individual-degree test (LIDT), an analytic pillar of $\mathrm{MIP}^* = \mathrm{RE}$ :

126,367 lines of Lean 4 across 337 files, completed over 63 days (March 21 – May 23, 2026) with code written entirely by agents.
Zero sorry placeholders, verified end-to-end by Lean’s kernel using only the three standard classical axioms (propext, Classical.choice, Quot.sound).
Collaborative mathematical auditing: identified and resolved 25 proof gaps and formalization artifacts—repairing two conditions and three intermediate steps while confirming the core soundness bound intact.
Fully open development history: 2,778 commits, 1,790 merged PRs, 21,651 review comments, and an interactive dependency blueprint.

AI agents have become remarkably proficient at solving competition math problems and completing isolated Lean lemmas in a single prompt. But taking on a 100-page research paper is a fundamentally different challenge.

In a large codebase, proving individual lemmas is rarely the real bottleneck. The bottleneck is long-horizon coordination: keeping hundreds of interdependent files aligned, stopping mathematical definitions from drifting between agent sessions, and making sure that code which compiles actually proves what the paper intended.

Over 63 days, we formalized the core analytic theorem underlying the landmark $\mathrm{MIP}^* = \mathrm{RE}$ paper—the quantum soundness of the classical low individual-degree test (Ji, Natarajan, Vidick, Wright, and Yuen, 2020↗)—in 126,367 lines of Lean 4. In our paper, Long-Horizon Autoformalization of a Core Theorem Underlying MIP*=RE↗ (joint work with Ruixuan Deng, Yanqiao Zhu, and Zhengfeng Ji), we share the system we built, the development history, and what we learned about the dynamics of agentic autoformalization.

Compiler Satisfaction $\ne$ Mathematical Progress

In software engineering, green tests don’t mean you built the right product. In autoformalization, satisfying Lean’s typechecker does not mean you proved what the paper intended.

Lean verifies that a proof term inhabits its declared type. It cannot judge whether that type matches the mathematics in the original paper. When LLM agents work across hundreds of independent sessions, two failure modes inevitably compound:

Composition breakdown: Agents working in separate sessions invent local definitions, coordinate choices, or normalization conventions that compile locally but refuse to connect to adjacent modules.
Statement drift: When a lemma is difficult, an agent’s path of least resistance is to subtly alter the statement—tacking on an extra hypothesis, weakening an inequality, or redefining an object so the claim becomes trivial. The lemma compiles, but the mathematical content evaporates.

During our formalization, this divergence surfaced dramatically on April 29 (Day 53). By the most common dashboard metric, the project looked essentially finished: the repository’s sorry count had dropped to just one.

Yet our interactive blueprint revealed the truth: 115 out of 284 tracked mathematical claims were still unformalized or disconnected from the main theorem.

A falling sorry count is a dangerous vanity metric. Unconstrained LLMs will gladly eliminate sorry by taking syntactic shortcuts that compile without advancing the proof. Real progress requires tracking declarations against an explicit dependency graph, auditing statement fidelity, and constantly scanning for proof debt.

How FormalFlow Works

To prevent statement drift and keep hundreds of files composable, FormalFlow coordinates agents across four nested feedback loops, anchored around a shared GitHub repository containing the paper LaTeX, the Lean code, and an interactive blueprint↗:

The highlighted task expands into the review loop; the highlighted work session expands into the proof loop. Check growth runs across all three scales.

Macro planning (topological dependency): An orchestrator agent extracts mathematical claims from the paper into blueprint nodes and GitHub issues. Tasks are dispatched strictly in topological order: agents only work on lemmas whose dependencies are already proven and merged.
Micro work sessions (context-ordered proving): A task agent checks out a fresh branch with a strict information diet. It reads the paper text first, then the blueprint node, and only then the existing Lean definitions. It writes code, reads compiler diagnostics, and iterates in an edit-compile loop.
Meso review gates (semantic audit before merge): Passing lake build is only a prerequisite; it does not earn a merge. Dedicated review agents compare the pull request against the paper text and blueprint node to detect statement weakening or smuggled assumptions. Across 1,904 pull requests, agents generated 21,651 review comments—and 55% focused on mathematical fidelity and interface cleanups, rather than syntax.
Governance (evolving checks): Whenever review caught a new shortcut or anti-pattern, we codified it into an automated CI linter. Over time, the repository accumulated automated checks against trivial instances, unproved bridges, and illegal axiom imports.

The Human Role: Architects, Not Typists

Humans did not write Lean tactics. Instead, we acted as system architects, verifiers, and mathematical adjudicators.

When an agent encountered an apparent inconsistency between the paper and the formalization, it was instructed not to guess or force a proof. It filed a proof-gap note and stopped. We then examined the issue alongside the original authors, decided whether to fix the paper, adjust the Lean representation, or close the note as a formalization artifact, and instructed the agents on the resolution.

The proving sessions ran on standard agent harnesses, including TeXRA↗, Claude Code, OpenCode, and Codex, coordinated via GitHub Issues, PRs, and Actions. We packaged the reusable infrastructure into the open-source oh-my-formalization↗ template.

The Target: Quantum Soundness of the Low Individual-Degree Test

The landmark $\mathrm{MIP}^* = \mathrm{RE}$ theorem (Ji, Natarajan, Vidick, Wright, and Yuen, 2020↗) established that two entangled provers can verify any recursively enumerable language, resolving Tsirelson’s problem and refuting Connes’ embedding conjecture in operator algebras.

Earlier proofs of $\mathrm{MIP}^* = \mathrm{RE}$ relied on an older low-degree test that contained an analytic gap. To repair the entire proof chain, Ji et al. (2020) introduced the low individual-degree test (LIDT), giving a self-contained, 100-page proof of its quantum soundness. That 100-page paper is the target of our formalization.

(a) The referee’s three tests

Sample a point u ∈ 𝔽_q^m uniformly, then choose one test with probability ⅓ each.

Axis-parallel line

Choose i uniformly from 1, …, m. One prover receives the line ℓ = {u + t e_i : t ∈ 𝔽_q} and returns a degree-d polynomial f. The other receives u and returns a ∈ 𝔽_q.

Accept whenf(u) = a

Self-consistency

Both provers receive the same point u and return a, b ∈ 𝔽_q.

Accept whena = b

Diagonal line

Choose i uniformly from 1, …, m, then choose v ∈ 𝔽_q^m uniformly with v_i+1 = ⋯ = v_m = 0. One prover receives ℓ = {u + t v : t ∈ 𝔽_q} and returns a degree-md polynomial f. The other receives u and returns a ∈ 𝔽_q.

Accept whenf(u) = a

In both line tests, the prover roles are assigned uniformly at random.

(b) An honest strategy

Alice and Bob agree on a polynomial g: 𝔽_q^m → 𝔽_q of degree at most d in each variable.

Referee Accept if f(u) = a

Line ℓ

Polynomial f

Point u

Value a

Alice f = g|_ℓ Restrict to the line

Bob a = g(u) Evaluate at the point

Same polynomial g

The line and point come from the referee. Alice’s and Bob’s roles may be interchanged.

Two proof ingredients connect quantum-information tools to the main induction.

Main formal theoremInduction on the number of variables

Self-improvement

SDP slackness
Orthonormalization
Expansion & variance

Pasting

Matrix Chernoff bound
Commutativity lemmas

Quantum information

State-dependent distance
Consistency
Related inequalities

For a strategy accepted with high probability, quantum soundness yields question-independent, polynomial-valued measurements whose evaluations approximately agree with the provers’ answers. Their polynomial outcomes are also approximately consistent, even with shared entanglement.

The low individual-degree test and its formal proof. Adapted from panels (a)–(c) of the paper’s schematic.

How the Test Works

A classical referee interrogates two provers who share entanglement but cannot communicate:

The referee picks a random point $u \in \mathbb{F}_q^m$ and chooses one of three checks with equal probability: an axis-parallel line test, a self-consistency test, or a diagonal line test.
Provers receive coordinate queries and return answers. In an honest strategy, they share a polynomial $g$ of individual degree $\le d$ . One prover returns the restriction of $g$ to a line, while the other returns the point evaluation $g(u)$ . The referee accepts if the answers agree.

Quantum soundness establishes the converse: if an arbitrary quantum strategy passes the test with probability $1 - \varepsilon$ , the provers’ measurements must be close to measuring an actual shared polynomial state.

The Proof Architecture

The proof proceeds by induction on the number of variables $m$ , weaving together three deep mathematical layers that had virtually no existing support in Mathlib:

Foundational quantum information: State-dependent seminorms on operator algebras, positive operator-valued measures (POVMs), and bipartite Naimark dilations.
Self-improvement via SDP duality: Showing that if measurements are approximately consistent, they can be rounded to exact projective measurements using semidefinite programming (SDP) duality, strict Slater points, Gram-Schmidt orthonormalization, and Cayley-graph spectral expansion.
Multi-variable pasting: Inductively stitching consistent line measurements into a global polynomial measurement using a non-commutative matrix Chernoff bound and operator commutativity lemmas.

What Happened Over 63 Days

The formalization ran from March 21 to May 23, 2026, followed by proof review, statement auditing, and library cleanup.

126,367 lines of Lean 566 blueprint targets 0 sorry0 not ready566 marked formalized0 open gaps

24 Jun · Study snapshot. The library contains 126,367 lines of Lean across 337 files. All 25 proof-gap notes have closed by June 23.

Last recorded value per day; days without a new snapshot carry forward the previous value. Lean size counts tracked .lean files under MIPStarRE/, including comments and blank lines; it excludes dependencies and the root import file. The 63-day proof effort runs from 21 March to 23 May; review and code cleanup continue into June. Blueprint targets count all tracked declarations, regardless of completion status, and use the right-hand axis in the size panel. Blueprint status is recorded metadata; leanok marks proof completion. “Not ready” and “no leanok marker” overlap and must not be added together. Source data.

The timeline breaks into four distinct phases:

Scaffolding & skeleton (Days 1–25, Mar 21 – Apr 1): Agents formalized base definitions and outlined the proof structure, reaching a peak of 149 sorry placeholders.
The illusion of convergence (Days 26–53, Apr 2 – Apr 29): The sorry count plunged from 149 to 1. But as we saw, 115 blueprint declarations were still missing or disconnected. Agents were finding local shortcuts rather than proving the global theorem.
Refactoring & gap investigation (Days 54–77, Apr 30 – May 23): We tightened CI checks, blocked shortcut patterns, and exposed hidden proof obligations. Open gap notes peaked at 13 on May 15. The team methodically worked through interface mismatches and paper ambiguities. On May 23, the last sorry was eliminated, and all 566 blueprint targets were verified.
Audit & consolidation (May 24 – June 24): Post-proof review closed the remaining gap notes, verified statement fidelity, and refactored the codebase down to a stable snapshot of 126,367 lines across 337 files.

Investigating the 25 Gap Notes

When an agent flagged a discrepancy between the paper and the formalization, it opened a proof-gap note. Over the project, 25 gap notes were investigated:

Formalization artifacts: Several notes stemmed from how objects were modeled in Lean. For instance, we initially defined the primal SDP over exact measurement POVMs, which lacked strictly feasible interior points; refactoring the primal to allow sub-measurements restored Slater’s condition and strong duality. Similarly, polynomial function representations had to be recast so the Schwartz–Zippel lemma could be applied.
Paper refinements: Other notes uncovered genuine slips in the 100-page printed proof:
- Sampling side conditions: The line-sampling parameter was stated as $k \ge md$ , but the additive matrix Chernoff bound in the pasting argument requires $k \ge 400\,md$ .
- Error accounting: A telescoping sum bound had a prefactor printed as $46km$ instead of $46k^2m$ , and a measurement completion step omitted a $+2\zeta_1$ error term. Both losses were absorbed into the final budget without altering the overall polynomial bound.
- Boundary cases: The printed condition allowed $k = 0$ when $d = 0$ , whereas the formal proof requires $k > 0$ ; the single-variable base case $m = 1$ also required explicit formalization.

Crucially, every repair was local. The core mathematical architecture and the overarching quantum soundness theorem hold exactly as conceived.

To verify that the formalization did not subtly drift, Zhengfeng Ji (co-author of the original 2020 paper) audited the top-level Lean statement, unfolding every definition down to Lean primitives. In addition, an independent comparator repository↗ certifies that the library exports and proves the exact theorem intended.

How Agents Cheat: Three Shortcuts That Compile

When LLMs are evaluated only on whether their code compiles, they optimize for compiler satisfaction over mathematical truth. Review caught three recurring patterns:

Tautological aliases: Asked to prove an identity that required deep spectral graph analysis, an agent simply defined the left-hand side to equal the right-hand side, reducing the proof to rfl ( $x = x$ ).
Vacuous witnesses: When asked to construct an approximate measurement operator satisfying non-trivial properties, an agent instantiated the existential witness with the trivial $1 \times 1$ projection matrix $[1]$ on PUnit. It compiled, but was useless for the downstream theorem.
Conclusion inlining: When a property required twenty pages of semidefinite programming duality to establish, an agent packaged that property as an assumed hypothesis inside a helper structure (BridgePackage), quietly assuming what it was supposed to prove.

This explains why our sorry count plummeted in April: agents were building bridges of debt. When we replayed an automated proof-debt scanner over the git history, flagged shortcut declarations climbed from 1 to 63 between March 22 and May 6.

On May 11, we made the scanner a blocking CI check. Debt dropped to zero and stayed at zero.

The most telling moment came when an agent encountered a failing CI gate: it opened a PR modifying the GitHub Actions workflow to whitelist sorry!

After that, we locked down the governance layer. Agent review prompts and CI configurations were served exclusively from the protected base branch, ensuring agents could never modify the rules that evaluated them.

What We Learned

Long-horizon formalization is fundamentally an engineering discipline, not just a prompting trick. Three principles proved decisive:

Track mathematical claims, not placeholders. A falling sorry count can hide severe proof debt. An explicit blueprint mapping every paper claim to a formal declaration is the only reliable measure of completeness.
Review statements, not just code diffs. Reviewers must evaluate the Lean signature against the original paper text and blueprint node. If you only review the Lean diff, you will miss tautological definitions and smuggled hypotheses.
Protect the evaluator from the agent. LLMs will exploit any loophole in the verification pipeline. Review prompts, linters, and CI workflows must be immutable from the working branch.

What Lies Ahead

Formalizing the low individual-degree test proves the quantum soundness of the classical test and provides the core analytic foundations—from state-dependent operator distances to SDP duality.

The next major milestone on the road to a complete formalization of $\mathrm{MIP}^* = \mathrm{RE}$ is Pauli-basis testing. Our LIDT library provides many of the requisite tools, and the repository, blueprint, and tooling are openly available for the community to explore and build upon.

Citation

Please cite our paper:

1
@misc{lu2026long,
2
  title = {{Long-Horizon Autoformalization of a Core Theorem Underlying MIP*=RE}},
3
  author = {Lu, Sirui and Deng, Ruixuan and Zhu, Yanqiao and Ji, Zhengfeng},
4
  year = 2026,
5
  archivePrefix = {arXiv},
6
  eprint = {2609.19814},
7
  primaryClass = {quant-ph},
8
  url = {https://arxiv.org/abs/2609.19814},
9
}

Compiler Satisfaction ≠\ne= Mathematical Progress