FormalFlow 用 AI 智能体完成 MIP*=RE 核心定理形式化

AI 智能体在人工监督下 63 天完成 MIP*=RE 核心定理的 Lean 4 形式化。

资讯摘要

论文提出 FormalFlow，在人工监督下协调 AI 证明智能体，用共享蓝图引导嵌套的规划、证明与审查循环，以应对长周期形式化中的陈述漂移与证明组合问题。作者报告用该系统在 63 天内完成经典低个体度测试量子可靠性定理的 Lean 4 机器验证证明，该定理是 MIP* = RE 的核心基础。最终库含 126,367 行 Lean 代码，全部由智能体生成。

要点速读

1. FormalFlow 以共享蓝图组织嵌套的规划、证明和审查循环，并引入软件工程实践。
2. 作者报告 63 天完成该定理的 Lean 4 机器验证证明，库共 126,367 行 Lean 代码，均由智能体生成。
3. 形式化过程修正了已发表证明中的边条件与中间误差界，并改进了主定理的误差指数。

中文摘要由 AI 根据公开来源生成，可能存在理解偏差；具体能力、数字、开放时间等信息请以原文为准。
采集于 2026/10/23 08:00:11（北京时间）。 arXiv 日期为本次公告时间，论文初次投稿日期请查看原文版本记录。