顶尖数学家含泪退圈：熬了多年的博士难题，被AI几周秒杀！

新智元报道 一个顶尖数学学者，靠AI几个月内连续攻破苦熬多年的博士课题。 这是好事啊。 然而， 他居然宣布退出学术圈！ 这位大哥名叫 Rishikesh Gajjala，刚从纽约大学阿布扎比分校做完博士后。 就在昨天，他在 X 上写下了一份让整个数学圈爆炸的帖子： 我决定离开数学学术界。 过去几个月，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 加速重写一切的时代，这可能才是最紧缺的角色。 参考资料： https://x.com/publishiperishi/status/2089337253055365226 https://spectrum.ieee.org/axiom-math-246-theorem-formalization 编辑：所罗门 秒追ASI ⭐ 点赞、转发、在看一键三连 ⭐ 点亮星标，锁定新智元极速推送！ 文章原文