722 篇数学论文一天上架之后：三篇撤回与验证的新经济学

10 月 6 日，数学界收到了一份没人点过的外卖：OpenAI 在自己的网站和 GitHub 上，一次性放出 722 篇数学预印本，覆盖 372 个此前悬而未决的结果，其中一部分还附带了 Lean 证明助手能机器验证的形式化版本。一天之内。纽约时报后来的标题用了两个词形容数学家的心情：叹为观止，如遭重击。Science 的说法更冷静也更准确——OpenAI 永远改变了数学，至于怎么变的，还没人知道。

三周过去，事件的第二幕比第一幕更值得看。第一幕是震撼，第二幕是数学界集体回答一个问题：机器一天写出的证明，人类打算怎么验收？

🧾 生产实现了自动化，验收还没有

先把账算清楚。722 篇手稿对应 372 个独立结果，这些结果由 OpenAI 的一个内部前沿模型产出，官方披露的平均成本是：每个结果约等于 3 小时 ChatGPT Pro thinking 模式的算力。一个职业数学家攻克一个开放问题，通常以年计。这两条时间线之间的比值，就是这次发布的全部冲击。

但生产的速度从来不是数学的瓶颈，验收才是。一条证明要成为公认的知识，需要别的数学家读懂它、检查它、试着找出反例，最后有人愿意把它写进教科书。这套流程按人类节奏走，一篇论文数月到数年。722 篇一起涌进来，全球数学家就是全部上线也不够用。

数学界对这件事其实早有预案，预案的名字叫 Lean。把证明翻译成这个形式化语言之后，对错的判定可以交给编译器，机器一秒钟给出结论，不需要仰仗任何人的资历。这就是为什么 722 篇里附带 Lean 形式化的那部分最受关注——按第三方汇总的口径，大约三百篇。剩下的大多数，短期内只有一条路：人工读。

🕳️ 三篇撤回与一条裂缝

撤回来得很快。10 月 8 日前后，OpenAI 撤下三篇预印本，事件链条是这样的：一篇证明里有一个符号错误，另两篇的结论依赖这一篇，一错带俩。Hacker News 上的讨论帖标题直接叫"OpenAI 撤回三个数学结果"。

真正值得记住的是裂缝的位置。新科学家的报道点出了一个细节：问题出在把数学翻译成 Lean 代码的环节——数学本身的对错，和翻译的对错，是两回事。翻译层出了错，机器验证再严格也只会一丝不苟地验证一个错的东西。这像极了软件开发里那句老话：测试通过，不代表需求对了。

十天里发生的事，把这次发布的性质讲清楚了：它算不上"AI 解决了 372 个问题"的胜利宣言，更像一次带伤的公开试运行。OpenAI 自己的动作也在印证这个定位——10 月 15 日的更新宣布，向西蒙斯基金会资助数学家核验 AI 结果的新倡议捐 500 万美元，同时给受资助的研究者提供模型和算力。生产 AI 出钱，验收也 AI 出钱，这个闭环承认了：验不动，生产就白搭。配套的还有制度动作：与普林斯顿高等研究院的合作咨询组参与制定了这次的发布规范，公司同时承诺会以负责任的方式发布产出这些结果的模型本身。

🧭 验证成了新的稀缺

把这次事件放进更大的画面里，它标记的是一个分工的变化。过去数学家的两条腿——想出新证明，以及检查证明——如今一条腿被机器接走了。提出候选证明的成本正在塌缩，从人年塌到机时。而验证这件事，Lean 能接走一部分，剩下最难的部分仍然需要人：判断一个结果值不值得验、把物理世界的直觉翻译成形式语言、以及在翻译层出错的情形下发现错位。

三周了，372 个结果里绝大多数仍未完成人类核验，那 719 篇存活者的成色，要按月甚至按年才能见分晓。真正尘埃落定的只有一件事：数学知识的流水线上，最贵的环节已经换人了。

信源与限定：发布规模（722 篇、372 个结果）、算力口径（每结果约 3 小时 ChatGPT Pro thinking）、Simons 捐赠、IAS 咨询组与模型发布承诺均来自 OpenAI 官方博文 Sharing AI Progress in Mathematics（2026-10-06，10-15 更新）；撤回事件与符号错误细节来自 Hacker News 讨论帖（10-08）与媒体转述；Navier-Stokes 翻译层问题的表述来自 New Scientist 报道标题与摘要；约三百篇附带 Lean 形式化为第三方汇总口径，未经逐篇核对；纽约时报与 Science 标题为转述；陶哲轩声明的具体内容本文未核到全文，仅确认其存在与日期。