顶尖数学家含泪退圈: 熬了多年的博士难题被AI秒杀

过去几个月，AI 帮他在读博期间钻研多年、最在乎的那些问题上接连取得突破。

按原来的节奏，这些难题够他钻研好几年。换成别人，这本该让他更加确信数学就是自己的天命。

结果，恰恰相反。每过一周，他就觉得自己在里面越来越像个多余的人。

Gajjala 说，数学对他的意义，从来不在答案本身。而在答案之前那一段几个月甚至几年的探索，一条条走不通的路，长时间的苦苦探索，直到隐藏的结构终于浮出来。那段挣扎让结果真正属于他。

现在他判断，我们正飞快逼近这样一个世界：上帝之书里的大多数答案，都只隔着一个 prompt。

想透这件事之后，把大半辈子花在比别人早一点找到那些答案上，他突然就没那么有意义了。

一份漂亮的证明和垃圾没有区别

但有个问题一直咬着他不放。

怎么知道这个神谕是对的？

智能一天比一天强，一天比一天便宜，数学论文跟着满天飞。但没有验证。

这些AI系统写出来的证明可以极其精巧。 同样，错误也可以藏得极深。

判断一个看起来漂亮的突破到底成不成立，有时要花掉他好几天。

Gajjala 说了句“暴论”：在通过验证之前，一份漂亮的证明和垃圾没有区别。

这话刺耳，但不只是他一个人这么想。

当世最伟大的数学家之一陶哲轩，在 2026 年国际数学家大会（ICM）上专门发表了题为《AI 时代的数学》的演讲，说的几乎是同一件事。

他造了一个词叫“证明的消化不良”（proof indigestion）——AI 生成证明的速度已经远超人类审核的速度，数学正从一个证明稀缺的时代冲进一个证明过剩的时代。

他特别提到，专门收集数学难题的网站上，已经堆满了 AI 生成的证明提交。很多可能是对的，但没有人类数学家有空去一一核实。

说白了，AI 写论文的速度是光速，人类读论文的速度还是蜗牛。当论文洪水般涌过来，没人读过的“正确答案”跟不存在没什么两样。

智能正在变成最便宜的东西，但能被信任的智能，还是最贵。

从找答案到造验证系统

想透这一层之后，Gajjala 做了一个决定，不找答案了，去造能给答案盖章的系统。

他转身走进形式化验证领域，用 Lean（一种定理证明助手语言）把那些借助 LLM 发现的长期猜想和 Erdős 问题一个个形式化。

随后他加入了刚拿到 Khosla Ventures 领投 2700 万美元种子轮的 PramaanaLabs，研究重心从“发现数学真理”换成“构建能证明 AI 答案正确的认证系统”。

有人在评论区问 Gajjala：AI 很快也能用超人速度把验证系统本身造出来吧？

他回了一句：我还不信。等我哪天真这么觉得了，我就再找一份新工作。

形式化验证就是把证明改写成机器读得懂的语言，让计算机逐行去查。

人会看漏，会疲倦，会被漂亮的行文带跑。但机器逐行核验时没有情绪，不会被作者文笔打动。

而同一时间，这条路上出现了迄今最硬的一次战果。

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

Axiom Math 用自家多智能体系统 AxiomProver，首次自动完成了“246 定理”证明的形式化验证。

创始数学家 Ken Ono 说，这个定理代表着人类目前关于素数知识的绝对边界。

246 是啥？

2、3、5、7、11、13……素数越往后越稀疏，但总有些挨得特别近，比如 3 和 5、11 和 13，只差 2。这种一对儿一对儿出现的素数叫孪生素数。

19 世纪法国数学家 Polignac 提了一个猜想：不管你沿着数轴走多远，这样的一对总会再冒出来。也就是说，孪生素数有无穷多对。

小学生都听得懂，但至今没人能证明。

2013 年，张益唐先撕开一道口子。他证明了存在无穷多对相差不超过 7000 万的素数。7000 万离目标的 2 还差得远，但这是人类历史上第一次证明这个间隙是有限的，数学界炸了。

几个月后，牛津的 James Maynard 换了套方法，一刀把 7000 万砍到了 600。这项工作对他 2022 年拿下菲尔兹奖（数学界的诺贝尔奖）贡献巨大。

再往后，Maynard 和陶哲轩在 Polymath8b 合作项目里联手，又把间隙压到了 246。

从 7000 万到 600 到 246，三步走了十年。246 是人类离目标 2 最近的一次。

AxiomProver 这回验证为正确的，就是这条定理——存在无穷多对相差 246 的素数。

更关键的是，它没停在秀肌肉。团队顺手把素数间隙的一批结果打包成了可复用的开源库，246 定理是里面的旗舰。这意味着以后其他 AI 系统想在素数问题上做研究，直接有一套经过机器验证的基础设施可以调用。

世界即将运行在没人读过的代码上

一位数学学者退出学术圈，看上去只是一个人的职业选择。

但，故事的底色完全不一样。

这个世界即将运行在没有任何人读过的计算机代码之上。

陶哲轩在 ICM 演讲里也给了一个惊人的判断：他在 2023 年还相对有信心预测未来三年的趋势，如今这种确定性已经消失。

“我不确定现在是否还有任何人能可靠预测一年以后的事情。”

Gajjala 退出了数学学术界，但他没离开数学。他只是从找真理的人，变成了给真理盖章的人。

在 AI 加速重写一切的时代，这可能才是最紧缺的角色。