证明可以无限廉价，但理解不能：陶哲轩最新长文谈 AI 时代的数学价值终局

二十世纪初，罗素悖论与哥德尔不完备定理的相继出现，曾给数学界带来了一场长达三十年的“基础危机”（Crisis in Foundations）。在那之前，数学家们依赖着某种朴素的直觉推导集合、数字与无穷，极少有人深究“证明本身到底是什么”。然而，正是那场被迫重审底层假设的剧烈动荡，逼出了现代严谨、公理化且标准化的形式数学大厦，让人类数学在经过一个世纪的严格检验后变得前所未有地坚固。

一百年后的今天，菲尔兹奖得主陶哲轩（Terence Tao）在 2026 年国际数学家大会（ICM 2026）的公开演讲文稿《Mathematics in the age of AI》中，抛出了一个同样震聋发聩的断言：我们正在步入一场同等烈度的新动荡。但这一次，遭受极限压测的不再是关于数学“真理”（Truth）的形式体系，而是数学界长期默许的“价值体系与实践框架”（Values and Practices）。

在铺天盖地关于“AI 模型能否拿到国际数学奥赛金牌”或“AI 能否独立攻克前沿猜想”的技术争论中，陶哲轩做出了一个极具穿透力的方法论切分：搁置充斥着营销噪音与幸存者偏差的能力口水战，直接设立一个工作假设（Working Hypothesis）——假设强 AI 能够以极低的成本、极少的人工干预，解决绝大部分研究级数学任务。

当算力彻底击穿了定理证明的生产成本，数学研究的真正目标与终极价值究竟是什么？

两次基础危机：当受压测的从“真理”变成“价值”

在传统学术体系中，数学研究的核心目标看似不言自明：攻克猜想、建立理论、培养后辈、理解世界、构建学者共同体、创造具有永恒美感的知识大厦。

在过去的几个世纪里，这些目标之间保持着近乎完美的正相关性。数学家为了解决一个硬核难题，往往不得不发明一套全新的数学工具；围绕着这套工具，会聚集起一群志同道合的研究者，进而诞生新的学派；教授据此编写教材、指导博士生，新的理论体系随之向其他科学领域溢出。正因为这种天然的正向协同，数学界长期形成了一种心照不宣的默契：我们可以放心地把“解出未解问题（Problem Solving）”当作所有隐式目标的代理指标（Proxy）。

谁先证明了著名的定理，谁就理所当然地享有教职、声誉与学术地位。法国数学家 David Bessis 将这种运行规则生动地概括为学术界的“定理经济（Theorem Economy）”。

然而，当生成式 AI 与自动化形式化证明工具（如 Lean、Rocq）强势介入时，这套维系了数百年的代理机制遭遇了毁灭性的逻辑断裂。

古德哈特陷阱：为什么“解题”不再是数学的好指标？

经济学中著名的古德哈特定律（Goodhart’s Law）曾冷酷地指出：“当一个指标变成目标，它就不再是一个好指标。”

在过去的探讨中，我们在《刷榜不是道德问题——从 Open ASR Leaderboard 的私有数据说起》中就曾剖析过评测基准一旦暴露，模型便会不可避免地滑向对指标本身的机械过拟合。而在纯粹数学的殿堂里，生成式 AI 对古德哈特定律的触发更为本质。

陶哲轩深刻剖析了其中的两个根源：

技术本质上的无根性（Ungrounded）：生成式 AI 优化的是“输出看起来令人满意的形式表象”，而非输出背后理应指代的深层数学结构。它极其擅长在“度量标准”与“被度量的事物本身”之间寻找套利空隙。
商业激励的量化偏好：AI 产业的资本逻辑与评测竞赛，天然青睐那些可量化、可打榜、可成为公关头条的硬指标（例如在未公开测试集上的解题成功率）。

当算力被无节制地用来单点优化“解出更多题目”时，原本凝聚在一起的数学目标开始急剧发散。

为了看清这种发散，陶哲轩以“解题流水线”的五重进化做了一场精妙的解剖：

第一阶段（原始目标）：制造尽可能多的证明。结果迅速崩溃——垃圾邮件里塞满了声称证明了黎曼猜想的荒谬手稿。
第二阶段（形式化验证）：制造证明并通过 Lean 等工具形式化机检。然而，机器跑通的数千行证明可能晦涩如天书，连生成它们的提示词作者都无法理解其内在机理。如 Erdős 猜想题库中积压的大量 AI 提交，陷入了“机检全绿、人类失语”的悬空境地。
第三阶段（清晰表达）：不仅正确，还要行文流畅。可正是在这一步，现代大语言模型暴露出了极其隐蔽的认知陷阱。

被抹平的“自然摩擦力”：过于顺滑的证明，为何学不到东西？

今天的 AI 已经能够写出语法无瑕、排版精致的数学论述。但陶哲轩指出，AI 产出的数学写作往往陷入了“过于顺滑（Too Slickly Written）”的病态。

在大语言模型的笔下，平凡琐碎的代数变形被浓墨重彩地铺陈，而最核心、最具突破性的本质飞跃却被一笔带过。更致命的是，它抹杀了人类思考中不可或缺的“自然摩擦力（Natural Friction）”。

在人类数学家撰写的经典论文中，作者感到困难的地方总是会留下清晰的“摩擦痕迹”：一句充满警惕的批注、一个极其小心翼翼的辅助引理、一段突然变得凝重的符号记法，或者一段明显经过反复推敲重写的艰涩段落。

这些看似不够优雅的摩擦力，恰恰是同行之间传递隐性知识（Tacit Knowledge）最高频的信道。 它像悬崖边上的防滑标记，无声地提醒读者：“请在这里放慢脚步，真正的深渊与宝藏都在这里。”

陶哲轩在论文中特意晒出了自己年轻时研读菲尔兹奖得主让·布尔甘（Jean Bourgain）1991 年论文时的复印件。泛黄的纸页上密密麻麻地写满了他当年的困惑、问号与挣扎批注。正是通过与那些艰深晦涩、充满阻力的手迹贴身搏斗，年轻的陶哲轩才得以穿透符号，真正领悟了布尔甘那种独特的数学直觉。

如果让 AI 来重写布尔甘的论文，它或许会把每一个公式打磨得光洁如镜，剔除所有“不规范”的措辞。然而，当人工摩擦（拼写与排版瑕疵）与自然摩擦（思想的险峻转折）被一并砂纸打磨殆尽时，留下的只是一篇**“读起来毫无阻碍，读完后毫无所得”**的空心文本。

正如数学大师威廉·瑟斯顿（William Thurston）早在 1994 年的名篇中写道的那样：“我们不是为了完成定义、定理和证明的抽象生产配额。衡量成功的标准是：我们所做的事情是否让人们能更清晰、更有效地理解和思考数学。”

证明泛滥时代：从“定理经济”退守“正典化”终局

当解题流水线继续推进，我们便来到了最深邃的两个阶段：社区消化（Proof Digestion）与范式化正典（Canonicalization）。

我们正在经历一场从“证明匮乏（Proof Scarcity）”向“证明泛滥（Proof Abundance）”的根本性转向。在过去，证明是稀缺的珍宝；而在未来，机器生成的证明将如同工业流水线上的标准化构件一样廉价喷涌。

随之而来的是整个学科生态的“阻抗失配”与“消化不良”：

AI 生成证明的速度，远超人类的验证速度；
形式化机检通过的证明，远超人类撰写深度综述的速度；
即使行文优美的正确证明，也已经彻底击穿了依赖学者无偿劳动的志愿同行评审网络；
泛滥的已发表成果，超出了人类文明将它们提炼进经典教科书的吸收带宽。

现有的期刊出版、职称晋升、优先权争夺等学术制度，全都是建立在“证明是稀缺品”的底层假设之上的。当供给无限膨胀，单纯“给出一个证明”的技术杂耍将迅速丧失溢价。

这与我们在现代软件工程中观察到的现象如出一辙——当大模型能够一秒生成上千行语法正确的代码时，代码本身不再是资产，而是负债；真正稀缺的壁垒，永远是人类对复杂系统架构的全局理解与克制取舍。

在数学的终局里，最高阶也是最不可替代的工作，是范式化（Canonicalization）。

它指的是一个重大猜想被攻克后，学术界花费数十年乃至上百年时间，剥除最初证明中笨拙冗余的脚手架，找到那个“最正确、最自然、最具穿透力的普适证明”，并将其编织进人类知识的正典体系中。这需要极其广泛的群体共识与代际沉淀，是 AI 最难优化的部分。

甚至可以说，今天所有前沿 AI 模型之所以具备数学推理能力，其全部养料正是人类数百年间辛勤完成的“正典化理论体系”。

黄金判据：向机器证明索要“人类的理解”

面对 2026 年 6 月国际数学联盟背书的《莱顿宣言》（Leiden Declaration），陶哲轩给出了一个极为朴素却切中要害的实操判据（Rule of Thumb）：

“如果论文作者无法令人信服地就其成果做出一场清晰、深入、正确且溯源完整的专家级学术报告，那么这项成果就不应该被发表。”

哪怕一份长达万行的机器证明在 Lean 编译器里绿灯全亮，只要没有任何人类能够站上讲台把背后的核心思想向同行解释清楚，它在本质上就依然是一份“未完成的半成品”。

这项黄金判据不仅是对数学期刊审稿防线的重构，更是给所有身处 AI 时代的智力工作者划出的一道精神底线：

拒绝无痛的顺滑，主动拥抱认知的阻力：如果在学习与研发中没有经历过困惑、推演与修正的“自然摩擦”，那么你所获得的只是信息的伪装，而非心智的升级。
警惕指标套利，将精力投注于意义的范式化：在算力泛滥的浪潮中，跑通一个 Demo、生成一个片段永远是廉价的。把离散的机器产物消化、重构、提炼为能够启迪他人的体系化知识，才是不可剥夺的人类尊严。

证明可以由算力无限廉价地制造，但理解与意义，永远只能在人类心智的摩擦与共鸣中诞生。

面对数以千计由 AI 形式化验证通过却无人能读的机器定理，你认为学术界应该优先投入精力去“消化”它们，还是任由它们作为算力档案静默沉睡？欢迎在评论区留下你的思考。