arXiv cs.AI· Sirui Lu, Ruixuan Deng, Yanqiao Zhu, Zhengfeng Ji·2026-10-23 12:00· 2 小时前精选AI 评分68

FormalFlow 用 AI 智能体 63 天完成 MIP* = RE 核心定理的 Lean 4 形式化

Long-horizon autoformalization of a core theorem underlying MIP* = RE

AI 导读

作者团队提出 FormalFlow 系统，在人类监督下协调 AI 证明智能体，用共享蓝图指导嵌套的规划、证明和审查循环，应对长期形式化中的陈述漂移和证明组合问题。

推荐理由

原文报告了用 AI 智能体协作完成的长期数学形式化成果，还修正了已发表证明并改进误差指数，读者可了解可信 AI 证明的实践路径。