陶哲轩联合多位菲尔兹发布声明，这件事本身很重要。但大众理解的是，你看数学家要失业了，所以他们开始愤怒了。这个理解，确实，搞笑。

我并不惊讶ai在各种猜想领域的攻城略地，一点也不惊讶，所以那些头条对我没什么吸引力。

为什么？因为十多年前，阿尔法狗在围棋领域的胜利，我已经认为那是分水岭。今天这些，不过是进程继续深化，算力更加强大的必然结果。

围棋长期被视为人类直觉的最后堡垒：10¹⁷⁰ 量级的棋局状态，无法暴力枚举，顶尖棋手靠棋感。但AlphaGo 的胜利其实证明了一件事，我们把它提炼出来就是，只要一个领域能被约化成，规则封闭 + 完美模拟器 + 廉价反馈的游戏， 那么模式识别 + 搜索就能碾压人类直觉。胜负信号清晰、终局即奖励、可以无限自我对弈——这就是强化学习的理想栖息地。

而形式化数学恰好长这样，所以它确实会陷落，一定会陷落。

数学有一个几乎所有科学领域都没有的东西：可检验的证明核（Lean、Coq 这类形式化系统）。一个证明对不对，编译器几秒内核验完毕——这就是数学版的棋规 + 模拟器。所以 AlphaProof 攻克 IMO 难题几乎是被围棋结局预告的。形式化后的数学子问题，和围棋属于同一类封闭游戏。

但所有人，包括我们普通人也应该理解的一点是，数学不止证明层。远远不止。今天的互联网叙事中，谁证明了什么，就是顶尖的成就。好像数学仅此而已。其实，远远不是。

围棋落子的价值由对局本身裁决，但数学命题的价值却没有裁判。比如"哪个猜想值得证"、"什么定义深刻"、"什么理论结构优美"——这些判断没有自我对弈式的无限反馈回路。AlphaGo 可以从零自我对弈几百万盘，数学却没法无中生有地生成有意义的对局。

目前的进展，是远远没有到达自主提出并解决自己的问题。拉马努金机器确实能自动生成连分数猜想——但筛出哪个值得人类关注这一步，又回到了没有裁判的地带。

总结一下，这个模式，一个领域会不会被 AI 攻破，不取决于它是否需要"直觉"，而取决于它是否拥有廉价、完美、可无限调用的反馈回路。围棋，有（规则 + 模拟器），形式化数学，有（证明核）， 正在陷落。物理，没有。数学的品味和提问，也没有。

国际象棋 1997 年就陷落了，但人类也并没有停止下棋——人机合体时代反而让棋类进入了新维度。数学也可能同样分裂成两层，AI 负责验证的存量攻坚，人类负责画地图——决定哪些新大陆值得勘探。这些，才是数学家的新工作，还觉得数学家会失业吗？

历史反复证明，每次最后堡垒陷落之后，人类都会把防线往后撤一段，然后宣布新的堡垒。

真正有趣的从来不是哪座堡垒陷落，而是每次陷落都在精确地标出那条反馈回路的边界在哪里（规则封闭，模拟器和廉价反馈）。