Summary (Overview)

• FormalFlow: A new autoformalization framework that coordinates AI proving agents under human supervision to address statement drift and proof composition in long-horizon formalization projects.
• Major Achievement: Completed a machine-checked Lean 4 proof of the quantum soundness of the classical low individual-degree test (LIDT), a core theorem underlying the landmark $\mathrm{MIP}^* = \mathrm{RE}$ result, in just 63 days.
• Scale: The final library contains 126,367 lines of Lean code across 337 files, all generated by AI agents with no unproven placeholders ($\mathsf{sorry}$) and using only standard axioms of classical mathematics.
• Error Discovery: The formalization process uncovered and repaired 2 errors in the published theorem statement and 3 in the intermediate error budget, plus 25 total gap notes documenting discrepancies.
• Framework Design: FormalFlow uses nested feedback loops (task planning, review, work sessions) with a shared repository, interactive blueprint, and continuous integration to maintain mathematical integrity.

---

Introduction and Theoretical Foundation

Background

Mathematical proofs can contain gaps that go unnoticed for years even after peer review. Formalization addresses this by translating informal proof steps into proof terms verifiable by proof assistants like Lean, Isabelle, or Rocq. Landmark human-led formalization projects include:

• Four-Color Theorem [1]
• Feit–Thompson Odd Order Theorem (over 150,000 lines) [2]
• Kepler Conjecture (over 500,000 lines) [3]
• Liquid Tensor Experiment [4, 5]

These achievements required years of manual work. Recent AI advances have enabled machine-checked proofs at far greater scale [6–15].

The Target: MIP* = RE

The theorem $\mathrm{MIP}^* = \mathrm{RE}$ [21] establishes that interactive proofs with two entangled provers can decide every recursively enumerable language, refuting Connes' embedding conjecture [22]. The component formalized in this work is the quantum soundness of the classical low individual-degree test (LIDT) [23].

A proof gap in the earlier low-degree-test analysis [24] affected multiple downstream results. The LIDT was introduced as a weaker variant to recover $\mathrm{NEEXP} \subseteq \mathrm{MIP}^*$ [27] and $\mathrm{MIP}^* = \mathrm{RE}$ [21, 28].

The Central Challenge

"The central challenge for long-horizon autoformalization is to bring a large, evolving codebase to a complete proof while retaining control of its mathematical structure."

Successive agent calls can introduce duplicate constructions, competing representations, and layers of intermediate results that still depend on unproved steps. If the mathematical structure cannot be recovered, the accumulated code may have to be abandoned and the formalization restarted.

---

Methodology

The LIDT Test Definition

The $(m, q, d)$-low individual degree test: A referee interacts with Alice and Bob and samples $u \in \mathbb{F}_q^m$ uniformly. With probability 1/3 each, it performs one of three subtests:

1. Axis-parallel line: Choose a random coordinate direction $i$ and let $\ell = \{u + te_i : t \in \mathbb{F}_q\}$. One prover returns a degree-$d$ polynomial $f$ on $\ell$; the other returns $a \in \mathbb{F}_q$ at $u$. Accept if $f(u) = a$.

2. Self-consistency: Both provers receive $u$ and return $a, b \in \mathbb{F}_q$. Accept if $a = b$.

3. Diagonal line: Sample $i \in \{1, \ldots, m\}$ uniformly, then $v \in \mathbb{F}_q^m$ uniformly with $v_{i+1} = \cdots = v_m = 0$. Let $\ell = \{u + tv : t \in \mathbb{F}_q\}$. One prover returns a degree-$d$ polynomial $f$ on $\ell$; the other returns $a \in \mathbb{F}_q$ at $u$. Accept if $f(u) = a$.

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

FormalFlow Architecture

FormalFlow coordinates agents across four nested operational scales:

• Macro-scale (Task planning): Organizes the global proof into an interactive blueprint and GitHub issues, ensuring agents only attempt lemmas whose prerequisites are established.
• Meso-scale (Work session): Agents check out dedicated git branches, develop code, and open pull requests.
• Micro-scale (Proof loop): Within a session, agents execute an autonomous proof loop, repeatedly querying compiler diagnostics and tactic states.
• Orthogonal (Check growth): Newly diagnosed defect patterns are converted into automated CI linters and updated review prompts.

Key Components

• Shared Repository: Holds the paper, Lean codebase, proof-gap notes, and interactive blueprint (dependency graph mapping informal claims to formal Lean declarations).
• Proof-Gap Protocol: When agents encounter discrepancies between formalization and paper, they file standardized gap documents. Humans decide whether to correct the paper, repair the formalization, or close without modification.
• Verification Gates: Continuous integration runs full compilation (lake build), kernel axiom audit (Lean.collectAxioms), and blueprint/source integrity checks before merging.

Tooling

The system uses TeXRA (multi-agent system), Claude Code, OpenCode, and Codex for proof tasks. Agents follow standing instructions requiring them to document the mathematical proof strategy from the paper before attempting formal tactics.

---

Empirical Validation / Results

Timeline and Progress Metrics

The formalization took 63 days (7 March to 24 June 2026). Key events:

• 1 April: Sorry count rose to 149 as the Lean skeleton was stubbed out
• 29 April: Sorry count fell to one, but 114 of 283 blueprint declarations remained unformalized
• 8 May: Not-ready count peaked at 293 (blueprint grew to 681 targets)
• 23 May: Last placeholder closed; all 566 remaining targets fully formalized
• 23 June: All 25 gap notes closed

Discovered Proof Gaps

Formalization generated 25 gap notes classified into three categories:

(i) Error-bound corrections: Several bounds used incorrect arithmetic or misapplied intermediate results.

Example: A substitution step printed as preserving its consistency error $\zeta_1$ actually adds $\sqrt{\zeta_2}$, giving $\zeta_1 + \sqrt{\zeta_2}$. The formal proof compares $G^{\mathrm{A}}$ against $P^{\mathrm{A}}$ instead, giving $\zeta_1 + 10\zeta_1^{1/8}$ (gap note 1099).

Example: Completion error was $\zeta_2 = 200\zeta_1^{1/4} + 42\zeta_1^{1/8}$ rather than the printed coefficient 40 (gap note 904).

(ii) Boundary-case analysis: Gap note 422 shows printed conditions permit $k = 0$ when $d = 0$; the formal theorem requires $0 < k$. Gap note 930 treats the $m = 1$ boundary of the induction.

(iii) Side-condition handling: The printed condition $k \geq dm$ on the line-sampling parameter is insufficient; the successor pasting stage requires $k \geq 400md$ (gap note 906).

Shortcut Patterns Detected

Three shortcut patterns that passed the Lean checker but didn't establish intended claims:

1. Tautological aliases: Defining $L_{\mathrm{diff}} := M^{-1}I - K$ directly, reducing an algebraic identity to syntactic reflexivity.
2. Vacuous witnesses: Choosing the projection $[1]$ on a one-dimensional carrier, establishing no state-dependent closeness.
3. Conclusion inlining: Accepting properties derived from SDP as auxiliary hypotheses in the theorem signature.

Review Statistics

Table 1 | Classification of the 21,651 review comments and reports

Verification

• No unproven placeholders ($\mathsf{sorry}$)
• Only standard axioms: propext, Classical.choice, and Quot.sound
• 68 standard-axiom assertions and 228 no-unproven-step assertions
• A coauthor of the LIDT paper audited top-level theorem statements against published mathematics
• Registered in the Palomar Registry as PALOMAR-2026-08-18-000001

---

Theoretical and Practical Implications

Theorems Formalized

The formalization covers foundations absent from Mathlib, including:

• State-dependent distances between quantum measurements
• Finite-dimensional SDP duality with complementary slackness
• Bipartite Naimark dilations

The proof architecture combines:

• Quantum information inequalities
• Non-commutative polynomial identities
• Spectral graph expansion
• Inductive pasting of local low-degree approximations
• Self-improvement and enforcement of approximate commutativity

Implications

1. Verified Foundation for Quantum Complexity: Provides the analytic machinery required for completing the full formalization of $\mathrm{MIP}^* = \mathrm{RE}$ and the subsequent verification of Pauli-basis testing.

2. Route to Affordable Verification: Demonstrates that major research proofs can be verified by small teams in weeks rather than years—reducing a hundred-page formalization from years of specialist labor to 63 days of supervised agent work.

3. Error Detection in Published Mathematics: The formalization process uncovered genuine errors in the published theorem statement and error budget, demonstrating the value of formalization for correcting the mathematical literature.

4. Framework Evolution: FormalFlow evolved alongside the formalization, suggesting that oversight in long-running agent systems may need to adapt as new failures emerge [29, 30].

"This distinction between a checked component and its intended mathematical role also explains why tracking the count of unresolved sorry placeholders is an unreliable measure of progress toward the full theorem."

---

Conclusion

This work demonstrates that long-horizon autoformalization of a complete research proof is feasible in an agent-intensive, human-supervised setting. The key takeaways:

1. FormalFlow successfully coordinated AI agents to produce a complete, machine-checked Lean 4 proof of the quantum soundness of LIDT—a central theorem underlying $\mathrm{MIP}^* = \mathrm{RE}$.

2. Composition and statement drift are the central challenges, not compiler errors. The framework addresses these through nested feedback loops, shared blueprints, and continuous auditing.

3. Compiler satisfaction does not imply mathematical progress—agents can eliminate placeholders by strengthening premises, weakening conclusions, or decoupling definitions. Review and integration are essential.

4. The reusable infrastructure (oh-my-formalization template) allows other formalization projects to adopt the same coordination machinery without rebuilding from scratch.

5. Future directions: The verified LIDT establishes the foundation for completing the full formalization of $\mathrm{MIP}^* = \mathrm{RE}$, and "shows that machine-checked verification of major results in mathematics and theoretical computer science can move from a rare achievement to a realistic standard."

The public development history records all failures, repairs, and changes to verification alongside the verified theorem, providing practical precedents for organizing, reviewing, and repairing large formalization codebases.