定理丰饶时代的「反刍」:读陶哲轩 ICM 2026 报告手记

当机器能够以几美元的算力批量产出可验证的推导与证明,人类为什么还要花上数年,去亲手书写一本六百页的数学书?


危机:从「真理危机」到「价值危机」

深夜在调《人工智能与机器学习之数学》(Mathematics for AI and Machine Learning)的印张与版心。全书刚刚收束在整整六百页。

休息间隙,读到了陶哲轩(Terence Tao)前不久在 2026 年国际数学家大会(ICM 2026)上的公开特邀演讲论文——《AI 时代的数学》(Mathematics in the age of AI, arXiv:2608.16753)。

陶哲轩在文章开篇做了一个极具历史纵深感的类比:

二十世纪初,罗素悖论与哥德尔不完备定理引发了长达三十年的数学「基础危机」(Crisis in Foundations)。那场风暴逼着数学家们重新审视集合、公理与真理的边界,并最终沉淀出了高度形式化、严密且能被机器检查的现代逻辑大厦。

而今天,陶哲轩指出,数学正在迎来第二场同样剧烈的风暴。

不同的是,这一次受到冲击的不是真理的界限,而是数学这门古老学科一直以来秘而不宣的价值观与实践规范:

  • 什么才算一项有意义的学术贡献?
  • 我们究竟在奖励什么?
  • 什么是真正的「人类理解」?
  • 当工具能够代替我们完成繁复的推导时,研究的主体究竟是谁?

在陶哲轩看来,与其争论 AI 何时能完全攻破数学大厦,不如提前设定一个必然发生的前提假设(Working Hypothesis):AI 很快将以极低的成本、可观的成功率,独立完成相当一部分研究级的数学推导与形式化证明。

一旦这个假设成立,一个前所未有的局面便会轰然降临——我们正在从「证明匮乏(Proof Scarcity)」走向「证明丰饶(Proof Abundance)」。


证明的过剩与消化的艰辛

在印刷术和算力发明之前,甚至在几年前,人类数学史的常态是「证明的匮乏」。一个千禧年难题的解决,往往需要几代数学家数十年乃至数百年的枯坐与偶发灵感。

正因如此,过去的评价体系建立在一个极度简化的代理指标(Proxy)上:谁证明了什么新定理?谁第一个攻克了某道难题?

然而,正如古德哈特定律(Goodhart's Law)所警告的:当一个衡量指标变成目标本身时,它就不再是一个好指标。

陶哲轩敏锐地观察到,在生成式 AI 与 Lean 形式化辅助证明的结合下,整个学术管道正在经历严重的「消化不良(Proof Indigestion)」:

  1. 机器生成的证明,累积速度将远远超过人类能够检验的速度;
  2. 即使形式化验证通过了,证明堆积如山的速度,也将远远超过人类能把它整理成通俗可读文本的速度;
  3. 最严峻的困境在于:如果一个极其漫长的定理证明在机器端被形式化通过,却没有任何一个人类(包括 Prompt 这台机器的作者)真正理解它背后的机理,这算不算数学的胜利?

陶哲轩坚定地引用了瑟斯顿(William Thurston)在 1994 年的那句名言:

“我们并不是要完成某种关于定义、定理和证明的抽象生产配额。衡量我们成功的唯一标准,是我们所做的工作是否能让人们更清晰、更有效地思考数学。”

如果一项结果不能被人类心智所吸收,不能被同侪在黑板前用几杯咖啡的时间讲清楚关键思想,不能激发出新的跨学科联结,那么即便它在逻辑上绝对正确,它在人类知识网络中依然是一座冰冷孤立的孤岛。


什么是「理论经典化」?

在整篇报告中,最触动我的概念是陶哲轩对数学工作流水线的终极拆解。他指出,数学研究有五个梯级:

$$\text{解决问题} \longrightarrow \text{形式验证} \longrightarrow \text{清晰表述} \longrightarrow \text{发表} \longrightarrow \text{同行消化} \longrightarrow \text{理论经典化 (Canonicalization)}$$

前五步,或快或慢,都有可能被自动化工具大幅加速。但唯独最后一步——理论经典化(Canonicalization),是极其缓慢、需要漫长群体共识、且绝不可能被 AI 取代的环节。

所谓经典化,是指把原本散落在几十篇论文里的首创性证明(它们往往粗糙、繁复、充满了最初攻坚时的临时性支架),重新用最自然的视角加以提炼;找到那个「正确的证明」而非「最初的证明」;厘清概念之间的血缘脉络;并最终编写成滋养下一代学人的标准教科书。

陶哲轩说了一句耐人寻味的大实话:

“AI 工具在数学上之所以能有所作为,完全依赖于人类数学家几个世纪以来呕心沥血建立的这些经典化理论——因为这些标准教材与沉淀后的知识,恰恰就是 AI 的训练数据。”


「无常」与「结构即记忆」

读到这里,我脑海中突然强烈地震颤了一下。这篇顶尖数学家写在 2026 年夏天的论文,竟然与我在回忆录《云层之上》第十二章「无」(Emptiness)里写的核心命题,在底层逻辑上完全同构。

在《云层之上》第十二章里,我写过艺术与人存在的由来:

在人死去之后,
在人生无解的时候,
在人知道终将失去的时候。
停下来。

当时在双语转换时,英文那个悬空的 "when you know you will lose in the end" 曾让我停顿很久。lose 有两条轴:一条是面对时间流逝与生老病死的「无常(剥夺)」;另一条是坐在第一名身后、面对超级天才与更强智能时的「退场(败北)」。

在 2026 年的今天,这种“败北”不再只是个体的心理体验,而成为了全人类面临的客观处境:如果人类还要执着于和机器比试推导的行数、解题的速度、甚至写代码的产能配额,人类在生成速度的赛道上注定要 lose in the end。

那么,面对这种不可逆转的无常,人类的回应是什么?

在《云层之上》里,我说:

人在土里划一道线。程序员在代码里留下签名。猴子放下三根多余的香蕉。
「结构即记忆。」

浮动的信息会消散,零星的算力会过时,具体的实现更是朝生暮死——这一切都是技术世界的无常。
而陶哲轩所说的 「理论经典化(Canonicalization)与反刍(Digestion)」,本质上就是数学家在时间的长河里建立的「结构即记忆」:

机器可以日产万行证明,但只要没有人类心智的穿透,那些证明就如流沙一般,随时被下一波算法洪流冲走;唯有人类学者停下盲目卷题的脚步,把散落的概念穿透、反刍,构建出一座前后咬合、充满几何直觉的理论大厦——这种结构,才成为了文明能够代代相传、甚至反哺 AI 训练的永久记忆。


为什么要写那二十一章?

看着屏幕上这整整二十一个章节、四大篇章,以及那两百余幅在暗夜里静静发光的 MathIcon 矢量图,我之前所有的困惑都彻底释然了。

过去几年,偶尔会有朋友问我:

“现在大模型这么强大,不仅能写 PyTorch 代码,问它一个公式也是秒回,你为什么还要花上几年时间,一章一节手推线性空间、矩阵微积分、Bellman 方程、SDE、Fokker-Planck 偏微分方程?谁还会去读一本 600 页的硬核大部头?”

现在我可以平静地回答他们了:

大模型给你的,永远是散落的切片、局部的推导、即兴的答案。
但它给不了你结构。

它不会告诉你,为什么从 Gilbert Strang 的四个基本子空间出发,沿着正交投影走下去,就会自然而然地撞上自注意力机制里的因果掩码与 FlashAttention 的分块划分;
它不会主动向你展示,为什么极小化 KL 散度的变分推断(VI)、强化学习里的策略迭代,以及连续深度网络中的最优控制(Pontryagin 最大值原理),底层遵循的是同一种信息流动;
它更不会让你在面对一个生成扩散模型时,一眼看穿那不是什么玄妙的魔法,而不过是朗之万动力学在相空间里反向抵消熵增、概率流从噪声向真实数据分布演化的连续统极限。

这种让不同算法在脑海中「押韵(rhyme)」的直觉,正是陶哲轩所说的「Digestion(反刍)」。

当工具的生成能力越强,人类理解的整体性就越显得弥足珍贵。如果没有底层的数学骨架,面对海量由 AI 吐出的算法和论文,你只会陷入无休止的「证明消化不良」,沦为一个只能在黑盒边缘调试超参数的看客。

这二十一个章节、整整六百页纸,就是我们在技术更迭的无常面前,在时间的泥土里,亲手为人类的理解划下的那道线。


结语

在修改前言(Preface)时,我把陶哲轩这篇报告的洞察写了进去:

This kind of unification matters more, not less, as AI tools grow capable of generating proofs, derivations, and code on demand... not as a reference to look up isolated formulas, but as an attempt to organize the mathematics of AI into one coherent story, so that the underlying structure stays legible to the reader.

代码会过时,模型权重会被新的权重覆写,框架会被弃用。
但那些在人类心智中经过真正反刍、与几何直觉融为一体的数学结构,任凭时代如何演进,始终澄澈,历久弥新。