OpenAI 这次没发新模型，发了一个数学 GitHub 仓库。然后整个数学圈开始加班验收。

10 月 6 日，OpenAI 官方博客 Sharing AI progress in mathematics + GitHub 仓库 openai/math 同步上线，核心数字：

1️⃣ 722 篇数学手稿，归成 372 个结果家族，全部由一个「未发布的内部前沿模型」产出，Apache-2.0 开源。

2️⃣ 怎么来的：评测里给模型丢了大约 4000 道开放研究问题，平均每个结果约等于 3 小时 ChatGPT Pro 级别的思考算力。

3️⃣ 目录里点名的硬骨头：Unique Games 猜想、Mahler 猜想、Kaplansky 零因子猜想的反例、自由群因子同构问题，还有 Dirichlet L 函数（含黎曼 ζ 函数）在 Re(s)>7/8 区域无零点。

4️⃣ 其中 162 篇的主结果已经配了 Lean 形式化证明，也就是电脑逐步检查，不靠审稿人的眼睛。

但真正该划重点的是后半句。

OpenAI 自己在 README 里写得很直白：这批结果处在不同的验证阶段，没有形式化的部分「可能有问题」，后面会持续补 Lean。

翻译一下：162 篇 ≈ 机器验过主结果；剩下五百多篇 = 模型写出了一篇论文，还没被完整验完。produced a proof 和 has a proof，是两回事。

另一个细节：OpenAI 说发布方式参考了 IAS 那个独立的数学与 AI 顾问组 AGMAI（Terence Tao 也在里面）的建议。但 AGMAI 官网写明自己独立运作、不拿钱、对公司决策没有决定权，结果对不对，责任在 OpenAI。

我的判断：

- 这比刷 benchmark 硬太多。benchmark 能过拟合，Lean 不吃这一套。

- 数学界的验收期才刚开始，接下来几个月真正的指标是：同行能把多少篇「拆开读懂并确认」。

- 那个模型 OpenAI 说在推进负责任发布。真上线那天，AI 订阅的性价比又得重算一遍。

搞 Web3 的应该最懂这句话：合约没审计 ≠ 安全，证明没形式化 ≠ 成立。

只筛选不教育：看到「AI 解决了 XX 猜想」的标题先别急着转，先看那一篇有没有 Lean。

来源：OpenAI 官方博客（10/6）、GitHub openai/math README 与 Lean formalization 目录、agmai.org。以上为信息整理，不构成投资建议。