OpenAI发布数学新成果：证明可由机器逐行核验

OpenAI 发布了一批新的数学成果，来自内部的前沿模型。结果已经放上 GitHub 仓库，论文修订和引用协议一并公开。OpenAI 还在探索其他社区托管方案，要求是符合咨询小组的指南。

许多证明换了一种形式公开：用 Lean 语言做了形式化。Lean 是一种编程语言，能让计算机自动检查数学证明。模型写出来的证明，机器可以逐行核验。

OpenAI 同时公布了 10 份模型推理摘要。它还给出了按 ChatGPT Pro 使用量估算的计算量，以及尝试问题的数量统计。推理过程打开了一部分，外界可以评估这些结果是怎么来的、靠不靠谱。

算力开销不算大。一个数学新结果平均用掉的计算量，约等于 ChatGPT Pro 思考三个小时。持续用 AI 做数学，在算力上可行。

发布方式上，OpenAI 咨询了普林斯顿高等研究院的独立数学与人工智能咨询小组，请他们帮着定发布规范。它还承诺，今后发布论文时会在引用、数学阐述和呈现方式上改进。GitHub 仓库会随着更多形式化证明的完成而持续更新。

OpenAI 还计划资助一系列围绕 AI 成果的研讨会、会议和特别项目，并正在争取负责任地发布产生这些结果的模型。它接下来会继续在数学和其他科学领域评估内部前沿模型，以加速开发工具。OpenAI 希望这些进展能推动人类知识的前沿。

社区反馈会被纳入后续发布标准。仓库会更新，研讨会和会议会落地，模型发布也在推进中。