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

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

平均每个结果所消耗的算力，相当于 ChatGPT Pro 思考 3 小时左右。仓库里还发布了 10 份模型推理摘要，以及根据 Pro 使用量估算的算力消耗数据。

关于这些结果是如何来的，OpenAI 在仓库里表示，他们用同一个未公开发布的内部模型做了这件事。在现有数学评测达到饱和之后，他们把评测扩展到了开放研究问题上。整个过程里面，模型被问了大约 4,000 道题目。把这些输出聚合成结果家族和手稿，再要求达到一定的显著性水平，就得到了目前的这份目录。

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

在这批结果里有两个例外，OpenAI 也都单独点了出来。第一个是黎曼 zeta 函数无零点区域的工作，第二个是 CM 阿贝尔簇上霍奇猜想的证明。霍奇猜想是克雷数学研究所七个千禧年大奖难题之一，至今依然未被证明。OpenAI 说的是 CM 阿贝尔簇这个特殊情形，仓库里还表示关于 zeta 函数 Re(s) > 11/12 无零点区域的那篇写作文本经过了人工编辑，旨在具备更好的可读性。

在这件事的过程里，还有一个值得留意的小插曲。OpenAI 最初联系了美国普林斯顿高等研究院的几位数学家，想请他们组成一个外部的顾问委员会。但是，数学家们没有接受这个安排，而是自己成立了一个独立小组，名字叫数学与人工智能顾问组。成员包括著名数学家 Timothy Gowers、Martin Hairer、Edward Witten 等人，他们不接受 AI 公司发放的报酬，独立发布对于 AI 公司所发布的数学成果的建议。该小组在自己的网站上写明，他们不拥有任何一家 AI 公司的决策权，AI 公司决策的责任仍然属于 AI 公司自己。

10 月 6 日，这个顾问组对 OpenAI 的发布成果给出了回应。他们说，这是一个非常重要的事件，对数学和数学界的影响远超单个结果的影响。同时，他们强调公开发布成果只是第一步。把结果进行公开，不等于人类已经真的理解了这些结果，也不等于这些结果已经融入了数学知识体系之中。

他们还说，未来数学研究不能只由 AI 产出的结果组成，数学家必须能够提出自己的问题，发展自己的方法，探索那些没有被 AI 系统选为能力展示的方向。要做到这一点，公平地获得强大的研究工具和足够的计算资源是必要条件。

OpenAI 方面表示，他们会资助一系列工作坊、会议和特别项目，围绕如何理解 AI 产出的重大结果展开讨论。他们也说，正在负责任地准备发布这个产出结果的模型，并会继续根据社区反馈更新未来披露科学进展的标准。

这件事的意义有两层：一层是数学本身，722 篇手稿，372 个结果家族，其中一部分已经被机器验证，这在几年前还很难想象；另一层是数学研究的组织方式，AI 开始进入开放问题的求解环节，数学家需要面对一个新问题，就是如何把 AI 产出的结果纳入人类理解，如何保证数学研究的方向不完全由 AI 系统的能力展示来决定。

参考资料：

https://openai.com/index/sharing-ai-progress-in-mathematics/

https://openai.com/index/sharing-ai-progress-in-mathematics/