数学「毕业」了：xAI 联创说英雄时代结束，我盯着日期看了两遍

Christian Szegedy 那篇《数学何去何从？》在 X 上炸开那天，我的第一反应不是点进去读，而是去看发布日期。xAI 联合创始人、Inception 第一作者、批归一化提出者之一，写长文宣判「数学的英雄时代结束了」——从一个数学特长生、波恩大学应用数学博士嘴里说出来，分量不太一样，我多核了两遍时间线。

Szegedy 其实押了十年。2019 年他写立场论文，主张走自动形式化这条路，让 AI 把人类写的数学翻译成机器能逐行检验的证明，目标是造出超人数学家，时间表定在 2029 年。2024 年他把表提前三年，还当众跟人对赌：2026 年 6 月之前出现超人 AI 数学家。之后的事，材料里给了很密的时间轴——今年 9 月 4 日，Anthropic 内部模型用 11 天在定理证明器 Lean 里写完费马大定理的完整证明；9 月 8 日，OpenAI 宣布 1 万个 Agent 跑 88 小时攻破千禧年难题 Navier–Stokes 方程；9 月 21 日，OpenAI 又说内部模型解决了 100 多个长期悬而未决的数学问题。全都发生在他最初预言的 2029 年之前。这大概是整件事最让人背脊发凉的地方。

他用的比喻很直白：数学家是原始丛林里徒手攀岩的探险家，AI 是一架飞机，已经把旗插上了没人爬上去过的山顶，甚至降落在了几块从没人上去过的石头上。探险家在丛林里干三件事——画地图、找矿、造工具，最受尊敬的是爬上前人失败的高山、在山顶画草图的人，朗兰兹纲领就是这样的成就。而飞机一旦便宜下来，私人飞机遍地都是，人类会发明卫星把整片丛林的矿藏测绘一遍再开采。场面会很脏很乱，今天的探险家会骂大公司糟蹋了他们热爱的丛林。「他们说得对，但这改变不了什么，大公司会在那里找到难以想象的财富。」他说别跟飞机打赌，「谁把自己的身份押在『AI 做不到 X』上，谁就是在沙子上盖房子。」

真正让我停下来的是长文最后一节。他写高中毕业考结束后的头两个小时是他这辈子最自由的时刻，随后空虚就来了，「我第一次不知道，没有了它，我是谁。」他要把这种感受转告给全世界的数学家：你们接下来要经历的，就是这种感觉。他说爬上别人爬不上的山，这种英雄主义会变得不那么重要，取而代之的是另外三种本事——选择哪片地形值得探索、指挥飞机编队、把发现讲给全世界听。他也承认「对体制里的很多人来说，这会感觉像降级，有些人会抗争」。

不是所有人都接过这张毕业证书。Szegedy 发文前 5 天，Wolfram 写了篇 7000 多词的长文说自己「有点不耐烦了」，说数学的目标几乎按定义来自系统之外、来自我们，还亲身踩过自动形式化的坑——AI 告诉他证明通过了，证的却不是他想证的东西。帝国理工的 Kevin Buzzard 则用「悲伤五阶段」给数学界画像，否认、愤怒、讨价还价、抑郁，前四个阶段都能找到大把代表；他提到菲尔兹奖得主舍尔策公开说不用 AI，「愿意为此死守到底」，还有个博士生被 ChatGPT 一次证出卡了许久的引理，开始怀疑自己做的一切还有什么意义。

Szegedy 说这份哀伤是真实的，只是不会持续太久。数学注定是第一个被 AI 工业化的基础学科，因为它的结果能被机器逐行检验，不用做实验，对就是对、错就是错。所以 AI 最先啃下的硬骨头——千禧年难题、雅可比猜想、费马大定理——全都在数学里。材料里那位斯坦福数学家 Jared Duker Lichtman 转发时说，自己从 2019 年读研究生起就在等这一刻：「我们准备把全部已知的数学，翻译成形式化代码。」

我不打算站队，只想提一个材料里的细节：Wolfram 那篇 7000 词的回应里，那句「证的不是我想证的东西」太真实了。自动形式化最漂亮的地方就是它对就对、错就是错，可难点从来不在形式化本身，而在把「人想要的问题」翻译成机器能检验的形式，这一步目前还得靠人。飞机的比喻很燃，可燃料和航线图，暂时还是画地图的人给的。数学这栋两千多年的智力大厦，可能真要毕业了，但毕业考试改卷的老师，眼下还不全是机器。