2026 年 10 月 6 日，OpenAI 在 GitHub 仓库通过一次毫无征兆的代码提交，打包丢出了 722 篇前沿模型产出的数学手稿。在这些覆盖了 372 个结果族的文档中，有超过三分之一没有给出可机器检验的证明代码。这些在一天内涌入 9.3k star 和 903 个 fork 的代码库里，甚至有 137 个结果族被官方直接打上了「可能有问题」的标签。
722 篇手稿只配了 235 份执行代码
这次名为「Sharing AI progress in mathematics」的批量发布，包含了庞大的数学推导。仓库里 92.1% 的内容是 Lean 形式化代码，剩下的 7.8% 是 LaTeX 排版的文档。这 722 篇手稿被归入 372 个结果族，每个结果族包含一个主定理及附带引理。它们覆盖了从基础数论到高阶流体力学的宽广光谱。
图：仓库里 overview.pdf 的首页，写明 372 个结果族和 722 篇手稿。来源：OpenAI 数学手稿仓库 overview.pdf
看似庞大的资料库掩盖了一个失衡：在这 372 个结果族里，只有 235 个附带了能够跑通的 Lean 证明。剩下那 137 个被 OpenAI 自己标记为存在疑点的文档，就这样被抛给了开源社区。官方在仓库里放了一份 41 页的 overview.pdf 来做总目录，把这次发布做成了一份可以核对的算力账本。
按官方披露的算力账本，生产一个类似数学结果平均只消耗 3 小时 ChatGPT Pro 推理用量。机器生成数学证明的单价已被算力打穿，但验证成本并没有下降。这种产量与验证能力的巨大落差，把「查错」这道工序默认交给了数学界。
三小时算力对冲人类二十四年
在这批没有跑通机器验证的手稿里，包含了一些异常坚硬的历史难题。编号为 001 的结果试图触碰 Milne 有理猜想，结果 002 指向了 BSD 公式。最惊人的是结果 180 给出了一篇关于 Barnette 猜想的证明论文，偏偏没有可执行的 Lean 代码。
图：涉及 Barnette 猜想的论文首页，署名 OpenAI。来源：OpenAI 数学手稿仓库 preprints 目录
另一些结果展示了工程巧思。结果 376 记录了用纳维-斯托克斯方程执行通用计算的构造：AI 构造了特殊光滑外力，让流体在固定区域内模拟图灵机，粒子进入特定区域的过程等价于图灵机停机状态。这类结果过去要靠跨学科团队打磨多年，现在成了几百页没人签字担保的 PDF。
一位在 Barnette 猜想上耗费 24 年心血的研究者看到这篇缺少形式化验证的论文后，坦言感觉像听说前女友出车祸死了。面对这些黑盒产出，普通研究者别说验证其逻辑链条的完整，连复现出相似思路的设备基础都不具备。算力和模型权重被锁在商业公司机房里。复现一套高深数学推导的前提不再是理解偏微分方程，而是掌握数万张加速卡集群的调用权。
独立顾问组按不住前沿模型出栏
这件事最核心的冲突点，在于它直接无视了学术圈试图建立的防线。早在 9 月 29 日，由 OpenAI 自己出面召集、挂靠在普林斯顿高等研究院的独立顾问组 AGMAI，就给出了一份严肃的公开建议。
AGMAI 的核心诉求非常明确：劝阻前沿实验室不要用闭源模型刷新高难度数学榜单。单边行动会打破数百年来形成的评价共识，对学术评估系统造成污染。
仅仅七天之后，OpenAI 在发布帖里引用这份建议，转身把 722 篇手稿全推上了网络。他们表态会继续和数学界商讨更好的发布方式，但动作已经先于共识发生了。一个有能力在一天内抛出七百多篇高质量手稿的商业机构，事实上接管了整个领域的议程设置权。
做题这一环的难度已经被算力打穿。这 722 篇手稿粗糙但充满压迫感地揭开了一个事实：生产大量对错未知的复杂知识在今天变得廉价。数学的瓶颈从谁能想出解题思路，直接变成了谁有资源跑通验证环节。而在这种全新的知识生产管线里，最终能够给这些数学定理签发正确证书的权力，正毫无悬念地向几家手里握着服务器集群的科技巨头集中。
参考链接：
- OpenAI 发布帖
- GitHub openai/math 仓库
- CONTENTS.md 手稿目录
- AGMAI 公开建议
- Hacker News 讨论
