arXiv cs.AI· Sirui Lu, Ruixuan Deng, Yanqiao Zhu, Zhengfeng Ji·· 13 小时前AI 评分64
FormalFlow 用 AI 智能体在 63 天内完成 MIP* = RE 核心定理的 Lean 4 形式化
Long-horizon autoformalization of a core theorem underlying MIP* = RE
AI 导读
研究团队提出 FormalFlow 系统，在人类监督下协调 AI 证明智能体完成长周期形式化，用 63 天完成了 MIP* = RE 背后核心定理即经典低个体度测试量子可靠性的 Lean 4 机器验证证明。最终库包含 126,367 行 Lean 代码，全部由智能体生成；形式化过程还修正了已发表证明中的边条件和中间误差界，并改进了主定理的误差指数。
正文 · 原文
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.
| Comments: | 74 pages. Main text 13 pages with 4 figures and 1 table, followed by supplementary appendices (59 pages, 9 figures, 17 tables) and references. Lean 4 library: this https URL |
| Subjects: | Quantum Physics (quant-ph); Artificial Intelligence (cs.AI); Logic in Computer Science (cs.LO) |
| MSC classes: | 68V20, 68V15, 81P68, 68Q15 |
| Cite as: | arXiv:2609.19814 [quant-ph] |
| (or arXiv:2609.19814v3 [quant-ph] for this version) | |
| https://doi.org/10.48550/arXiv.2609.19814 arXiv-issued DOI via DataCite |
Submission history
From: Ruixuan Deng [view email]
[v1]
Thu, 17 Sep 2026 07:26:49 UTC (2,231 KB)
[v2]
Thu, 24 Sep 2026 02:56:53 UTC (2,232 KB)
[v3]
Wed, 21 Oct 2026 15:48:01 UTC (2,239 KB)
来源：arXiv cs.AI · arxiv.org