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

OpenAI在当地时间10月6日发布了一批由内部前沿模型产出的数学结果。这批结果被整理成一个GitHub仓库，其中包含722篇手稿，归入372个结果家族，覆盖了从数论到量子场论的多个数学分支。仓库里还发布了10份模型推理摘要，以及根据Pro使用量估算的算力消耗数据。

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

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

平均每个结果所消耗的算力，相当于ChatGPT Pro思考3小时左右。这一数字来自仓库根据Pro使用量估算的算力消耗数据，属于OpenAI方面的自述。

仓库里有一部分手稿附带了Lean形式化证明。Lean是一种编程语言，数学证明可以在它里面写成代码，然后由计算机检查每一步推导是否合法。这就等于把一部分验证工作从人眼转移到了机器。

但形式化并非全覆盖。OpenAI在仓库里也说明，未形式化的结果可能存在一定问题，他们也会尽快修正。与此同时，他们还在探索由社区托管的仓库来存放这些材料。这意味着，附带Lean证明的部分与未形式化的部分，在可验证性上处于不同状态。

在这批结果里有两个例外，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产出的重大结果展开讨论。他们也说，正在负责任地准备发布这个产出结果的模型，并会继续根据社区反馈更新未来披露科学进展的标准。

但几个关键问题仍无定论：这批数学结果的正确性尚未经独立第三方验证；未形式化手稿的具体问题范围与严重程度不明；社区托管仓库的探索尚无明确结果；AI产出结果如何纳入人类理解与数学知识体系仍无定论；未来披露科学进展的标准将如何随社区反馈更新尚不明确。