AlphaProof Nexus：用 Lean 证明开放的 Erdős 问题和 OEIS 猜想

Google DeepMind 的 AlphaProof Nexus 自主证明了 353 个开放 Erdős 问题中的 9 个（其中几个是变体或部分）以及 492 个 OEIS 猜想中的 44 个，全部经过 Lean 检验；相关论文于 2026 年 10 月发表在 Science 上。

问题
AI 系统能否自主为开放的研究问题找到形式化证明？
贡献方
AlphaProof Nexus（Google DeepMind） · 基于 Gemini、搜索 Lean 证明的智能体
验证
Lean 4 证明，构建方法公开发表于 Science（2026-10-08）
时间线
arXiv 2605.22763（2026-05-21）→ Science（2026-10-08）
来源
论文（arXiv:2605.22763）结果仓库专家评论（西班牙科学媒体中心）
完整解Lean 检验 · 同行评审（Science）

问题

AI 在数学上的大多数成果给出的是非形式化证明，需要人去检查。Google DeepMind 的 AlphaProof Nexus 直接在 Lean 证明助手中搜索证明，因此一个结果要么经过机器检验，要么根本不会产生。

AI 做了什么

论文（Tsoukalas 等，arXiv:2605.22763，2026 年 5 月；2026 年 10 月 8 日发表于 Science）报告说，该系统在所尝试的问题中自主证明了 353 个开放 Erdős 问题中的 9 个和 492 个 OEIS 猜想中的 44 个，每个问题的成本为几百美元。公开仓库中的 Erdős 结果包括：#12（第 i、ii 部分）、#125（正下密度的变体）、#138（一个变体）、#152、#26（一个变体）、#741（第 i、ii 部分）和 #846。论文还报告了与数学家合作得到的结果。这些 Erdős 问题在本站也各有一条依据 Tao 的 Wiki 整理的记录。

如何验证

每个证明都能在 Lean 4 中编译通过，构建方法也已公开。论文中的自然语言证明是人根据 Lean 证明写出的。

局限

其中几个 Erdős 结果是问题的变体或某一部分，不一定是原问题本身。Lean 只能证明形式化后的陈述，如果陈述翻译有误就不会被发现；Josep Curto（加泰罗尼亚开放大学）指出了这一点，还提到了"方法上的不一致"。也有人质疑其中一些问题是否真的是开放的。成功率不高，约为所尝试 Erdős 问题的 2.5%。

∎