OpenAI发布前沿模型生成的数学成果，含Lean形式化证明

OpenAI通过GitHub仓库发布由一款内部前沿模型生成的一系列数学成果，包括用Lean语言完成、可由计算机自动校验的形式化证明，并附论文修订和引用规范。仓库包含10份模型推理摘要和已尝试问题的统计数据，平均每项成果消耗的计算量约相当于ChatGPT Pro三小时的推理时间。OpenAI计划资助围绕AI生成数学成果的研讨会、会议和专项项目，并表示正致力于以负责任的方式发布生成这些成果的前沿模型。