AI system completes complex quantum math proof in two months
Long-horizon autoformalization of a core theorem underlying MIP* = RE
Artificial IntelligenceLogic in Computer Science
Summary
Long and complex math proofs often take years and many experts to finish. The authors created a system called FormalFlow that uses AI helpers working under human guidance to break down big proofs into smaller tasks. This system successfully completed a very important quantum math proof in 63 days, producing a large, verified code library. Their work corrects some previous errors while keeping the main result intact, showing that smaller teams can reliably check big math proofs with AI help.
What this means in practice
- •For formal methods teams: Coordinate AI agents to automate long, complex proof formalizations under human oversight, speeding verification of critical mathematical results.
- •For complexity theory software developers: Use FormalFlow to build and verify libraries formalizing key theorems in quantum complexity, ensuring correctness of foundational proofs for new algorithms.
Authors
Sirui Lu, Ruixuan Deng, Yanqiao Zhu, Zhengfeng Ji
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.