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

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

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

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

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

一夜之间，AI正以前所未有的速度疯狂输出数学证明。但问题也随之而来——

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

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

• 证明生成（Proof generation）
  ：将一个猜想从“未解决”状态，推到“有解”的彼岸。

• 证明验证（Proof verification）
  ：确认这个解是正确的，逻辑链条严密无瑕。

• 证明消化（Proof digestion）
  ：将证明读懂、讲透、提炼出核心思想与方法论，让整个领域都能从中受益。

在过去几百年里，这三件事基本由同一群人包办——

三个环节紧密咬合，不存在明显的速度差或“瓶颈”。

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

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

陶哲轩用一个精准的工程学术语来形容这种错位：

三个环节的速度严重失调了：

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

在

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

而在

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

回到数学领域，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小时内验证了证明的核心思路，随后将其扩展、重组、打磨，最终揭示出这个证明背后隐藏着一条更深层的联系——

它解决的不仅是“对不对”的问题，更是“它意味着什么”的问题。

陶哲轩认为，#1196是目前唯一一个生成、验证、消化三阶段都基本跑通的典型案例。也正因如此，他反复强调一个核心原则：

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

三处表态，同一判断

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

正式提出“证明稀缺→证明过剩”的范式级判断。

他对记者Da vide Castelvecchi表示，数学家的“岗位描述”正在改变。一个拒绝接触AI工具、只想用传统方式做证明的研究生，未来可能会发现自己的机会越来越少。真正能繁荣发展的，是那些在深厚传统数学功底之上，还能熟练运用新工具的人。

他与Klowden花费超过一年写成这篇论文，试图超越眼前的技术细节，直面更根本的哲学问题——数学证明的本质是什么？论文的目的是什么？我们这个职业存在的意义是什么？他在文中写道：

三处表态，指向同一个内核：

更大的震荡：学术评价体系面临重写

如果只是数学家的工作方式改变，那或许还是一个学科内部的事。但陶哲轩看到的远不止于此。

当AI将证明的生成成本压到近乎为零，当Lean/Coq等形式化引擎将验证过程大幅自动化，“证明消化”这个环节的价值将被彻底重估。

过去，消化证明是“免费的”。你证明了一个定理，自然会理解它，并在论文中解释它。这份劳动从未被单独计价。

但当证明的生产者（AI）和理解者（人类）被拆分开之后，

这意味着，整个学术声望的分配逻辑将要改变。

引文（Citation）体系、论文评审标准、奖项评选规则，甚至招聘和晋升的依据——所有这些围绕“谁先证明了什么”建立起来的激励结构，都将面临重构。

陶哲轩预测：就像现代社会不再把生食原料当作一顿饭一样，

AI for Math所引发的这场范式漂移，将成为所有

的预演——理论物理中的计算验证、密码学中的安全性证明、软件工程中的形式化验证……所有依赖“正确性论证”作为核心产出的领域，都将面临同样的“阻抗失配”。

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

证明的时代没有结束。

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