最近，陶哲轩在 Mastodon 抛出一记重磅判断——
数学正在从证明稀缺时代，进入证明过剩时代（from an era of proof scarcity to an era of proof abundance）！
在AI对Erdős问题的贡献Github页面上，20多份 AI 提交的全部或部分解，正堆在「pending assessment」（待评估）那一栏。
而在此之前，这个分类常年只有1-2份。
一夜之间，AI 正在以令人窒息的速度疯狂输出数学证明。
问题是——没人来得及看。
问题求解「三件套」
生成、验证、消化
陶哲轩把这次的思考建立在一个简洁的框架上。
他说，数学问题求解从来不是一件事，而是三件事：
Proof generation（证明生成）：把一个猜想从「未解决」推到「有解」。
Proof verification（证明验证）：确认这个解是对的，逻辑没有漏洞。
Proof digestion（证明消化）：把证明读懂、讲透、提炼出方法论，让整个领域受益。
在过去的几百年里，三件事基本由同一拨人完成——你证了一个定理，你自然理解它，你写论文解释它。
这三个环节之间不存在「瓶颈差」。
但 AI 来了之后，情况变了。
生成环节被 LLM 大幅加速，验证环节有 Lean、Coq 等形式化工具兜底，唯独消化环节——那个需要人类大脑去理解「这个证明到底意味着什么」的环节——完全跟不上。
陶哲轩用了一个精确的工程术语来形容这种错位：impedance mismatch（阻抗失配）。
三个环节的速度不匹配了：证明像洪水一样涌来，但理解的堤坝还是手工砌的。
他说，想象两种社会。
食物稀缺的社会，最受尊敬的人是猎手和农夫——是那些「bring home the bacon」（把食物带回家）的人。
你猎回一头鹿，不管肉质如何，整个部落都会感激你，会有人主动帮你清洗、烹饪、分配。几乎任何没有毒的食物贡献都受欢迎。
食物过剩的社会则完全不同。
想象一个 pot-luck 派对（每人带一道菜的聚餐）。如果一个陌生人闯进来，扔下一块来路不明的生肉，让大家自己去处理——没有人会高兴。
甚至超市买来的预包装食品，也只是勉强算数。
真正受欢迎的，是社区里受信任的成员精心烹制的家常菜——不仅因为好吃，更因为围绕这道菜的对话本身就是社交的一部分，也是培养下一代厨师的机会。
回到数学——AI 跑出来的「生肉证明」（raw proof），就是那块被陌生人扔在派对上的神秘肉。
它可能是正确的。它可能通过了形式化验证。
但没有人清洗过它、烹饪过它、也没有人能告诉你它到底好不好吃。
陶哲轩直言：这种「贡献」不仅没有推进问题的实际进展（do not measurably advance the progress），反而可能产生一个「负面效果」——它杀死了人们继续研究这个问题的兴趣。
问题被宣告「已解决」了，但没人懂这个解。
好比一道菜被端上桌，但没人敢动筷子。
于是这道菜——连同围绕它可能产生的所有对话和灵感——就这样凉了。
Erdős #1196，唯 一跑通「三件套」的案例
理论都需要一个切片去检验。
陶哲轩反复提到的那个切片，就是 Erdős 问题 #1196。
这是一个关于「primitive sets」（本原集）的猜想：在一个整数集合中，如果没有任何元素整除另一个元素，那么对所有元素 a 按 1/(a·log a) 求和，当集合元素趋于无穷大时，这个和是否趋近于1？
1968年，Erdős、Sárközy 和 Szemerédi 提出了这个猜想。
此后将近60年，数学家们不断逼近——斯坦福数学家 Jared Lichtman 花了数年证明了一个相关的上界（约1.399），但最终的渐近猜想始终悬而未决。
2026年4月的某个周一下午，23岁的 Liam Price 把这道题丢进了 GPT-5.4 Pro。
Price 没有数学博士学位，没有多年的专业训练。他用的是一个20美元/月的 ChatGPT Pro 订阅——任何人都能用的工具。
80分钟。
模型走通了一条数学界忽视了近90年的路径：用 von Mangoldt 函数（一种经典的解析数论权重函数）结合马尔可夫过程理论，构造出了一个全新的证明框架。
这个技术组合已经存在了几十年，但从未有人想到把它用在本原集问题上。
证明出来了。
但如果故事到这里就结束，它只不过又是一块「神秘肉」。
关键在于接下来发生的事：陶哲轩亲自下场。
他在24小时内验证了证明的核心思路，随后将其扩展、重组、打磨，最终揭示出这个证明背后隐藏着一条更深层的联系——整数解剖学（integer anatomy）与马尔可夫过程理论之间一条此前未被描述的全新桥梁。
这就是证明消化（proof digestion）。
不只是「对不对」的问题，而是「它意味着什么」的问题。
陶哲轩称 #1196 是目前唯 一一个三阶段——生成、验证、消化——都基本跑通的案例。
也正因如此，他反复强调一个原则：理想状态是同一拨人完成全部三件事。
而现实中，越来越多的人在用 AI 生成证明后，没时间去验证和消化，就直接提交了。
这正是 Erdős 问题近20多份待评估方案堆积的直接原因。
三处表态，同一判断
陶哲轩不是在一个地方随口说说。
他在几乎同一时期，通过三个不同渠道发出了同一个信号。
4月27日，Mastodon 长帖：正式提出「证明稀缺→证明过剩」的范式判断。
4月27日，Nature 访谈（The job description is changing）：他对记者 Davide Castelvecchi 说，数学家的「岗位描述」正在改变。一个拒绝碰 AI 工具、只想用传统方式做证明的研究生，未来可能会发现自己的机会越来越少。
能在传统数学功底之上熟练运用新工具的人，才会真正繁荣。
3月29日，博客长文《Mathematical methods and human thought in the age of AI》：他和 Klowden 花了超过一年写成这篇论文，试图超越眼前的技术细节，直面更根本的哲学问题——数学证明的本质是什么？论文的目的是什么？我们这个职业存在的意义是什么？
他在博客中写道：如果我们自己不回答这些问题，它们就会被科技公司或经济激励机制替我们回答。
三处表态，同一个内核：数学家的核心竞争力正在迁移——从「谁先生成证明」，转向「谁能选对问题、设计工作流、验证并消化结果」。
稀缺的不再是答案，而是理解。
更大的震荡：学术评价体系要重写
如果只是数学家的工作方式变了，那还只是一个学科内部的事。
但陶哲轩看到的远不止此。
当证明的成本被 AI 压到接近于零，当证明验证被 Lean/Coq 等形式化引擎大幅自动化——证明消化这个环节的价值就会被重估。
过去，消化证明是「免费的」。
你证了一个定理，你自然会理解它，会在论文里解释它。这个劳动从未被单独计价。
但当证明的生产者（AI）和理解者（人类）被拆开之后，消化就从隐性劳动变成了显性稀缺资源。
这意味着整个学术声望的分配逻辑要变。
Citation 体系、论文评审标准、奖项评选规则、甚至招聘和晋升的依据——所有这些围绕「谁先证了什么」建立起来的激励结构，都将面临重构。
陶哲轩预测：就像现代社会不再把生食原料当作一顿饭一样，数学研究文化将不再把「未消化的裸证明」（raw, undigested proofs）视为对一个问题的解决方案。
未来的评判标准，将聚焦于一个贡献究竟在多大程度上丰富了整个领域，而非仅仅「解决」了问题本身。
而且这不只是数学一个学科的事。
AI for Math 的范式漂移，将成为所有强证明型学科的预演——理论物理中的计算验证、密码学中的安全性证明、软件工程中的形式化验证——所有依赖「正确性论证」作为核心产出的领域，都将面临同样的「阻抗失配」。
证明会越来越多，越来越快，越来越便宜。
证明的时代没有结束。
但「证明即一切」的时代，正在落幕。
未来属于那些不仅能「算出来」，更能「讲明白」的人。
