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