陶哲轩警告：AI可能把数学推向“证明过剩”，多到没人看得懂

陶哲轩给 2026 年国际数学家大会写了篇文章，核心意思是：数学界该停止争论 AI 能做什么，转而面对一个一直被绕开的问题——我们做研究到底是为了什么。

他把当下类比成 1900 到 1930 年那段时间。罗素悖论和哥德尔不完备定理把整个数学基础掀了个底朝天，逼着这门学科重新想清楚”什么算证明”。他认为现在是同一量级的时刻。

他引了 First-Proof 项目的数据。第二轮里放了 10 道未发表的研究级题目，让 4 个 AI 系统去做，结果 7 道至少被其中一个系统给出了合格的解答，每道题的成本从几十美元到几百美元不等。这个成本区间是关键——如果一个新定理的边际成本是两百美元，那么产出速度会以什么曲线增长，不难推算。

陶哲轩的担心不是”AI 会取代数学家”，是数学可能从”证明稀缺”翻转成”证明过剩”。过去几百年，数学的组织方式建立在证明很难产出这个前提上：同行评议、期刊、引用网络，都是筛选稀缺品的机制。当证明变得便宜且海量，这套机制会直接过载。

他提了一个判据，我觉得是全文最有分量的一句：没人能清晰讲解的证明，即便通过了形式验证，也应该视为不完整。这句话把数学的目的重新拉回到理解上，而不是正确性上。机器可以验证一百万行的 Lean 代码确实无误，但如果没有任何人类能说清楚这个定理为什么成立，数学作为一种人类知识的意义就被掏空了。

这个立场在计算机辅助证明的圈子里会有争议。四色定理当年就是这么过来的，几十年过去，大家慢慢接受了”人看不完的证明也是证明”。但四色定理只有一个，如果每年冒出几万个这种东西，情况就完全不同了。

值得一提的是，陶哲轩本人一直是 AI 辅助数学最积极的实践者之一，他不是站在外面唱衰。这种从内部发出的警告，通常比外部的批评更值得听。