OpenAI通过前沿模型发布新的数学成果

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