（...接续）

四、证明过剩时代的数学家：从猎手到厨师

陶哲轩提出了一个关键判断：数学正在从“证明稀缺”进入“证明过剩”时代。

他用了一个精确的比喻来描述这种转变。在食物稀缺的社会，最受尊敬的人是猎手——那些把食物带回家的人。你猎回一头鹿，不管肉质如何，整个部落都会感激你。在食物过剩的社会则完全不同——想象一个pot-luck派对，如果一个陌生人闯进来扔下一块来路不明的生肉，让大家自己去处理，没有人会高兴。

AI跑出来的证明，就是那块被陌生人扔在派对上的“生肉证明” ——它可能是正确的，可能通过了形式化验证，但没有人清洗过它、烹饪过它，也没有人能告诉你它到底好不好吃。

陶哲轩指出，数学问题求解从来不是一件事，而是三件事：

1. 证明生成：把一个猜想从“未解决”推到“有解”。

2. 证明验证：确认这个解是对的，逻辑没有漏洞。

3. 证明消化：把证明读懂、讲透、提炼出方法论，让整个领域受益。

AI极大地加速了生成环节，验证环节有Lean等工具兜底，唯独消化环节——那个需要人类大脑去理解“这个证明到底意味着什么”的环节——完全跟不上。陶哲轩用一个精确的工程术语形容这种错位：impedance mismatch（阻抗失配）。

数学家最重要的工作，已经不再是“做出证明”，而是验证它、消化它，并把一块AI吐出的“生肉证明”变成人类真正吃得下的知识。

五、人类最终的保有量：判断“什么值得消化”

如果AI能生成证明，AI能验证证明（通过Lean等形式化工具），那么人类还剩下什么？

构造学的回答是：人类最终的保有量，是对“什么值得消化”的判断力。

AI可以生成一万个证明。但哪个证明值得被仔细阅读、被重构、被纳入教科书、被转化为新的方法？哪个证明虽然正确但无关紧要？哪个证明虽然不完整但指向了一个重要的新方向？

这些判断无法通过形式化来完成。它们是价值判断——它们依赖于对系统“地形图”的整体理解，依赖于对“什么方向是重要的”这个问题的长期感知，依赖于一个构造者在系统中积累的“地形感”。

陶哲轩在ICM 2026的演讲中说，如果解题这件事AI也能干，那数学家必须重新回答一个根本问题：数学研究，到底图什么？

这个问题的答案，不是“解题”。数学研究的理由包括解决未解问题、发展新理论、理解世界、建设共同体、培养下一代、创造有审美价值的作品。过去几百年，这些目标高度绑定——解决一个大问题，通常顺带推进了理论、培养了学生、凝聚了共同体。

但当AI可以解决大问题时，这些目标开始解绑。你需要单独问这个证明推进了理论吗？它帮助我们理解世界了吗？它有审美价值吗？它值得被纳入教科书吗？

这些问题，AI不能回答。它们需要人类来判断。

六、构造学论的立场：思想的剩余是判断的领地

回到最初的问题。当AI的“智能”超越人类之后，数学中还剩下什么？

构造学论的回答是：剩下的是判断——对“什么值得”的判断。

智能负责在给定棋盘上找到最优路径。思想负责重新画线，改变棋盘的形状。但在这两者之外，还有一个更基础的构造活动：判断哪些线值得画，哪些路径值得走，哪些缺口值得被标记。

AI可以证明循环双覆盖猜想。但AI不能判断这个证明是否改变了图论的地形图？它是否打开了新的方向？它是否值得被纳入教科书？它是否应该被用来指导后续研究？

这些判断，需要一种在系统中长期浸泡形成的“地形感” ——一种对系统历史、现状和未来可能性的整体感知。这种感知不是数据，不是算法，不是模式匹配。它是一个构造者在持续的构造活动中积累的、无法被外部系统复制的具身知识。

陶哲轩说，AI让他的论文更丰富了，核心突破仍然要靠纸笔完成。AI擅长广度，人类擅长深度，二者高度互补。但他也说，数学正在进入一个动荡的时期——一场关于数学价值观与实践方式的基础危机。

这场危机的实质是：当智能被外部化之后，思想必须重新定位自己。 它不能再把自己定义为“解题”或“证明生成”——因为这些已经被AI覆盖了。它必须转向那些AI无法触及的领域。判断什么是重要的，判断什么值得被消化，判断什么方向应该被探索。

结语：猎手退场之后

2026年菲尔兹奖颁给了王虹和邓煜。有人把这一年称为“最后一届没有AI参与的菲尔兹奖”。

这个说法可能夸张，但它指向一个真实的变化：AI正在以前所未有的速度进入数学的核心领域。GPT-5.6在一小时内证明了50年未解的猜想。AlphaProof Nexus以数百美元的成本解决了9道Erdős难题。证明正在从稀缺品变成过剩品。

猎手的时代正在退场。厨师的時代正在到来。

数学家不再只是“把食物带回家”的人。他们是把生肉变成菜肴、判断什么值得烹饪、并围绕这道菜组织对话和传承的人。烹饪本身不产生新的肉，但它使肉可以被食用、被分享、被转化为共同体的养分。

那个判断“什么值得烹饪”的能力，是AI无法复制的。它不是智能，不是算法，不是模式识别。它是一个构造者在系统中长期浸泡后形成的地形感——知道哪些缺口值得填补，哪些路径值得铺设，哪些证明值得被消化、被讲述、被传递。

这就是思想的剩余。在智能被外部化之后，思想收缩到了判断的领地。那块领地不大，但它是人类在数学中最后的保有量。它不是解题。它是判断什么题值得解。

支持单位：