OpenAI 公开一批由内部前沿模型产出的数学结果：发布到 GitHub，并为许多证明提供 Lean 形式化

发布方式本身是这次最值得看的部分。官方说，这次把结果发布在一个 GitHub 仓库里（github.com/openai/math），并制定了论文修订与引用的协议；同时仍在探索其他符合委员会指南、由社区托管的替代方案。对未来的发布，官方承诺会继续通过更好的引用、数学表述与结果呈现来提升论文质量。把数学结果放进一个带修订和引用协议的公开仓库，和传统上「发一篇论文、投一个期刊」的路径很不一样。

第二块是可验证性。作为仓库的一部分，OpenAI 说它分享了许多证明在 Lean 中的形式化。Lean 是一种允许数学证明被计算机检查的编程语言——也就是把「这个证明对不对」这件事交给机器验证，而不是只靠同行阅读。官方说会在获得更多形式化后持续更新仓库。对读这些结果的人来说，这是目前能拿到的最硬的一层证据。

第三块是过程透明度，这部分在 AI 研究发布里并不常见。官方说，为了促进科学透明度与开放性，它还发布了如何得到这些结果的额外细节，包括三类内容：10 份模型推理摘要；以「ChatGPT Pro 用量」表示的算力花费估算；以及尝试问题数量的统计。官方给出的一个关键数字是：平均每个结果使用的算力大约相当于 3 小时的 ChatGPT Pro 思考。

第四块是后续安排。官方说想让这项进展推动人类知识的边界、促成数学上更多的进展，因此将资助一系列围绕「理解 AI 产出的重大结果」的研讨会、会议与特别项目，并表示「近期会分享更多」。至于产出这些结果的模型，官方说正在努力「负责任地发布」（responsibly release），并且强调这正是继续在数学与其他科学领域评估其内部前沿模型的原因。

有一点需要说明：官方这篇博文没有给出结果论文的数量、也没有给出模型名称。网上有第三方报道给出了不同的数字与外部数学家的质疑，但这些不在官方原文里，本文不做引用。这里只呈现官方博文本身写明的信息。