OpenAI 公布前沿模型数学成果 引入 Lean 形式化验证

OpenAI 近日公布了一系列由其内部前沿模型生成的最新数学研究成果。

为更好地与数学界分享研究进展，OpenAI 咨询了普林斯顿高等研究院独立的数学与人工智能咨询小组（AGMAI），参考其专业建议与公开指导方针制定了本次成果发布规范。

本次成果已整理至 GitHub 仓库，并附带论文修订与引用规范。OpenAI 正在探索更多符合学术委员会指南的社区托管方案。在未来的发布中，团队将进一步优化论文的引用、数学阐述与结果展示，便于学术界更清晰地理解与检验。

作为开源内容的一部分，OpenAI 在 GitHub 仓库中提供了基于 Lean 语言的形式化证明代码。Lean 是一种允许计算机自动验证数学证明的编程语言，随着更多证明完成形式化，该仓库将持续更新。

为了推动科学透明度与开放性，OpenAI 还披露了成果生成的具体细节，包括 10 份模型推理过程摘要、以 ChatGPT Pro 用量为基准的算力消耗估算，以及尝试解题的统计数据。数据显示，生成单个成果平均消耗的算力，大约相当于 ChatGPT Pro 进行 3 小时的深度思考。

OpenAI 表示，希望这些进展能够拓展人类知识边界，加速数学研究。为此，OpenAI 将出资赞助一系列围绕“AI 生成重大科研成果”的研讨会、学术会议及专项计划。

OpenAI 正在推进该前沿模型的负责任发布，并持续在数学及其他科学领域评估内部模型能力，未来将根据学界反馈不断更新重大科学突破的信息披露标准。