2026 年 10 月 6 日傍晚，纽约国家数学博物馆正在办年度晚宴。罗格斯大学的数论学家 Alex Kontorovich 一手拿着威士忌，一手刷手机。OpenAI 说好当晚放出一批结果，没人知道有多少，有人猜三四百。实际是 722 篇。知乎
第二条标题写着“拟黎曼猜想”。Kontorovich 后来在播客里回忆，他一时没反应过来：“拟”是什么意思？对什么成立？再一看，是对 ζ 函数，对所有狄利克雷 L 函数。
黎曼猜想说，ζ 函数的非平凡零点全在实部 1/2 的那条竖线上。拟黎曼猜想退一步，只要求把所有非平凡零点关进一条比 0 到 1 更窄的竖带。OpenAI 给了两个版本：9 月 30 日的 199 页，附了 Lean 形式化证明（Lean 是一种机器能逐行检查的证明语言）；10 月 5 日的 49 页，还没形式化。数学家们后来集中读的，是 49 页那篇。理由很实际：两篇都写得糟糕，但短的至少读得动。整批七百多篇里，也只有这一篇的写作文本被人编辑过——不是为了改数学，而是为了让人读得下去。Quanta Magazine
更意外的是它怎么证出来的。Quanta 报道说，这个证明没有引入新概念，而是把旧工具重新组合：用了 Alexander Dunn 研究了五年的 metaplectic forms（一种数论里长期冷门的对象），用了 Dunn 和 Maksym Radziwiłł 2021 年的一条公式，还挑中了一个 Henryk Iwaniec 在 2002 年几乎碰到、又错过的函数族。Radziwiłł 说，AI 敢“相信”这套工具够用，本身就是一个相当大胆的判断。Quanta Magazine
Kontorovich 的总结是：每一步都是人类已知的招数，只是串得极长、极准。这大概是 AI 和人类最不一样的地方之一：它不背“哪些路走过、走不通”的包袱。人类数学家靠品味和直觉排除掉大量“显然没希望”的方向；AI 没有这种包袱，所以会在人类已经放弃的地方再试一次。
但“证出来”不等于“数学界能接住”。OpenAI 仓库里约 42% 的核心结果有 Lean 证书。发布第二天，3 篇因一个符号错误撤回。 Lean 能检查每一步是否从公理推出，却检查不了这篇论文的命题是不是数学家真正想要的那个。Quanta 的比喻很准：像被瞬移到一座山顶，四周是雾，你不知道自己在哪里，也不知道这座山和别的山怎么连。GitHubRetraction Watch
这也是为什么，10 月 6 日之后，数学家花了很多时间做的事，不是继续证明，而是把证明变短、变清楚、变成可以教的东西。Radziwiłł 现在能用半页纸勾勒整篇论证；Peter Sarnak 把本学期的一门课改成专门读这篇论文；Kontorovich 和两位同行在播客里花了三个半小时，把包括这道题在内的结果讲给外行听。这些事看起来像“消化”，其实一直是数学研究的一部分：把一个证明压缩成定义、引理、可复用的工具，下一代人才能接着走。
所以，“数学研究会被取代吗”这个问题，只问对了一半。被取代的不是“数学研究”，而是“证明”作为稀缺品的位置。过去，一个数学家最值钱的能力是找到一条别人找不到的证明路径；现在，这条路可以由机器以三小时一道的速度铺出来。这批评估里，模型被问了约四千个问题，平均每个结果花三小时算力。 Scott Aaronson 写得很直接：余生大概不会再因为“非我不可”而证明一个定理，人类从此不再是地球上主要的定理证明者。GitHubQuanta Magazine
但定理证明者不等于数学研究者。选什么问题、把证明压缩成什么概念、判断哪个方向值得下一代人投入、把一个结果讲成共同体能接住的知识——这些事没有因为证明变便宜而变便宜。恰恰相反，当证明多到读不完时，它们变得更贵。这不意味着机器永远学不会提纯；至少在这批结果里，它把最难的那部分留给了人。
真正的危险也在这里。arXiv 已经把作者每月投稿数限制在两篇，MathOverflow 的活跃度也在下降，审稿人被 AI 证明淹没；年轻研究者被推到验证的一线。如果院系和期刊仍然只奖励“谁先证出来”，不奖励“谁把它讲清楚”，那么 AI 证明越多，人类越没有时间产生下一个问题。到那时，不是机器取代了数学，而是数学的反馈回路被自己的产出堵住了。Quanta Magazine
Kontorovich 在那个晚宴上没能消化眼前的东西。三周后，他和同行花了三个半小时，把它讲给外行听。这大概就是数学研究接下来的样子：AI 负责把人送到山顶，数学家负责修一条让人上得去的路。路修不修得出来，不取决于 AI 还会证多少题，而取决于数学界愿不愿意把“修路”算作真正的工作。
