AI 攻破数学圣殿：AlphaProof Nexus 一夜解决 9 道人类 56 年未解难题

9 道题。56 年。几百美元。

把这三个数字放在一起，你会觉得哪个最不可思议？

2026 年 5 月 21 日，Google DeepMind 发表了一篇预印本论文。标题很学术，内容很炸裂——他们的 AI 系统 AlphaProof Nexus，自主解决了 9 道埃尔德什（Erdős）开放问题。这些问题中最古老的那个，从 1970 年提出至今，整整悬了 56 年，全世界最聪明的数学家都没搞定。

而 AI 花了多少钱？每道题的算力成本只有几百美元。

还不够震撼？它还顺手证明了 OEIS（整数序列百科）里的 44 个猜想、搞定了一道搁置 15 年的代数几何难题、改进了凸优化领域一个沿用已久的理论边界。

更反直觉的是——DeepMind CEO Demis Hassabis 第一时间跑出来降温："这还不是 AGI。"

等等，解了 56 年没人解开的数学题，还不算通用智能？那什么才算？

答案藏在 AlphaProof Nexus 的工作方式里。读完你会发现，这个 AI 最厉害的地方，恰恰是它最"笨"的地方。

---

埃尔德什是谁？为什么他的问题值钱？

如果数学界有一个人能被称为"出题之王"，那一定是保罗·埃尔德什（Paul Erdős）。

这个匈牙利数学家一辈子发表了超过 1500 篇论文——没写错，一千五百篇。他没有固定住所，拎着一个旧皮箱在全世界数学家的沙发上轮流睡。每到一个地方，他做的第一件事就是：掏出一个问题，拍在桌上，然后说："这题有意思，谁解出来我给钱。"

这不是玩笑。埃尔德什一生悬赏了上百个数学问题，赏金从 25 美元到 10000 美元不等。金额大小取决于他认为这道题有多难——25 美元的是"有点意思"，10000 美元的是"我赌你们这辈子解不出来"。

1996 年他去世后，他的好友、数学家 Ronald Graham 接管了一笔基金，专门用来兑现这些悬赏。到今天，仍有 353 道埃尔德什问题处于"未解决"状态。

打个比方：如果千禧年七大数学难题是武林里的"七大绝世武功秘籍"，那埃尔德什问题就是散布在江湖各处的"悬赏令"——每张看起来都不难懂，但要真正解开，需要的功力一点不少。

为什么这些问题这么难？因为埃尔德什有一种天赋——他能把极其深刻的数学本质，浓缩成一个看起来"小而美"的问题。你以为门槛很低，推开门才发现里面是一片深渊。

比如这次被攻破的 Erdős #12（1970 年提出）：找一个无限的整数集合，满足——任意两个数的和，都不能被集合里的第三个数整除，同时这个集合在自然数中的密度不能为零。

听起来不复杂？全世界的组合数学家试了 56 年。

每道埃尔德什问题，都是数学家的勋章。解出一道，够吹一辈子。

---

AlphaProof Nexus 到底怎么"想"的？

先纠正一个常见误解：AlphaProof Nexus 不是那种"用大白话写一篇证明，看起来头头是道"的 AI。

恰恰相反。它做数学题的方式，更像是一个程序员写代码，而不是一个学生写作文。

怎么理解？你想想，当 ChatGPT 做数学题的时候，它在干什么？它在用自然语言一步步推导，就像写一篇论证文章。问题是，语言模型最大的弱点就是"看起来对但其实错了"——它可能在第 17 步偷偷犯一个逻辑错误，然后自信满满地推出一个错误结论。

AlphaProof Nexus 换了一个思路：别用人话写证明，用代码写。

它把证明写成 Lean——一种形式化证明语言。Lean 有一个编译器，和写代码一模一样：你的证明每一步都必须通过编译。编译器不会被花言巧语忽悠，逻辑错了就是编译报错，没有商量余地。

这套系统的架构分四层，像俄罗斯套娃一样一层比一层强：

Agent A 是最基础的版本：Gemini 3.1 Pro 生成一段 Lean 证明代码 → 编译器检查 → 如果报错，把错误信息喂回给 LLM → LLM 修改后重新提交。就这么来回循环，直到编译通过。

Agent B 在 A 的基础上加了一把"手术刀"——当 LLM 卡在某个子问题上时，调用 AlphaProof（DeepMind 2024 年在 IMO 拿银牌的那个强化学习系统）来定点爆破。

Agent C 引入了"进化搜索"。想象一群 AI 同时在写不同版本的证明草稿，每个草稿会被一个"裁判 AI"（基于 Gemini 3.0 Flash）打分——评估合理性、清晰度、新颖性，然后用 Elo 评分体系排名。高分草稿存活，低分淘汰，像自然选择一样迭代。

Agent D 是全量版，三者融合。用来解那 9 道埃尔德什问题的，正是这个最强组合。

但是——这里有一个让研究人员自己都惊讶的发现。

事后分析显示，最基础的 Agent A，也能解出这 9 道题。只是花的算力更多一些。

这意味着什么？意味着真正的核心不是那些花哨的进化算法和强化学习，而是一个最朴素的循环：LLM 猜 → 编译器验 → 反馈修正 → 再猜。

研究团队在论文里写了一句意味深长的话："随着底层语言模型的快速进步，AI 数学正在从'专门训练的特化系统'转向'简单的 Agent 循环'。"

AlphaProof Nexus 最厉害的地方，不是它有多聪明，而是它不会自欺欺人。编译器通过了，证明就是对的。不通过，就继续改。没有幻觉的空间。

---

几百美元一道题，凭什么这么便宜？

你可能对"几百美元"没有直观感受。让我换一种方式说。

一个数学博士生，从入学到毕业，通常需要 5-7 年。在这期间，如果他能解决一道埃尔德什问题，足以奠定整个学术生涯。这期间他的生活费、学费、导师薪酬，保守估计几十万美元。

而且他大概率解不出来。

AlphaProof Nexus 在几小时内，用了不到一杯奶茶的价格——好吧，大概是一百杯奶茶——搞定了同样的事。

为什么能这么便宜？三个原因。

第一，试错成本趋近于零。人类数学家试一个思路，可能要花几个月推演、写几十页手稿，最后发现这条路走不通。AI 试一个思路，只需要跑一次 Lean 编译——几秒钟出结果。错了？换一个方向再来。它可以在人类喝一杯咖啡的时间里，试完人类一辈子都试不完的方向。

第二，Lean 编译器是免费的裁判。数学证明最贵的环节是什么？验证。一篇顶级数学论文的同行评审可能要半年到一年。而 Lean 编译器的验证是即时的、免费的、绝对可靠的。这把原来最昂贵的环节变成了最廉价的环节。

第三，LLM 的推理成本在暴跌。Gemini 3.1 Pro 的每 token 价格比一年前的模型便宜了一个数量级。当底层模型的成本每半年砍一半，"暴力搜索"就从奢侈品变成了日用品。

有意思的是，这个"便宜"的背后藏着一个更深的洞察。

Agent A 的故事告诉你：解题最贵的不是算力，是方向。当 LLM 能力足够强的时候，你甚至不需要进化算法和强化学习这些"高级武器"——一个简单的"猜-验-改"循环就够了。

过去，最贵的是"算一步"。现在，最贵的是"想到往哪个方向算"。而这恰恰是大语言模型最擅长的事。

---

谷歌 vs OpenAI：AI 数学的两条路线之争

就在 DeepMind 发布 AlphaProof Nexus 的前一周，OpenAI 也搞了一个大新闻：他们的模型推翻了一个 80 年的离散几何核心猜想。

同样是 AI 做数学，两家的路线却截然不同。

OpenAI 的做法是什么？让模型用自然语言写证明。没有 Lean，没有编译器验证。模型需要自己扛住整条逻辑链——从第一步到最后一步，全靠"语感"和"推理能力"。

DeepMind 的做法呢？LLM 只负责"猜方向"，Lean 编译器负责"判对错"。模型可以猜得天马行空，但每一步都必须过编译器这个"铁面判官"。

维度	AlphaProof Nexus（DeepMind）	OpenAI 路线
验证方式	Lean 编译器形式化验证	自然语言推理 + 自洽性检查
幻觉风险	编译通过 = 零幻觉	存在"看起来对但逻辑有缺陷"的风险
灵活性	受限于 Lean Mathlib 库的覆盖范围	理论上可处理任何领域
可扩展性	批量自动化，成本可控	依赖模型本身推理能力的上限
核心哲学	"信任但验证"（Trust but verify）	"模型足够强就不需要拐杖"

打个比方：

OpenAI 的路线像闭卷考试——考的是模型的"真功夫"。如果它能在没有任何外部工具辅助的情况下写出正确证明，说明它真的"理解"了数学。

DeepMind 的路线像开卷考试加自动批改——模型可以翻书、可以试错，但每一步都有一个不会撒谎的批改系统。考的不是"一次做对"，而是"最终做对"。

哪条路线更好？这取决于你问的是什么问题。

如果你问的是"AI 到底有没有真正理解数学？"——OpenAI 的路线更有说服力。模型不依赖外部验证就能给出正确证明，这是实力的硬指标。

如果你问的是"AI 怎么才能大规模、可靠地辅助数学研究？"——DeepMind 的路线更务实。你不需要 AI "理解"数学，你只需要它能源源不断地生成正确的证明。编译器不在乎 AI 是理解了还是蒙对了。

我的判断是：短期内 DeepMind 的路线更实用，长期来看两条路线会合流。OpenAI 的模型迟早会接入 Lean，而 DeepMind 的 LLM 也会越来越强。最终，"猜得好"和"验得准"不是二选一，而是缺一不可。

AI 数学的终极形态，不是选"聪明"还是选"靠谱"，而是用"靠谱"来释放"聪明"。

---

数学家要失业了吗？

每次 AI 取得突破，这个问题都会被问一遍。

先说数据：AlphaProof Nexus 在 353 道埃尔德什问题上的成功率是 2.5%。在 492 个 OEIS 猜想上的成功率是 9%。

这意味着，97.5% 的埃尔德什问题，AI 目前连门都没摸到。

但这 2.5% 里的含金量极高——其中有几道题悬了半个世纪以上。AI 的优势不在于"什么都会"，而在于"试得起"。它可以用极低的成本扫过几百道题，把那些恰好在当前能力范围内的摘下来。

数学家们的反应也很有意思。论文中提到，有数学家表示，即使 AI 的失败尝试也很有价值——因为形式化的证明草稿让专家可以快速定位"卡在哪里"，而不用从零开始验证整个论证链。

AI 系统甚至发现了已发表论文中的形式化错误。形式化验证可以作为一个过滤器，决定哪些证明值得人类花时间审查。
—— AlphaProof Nexus 论文

这其实透露了一个重要信号：AI 的角色不是取代数学家，而是改变数学家的工作方式。

打个比方：望远镜发明之前，天文学家用肉眼观星。望远镜发明之后，天文学家没有失业——他们看到了更多的星星，提出了更多的问题。

AlphaProof Nexus 就是数学家的"望远镜"。它不会替你思考，但它能帮你看到原来看不到的地方。

Demis Hassabis 在播客采访中说了一句大实话："真正的 AGI 需要原创性、创造力，以及跨多个领域的广泛能力，而不仅仅是某一个专门领域。"

他说得对。AlphaProof Nexus 在组合数学和数论上很强，但那是因为 Lean 的 Mathlib 库在这些领域最完善。换到拓扑学或代数几何的某些分支，它可能连问题都读不懂。

但这并不减损它的意义。

想想看：2024 年，AlphaProof 初代在 IMO（国际数学奥林匹克）拿了银牌。2025 年，DeepMind 和 OpenAI 都拿了金牌。2026 年，AI 开始啃研究级的开放问题。这个进化速度，用"指数级"来形容都显得保守。

AI 不是数学家的替代者，它是数学家的新显微镜——只不过这个显微镜，每半年自己就会进化一次。

---

最后，我做两个预测，给自己设个 deadline：

预测一：2027 年底之前，AI 系统将解决至少 50 道埃尔德什开放问题——目前是 9 道。成功率从 2.5% 提升到 15% 以上。驱动力不是算法突破，而是底层 LLM 能力的持续提升和 Lean Mathlib 库的扩展。

预测二：2028 年之前，至少一个千禧年数学难题（Millennium Prize Problems）的关键子问题，将由 AI 系统首次给出形式化证明。不是完整解决，但足以让数学界震动。

一年半后回来看看，我说得对不对。

如果你问我 AlphaProof Nexus 这件事最大的启示是什么，我觉得不是"AI 多聪明"，而是一个更朴素的道理：

把"猜"和"验"分开，用最笨的方式确保正确性，然后让试错成本趋近于零——这不仅是 AI 做数学的方法论，也是我们做任何困难决策时，值得借鉴的思路。