AI「生肉证明」堆爆GitHub！陶哲轩重磅发声：只会解题没用了

最近，陶哲轩在 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 的范式漂移，将成为所有强证明型学科的预演——理论物理中的计算验证、密码学中的安全性证明、软件工程中的形式化验证——所有依赖「正确性论证」作为核心产出的领域，都将面临同样的「阻抗失配」。

证明会越来越多，越来越快，越来越便宜。

证明的时代没有结束。

但「证明即一切」的时代，正在落幕。

未来属于那些不仅能「算出来」，更能「讲明白」的人。

参考资料：

https://mathstodon.xyz/@tao/116477351524980995

https://mathstodon.xyz/@tao/116450581967483825

https://www.nature.com/articles/d41586-026-01246-9

https://terrytao.wordpress.com/2026/03/29/mathematical-methods-and-human-thought-in-the-age-of-ai/

文章来自于微信公众号 "新智元"，作者 "新智元"