OpenAI 官方博客 · 2026/10/6 12:00:00
OpenAI 发布前沿模型数学成果并开源 Lean 证明
OpenAI 公开了其内部前沿大模型在数学领域产生的多项新成果，并遵循高等研究院顾问组的建议，通过 GitHub 仓库正式披露。此次发布不仅包含论文草稿，还重点提供了基于 Lean 语言的计算机可验证形式化证明，旨在建立 AI 科学发现的透明分享标准。
报道全文原始报道全文
我们发布了一系列由 内部前沿模型 产生的全新数学成果。
为了改进我们与数学界分享成果的方式，我们一直与独立机构——高等研究院数学与人工智能咨询组(在新窗口中打开) 合作，共同制定最佳实践规范，并参考其建议及 公开推荐意见(在新窗口中打开) 来指导本次成果的发布。
在本次发布中，我们将成果公布于一个 GitHub 代码仓库中，并制定了论文修订和引用的相关协议。我们正在继续探索其他符合该委员会指南的社区托管替代方案。对于未来的发布，我们承诺通过完善引用、优化数学阐述以及改进结果呈现方式，进一步提升论文质量，以促进更好的理解。
作为 GitHub 仓库的一部分，我们分享了其中许多证明在 Lean 中的形式化版本。Lean 是一种允许计算机验证数学证明的编程语言。随着我们获得更多形式化成果，我们将持续更新该仓库。
为促进科学透明度和开放性，我们还在仓库中发布了关于如何获得这些结果的更多细节。其中包括 10 份模型推理过程的摘要、以 ChatGPT Pro 使用量估算的计算资源消耗，以及尝试解决问题数量的统计数据。平均而言，每项成果大约相当于使用了三小时的 ChatGPT Pro 思考算力。
我们希望这一进展能够推动人类知识的前沿，并促进数学领域的进一步发展。我们将资助一系列围绕理解 AI 产生的重大成果而举办的研讨会、会议和特别项目——我们将在近期分享更多相关信息。
我们旨在直接赋予科学家最先进的能力，并正努力负责任地发布产生这些成果的模型。这就是为什么继续在数学及其他科学领域评估我们的内部前沿模型至关重要，以便加速开发推动这些领域进步的工具。我们将持续根据社区反馈采取行动，并更新未来披露重大科学进展的标准。