当AI秒杀数学难题：一位学者退圈，一场证明过剩危机

一位刚从纽约大学阿布扎比分校完成博士后的数学学者 Rishikesh Gajjala，近日在 X 上宣布退出数学学术界。过去几个月，AI 在他攻读博士期间长期钻研的问题上接连取得突破，而他原本需要数年才能推进这些难题。这种「被取代」的感受让他重新审视了数学对自己的意义——他真正看重的从来不是答案本身，而是答案出现之前的那段探索。当 AI 让「上帝之书里的大多数答案都只隔着一个 prompt」时，提早找到答案这件事突然失去了吸引力。

「证明过剩」时代的核心焦虑

Gajjala 留下的一句判断很尖锐：「在通过验证之前，一份漂亮的证明和垃圾没有区别。」他观察到，AI 系统生成的证明可以极其精巧，但错误也可能藏得极深，要判断一个「漂亮突破」是否成立，有时需要花掉好几天。当世最伟大的数学家之一陶哲轩在 2026 年国际数学家大会（ICM）上发表了题为《AI 时代的数学》的演讲，几乎在回应同样的问题。他造了一个词叫「证明的消化不良」（proof indigestion）——AI 生成证明的速度已经远超人类审核的速度，数学正从「证明稀缺」冲进「证明过剩」。他提到，专门收集数学难题的网站上已经堆满 AI 提交的证明，多数可能正确，但缺少人类数学家逐一核实。换句话说：智能正在变成最便宜的东西，但「能被信任的智能」还是最贵的。

从「找答案」到「造验证系统」

想通这一点后，Gajjala 没有继续做数学，而是转向形式化验证：用 Lean 等定理证明助手语言，将 LLM 发现的长期猜想与 Erdős 问题逐条形式化。随后他加入了刚完成 Khosla Ventures 领投 2700 万美元种子轮的 Pramaana Labs，研究重心从「发现数学真理」转为「构建能为 AI 答案盖章的认证系统」。有读者在评论区追问：AI 会不会同样以超人速度造出验证系统本身？他的回答是：「我还不信。等我真这么觉得了，我就再找份新工作。」形式化验证的做法是把证明改写为机器可读的语言，逐行核验——人会被漂亮的行文带跑，机器不会。

246 定理：人类离孪生素数最近的一次

与此同时，Axiom Math 的多智能体系统 AxiomProver 完成了「246 定理」证明的形式化验证。创始数学家 Ken Ono 表示，这个定理代表了人类目前关于素数知识的绝对边界。孪生素数指的是差为 2 的素数对，如 (3,5)、(11,13)。19 世纪法国数学家 Polignac 猜想：这样的素数对有无穷多。看似简单，至今无人能证。人类走向这条目标的关键节点包括：

• 2013 年，张益唐首次证明存在无穷多对差不超过 7000 万的素数，把间隙从「无穷」变为「有限」。
• 几个月后，牛津的 James Maynard 用新方法将 7000 万砍到 600，并因此项工作获得 2022 年菲尔兹奖。
• 此后 Maynard 与陶哲轩在 Polymath8b 合作项目中把间隙压到 246——这也是目前人类距离目标 2 最近的一次。

AxiomProver 验证的正是「存在无穷多对相差 246 的素数」，并把素数间隙相关的一批结果打包成可复用的开源库，246 定理是其中的旗舰。

「没人读过的代码」将成为常态

陶哲轩在 ICM 演讲中直言，他曾对预测未来三年相对有信心，如今这种确定性已经消失：「我不确定现在是否还有任何人能可靠预测一年以后的事情。」Gajjala 退出数学学术界，但并未离开数学——他从一个找真理的人，变成了给真理盖章的人。在 AI 加速重写一切的时代，或许这才是真正紧缺的角色。