两周前，OpenAI 公开数学仓库、一次性放出 722 篇手稿时，讨论的焦点是「量产」：每条结果约三小时的 ChatGPT Pro 算力，对数学界数十年积累的降维式冲击。两周后的 10 月 7 日，仓库的 history 页面更新了一条安静但分量更重的记录：撤稿三篇，修复十四篇，更新十三篇。同一天，Terence Tao 在 mathstodon 上写下了后来被顶到 HN 首页 589 分的那段话——「Math 2.0」需要重新定义什么算数学进步。
这两件事在同一天发生，不是巧合。它标志着这场实验从「AI 能不能解出难题」的第一幕，进入了「AI 产出的数学如何被检验」的第二幕。而第二幕的问题，比第一幕难得多。
一、一条符号错误的杀伤半径
先看撤稿的技术细节。官方记录写得很克制：《Split Abelians 八fold 上 Weil 代数性》一文中，一处符号错误使稳定化迹抵消论证（stabilization-trace cancellation argument）失效，而这个构造被两篇后续论文——《K3 曲面的 Kuga-Satake 对应代数性》与《K3 曲面乘积的有理 Hodge 猜想》——直接依赖。三篇一起撤下。
数学证明的依赖链是单向透明的：上游错一步，下游全盘皆输。这正是数学与多数经验科学的区别——它理论上有绝对的可验证性，但人工验证的成本极高，以至于现代数学的日常现实是：大量已发表证明从未被第二个人逐行读过。Voevodsky 在 2012 年就公开说过，他对自己的早期工作是否完全正确「没有信心」，这直接推动了他转向形式化验证。
现在把这条依赖链的语境换成 AI：机器以周为单位产出证明，验证瓶颈没有变，产出速度提高了一百倍。验证带宽与产出速度的比值，就是这个体系的实际可靠性。722 篇手稿、约 42% 的形式化覆盖率，意味着超过半数的结果处在「有人读之前都算存疑」的状态。三篇撤稿不是体系失败的证据，而是这个比值的第一次公开定价。
二、42%：形式化作为分界线
仓库记录的另一半信息同样重要：新增六个形式化后，顶线结果的形式化覆盖推进到 300/719，约 42%。
形式化验证（Lean 检查器）在这个体系里扮演的角色值得仔细拆开。它是目前唯一能对数学证明给出机械可查判定的工具——不被审稿人的疲劳、名望或善意影响。撤掉的三篇论文恰好都没有完成形式化；而被修复的十四篇（Lipschitz 高度、Kähler 极小模型纲领、超辛形变等）在修复说明里都指明了验证路径。也就是说，这批手稿的可靠性分布，几乎完美地沿着「是否形式化」这条线切分。
这给「AI 数学的质检体系」提供了一个朴素但有效的结论：验证成本应该优先花在形式化上，而不是人类专家复核上。三小时算力出一条结果，而一条结果的形式化可能需要数天——这个比例仍然倒挂，但方向已经明确：42% 不是终点，而是这个体系从「预印本文化」迁向「机器可查文化」的进度条。
顺带一提，剑桥团队 10 月 7 日在 arXiv 上发表的《Navier–Stokes Lost in Translation》（2610.08144）从反面补了一刀：他们论证自动形式化中的消歧难题在一般情况下难于停机问题。形式化是质检的金标准，但把自然语言证明自动转成形式化证明本身就有理论边界——质检线本身也需要人工投入。这不是坏消息，而是给「全自动化数学」的预期画了一条清晰的线。
三、Tao 的提问：当解题不再稀缺
如果说撤稿是工程层面的事件，Terence Tao 的帖子则是哲学层面的。他在 10 月 8 日的原话：
Math 1.0 把溢价押在「第一个解出公开问题」上，哪怕解法最初并未被充分理解。如今这个目标已被优化到不可持续的程度，Math 2.0 将需要弱化原始解题的中心地位，更整体地衡量数学进步的价值。
这段话里最刺眼的词是「不可持续」（unsustainability）。当解题的稀缺性被机器消解，数学共同体的价值锚点必须迁移。Tao 给出的方向包括：证明是否被理解、结果是否可组合、是否训练了更好的数学家。他甚至提出一个更激进的设想——可能有必要把某类数学问题划为自动求解的禁区，以保全它们对数学生态（比如训练未来数学家）的价值。这条设想在 Reddit 数学版引发了激烈争论，因为它触碰了一个根本问题：学科的价值是否可以、应该被管理。
Scott Aaronson 同期的长文《The Mathocalypse》从另一个侧面呼应了同一情绪：数学界正经历一场「末日感」，不是因为有太多问题被解出，而是因为解出的方式让「理解」这件事变得可有可无。加上 Vitalik Buterin 因「AI 数学进展太快」公开呼吁加密行业进入「bunker mode」——一条密码学抗性时间线被 AI 数学压缩的新闻——你会发现这次冲击波远不止数学界内部的事。
四、值得肯定的部分：撤回也是产出
批评之外，这次事件里有一个常被忽略的亮点：撤回与修复被写进了公开记录。
history 页面把撤稿原因、依赖关系、十四篇修复的具体内容（修了哪个引理、加了什么假设、删了哪条过时引用）全部公开列出，被撤论文带着解释缺口的通知和存档链接留在原处。对照学术出版界的现实——大量撤稿遮遮掩掩、依赖链上的论文从不下架——这份透明度是教科书级的。
这也是「量产数学」若要成立的前提条件之一：产出、验证、撤回、修复必须形成闭环，且全程可查。OpenAI 两周一次的记录更新节奏，无意中演示了一种新的科研基础设施形态——仓库即期刊，history 即勘误表，形式化覆盖率即质量指标。
五、结语：质检带宽才是新瓶颈
把三件事放在一起——三篇撤稿、42% 形式化覆盖率、Tao 的 Math 2.0——可以看到同一个结论从三个层面浮现：
- 工程层面：自动求解的产出速度已经跑赢验证带宽，可靠性的瓶颈从「能否解出」转移到「如何检验」；
- 基础设施层面：形式化验证是唯一可规模化的质检手段，但它自身的自动化有理论边界，人机协作的验证流水线是中期形态；
- 共同体层面：当「解题」不再稀缺，数学进步的价值标尺必须从结果优先转向验证与理解优先。
两周前我们写过 722 篇手稿的量产故事，当时留下的悬念是「数学界如何消化」。现在第一个答案来了：不是靠消化，而是靠重建质检体系。速度已不是变量，带宽才是。这个结论不只属于数学——所有正在被 AI 加速的科学领域，都会在各自的「撤稿时刻」重新学习它。