陶哲轩 ICM 重磅演讲震动数学界：AI 正把证明“喂到撑死”，百年一遇的价值危机来了

luyuanhong

陶哲轩 ICM 重磅演讲震动数学界：AI 正把证明“喂到撑死”，百年一遇的价值危机来了

原创  AGIWords  代码绝笔  2026 年 8 月 10 日 17:11  北京

2026 年 7 月 24 日，费城，全球最大的数学家聚会，国际数学家大会（ICM）的公开讲座环节，一个让全场安静下来的词，被菲尔兹奖得主陶哲轩缓缓投到大屏幕上：

Proof Indigestion（证明消化不良）。

这场演讲没有发布新定理，也与又一篇“AI 解出未解难题”的喜报无关。

数学界顶级大脑发出了一封警告信：AI 产出证明的速度，已经快到人类消化不了了。


▲ 陶哲轩 ICM 2026 公开讲座封面：《Mathematics in the age of AI》

从“饥荒”到“撑死”：数学正经历什么？一个根本性的翻转已经发生

过去几百年，数学是一门证明极度稀缺的学科。

一道未解问题可能悬在那里几十年、上百年，等待某位天才在某个灵光一闪的下午写出关键突破。

谁先解出，谁就登上荣誉殿堂。

期刊围绕“第一个证明”分配版面，评审围绕正确性展开，教科书围绕“经典定理”组织章节。

整套系统，都建立在“证明很贵”这个隐含假设之上。

然后 AI 来了。

陶哲轩在讲座中展示了一组受控实验数据：First Proof 项目第二批测试中，十道全新研究级数学问题交给四个 AI 系统，结果七道被做到了发表级质量，每题的算力成本大约在 10 到 1000 美元之间。


▲ 核心幻灯片：若工作假设成立且无政策调整，将出现“proof indigestion”，红字标出 proof scarcity → proof abundance

十美元，一道研究级数学题。

数学正由证明稀缺时代一脚踏入证明过剩时代。

而稀缺时代精心搭建的一切制度，谁获得荣誉、谁负责审稿、谁决定教科书收什么，全部开始阻抗失配。

生一个孩子容易，养大才难

陶哲轩把问题拆成了一条清晰的流水线：

证明生成 → 验证 → 阐述 → 发表 → 消化 → 典范化


▲ ICM 幻灯片：从 Open Problems 到 Definitive Solutions 的完整流水线

前两步，生成和验证，正被 AI 与形式化工具急速压缩。

Lean 这样的证明助手能在逻辑层面自动检查每一步推理是否成立，效率堪比编译器检查代码。

但后面四步呢？

阐述要有人写成人话，发表要过同行评审，消化要被领域深入理解，典范化要进入教科书和标准理论。

这些步骤，每一个都极慢，每一个都需要人类大脑深度参与。

2026 年 8 月 4 日，陶哲轩在 Mathstodon 上打了一个比方：证明像新生儿。

生成只是出生，你还得把它养到成年，教科书级的正典证明。

有些人（或公司）用 AI 生成并验证了证明之后就扔下不管了，像是只负责生、不负责养的父母，把后续照料全甩给社区志愿者。

他更早时候还用过一个更辛辣的食物类比：稀缺社会里，谁把猎物带回营地最受尊敬；

但到了食物充裕的聚会上，一个陌生人扔下一块来历不明的生肉让别人去洗、去切、去烹饪，这不叫贡献，这叫添乱。

“百年一遇的危机”，落在价值基础

讲座开篇，陶哲轩把当前动荡类比为 1900–1930 年的数学基础危机：罗素悖论、哥德尔不完备定理……那次危机逼迫数学家把“集合”“无穷”“公理”这些模糊概念全部重新显式化，阵痛三十年后得到了 ZFC 公理体系。

但他紧接着强调：这一次出了问题的是价值基础，逻辑基础仍然稳定。

什么意思？

历史上，数学的诸多目标，解题、建理论、理解世界、培养后人、审美创造，基本正相关。

你在一个方向努力，其他方向也跟着受益。

但 AI 介入后，古德哈特定律开始生效：当“解出多少道题”变成可被单独优化的指标，它就不再是好指标了。

你可以用 AI 横扫一千道未解问题的形式证明，但如果没人理解、没人消化、没人教授，数学作为人类文明的共有理解，进步仍无从谈起。


▲ 讲座的条件框架：“工作假设”明确声明后续分析是条件推理，不要求听众相信 AI 一定做到

这就是他所说的“目标撕裂”：当某一目标被机器廉价满足，其余目标不再免费搭便车。

社交媒体：谁在转发，谁被忽略？

讲座幻灯片上传后，“proof abundance”那张图迅速刷屏。


▲ 数学家 Alessandro Della Corte 提醒：陶哲轩对未来能力的表述非常谨慎，但网上的反应好像“证明过剩”已是既定事实

但有一张幻灯片，几乎没人转。

那张幻灯片上写的是：如果人类作者无法就结果做一场令人信服的专家级报告，则该结果不应发表。


▲ 大家只转“过剩”那张，不转“做不了报告就别发”那张，毕竟氛围数学（vibe-mathing）做不到后者

这条回复精准地刺穿了讨论中的选择性引用：人们对“ AI 太强了”的焦虑与兴奋爱不释手，却本能地回避了陶哲轩所设的行为门槛。

他主张负责任地使用 AI

陶哲轩从未主张停止使用 AI 。

他在讲座中引用了莱顿宣言（Leiden Declaration on Artificial Intelligence and Mathematics，2026 年 6 月，国际数学联盟背书），作为共同体书写自身价值规范的起点。


▲ 莱顿宣言官网：数学共同体试图在产业节奏之外，自己定义“负责任使用”的语言

他的方向性建议极其务实：

● 声望迁移：把更多荣誉分配给完成验证、阐述并将证明推进到教科书阶段的人。

● 发表门槛：以“能否做专家级报告”作为经验闸门。

● 披露规范：最坏情况是隐蔽使用 AI 以逃避同行批评。

● 新角色：把丑陋的机器证明改写成人类可理解文本的“翻译者”，可能是未来的稀缺工种。

“AI 饮食”：你不会饿死，你会撑出病

在教育侧，陶哲轩同样敲响警钟。

他把 AI 比作食物历史的翻版：人类摆脱饥荒、食物充裕后，迎来的还有肥胖、糖尿病与运动不足。

当 AI 可靠到可以替代思考过程本身，它可能成为认知代餐：学生失去耐心、失去承受失败的能力、失去被真实批评锤炼的机会。

他列出的教育伤害清单包括，作弊、技能退化、耐心萎缩、谄媚输出导致无法接受真反馈，以及“权威感的腐蚀”。

这和研究侧的“消化不良”共享同一结构：当生成便宜，稀缺的是有益的摩擦。

为什么你该在意

即使你身处数学界之外，也请留意一条已经在社交媒体上引发共鸣的推论：

“证明消化不良将冲击每个行业。生成变便宜了，验证没有。总还得有人去读。”


▲ 评论者将“proof indigestion”推广至所有知识生产：代码、法规、报告、论文……

代码审查跟不上代码生成。

法规草案跟不上 AI 起草。

研究报告堆积如山却无人通读。

“消化不良”早已越出数学，成为整个知识经济在 AI 加速后必须面对的结构性病症。

陶哲轩不过是在他最熟悉的领域，第一个把这个词说出来的人。


▲ “Proof abundance creates proof indigestion”，术语在社区中的凝练表达

尾声：直升机可以把你送到山顶，但你错过了沿途所有的路标

陶哲轩用过一个登山比喻：AI 像直升机，能直接把你空降到山顶。

你到达了，但你没钉路标、没画地图、没留下任何后人可以循着走的东西。

而这些被跳过的中间过程，往往才是科学最珍贵的产出。

数学正站在一个岔路口。

一条路是“让 AI 扫荡一切未解问题，堆出论文山”，另一条是“重新定义什么算完成，让理解回到核心”。

2026年 夏天，这位当世最受尊敬的数学家用整场 ICM 讲座告诉同行们：

不要只追求喂饱，要追求消化。

代码绝笔