arXiv 量子物理· Sirui Lu, Ruixuan Deng, Yanqiao Zhu, Zhengfeng Ji·· 2 小时前精选AI 评分78
FormalFlow 用 AI 智能体在 63 天内完成 MIP* = RE 核心定理的 Lean 4 形式化
Long-horizon autoformalization of a core theorem underlying MIP* = RE
AI 导读
研究团队提出 FormalFlow 系统，在人类监督下协调 AI 证明智能体，用 63 天完成了经典低个体度测试量子可靠性定理的 Lean 4 机器验证证明，该定理是 MIP* = RE 的核心基础。最终代码库包含 126,367 行 Lean 代码，全部由智能体生成。形式化过程还修正了已发表证明中的边条件和中间误差界，并改进了主定理的误差指数。
推荐理由
材料给出 FormalFlow 在 63 天内完成 Lean 4 形式化的过程记录，可供评估 AI 智能体参与长周期数学证明的可信度。
来源：arXiv 量子物理 · arxiv.org