Long-horizon autoformalization of a core theorem underlying MIP* = RE
Sirui Lu, Ruixuan Deng, Yanqiao Zhu, Zhengfeng Ji
quant-ph
Sep 17, 2026 · v3
cs.AI cs.LO
TL;DR
AI agents under human supervision produced 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. Using FormalFlow, 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, in 63 days. The final library contains 126,367 lines of Lean code, all generated by agents. Beyond providing a verified foundation for quantum complexity, the formalization corrects side conditions and intermediate error bounds in the published proof and improves the error exponent of the main theorem. The development record shows what it takes to trust proofs written by AI agents and provides reusable tools for verifying research mathematics at scale.
Problem
Long-horizon formalizations of research mathematics run into composition failures and statement drift when many AI agents with limited context contribute code. The target result, quantum soundness of the classical low individual-degree test central to MIP* = RE, had never been formalized.
Approach
FormalFlow coordinates proving agents through a shared GitHub repository, continuous integration, code review, and an interactive blueprint that links each Lean declaration to a claim in the paper. Nested planning, proving, and review loops are combined with audits and validity gates that check for weakened statements and unproved obligations. Foundations missing from Mathlib were formalized, including SDP duality with complementary slackness, bipartite Naimark dilations, and state-dependent distances between measurements.
Results
A complete machine-checked Lean 4 proof was finished in 63 days: 126,367 agent-generated lines across 337 files, registered in the Palomar Registry. The formalization corrected side conditions and intermediate error bounds in the published proof and improved the main theorem's error exponent. The reusable infrastructure was released as the oh-my-formalization template.
