OpenAI公开内部前沿模型数学成果：同步发布Lean形式化证明

事件概述：OpenAI于2026年10月6日发布研究公告，公开一批由内部前沿模型产生的数学结果，并把结果、论文修订与引用协议放入GitHub仓库，向数学研究社区提供可追踪的材料。

对象与发布方：项目由OpenAI研究团队发布，面向数学研究者、形式化验证开发者、AI科学研究人员和希望复核模型产出的读者。公告没有公开产生这些结果的内部模型名称，也没有把结果表述为已由模型自动完成全部证明。

关键能力与改动：OpenAI为多项证明提供Lean形式化版本。Lean是一种可由计算机检查数学证明的编程语言，仓库会在获得更多形式化内容后持续更新。此次发布还提供10份模型推理摘要、以ChatGPT Pro使用量估算的计算投入，以及尝试题目数量等过程信息；官方称单项结果平均使用了约相当于ChatGPT Pro思考三小时的计算量。

适用对象：需要核验数学论证、研究AI辅助科学发现、构建形式化验证流程，或想比较模型结果与人工证明质量的高校、研究机构和开发者。Lean文件可以作为机器检查的辅助材料，GitHub仓库的版本和引用协议也便于跟踪论文修订。

实际影响：把数学结果、证明形式化和部分生成过程信息放在同一公开仓库，有助于研究者复核、引用和继续形式化，也为今后公开AI科学成果建立更透明的发布流程。OpenAI表示其做法参考了高等研究院数学与人工智能独立咨询组的建议，并计划继续改进论文引用、数学表达和结果展示。

限制与注意：这是内部前沿模型产出的研究材料，不等于所有结论已经获得数学界独立认可，也不等于模型可稳定解决开放问题；推理摘要和计算量估算不能替代逐步证明检查。Lean形式化覆盖范围会随仓库更新而变化，使用者仍需逐条检查定义、依赖、版本和论文修订记录。

官方来源：https://openai.com/index/sharing-ai-progress-in-mathematics/