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

数学正在从证明稀缺时代，进入证明过剩时代

最近，数学界被陶哲轩在Mastodon上抛出的一记重磅判断所震动——

数学，正从证明稀缺的时代，大步跨入证明过剩的时代（from an era of proof scarcity to an era of proof abundance）。

看看Erdős问题的AI贡献页面就知道了。在Github上，超过20份由AI生成的全部或部分解答，正堆积在“待评估”（pending assessment）的栏目里。

而在此之前，这个分类常年只有孤零零的一两份。

一夜之间，AI正以前所未有的速度疯狂输出数学证明。但问题也随之而来——速度太快了，快得让人喘不过气，快得根本没人来得及看。

问题求解「三件套」：生成、验证、消化

陶哲轩的洞察建立在一个极其简洁的框架之上。他指出，数学问题的求解从来不是单一动作，而是一个包含三个环节的完整链条：

• 证明生成（Proof generation）：将一个猜想从“未解决”状态，推到“有解”的彼岸。
• 证明验证（Proof verification）：确认这个解是正确的，逻辑链条严密无瑕。
• 证明消化（Proof digestion）：将证明读懂、讲透、提炼出核心思想与方法论，让整个领域都能从中受益。

在过去几百年里，这三件事基本由同一群人包办——你证明了一个定理，你自然理解它，然后你撰写论文来解释它。三个环节紧密咬合，不存在明显的速度差或“瓶颈”。

但AI的介入彻底打破了这种平衡。

生成环节被大语言模型（LLM）大幅加速；验证环节有Lean、Coq等形式化验证工具兜底。唯独第三个环节——那个需要人类大脑去深度理解“这个证明到底意味着什么”的消化环节——其速度依然如故，完全跟不上前两者的步伐。

陶哲轩用一个精准的工程学术语来形容这种错位：阻抗失配（impedance mismatch）。

三个环节的速度严重失调了：证明像洪水一样涌来，但理解的堤坝还是手工砌筑的。

他打了个比方。想象两种社会：

在食物稀缺的社会，最受尊敬的是猎手和农夫，是那些能把食物带回家的人。你带回一头鹿，无论肉质如何，整个部落都会感激你，并有人主动帮你处理、烹饪。几乎任何无毒的食物贡献都受欢迎。

而在食物过剩的社会，情况截然不同。想象一个每人带一道菜的聚餐派对。如果一个陌生人闯进来，扔下一块来路不明的生肉让大家自己处理，没人会高兴。即便是超市买的预包装食品，也只是勉强算数。真正受欢迎的，是社区里受信任的成员精心烹制的家常菜——不仅因为美味，更因为围绕这道菜的交流本身就是社交的一部分，也是培养下一代厨师的机会。

回到数学领域，AI跑出来的那些“生肉证明”（raw proof），就像是被陌生人扔在派对上的神秘肉块。

它可能是正确的，甚至可能通过了形式化验证。但问题在于，没有人清洗过它、烹饪过它，更没有人能告诉你它到底味道如何。

陶哲轩直言不讳：这种未经处理的“贡献”，不仅难以切实推动问题的实际进展，反而可能产生一个“负面效果”——它扼杀了人们继续深入研究这个问题的兴趣。

问题被宣告“已解决”了，但没人真正理解这个解。好比一道菜被端上桌，却无人敢动筷子。于是，这道菜——连同围绕它可能激发的所有对话与灵感——就这样凉掉了。

Erdős #1196：唯一跑通「三件套」的案例

任何理论都需要一个切片来检验。陶哲轩反复提及的那个切片，就是Erdős问题#1196。

这是一个关于“本原集”（primitive sets）的猜想：在一个整数集合中，如果没有任何一个元素能整除另一个元素，那么对所有元素a按1/(a·log a)求和，当集合元素趋于无穷大时，这个和是否趋近于1？

该猜想由Erdős、Sárközy和Szemerédi于1968年提出。

此后近60年，数学家们不断逼近答案。斯坦福数学家Jared Lichtman曾花费数年证明了一个相关的上界（约1.399），但最终的渐近猜想始终悬而未决。

转机出现在2026年4月的一个周一下午。23岁的Liam Price将这道题丢进了GPT-5.4 Pro。

Price没有数学博士学位，也没有多年的专业训练。他使用的工具，是一个月费20美元的ChatGPT Pro订阅——几乎任何人都能获得。

80分钟。

模型走通了一条被数学界忽视了近90年的路径：它巧妙地结合了冯·曼戈尔特函数（一种经典的解析数论权重函数）与马尔可夫过程理论，构造出了一个全新的证明框架。这个技术组合本身已存在数十年，但从未有人想到将其应用于本原集问题。

证明生成了。但如果故事到此为止，它不过又是一块无人问津的“神秘肉”。

关键在于接下来的发展：陶哲轩亲自下场了。

他在24小时内验证了证明的核心思路，随后将其扩展、重组、打磨，最终揭示出这个证明背后隐藏着一条更深层的联系——在“整数解剖学”（integer anatomy）与马尔可夫过程理论之间，架起了一座此前从未被描述的全新桥梁。

这就是证明消化（proof digestion）。它解决的不仅是“对不对”的问题，更是“它意味着什么”的问题。

陶哲轩认为，#1196是目前唯一一个生成、验证、消化三阶段都基本跑通的典型案例。也正因如此，他反复强调一个核心原则：理想状态下，应由同一批人完成全部三件事。

然而现实是，越来越多的人在用AI生成证明后，没有时间或能力去完成验证和消化，便直接提交了。这正是Erdős问题页面堆积了20多份待评估方案的直接原因。

三处表态，同一判断

陶哲轩并非在一处随口说说。他在几乎同一时期，通过三个不同渠道发出了同一个强烈信号。

4月27日，Mastodon长帖：正式提出“证明稀缺→证明过剩”的范式级判断。

4月27日，《自然》杂志访谈（The job description is changing）：他对记者Da vide 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所引发的这场范式漂移，将成为所有强证明型学科的预演——理论物理中的计算验证、密码学中的安全性证明、软件工程中的形式化验证……所有依赖“正确性论证”作为核心产出的领域，都将面临同样的“阻抗失配”。

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

证明的时代没有结束。

但“证明即一切”的时代，正在落幕。

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