OpenAI 发布史上最大数学项目：涵盖 4,000 个经过 Lean 验证证明的问题

OpenAI 发布了由其内部前沿模型生成的大量数学研究成果，使数学家能够获取数百项机器生成的成果。

该集合发布在一个公开的 GitHub 仓库中，包含组织成 372 个研究系列的 722 篇手稿。这些工作涵盖了纯数学、理论计算机科学和数学物理领域。

多项成果解决了需要长链数学推理的问题。OpenAI 还发布了许多证明的 Lean 正式版本，允许计算机检查底层的论证过程。

数百项成果

该仓库涵盖了涉及数论、复杂度理论、几何学和数学物理的问题。一些成果还延伸到了即使是很小的进展也需要大量技术性工作的领域。

一个例子涉及 pi 的无理性指数。该数值衡量了有理数逼近 pi 的程度。该模型生成了一项针对该逼近的数学行为的成果。

另一个研究系列探讨了 NP-hardness。这些问题属于计算复杂度理论，涉及被认为难以高效解决的任务。该模型的工作为这一更广泛的研究领域增添了数学成果。

其他手稿涉及 Mahler conjectures、等差数列和自由群因子。该集合还包括关于量子 Heisenberg ferromagnets 和相对论 Vlasov-Maxwell equations 的研究工作。

OpenAI 将相关手稿分组为研究系列，以展示各个成果之间的联系。该仓库还确定了 10 个系列，并附有模型推理过程的简要总结。

Lean 增加了验证环节

Lean 为此次发布提供了一个重要的验证层。这种编程语言允许研究人员将数学陈述和证明翻译成正式代码。

计算机随后可以检查每一个逻辑步骤是否遵循所述假设。这并不意味着集合中的每一项研究主张都被自动确认为正确。

许多手稿仍缺乏正式的 Lean 版本。OpenAI 表示，随着研究人员完成验证工作，它将增加更多的形式化版本。

该仓库还跟踪论文修订并提供引用指南。这为研究人员在作者更正或扩展早期手稿时提供了更清晰的记录。OpenAI 在 Institute for Advanced Study 的独立 Advisory Group on Mathematics and Artificial Intelligence 的建议下开发了发布流程。

模型测试了数千个问题

OpenAI 还披露了其数学评估规模的细节。在研究过程中，该模型尝试了大约 4,000 个问题。

一项被采纳的成果平均消耗了大约 3 个小时的 ChatGPT Pro 等效思考计算量。OpenAI 还发布了涵盖尝试过的问题和研究产出的额外统计数据。

该公司表示，推理总结为研究人员提供了更深入了解模型如何处理特定数学问题的机会。这些总结与 Lean 中的正式证明保持分离。

OpenAI 计划支持研讨会、会议和特别项目，重点是理解由 AI 生成的重大数学成果。它还期望数学家的反馈能影响未来的披露。

因此，此次发布不仅是一系列论文的集合。它提供了一种测试，即机器生成的 mathematics 如何通过可复现的记录、计算机可检查的证明以及对成果产生过程的更高透明度进入研究过程。