AI and the World's Hard Problems · Theoretical computer science · arXiv · 2026-10-22
Long-horizon autoformalization of a core theorem underlying MIP* = RE
The authors present FormalFlow, a system that coordinates AI proving agents under human supervision to address statement drift and proof composition in long-horizon formalization, using a shared blueprint to guide nested planning, proving, and review loops. With it, they 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, with a final library of 126,367 lines of agent-generated Lean code. The formalization corrects side conditions and intermediate error bounds in the published proof and improves the error exponent of the main theorem, and the development record provides reusable tools for verifying research mathematics at scale.