Long-horizon autoformalization of a core theorem underlying MIP* = RE
Sirui Lu, Ruixuan Deng, Yanqiao Zhu and Zhengfeng Ji present FormalFlow, which coordinates AI proving agents under human supervision, and use it to complete a machine-checked Lean 4 proof of the quantum soundness of the classical low individual-degree test, a core theorem underlying MIP* = RE.
Ask this paper
126,367 lines of Lean, all agent-generated. The completed library is the deliverable, and the proof was developed in 63 days where comparable landmark formalizations have taken specialist teams years.
A shared blueprint controls statement drift. Nested planning, proving and review loops read from one blueprint, which is how the system keeps intermediate statements consistent across a formalization long enough to outlast any single session.
The formalization corrected the source. Side conditions and intermediate errors in the published proof were fixed while the final error bound was preserved under the corrected assumptions.
Software engineering practice is the organising idea. Verification and review are strengthened by agents throughout rather than applied at the end, which is what makes cross-module composition of the inductive proof tractable.
The claim is about cost. The result is presented as a route to affordable verification of major research proofs by small teams, not as a fully autonomous proving system.
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.