arXiv cs.AI· Sirui Lu, Ruixuan Deng, Yanqiao Zhu, Zhengfeng Ji·· 12 小时前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 代码，全部由智能体生成；形式化过程还修正了已发表证明中的边条件和中间误差界，并改进了主定理的误差指数。
正文 · AI 翻译
摘要：里程碑式的数学形式化工作曾需要专家团队花费数年才能完成。我们提出 FormalFlow，一个在人类监督下协调 AI 证明智能体的系统，用于应对长周期形式化中的陈述漂移与证明组合问题。借鉴软件工程的原则与实践，它使用共享蓝图来指导嵌套的规划、证明与审查循环。借助 FormalFlow，我们在 63 天内完成了经典低个体度检验量子可靠性（MIP* = RE 背后的核心定理）的机器校验 Lean 4 证明。最终库包含 126,367 行 Lean 代码，全部由智能体生成。除为量子复杂性提供经过验证的基础外，该形式化还纠正了已发表证明中的附带条件与中间误差界，并改进了主定理的误差指数。开发记录展示了信任 AI 智能体所写证明需要什么，并为大规模验证研究数学提供了可复用工具。
| 注释： | 74 页。正文 13 页，含 4 幅图和 1 张表，其后为补充附录（59 页、9 幅图、17 张表）及参考文献。Lean 4 库：此 https URL |
| 主题： | 量子物理（quant-ph）；人工智能（cs.AI）；计算机科学中的逻辑（cs.LO） |
| MSC 分类： | 68V20, 68V15, 81P68, 68Q15 |
| 引用为： | arXiv:2609.19814 [quant-ph] |
| （或本版本使用 arXiv:2609.19814v3 [quant-ph]） | |
| https://doi.org/10.48550/arXiv.2609.19814 由 DataCite 颁发的 arXiv DOI |
提交历史
来自：Ruixuan Deng [查看邮箱]
[v1]
2026 年 9 月 17 日星期四 07:26:49 UTC（2,231 KB）
[v2]
2026 年 9 月 24 日星期四 02:56:53 UTC（2,232 KB）
[v3]
2026 年 10 月 21 日星期三 15:48:01 UTC（2,239 KB）
来源：arXiv cs.AI · arxiv.org