陶哲轩重磅发声：只会解题没用了新智元

陶哲轩最新判断，数学正在从「证明稀缺」进入「证明过剩」时代——数学家最值钱的工作已不再只是「做出证明」，而是验证它、消化它，并把一块 AI 吐出的「生肉证明」变成人类真正吃得下的知识。

最近，陶哲轩在 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），反而可能产生一个「负面效果」——它杀死了人们继续研究这个问题的兴趣。