（来源：图灵人工智能）
10 月 6 日，OpenAI 在 GitHub 放出 722 篇数学手稿，归成 372 个「成果家族」，覆盖 17 个领域。一部分附 Lean 形式化证明，机器可以逐步检查每一步推导；另一部分只有文字论证，只能靠人读。
编号 003 那篇，标题里有准黎曼猜想——黎曼猜想的弱化版本，同样是悬了上百年的难题。罗格斯大学的 Alex Kontorovich 留下一句话：
「如果这是人类做出来的，立刻就是一枚菲尔兹奖，毫无疑问。」
四十八小时后，OpenAI 发布第一份更新日志：撤回 3 篇，修订 14 篇，722 变成 719。撤稿理由是一处符号错误——它让一篇的论证失效，连带拉倒两篇依赖该构造的论文。三篇撤稿，全部与霍奇猜想有关。
一枚菲尔兹奖和一个错别字，出现在同一批文件上，中间隔了两天。
如果只把它读成「AI 到底行不行」，这个故事就浪费了。真正的信息在另一个地方：每一篇都可以被检查，但没有一个人能检查完。
这不是算力问题。这是「证明」这个东西，在数量级变化之后，性质变了。
而这件事的根，比 AI 老九十五年。
一、哥德尔不完备定理
1931 年，哥德尔证明了一件事：任何足够强、一致、公理可枚举的形式系统，都存在一个句子 $G$，使得 $G$ 与 $\neg G$ 都不可证。
用一句更朴素的话说：可证的，永远少于真的。
这个命题常被讲成一个神秘结论——好像存在一个数学天堂，里面堆着我们永远够不到的真理。不是的。
哥德尔证明的是一件更朴素的事：在一个固定的符号系统里，「能推出来」比「是真的」更窄。这不是宇宙藏了东西，是语言装不下自己。
它也常被讲成「真理比证明多得多」，这句在数量上并不成立——两者都可数，一样多。真正成立的是另一种落差，而且要分层才看得见：算术命题可以按量词的复杂度分层。最底层是「存在某个 n」，这一层的真句子全都可证——因为那个 n 如果真的存在，它就在那里，你把它算出来验一遍，就是一条证明。缺口从「对所有 n」这一层开始出现，越往上越大；到顶处，算术真集穿透整个层级，没有任何一层装得下它。
这个结论对当下的讨论有一处直接后果：如果 AI 的工作是在一个形式系统里搜索证明，那么哥德尔说的不是「算力不够」，而是有些真理根本不在这个搜索空间里。
你可以把空间扩到无限，你仍然在系统内部。要够到那些真理，只能跳出去：加公理，换系统，换语言。
但这里要分清两件事。
哥德尔说的是「证不完」。2026 年 10 月发生的是「读不完」。
证不完是结构性的：任何系统都装不下自己的全部真理，这是宿命，不需要任何人付出代价。读不完是实践性的：它取决于产出速度和消化速度的比值，可以改善，也可以恶化。
哥德尔那道边界不收费。722 篇这道边界，收的是人的时间。
二、证明为什么曾经值钱
在 2026 年之前，「读不完」从来不是问题。因为证明稀缺——稀缺的东西，总有人愿意读。
价值链条很直接：证明难写，所以稀缺；稀缺，所以可署名；可署名，所以可评价；可评价，所以能分配职位、经费、奖项、声望。三百年学术制度的地基，是「证明很贵」这个事实。
这像一套金本位：钞票（证明）背后压着黄金（理解）。你可以不认识印钞的人，但你知道每张票子都能兑成真金。所以钞票稀缺、可信、可流通。
金本位之所以稳，是因为它有物理上限。证明的上限，就是人的理解力。
我读欧几里得素数无穷的证明时，第一次感到某种奇怪的东西。那个证明只有几行：假设素数有限，全乘起来再加一，得到一个不能被列表中任何素数整除的数。矛盾。
它没告诉我「下一个素数是多少」，它告诉我「你不可能列完」。这个结论不依赖我的计算能力，不依赖纸笔，不依赖任何机器。
证明的力量在于压缩：把无穷多实例收进一个洞见。一万亿次数值验证替代不了一句「为什么」。而压缩之所以可能，是因为有人真的看懂了。
所以证明的稀缺不是缺陷，是保护机制。它保证了一个下限：一条结果要进入教科书、要被人引用进自己的证明，就必须先有某个人真正读懂它。
三、证明印钞机启动
2026 年，这个保护机制被一个数字击穿了。
OpenAI 说，绝大多数结果用同一个流程产出，平均每个结果耗费相当于 ChatGPT Pro 三小时的算力。评估时给模型喂了 4000 个问题。
三小时，一张钞票。
陶哲轩给了一个很准的诊断：证明消化不良。他的逻辑是，如果 AI 只加速「生成证明」这一段，而评审、理解、整合、教学不跟着加速，系统就会堵住。所以他主张的不是停用 AI，而是减少对抢先生成证明的强调，增加对解释、评审、知识整理的重视。
他把标准提得比形式化更硬：讲不清楚的成果是不完整的。
第一次退让
这个标准其实已经被退让过一次。
1976 年，Appel 与 Haken 用计算机检验 1936 个可约构型、耗费约 1200 小时机时，证明了四色定理。Tymoczko 在 1979 年提出质疑：如果没有人能整体检验这条证明，它还算是证明吗？
数学界当时的回答，是把「可理解」从合格标准里划掉，只留「可检验」。
这就是取消金本位的那一刻。钞票不再承诺兑付黄金，只承诺「这是一张合法钞票」。
这个让步在当时是划算的，它让数学保住了扩张能力。但 722 篇把它推到了极限：当可检验的东西多到没人检验得完，「可检验」也开始失效了。
因为可检验性有一个隐含前提——有人会去检验。当供给量超过共同体的消化能力，这个前提就崩了。
纸币靠信用维持，信用靠有人相信它。当没有人有时间去相信，信用就变成了传闻。
挤兑
10 月 7 日，陶哲轩在个人博客全文转发「人类数学协会」（AHM）的联合声明，其中一句被广泛引用：
「一次性发布 700 多份文件，展示的不是学术研究，而是权力。」
更早的 9 月，他与邓煜等 25 位数学家发表过《人工智能在数学中的严重错位》。席南华指出的是规则问题：企业不受学术规范约束，发布成果不需要同行核验，甚至允许错误内容流出。
另一边的语气完全不同。Villani 说这是「至少四个世纪以来、甚至可能是一千年以来数学领域最根本的变革」，但同时说，OpenAI 对成果的描述「更像是一种刺耳的傲慢」——「世界上没有一所大学能以如此高效的速度产出高水平的数学研究」。
丘成桐的说法更有画面感：「就像海啸来了，我们该如何应对？」他给了一个比喻：从古到今，数学的进展基本上是几个人在思考，是微分式的进步；AI 的出现是积分效应，它把人类有史以来所有思考，用机器的算力聚合起来。
印钞厂不需要说服央行。它只需要把钞票印出来，然后看着央行手忙脚乱。
四、三种合法性
陶哲轩把这之前的时代叫「数学 1.0」，说 AI 正在让证明泛滥，建立在证明稀缺之上的 1.0 即将落幕。
他说的「数学 2.0」容易被读成版本升级。不是的。它的含义是：
数学的合法性来源，从一元变成了多元。
今天的数学疆域，按认知可达性可以分成三块。这不是按学科分的，同一个领域里可以同时存在三块。
| 区域 | 特征 | 合格标准 |
|---|---|---|
| 可压缩区 | 证明能被压缩成一个可讲述的思想 | 可理解 |
| 勘探区 | 能被算法触及，但规模超出人类压缩能力 | 可机器检验 |
| 不可判定区 | 连「存在一个证明」都不保证 | 边界刻画 |
可压缩区是黎曼-罗赫、Atiyah-Singer、Langlands 的局部。这里证明中心主义没有失效，也不会失效。
勘探区是四色定理、开普勒猜想、有限单群的计算。这里证明变成了一份机器可检验、人类只能局部理解的证书。
不可判定区是连续统假设独立于 ZFC、群论字问题不可判定、希尔伯特第十问题无解。这里不问答案，问的是能问到什么程度。
722 篇大部分落在第二块。这正是争议的核心：它们不是「更好的数学」，而是「另一种合法性的数学」。 用第一块的标准衡量，它们大多不合格，因为没人讲得清，也没人读得完；用第二块的标准衡量，其中一部分确实成立。
两派人吵的，本质上是用哪一把尺子。
五、稀缺的将是数学判断力
两派人吵的是尺子。而选尺子这件事，本身就是判断力。
所以真正的问题不是证明还剩多少价值，而是：什么变稀缺了？
判断力。
这个说法听起来抽象，但陶哲轩把它讲得很具体。他被问到「AI 时代还要不要读博」时回答得很干脆：关键不在于能不能产出论文，而在于培养出一套吸收困难材料、综合知识、提出好问题的系统能力。他用了一个饮食比喻：食物充裕之后，人反而得自己学会运动。答案随手可得之后，认知能力需要被有意识地维护。
如果只为产出成果，读博的必要性确实在下降。如果是为了被训练成能啃硬问题的人，它反而更值钱。
一个新的坐标
判断力其实分两步：先判断什么该读，再判断读到的东西能不能接进已有的体系。第一步是筛选，第二步是整合，而第二步可以给出一条更硬的判据：
一个数学结果的价值，不再只等于它的正确性，而等于它能不能被吸收进人类已有的理解网络。
722 篇里，大部分可能都是对的。但它们的可整合性接近零——因为它们没有被翻译成任何人能接住的形式。
这就是「讲不清楚的成果是不完整的」的真正含义。它不是学术礼貌，它是在说：在过剩时代，不完整的产物等于零。
正确性是入场券。可整合性才是价值。
AI 卡在哪
AI 现在产生的是路径，不是概念。
人类顶级数学工作是换语言：伽罗瓦换成群，黎曼换成复平面，Grothendieck 换成函子。换完之后，原来难的问题变简单了，因为表示变了。
当前强系统都在一个固定的形式语言里搜索。换语言在搜索框架里是看不见的，因为目标函数定义在旧语言上。这是第一个障碍：表示锁定。
第二个障碍是奖励错位：Lean 只检查证明存在，不检查解释。以形式化通过为唯一奖励的系统，结构上无法优化「讲清楚」。
陶哲轩把实现数学 2.0 的瓶颈归结为想象力——不是模型的想象力，是人类的：供给变了，但我们还没想清楚拿它做什么。
六、为什么是数学先撞墙
这件事先发生在数学，答案在它的产品形态上。
数学是唯一一个「正确性可以被机器完全判定」的学科——证明写下来，检查就是机械的。
它的产品是标准件，而标准件最先被流水线取代。
所以数学不是特例，是先兆。凡是能被形式化的领域，都会依次经历这个翻转：程序、法律条文、会计审计、部分医学诊断、部分新闻报道。顺序不取决于重要性，取决于可形式化的程度。
过去五百年，文明只解一个函数：如何生产更多知识。印刷术、科学方法、公共教育、互联网，都在放大同一个函数。所有制度都默认参数是「信息不足」。
互联网把信息变成过剩品，但旧系统撑住了——因为知识还需要被组织、验证、理解。淹在水里的是沙子，金子还在岸上。
2026 年 10 月，第一次有一个领域，连知识本身都变成了过剩品。
我们一直以为知识的敌人是无知。2026 年开始，可能要改口：知识的敌人是它自己的产量。
而代价不是失业，是评价体系的失效。旧体系衡量的是产出：你证了什么，发了什么，写了多少。新世界需要衡量的是鉴别：你判断出什么值得读，整合了什么，让多少东西变得可用。
结语：以物易物
通胀走到尽头，是货币失去计价功能，人们退回到以物易物。
数学正在走到这一步。
当证明不再是通货，人们会拿什么交换？会拿「我读过，我讲得清」交换。
这听起来像是退步，其实是回到起点。数学从来不是由证明组成的，它是由被理解的证明组成的。那些没被理解的，只是文件。
所以「数学 2.0」不是 AI 取代数学家的故事。它是这样一个故事：证明从稀缺的货币，变成了过剩的原料。
稀缺没有消失，它搬了家：
从「能不能证出来」，搬到「值不值得读」。 从「谁先证明」，搬到「谁能说清楚为什么它必须如此」。这件事真正说的不是 AI 有多强，而是——当证明可以无限印刷，唯一还硬的通货，是有人真的读懂了它。
