OpenAI 用 Lean 形式化十项数学成果：内部模型扮演了什么角色

8月1日，OpenAI 发布手稿《Ten Advances in Mathematics and Theoretical Computer Science》，将这些成果归于自家的一个内部模型。与此同时，GitHub 仓库 `openai/ten-proofs` 上线，公开了十项证明的 Lean 4 形式化。成果中最醒目的，是球堆积指数的改进——1978年以来的第一次——、一个非索菲群的构造，以及对孔涅刚性猜想的一个反例。该仓库是基于 mathlib 的 Lean 4.32.0 项目，采用 Apache-2.0 许可：任何人都可以用 `lake exe cache get` 和 `lake build All` 重新编译这些证明，ComparatorChallenges 文件夹则说明了如何独立完成验证。

媒体把这些成果与「Astra」联系了起来，那是 OpenAI 同在8月1日宣布的下一代模型家族的名字；但手稿只提到「一个内部模型」，并未发布。诸如约2000美元的 token 成本、文档249页这类数字，来自第三方报道，因为官方公告页面目前无法访问。论文对参与复核的人类数学家致谢，并提到 Shuoxing Zhou 一项独立且同期的工作，该工作部分借助了 GPT-5.6 Sol。

据 SiliconANGLE，数学论证出自模型，但把输出整理成可发表手稿的是人类研究者：这道打磨的分量有多重，无人量化。Lean 4 的使用改变了争论的落点：证书保证证明在逻辑上成立，却不会自动确认形式化后的命题就等同于那道历史上的未解难题——这项核对仍归人类。十项成果没有一项通过正式同行评审。前车之鉴很重：2025年10月，关于 GPT-5「解决」十道埃尔德什问题的宣布被证明毫无依据，erdosproblems.com 的维护者 Thomas Bloom 称之为严重的失实表述。而对今天这十项成果，同一个 Bloom 说的是「big news」。正如理论物理学家 Tobias J. Osborne 所指出的，被引用的2000美元只是成功 token 的成本，并非全部尝试的总「收成」，而 OpenAI 对此没有提供任何信息。这一切发生在《Leiden Declaration on Artificial Intelligence and Mathematics》的背景之下：该宣言发布于2026年6月，据 the-decoder 获得超过3000名数学家和国际数学联盟的支持，要求透明、保护作者权利，并由人类对结果负责。

真正的新闻不是机器做了数学——这已经持续好几个月了——而是这一次每项成果都带着一份可重新编译的 Lean 证书：要作判断，不必相信宣布者。然而，只要失败尝试与成功之间的比例仍是商业机密，对这些模型效率的评估就依旧更像是一种信仰，而不是统计。