Google DeepMind 登《科学》：Lean 形式化证明 Agent 解决 353 道开放 Erdős 问题中的 9 道、证明 44 条 OEIS 猜想，最简单的「生成+验证」循环也能复现

这件事意味着什么

【要点】

10 月 8 日出版的《科学》（Science 第 394 卷第 6820 期，234–239 页）刊登了 Google DeepMind 的论文《用 AI 驱动的形式化证明搜索推进数学研究》。作者共 20 位，除一位来自丹麦奥胡斯大学数学系、一位来自 Google 外，其余都在 Google DeepMind，包括 Thomas Hubert、Matej Balog、Aja Huang 和 Pushmeet Kohli。

团队做了一个形式化证明搜索 Agent：大模型负责写 Lean 证明，Lean 编译器逐步检查每一步推理，不通过就把报错反馈回去重试。按论文摘要，这个 Agent 自主解决了 353 道开放 Erdős 问题中的 9 道，证明了整数数列百科（OEIS）492 条开放猜想中的 44 条，目前已用于组合、优化、图论、代数几何和量子光学等方向的研究。

论文还做了一个对照：只让大模型生成、再交给 Lean 验证、如此反复的「基础版」Agent，也复现了这 9 道 Erdős 问题的解法。

【可核验】

论文 DOI 为 10.1126/science.aej2213，Crossref 元数据显示出版日期 2026 年 10 月 8 日，作者单位可在元数据中逐一核对。9/353 和 44/492 两组数字、「基础版 Agent 复现 Erdős 结果」这一点都写在摘要里。Lean 证明的价值在于任何人都能重新编译检验，不必只信作者的说法。

【我们的判断】

把它和本周 OpenAI 的 722 篇数学稿放在一起看最清楚。OpenAI 那批是自然语言证明，两天内就因一处符号错误撤回 3 篇、修订 14 篇；DeepMind 这篇的每个证明都由机器逐行检验过，量小得多，但「对不对」不再靠人审。我们认为，AI 数学接下来比的不是谁产出更多，而是谁的结果能被机器核验。

基础版 Agent 也能复现，说明进步主要来自底层模型和可靠验证器的组合，而不是外面那层复杂的搜索框架。这和上周 Apple 与 EPFL 那篇「极简编程 Agent 追平复杂框架」的结论方向一致。

也要看清边界：353 道里解出 9 道，成功率约 2.5%，说明大多数开放问题仍然够不着；Lean 只能保证证明与形式化陈述一致，陈述本身是否忠实于原问题，仍要数学家把关。