AI 解出 9 道悬了 56 年的数学题，数学界却吵起来了

luyuanhong

AI 解出 9 道悬了 56 年的数学题，数学界却吵起来了

原创  小木 AI 笔记  小木 AI 笔记  2026 年 10 月 16 日 09:00  北京

《科学》10 月 8 日那篇论文的摘要里，两个数字隔了不到一行：353 和 9 。

353 是它尝试的开放数学问题总数，9 是解出来的数量。这 9 道里，有两道从 1970 年提出起，56 年没人解出来。

论文来自谷歌 DeepMind 和丹麦奥胡斯大学，系统叫 AlphaProof Nexus ，底座是今年 2 月发布的 Gemini 3.1 Pro 。消息传开之后，大多数标题都是“ AI 破解 56 年数学难题”；但论文自己把分母写在了最前面。

这个分母，是团队自己写进去的

厄多斯这份名单不是随便凑的。保罗·厄多斯一生提出的问题横跨组合数学、数论和图论，相关目录里有一千两百多道仍未解决。而这次实验用的 353 道，是其中已经被志愿者翻译成 Lean 代码的那一部分——也就是说，这批题本身就偏向"能被现有数学库接住"的类型。

在这个前提下，成绩是这样：系统自主解出 9 道，约占全部尝试的 2.5% 。其中两道从 1970 年悬到今天。



论文里还有两组结果。一组来自整数序列在线百科全书 OEIS ：先从 2649 个猜想里选出 500 个，再交给另一个智能体做形式化，中间有 8 个因为 Lean 版本升级而丢失，最后在 492 个开放猜想里证明了 44 个。另一组更散，包括与奥胡斯大学合作解决 Hilbert 函数四个开放问题中的两个，以及在凸优化里给出一个更精确的收敛速率。

成本写得也挺实在：每道题的推理成本约几百美元。

我不太想把这个成绩读成“AI 会解任何难题”。它更像一份已经划好边界的实验报告——在一个提前整理干净的清单上，机器啃下了很小的一块。

让论文作者意外的，是那个对照实验

先说它怎么解题。数学证明里有大量“显然”“不难证明”的省略，机器读不了，所以第一步要先把命题写成 Lean 能逐行校验的形式化代码。

然后是一个很朴素的动作循环：模型起草证明，Lean 编译器逐行检查，报错信息直接喂回下一轮。报错不是失败，是下一轮的线索。

完整版的系统搭得更复杂——四个层次的智能体，用进化算法协调子智能体，还能调用 2024 年在国际数学奥林匹克拿过银牌的 AlphaProof 当专门工具。



然后团队做了一次事后对照，把简单版本单独跑了一遍：不共享尝试、不调用 AlphaProof ，只靠大模型加编译器反馈。结果是，它同样解出了全部 9 道，差别只在最难的题上要花更多算力。

论文作者之一公开表示意外。



这个结果的方向很有意思。它说明在这 9 道题上，真正起作用的是底座模型的能力，而不是外面那层智能体架构搭得多精巧。工程做得再花，也得模型自己会。

机器能确认你没算错，不能确认你要的是这道题

到这里，成绩单是漂亮的。门槛在后面。

Lean 有一个边界：它校验的是你交给它的那句形式化陈述，它不能保证这句陈述忠实翻译了你原本想问的问题。翻成代码时跑偏，就会出现“正确地证明了一个错误的定理”。

这不是假想。今年 7 月，一份声称“证伪考拉兹猜想”的 Lean 证明被 Lean 内核和一个独立检查器同时接受，几天后才发现，它利用的是内核在处理嵌套归纳类型时的一个实现缺陷。那个夏天，Lean 接连暴露了几个这类健全性问题。



把镜头挪到同一周的另一个发布，对比会更清楚。

10 月 7 日凌晨，OpenAI 在 GitHub 上一次性放出 722 篇由内部模型生成的数学手稿，分成 372 个"结果族"，覆盖 17 个领域。平均每个结果花费的算力，约等于 ChatGPT Pro 跑三个小时，部分成果附了 Lean 形式化证明。

第二天，OpenAI 在官方仓库发布了第一份更新日志：撤回 3 篇、修订 14 篇、13 篇更新引用。撤稿的原因是一处符号错误，让其中一篇的论证失效，并连带影响了两篇依赖它的论文。

一边是等几个月走完同行评审、把形式化证明全部公开、逐题说明哪道成了哪道没成；另一边是先发出去、第二天再修。两种做法没有谁“赢”，但前者把“验证”放在了发布之前。

顺带说一句，这次被解出来的 9 道里，有两道也被 OpenAI 的内部模型独立找到了。数学不会因为谁先发就归谁。

数学家吵的其实是后面那三环

菲尔兹奖得主陶哲轩 10 月 9 日做了一场演讲，标题叫《数学 2.0》。

他把一份证明的一生拆成五环：生成证明、验证正确性、讲清楚、被同行理解和接受、最终进入教材。

AI 在前两环疯狂加速，后三环几乎为零。他给这种状态起了个名字：证明消化不良——像二十世纪初的汽车涌进为马车设计的街道。

他的担心很具体：如果 AI 几小时就能生成一份没人在读的证明，那么“在试图解决一个难题的过程中长出来的新方法”，也就一起消失了。



曼彻斯特大学的 Thomas Bloom 维护着一份跟踪一千多道厄多斯问题的清单。据公开报道，他决定不再给问题标注“开放”还是“已解决”，同时关掉了评论——理由是他的站点从“一起讨论问题”变成了“比赛谁先用 AI 把题关掉”，他不想整天给 AI 生成的工作当审稿人。

在清华的一场活动上，中国科学院院士、中国数学会会长席南华的说法更平和一些：企业发布成果不受学术规则约束、不需要同行核验，确实给学界带来冲击；但不必陷入焦虑，新的共识还在形成。

吵的从来不是“ AI 能不能解题”。是解出来之后，谁来读、谁来验、谁来把它变成后人能用的东西。

我拿走的一条判断标准

这件事离日常很远，但它给的判断标准很近，翻译过来就是三句话。

听到“ AI 攻克了某个难题”，先找分母：试了多少、成了多少。

收到 AI 给的方案或数据，先问依据在哪、哪一步是我能自己核验的。

一份结果能不能“摊开给你看每一步”，比它看起来像不像对的更重要。

AI 降的是“做出来”的门槛，没有降“确认它对”的门槛。Lean 这种机器裁判已经把校验做到极致了，还是要有人在旁边确认“你要的到底是哪道题”。

我还没想清楚的是另一件事：如果那后三环一直没人接，这些被解出来的题，最终算不算真的被解开了。这个问题，可能要等最早的一批 AI 证明真的写进教材之后，才会有答案。

小木 AI 笔记