【OpenAI公布722篇数学手稿，其中一部分可被计算机逐行验证】

一道曾经困扰数学界多年的开放问题，一个内部模型使用大约 3 小时的推理算力给出了答案。OpenAI 在当地时间 10 月 6 日发布了一批由内部前沿模型产出的数学结果。这批结果被整理成了一个 GitHub 仓库，其中包含 722 篇手稿，归入 372 个结果家族，覆盖了从数论到量子场论的多个数学分支。

平均每个结果所消耗的算力，相当于 ChatGPT Pro 思考 3 小时左右。仓库里还发布了 10 份模型推理摘要，以及根据 Pro 使用量估算的算力消耗数据。关于这些结果是如何来的，OpenAI 在仓库里表示，他们用同一个未公开发布的内部模型做了这件事。

在现有数学评测达到饱和之后，他们把评测扩展到了开放研究问题上。整个过程里面，模型被问了大约 4,000 道题目。把这些输出聚合成结果家族和手稿，再要求达到一定的显著性水平，就得到了目前的这份目录。

仓库里有一部分手稿附带了 Lean 形式化证明。Lean 是一种编程语言，数学证明可以在它里面写成代码，然后由计算机检查每一步推导是否合法。这就等于把一部分验证工作从人眼转移到了机器。OpenAI 在仓库里也说明，未形式化的结果可能存在一定问题，他们也会尽快修正。与此同时，他们还在探索由社区托管的仓库来存放这些材料。

戳链接查看详情：http://t.cn/AXlvSWQJ