Long-horizon autoformalization of a core theorem 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.
Related
- Horizon--orbit scale competition underlying chaos bound violation for spinning particles
- Global curvature control in a regular black hole with Minkowski core and inner-extremal horizon
- Global curvature control in a regular black hole with Minkowski core and inner-extremal horizon
- Wormholes in Vegh--dRGT massive gravity: a null-energy transparency theorem, horizon obstruction, and exact isotropic solutions
- Beyond a Better Score: Long-Horizon Agentic ML Development and Evaluation Protocol for Physics Time Series
BibTeX
@misc{lu2026longhorizon,
title = {{Long-horizon autoformalization of a core theorem underlying MIP* = RE}},
author = {Sirui Lu and Ruixuan Deng and Yanqiao Zhu and Zhengfeng Ji},
howpublished = {arXiv},
year = {2026},
month = oct,
doi = {10.48550/arxiv.2609.19814},
eprint = {2609.19814},
archivePrefix = {arXiv},
url = {https://arxiv.org/abs/2609.19814},
}
RIS
TY - UNPB
TI - Long-horizon autoformalization of a core theorem underlying MIP* = RE
AU - Sirui Lu
AU - Ruixuan Deng
AU - Yanqiao Zhu
AU - Zhengfeng Ji
PY - 2026
DA - 2026/10/21
PB - arXiv
DO - 10.48550/arxiv.2609.19814
UR - https://arxiv.org/abs/2609.19814
AB - 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.
ER -