OpenAI 一次性公开 722 篇数学手稿：仅约两成经 Lean 校验，数学家要求「出示收据」
2026 年 10 月 6 日，OpenAI 在 GitHub 上公开 722 篇数学手稿，归入 372 个「结果族」，横跨数论、代数几何、理论计算机科学等 17 个领域，含准黎曼假设（ζ 与狄利克雷 L 函数在实部大于 7/8 的半平面内无零点）、希尔伯特第十问题、Mahler 猜想等进展，不含剩余五道千禧年大奖难题的完整解答。成果由一款未公开的内部前沿模型产出；OpenAI 称模型被投喂约 4,000 个数学问题，平均每项消耗相当于 ChatGPT Pro 约 3 小时的推理。
软肋写在同一份文件里：仓库的形式化目录显示，722 篇中只有 162 篇的主结果经 Lean 计算机校验，约占 22%，OpenAI 自己注明「部分未形式化的结果可能存在问题」；仓库关闭了 Issues、从未接受过 pull request，想补交形式化的研究者无处投递。OpenAI 发言人称几乎全部结果出自「单个 prompt 交给单个 agent」，该说法在模型公开前无法复现。
数学界的反应
| 人物 / 机构 | 表态 |
|---|---|
| 伦敦大学学院 Francis Johnson | 为沃尔 D(2) 问题写了两本书、研究 25 年后放弃，「精灵已经从瓶子里出来了……只能静观，为之惊叹」 |
| 帝国理工 Kevin Buzzard | 其数论领域 30 篇里仅 7 篇质量突出、1 篇通过 Lean 校验；若多数被证实正确，「机器似乎拥有了精通全部数学领域的能力」 |
| MIT Andrew Sutherland | 单 prompt 单 agent 的说法未经验证，除非公开模型复现，「我们应该要求出示收据」 |
| 普林斯顿高等研究院 AGMAI | AI 已能在提出者无法理解、验证或负责的情况下输出数学论证，人的理解仍至关重要 |
| 剑桥 Ben Alanak / Anthropic Levent Alpöge | 对 AI 公司而言数学发现是「智力领域的奖杯」；也可能是部分数学家在研课题被抢先完成的时刻 |
争议的根子不在对错，在程序。 8 月 OpenAI 曾私下召集约 40 位数学家闭门讨论「AI 若在数学上超越人类该怎么办」，现场学者建议走正规发表流程、给学界留出验证时间；西北大学 Bryna Kra 形容当时的气氛是「极致的兴奋与极致的恐惧并存」。两个月后手稿直接公开，纽约大学访问教授 Nestor Guillen 称头部 AI 公司的做法「就像黑帮」。
观点
- 成本曲线被改写了。 3 小时 ChatGPT Pro 的算力换一项成果，与上月 N-S 问题「一万个 agent 跑 88 小时」是两条完全不同的账；前者若成立，科研推理算力会从「少数旗舰任务拉动」转向「大批量、低单价」的需求结构。
- Lean 形式化已是事实上的准入门槛，且产能不足。 只有 22% 通过校验、仓库却不收外部形式化提交，瓶颈落在定理证明器工具链与形式化数学数据集上，不在模型本身。
- 评议权外移比「AI 会不会做数学」更实。 由企业决定放什么、放多少、何时放，学界只能事后验货；这套程序被同行效仿后，学术优先权与署名规则需要重写。
事件前情见同站笔记《OpenAI 宣称 88 小时解出纳维-斯托克斯方程》。
来源：科技日报、Decrypt、参考消息／腾讯新闻、腾讯新闻