谷歌DeepMind最近搞了个大动作——AlphaProof Nexus，一个由Gemini驱动的形式化证明框架，一口气解决了9道悬而未决的埃尔德什（Erdős）数学开放问题，其中最老的已经被卡了56年。与此同时，它还顺手证明了在线整数序列百科（OEIS）里44个未解猜想。
不是”AI猜答案”，而是”机器可验证的证明”
这次和以前那些”AI做数学题”的新闻不太一样。AlphaProof Nexus 的核心是把大语言模型（LLM）和 Lean 形式化验证工具绑在一起——LLM负责生成证明思路，Lean 负责严格校验每一步逻辑是否真的成立。
这样做的好处是：证明不是”看起来对”，而是”机器严格验证过对”。传统数学界对AI生成证明最大的质疑就是”你咋知道它没在胡说”，Lean 验证正好堵住了这个漏洞。
关键突破：单次推理成本仅数百美元，论文与代码已在 GitHub 开源（arXiv:2605.22763，CC BY-NC-ND 4.0 协议）。
哪些问题被解决了？
这次解决的9道 Erdős 问题横跨组合数学和图论，其中两个最引人注目的问题已经被卡了56年。完整列表在论文附录里，这里说几个有意思的：
- Erdős #12：关于整数序列中等差数列密度的猜想，困扰学界超过半个世纪
- Erdős #125：30年无人给出完整证明的图论问题
- Erdős #846：34年悬而未决的组合数学问题
- 其余6道问题同样来自 Erdős 遗留的353道开放问题清单，这次共解决了9道
- 额外证明了 OEIS 百科中44个序列猜想，覆盖组合学、优化、图论、代数几何、量子光学等领域
和 OpenAI 的那次突破有什么区别？
就在前不久，OpenAI 宣布他们的 AI 推翻了一个有80年历史的 Erdős 猜想。两边都在做”AI+数学证明”，但路径不太一样：
OpenAI 那次更多依赖强化学习驱动的推理，而 DeepMind 这次走的是”LLM生成 + Lean 形式化验证”的路线，两种路径各有优劣。形式化验证的好处是证明可以被机器完整检查，数学界更容易接受。
目前 AlphaProof Nexus 还不能解决那些需要全新数学构造的问题——它强在”验证了，不是”从无到有发明了新数学”。这个界限，也是整个领域下一步要攻克的。
这个方向意味着什么？
以前数学家要验证一篇论文的证明是否正确，往往要花数周甚至数月。如果 AI 能快速生成”机器可验证”的证明草稿，数学研究的速度会被整个提起来。
当然，现在说”AI 取代数学家”还早得很。目前系统能处理的是”已经被明确表述出来的数学问题”，那些需要人类直觉去”发现正确的问题”的部分，AI 还差得很远。但作为一个”超级研究助手”，它已经很能打了。