OpenAI公布前沿模型生成的数学研究成果
OpenAI发布一批由内部前沿模型产出的数学成果，同时公开Lean形式化证明、推理摘要与计算量信息。
OpenAI公布了一批由内部前沿模型产出的数学研究成果，并通过公开GitHub仓库提供相关材料。此次发布包括研究说明、论文修订与引用协议，以及多项使用Lean形式化的证明。Lean是一种可由计算机检查数学论证的证明助手。
公司还披露了较为具体的研究过程信息，包括10份模型推理摘要、以ChatGPT Pro使用量估算的计算资源，以及模型尝试题目的统计数据。OpenAI称，每项平均成果所消耗的计算量，大致相当于ChatGPT Pro思考三小时。
这次发布参考了高等研究院“数学与人工智能咨询组”的建议。OpenAI表示，团队仍在探索符合委员会指导原则的社区托管发布方式，未来也会继续改进数学表达、引用和成果披露标准。
需要注意的是，这并不是模型本身的公开发布。OpenAI只表示正在研究如何负责任地开放生成这些成果的系统，尚未给出时间表。眼下对数学界开放的是一组可供核验和继续研究的成果与形式化证明，而不是一个人人可用的数学研究助手。
为什么重要：AI生成数学正在从基准测试演示，走向可检查、可形式化、可复用的科研流程。真正决定其影响力的，将是独立数学家能否验证这些结论，以及发布规范能否跟上模型能力的增长。