夜雨聆风数学，人类理性皇冠上最硬的那颗宝石，正在被撑到胃痉挛。
新的麻烦来自证明过剩：证明太多了
2026年7月24日，费城四年一届的国际数学家大会（ICM），数学界的"奥运会"，菲尔兹奖在此颁发，全球数学共同体最盛大的聚会。台上站着的是陶哲轩，UCLA教授，2006年菲尔兹奖得主，被媒体称为"数学界的莫扎特"，当今在世最具影响力的数学家之一。
他谈的却是AI成功之后的代价
他说：数学正在进入一场"证明消化不良"（proof indigestion），AI能以几百到几千美元的成本批量产出研究级证明，但人类读不完、审不完、理解不了、也来不及把它们变成教科书里的知识。数学共同体正从"证明稀缺"时代，一脚踏进"证明过剩"时代。
问题随之逼近：有没有可能，一个重大数学结果的证明已经被机器验证为正确，却没有任何活着的人类能解释它在说什么？
▲ 陶哲轩ICM 2026公开讲座《AI时代的数学》封面页
一、一道"消化不良"的诊断书
陶哲轩的演讲标题是《Mathematics in the age of AI》。52页幻灯片略过炫技式演示，开篇就把当前局面比作上一次数学界的存在危机，1900年前后的基础危机。那一次，罗素悖论炸碎了集合论的地基，哥德尔定理永久划定了形式系统的天花板。整个学科被迫停下来，追问最基本的问题：什么是数、什么是证明、什么是无穷。
结果呢？数学没有崩溃，反而因为被迫"把隐含的规矩写成白纸黑字"，变得更强韧了。
陶哲轩说，今天这场湍流指向价值观与实践的危机。AI来了，我们突然需要回答一些原本不必问的问题：数学的目的到底是什么？解题是目的本身吗？谁来负责把一条新证明变成共同体充分"消化"了的知识？
他特别拿出经济学家熟悉的古德哈特定律提醒在场数百位数学家：当一个指标变成目标，它就不再是好指标。
过去，"解更多题"、"建新理论"、"培养学生"、"创造美的证明"，这些目标大致同向。你解了一个好问题，过程中你理解了它、写清楚了它、也顺带训练了学生。但AI把"解题"这个单一维度优化到极致之后，这些目标开始分叉。就像一家公司疯狂刷GMV却不管复购和利润一样，指标在涨，系统在坏。
▲ 陶哲轩展示的"证明全生命周期管道"：从未解问题到经典化，中间有六道关卡
二、六道关卡，五道在堵
陶哲轩把一条数学证明从"诞生"到"成为人类知识"的过程拆成了六个阶段：
生成 → 核验 → 阐述 → 发表 → 消化 → 经典化
这个拆法本身就是洞见以前我们觉得"证明出来了"就大功告成，现在他告诉你：证明被写出来，只不过是旅程的第一步。
AI和形式化工具（如Lean证明助手）正在加速前两步：生成变得便宜，核验可以用机器完成。幻灯片引用了First Proof项目的数据，这个独立评估计划在受控条件下让AI挑战全新的研究级问题，十道题中有七道被至少一支团队做到了可发表质量，单题成本仅10到1000美元。
▲ First Proof项目：独立、透明地评估AI在研究级数学中的真实能力
但后面四道关卡全在堵车
阐述，AI写的证明在拼写语法上近乎完美，却常常在最难、最新颖的步骤上一笔带过，在无关紧要的琐碎细节上大书特书。AI打磨过的文本还会消除一种珍贵的东西：人类作者在"自己也觉得难"的地方自然留下的摩擦感。那种"写得磕磕巴巴"恰恰是给读者的信号，"慢下来，这里是关键"。
发表，同行评议本就是瓶颈全靠志愿审稿人无偿劳动当AI草稿像洪水一样涌来，谁来审？
消化，结果被发表了，然后呢？它有没有进入其他人的工作、课程和直觉？还是只是仓库里多了一份正确的文件？
经典化，写进教科书，成为"标准知识"这是最慢、最不可能被AI替代、却对后续一切（包括AI自身进步）最有价值的环节。
陶哲轩引用了1994年拓扑学家瑟斯顿（William Thurston）的话，大意是："定义，定理，证明"的抽象产量不足以衡量数学工作的成功；人类能否因此更清楚、更有效地思考数学，才是标准。
▲ 关键页：若不做政策与文化调整，"证明消化不良"将贯穿整个管道
三、直升机送到山顶，旅程呢？
陶哲轩有一个精妙的比喻：传统数学研究像远足。你走去山顶的路上，会踩出小径、立下路标、画出地图，这些"副产品"对后来的登山者极为珍贵。AI像一架直升机，直接把你空投到山顶。结果确实到了，但旅程中那些对他人有用的东西，全丢了。
这种担忧已经有了现实案例
erdosproblems.com，一个收录传奇数学家埃尔德什留下的数百道公开问题的网站，已经堆积了大量AI生成的证明提交。许多可能是正确的，但没有足够的专家志愿者来核验。有些提交者甚至自己声明"我不够格评判这条证明对不对"。
▲ 数学博主指出：数学界正被AI证明淹没，合格评判者严重不足
更深层的担忧是：帕斯卡说过"我把信写长了，因为没时间写短"。现在AI面临同样的悖论，生成一个冗长但正确的证明，往往比生成一个简短而优雅的证明更容易。而长证明更难核验、更难阐述、更难消化。失配在每一个环节加剧
四、不止数学：每个行业的"消化不良"
X（推特）上，陶哲轩的幻灯片被大量转发。认知科学家Gary Marcus称之为"必读"，并把论点接到更广的AI讨论上：AI擅长在框架内解题，但发明框架是另一种完全不同的能力。
▲ Gary Marcus转发陶哲轩讲座，称之为"必读"
评论区最犀利的一条来自@MarcusSpillane：
"证明消化不良将冲击每一个行业，不止数学。生成变便宜了，验证没有。总得有人去读这些东西。"
▲ "总得有人去读这些东西"，点出了"AI生成一切"讨论中的盲点
这话听着耳熟吗？代码生成与code review、AI论文草稿与审稿、法律意见书与合规审查，结构完全同构：供给冲击精准砸在管道最慢的那个环节：人类的注意力。
科学出版本就有"可重复性危机"、预印本洪水、掠夺性期刊的老病。AI草稿进一步加压而数学因为"输出可自动检查"，成了AI公司最干净的成功橱窗，也因此最早撞上丰裕之后的代谢危机。
另一位评论者@0xCapexOG精准地切了一刀：
"解证明与创理论是根本不同的能力。一个在框架内优化，一个发明框架。"
▲ 解题与建理论：框架内优化vs.发明框架
五、三张处方，一条底线
陶哲轩没有停留在诊断他给出了三条实践建议：
第一，常态化披露AI协助 他最担心学者用了却藏着掖着，怕被同行看不起。他身体力行：幻灯片脚注写明"本演示文稿使用了AI辅助文字和图表"。
第二，降低"抢先解题"的权重，提高"消化"的权重。 也就是说，学术声望和资助体系要开始认真奖励那些审稿的人、写综述的人、把丑陋机器证明翻译成人话的人。
第三，一条底线经验法则：如果一个结果的作者没有能力做一场清晰、专家级、正确且归因得当的学术报告（talk）来介绍它，那这个结果不应该被发表。
▲ 陶哲轩的"报告测试"：讲不清楚就不该发表
这第三条最狠它实际上是在说：你可以用AI帮你飞到山顶，但你必须能回头给别人画出地图。画不出来？对不起，这座山你还没有"到过"
六、当正确不再稀缺，什么才稀缺？
让我们退远一步看这件事的结构
几百年来，数学的核心稀缺资源是正确的证明。找到一个正确证明是一件极其困难、极其昂贵的事。整个学术体系，期刊、教职、奖项、优先权，都围绕"谁先找到正确证明"来建设。
现在，AI正在让正确证明变得不那么稀缺。
那么稀缺资源转移到了哪里？
理解判断选对问题的品味把一堆正确的碎片压缩成一个概念的能力。决定哪些论证值得变成理论的眼光以及，让下一代人类学会这一切的教育。
这是比"AI能不能解数学题"深刻一百倍的问题。它问的是：当"正确"变得廉价，"有意义"由谁来定义？
陶哲轩的回答来自音乐，跳过了人们常说的国际象棋。电子合成可以完美复制甚至生成风格难辨的新曲，但人们仍然珍视现场音乐会，因为珍视的是人类连接。数学"其实一直是以人类为中心的"，只是从业者习惯用"数学只关乎抽象"的托词来掩饰这一点。
现在，是时候更诚实了
在讲座最后的气氛中，几百位数学家安静地看着幻灯片上的最后一行。现场既不为AI欢呼，也听不到末日式喊声。空气中弥漫着一种更微妙的情绪，一个古老学科突然意识到，它需要重新想清楚自己到底是什么。
证明从来只是路径理解才是目的
