Long-horizon autoformalization of a core theorem underlying MIP* = RE
Sirui Lu, Ruixuan Deng, Yanqiao Zhu, Zhengfeng Ji
quant-ph
Sep 17, 2026 · v1
cs.AI cs.LO
TL;DR
A multi-agent AI system, FormalFlow, generated a 126,367-line Lean 4 proof of the quantum soundness of the low individual-degree test underlying MIP*=RE.
Abstract
Landmark mathematical formalizations have taken specialist teams years to complete. We present FormalFlow, a system that coordinates AI proving agents under human supervision to address statement drift and proof composition in long-horizon formalization. Drawing on software engineering principles and practices, it uses a shared blueprint to guide nested planning, proving and review loops. Agents strengthen verification and review throughout formalization. We completed a machine-checked Lean 4 proof of the quantum soundness of the classical low individual-degree test, a core theorem underlying MIP* = RE. Developing the proof took 63 days; greater parallelism could further reduce this time. The final library contains 126,367 lines of Lean code, all generated by agents. The formalization corrects side conditions and intermediate errors while preserving the published final error bound under corrected assumptions. This work provides a verified foundation for quantum complexity and demonstrates a route to affordable verification of major research proofs by small teams.
Problem
Long-horizon formalization of research-level proofs is expensive and prone to statement drift and composition failures as an evolving codebase grows. Formalizing the quantum soundness of the low individual-degree test, a core theorem underlying MIP*=RE, requires coordinating thousands of interdependent lemmas.
Approach
FormalFlow coordinates AI proving agents under human supervision using a shared GitHub repository, continuous integration, and code review. It employs an interactive blueprint linking Lean declarations to paper claims across four nested operational scales of planning, proving, and review. Agents track error propagation and maintain compatible definitions, assumptions, and bounds while comparing intermediate declarations against the blueprint and paper.
Results
A machine-checked Lean 4 proof of the quantum soundness theorem was completed in 63 days, producing 126,367 lines of Lean code entirely generated by agents. The formalization corrected two side conditions and intermediate errors while preserving the published error bound, and reusable tooling was distilled into an open template.
