722 篇手稿、162 篇过了 Lean：OpenAI 公开内部模型的数学成果合集

仓库里有什么

• 722 篇手稿，归为 372 个结果系列，据外媒统计覆盖 17 个数学领域；
• 评估期间共向模型提出约 4000 道题，平均每项结果耗用约 3 小时 ChatGPT Pro 级别的思考算力；
• 附带 Lean 形式化证明、成果目录，以及 10 份模型推理过程摘要；
• 以 Apache 2.0 协议发布，后续会继续补充新的形式化结果。

据报道，产出这些结果的就是 9 月 8 日宣布 Navier–Stokes 方程有限时间奇点证明的同一个内部系统，至今没有对外开放。

“发了 722 篇”和“证了 722 个”不是一回事

读这条新闻最容易犯的错，是把手稿数量当成定理数量。按第三方的统计，Lean 覆盖主结果的只有 162 篇，约占 22%；剩下五百多篇目前是“模型写的、看起来像证明的文本”，正确性要靠人工审读。仓库 README 自己也提醒，未形式化的部分可能存在问题。

Lean 的意义正在于此：它把“我相信这段推理”变成“编译器检查过每一步”。对 AI 生成的证明来说，这几乎是唯一能规模化建立信任的办法——人类审稿人不可能在合理时间内逐行核对几百篇长证明。所以这批成果的可信度会呈现明显的两层：162 篇可以较放心地引用，其余需要等数学界一篇篇去啃。

为什么选择“整批倒出来”

这种发布方式本身就是一种表态。过去 AI 数学的成果多以单篇论文或单个难题突破的形式出现，容易被质疑“挑了最好看的一个”。一次放出约 4000 道题里跑出的全部结果系列，相当于把命中率和覆盖面一起摊开，让外界去统计成功与失败的比例。

但批评也会随之而来：模型本身不开放，复现无从谈起；成果放在 OpenAI 自己的 GitHub 上，而不是 arXiv 或社区维护的平台，引用、勘误与署名的规范都还没有着落。此前已有数学界人士呼吁 AI 生成成果应走公开、可复核的渠道，这次 OpenAI 只做到了一半。

3 小时一题的账

平均每项结果约 3 小时 Pro 级思考算力，乘以几百个系列，算力投入可观，但相对于一位数学家在某个开放问题上动辄数月乃至数年的投入，又显得便宜得多。真正的瓶颈已经从“谁能想出证明”悄悄移到了“谁来验证证明”。如果后续形式化覆盖率能从 22% 持续往上走，这个仓库的分量才会真正落地；否则它更像一份规模惊人、但需要大量人力兑现的期票。