「没人能解释的证明，就算不完整」——陶哲轩把 AI 之问，从「何时到来」换成了「我们图什么」

先说结论

陶哲轩刚做了一件比「预测 AI 什么时候能做研究」更有用的事：他不再正面回答这个预测。今年 7 月国际数学家大会（ICM 2026）的公开报告上，8 月 17 日挂上 arXiv 的论文《Mathematics in the age of AI》里，他直接假设「AI 能做研究级数学」会发生——原话是「我并不要求读者希望它为真、相信它为真，或接受它为真」——然后把全部力气用来问一个被能力争论埋住的问题：数学共同体到底图什么。9 月 2 日，他又更新了自己那份「AI 观点」汇总页，把这几个月的判断归拢了一遍。

他给出的答案里最狠的一句是：「一个没有人能妥当解释的证明，应当被视为不完整的——哪怕它已经通过了形式化验证。」

事情是怎么发生的

这组观点有实打实的战绩做底。2023 年 6 月，他预测「2026 年水平的 AI，配合形式化验证工具，会成为数学研究里可信赖的合作者」。今年他自评：几乎准时兑现，当前水平大致相当于一位初级人类合作者。证据是他牵头的 PFR 项目：约二十个多数从未谋面的人，用三周把一篇 33 页的论文形式化——「无需信任彼此」的大规模协作，就此有了跑通的样板。

但同一页上他也承认，自己对「预测」这件事的信心在下降。这正是他换问题的原因：既然判断不可靠，就把「何时发生」设为条件，专心做条件分析。

为什么重要

第一，他点破了生成与消化的剪刀差。AI 让「产出证明」急速变便宜，但读懂、审核、讲清楚并没有变快，于是出现证明过剩，他称之为阻抗失配。他的处方是动声望结构：降低「证明生成」的文化权重，提高「证明消化」——把结果讲清楚、认真审稿、整理成领域里能反复引用的标准表述——的地位。这一步不只关乎数学：任何产出能被机器批量生成的行业，稀缺资源都会向下游的验证与解释迁移。

第二，他把 Goodhart 定律对准了 AI：生成式模型是「无根基的」，它优化的是「输出的外观」而不是「底层的性质」，产量一旦成为指标就会被玩坏。所以他不认为人类评审能撤出出版流程，还提了一个操作性极强的测试：作者若不能把自己的工作讲成一场清楚的专家级报告，这个结果就不该发表。

第三，摩擦被他说成了功能：人写的证明里那些难读的地方，「提示读者哪里该慢下来」；过度顺滑的 AI 文本「好读，但学不到东西」。

站得住与站不住的地方

站得住：方案在他自己的领域内几乎自洽——数学「几乎独一无二」地允许对输出做自动检查，验证器真实存在，而且他身体力行，那份观点页就是 AI 起草、本人逐条审校的。

站不住的有三处。其一，外推性存疑：「能机械验货」是数学的特殊待遇，实验科学、法律、医疗并没有等价的形式化验证器，这套处方搬不过去。其二，「几乎准时兑现」是自我评分，初级合作者的类比也没有独立基准可查。其三，声望再定价听起来优雅，动的却是别人的奶酪——期刊、经费、职称全都锚定在「谁先证出定理」上，而数学共同体的行动速度从来不是强项。形式化验证本身也有成本和覆盖面问题，不是每个领域都能塞进证明助手。

接下来该盯什么

一是那份主张「作者身份属于人类」的 Leiden 声明能签下多少名字、进多少期刊政策；二是看哪个领域第一个长出自己的「证明消化」运动——比如把「把复杂结果讲清楚、复现出来」变成能换职级的贡献；三是学界与厂商争夺规则制定权的下一场碰撞，他的原话是「按我们自己的条件，而不是按厂商替我们定的条件」。这三件事，比任何一条新基准分数都更值得放进观察清单。