人工智能写出的 722 份证明：现在能检验什么

10 月 6 日至 7 日的夜间，西班牙已是凌晨，OpenAI 在 GitHub 上传了 722 份数学手稿。它们由一个内部模型写成，该公司既没有发布这个模型，也没有公开它的名称。这些手稿分为 372 个“家族”：每个家族包含一个主要结果及其变体和推论。OpenAI 解释说，它用尚未解决的研究问题来评估自己的模型，并公布了其中重要程度足够高的结果。

9 月 21 日，该公司曾表示其模型已经解决了“一百多个”未解问题，却一个也没有展示。现在它展示了，而且数量更多。其中一些论断如果得到证实，将终结悬置了数十年的问题：素数如何分布，优化算法的极限在哪里，或者为什么磁铁始终是磁铁。

计算理论领域的资深学者 Lance Fortnow 第二天写道，他的领域在 24 小时内取得的进展，超过了此前三十年的总和。在同一篇文章中，他也补充说，这些成果目前都还没有经过验证。

这一保留意见，正是本文要回答的问题：说这些结果“已被检验”，究竟意味着什么。这一次，其中一部分可以由机器审查，这是以往任何一次公告都没有做到的。但这种审查分为几个层次，而且大部分工作仍有待完成。

仓库里究竟有什么

根据仓库的 README，模型共收到约 4000 个问题，每个结果平均消耗的算力，相当于 ChatGPT Pro 推理三个小时。公司没有说明这些问题是如何挑选的，但透露了一个比例：约 4000 次尝试，产生了 372 个家族。正如 Fortnow 指出的，模型解决的问题不到所给问题的 10%。

几乎所有结果都是通过同一套自动流程得到的。README 承认有两个例外，但没有详细说明：黎曼 zeta 函数的一个不含零点的区域，以及针对某一类几何对象的霍奇猜想。这恰恰是最接近千禧年大奖难题的两个结果。此外，关于 zeta 函数的其中一篇文本经过人工编辑，以便阅读。

仓库包括：

• PDF 格式的论文及其源文件；
• 模型推理过程的十份简要摘要；
• 一个 Lean 形式化证明库，我们稍后会谈到；
• 以及一项保留历史记录的承诺：修正将作为新版本发布，不会删除旧版本。

README 本身就提醒：“Some of the unformalized results could have issues”（部分未经形式化的结果可能存在问题）。

发布公告没有重点介绍任何具体结果。这些天流传的“重大成果”清单，是媒体和数学家们自己挑选出来的。我们选了四个，帮助理解这些论断的规模。

四个结果，看清其中的分量

素数与 zeta 函数

素数看似毫无规律地分布，但它们遵循一条平均规律，这条规律在 1896 年得到证明：不超过某个数 x 的素数大约有 x/ln x 个。有意思的问题是，实际数目会偏离这条规律多远。答案取决于黎曼 zeta 函数的零点在哪里，也就是这个函数取值为零的那些点。

黎曼猜想于 1859 年提出，是七个千禧年大奖难题之一。它断言所有这些零点都位于一条特定的直线上，即实部为 1/2 的直线。如果它成立，素数计数的误差就是可能的最小值。迄今为止，人们只知道在边界上，也就是实部为 1 的地方没有零点，在一条随高度上升而变窄的带状区域内也没有。从来没有人能证明，存在一条宽度固定、不含零点的带状区域。这个弱化版本就是所谓的拟黎曼猜想。

OpenAI 声称已经证明了它：实部大于 7/8 的地方没有零点。这不是黎曼猜想，后者要求一直推进到 1/2，但这将是该问题提出以来的第一个此类进展。同一家族的另一份手稿还排除了所谓的西格尔零点（Siegel zeros）。这是一种假想中的异常，它迫使许多关于素数的定理依赖于无人知道如何计算的常数。第二份手稿则通过另一条路径，证明了一个略小的区域，从 11/12 开始。这正是经过人工编辑的那篇文本。

优化算法的极限

许多实际问题在大规模下太难，无法精确求解。一个例子是把一个网络分成两组，使被切断的连接尽可能多（最大割，Max-Cut）。另一个例子是选出最少的节点，使它们触及所有连接（顶点覆盖，Vertex Cover）。对于这些情况，我们使用能给出近似答案、并且质量有保证的算法。例如，Max-Cut 的算法保证至少达到最优值的 87.8%。

自 2002 年起，Subhash Khot 提出的唯一游戏猜想（Unique Games）就预言，在合理的时间内无法做得更好。如果它成立，我们已经在使用的许多近似算法就是最好的，除非 P = NP。OpenAI 声称证明了这一猜想。此外，在另一项独立结果中，它声称不依赖该猜想就证明了：改进 Max-Cut 和 Vertex Cover 的这些保证是 NP 困难的，也就是说，与其所属类别中最难的问题一样难。

这里还有一段关于人的故事。据 Quanta Magazine 报道，9 月 11 日开始流传 OpenAI 已经掌握证明的传言。Dor Minzer（MIT）和两名学生在这个问题的一个变体上已经研究了七年，并在 4 月将其解决。传言出现三天后，他们发布了 95 页的论文，首页附有一条说明：文本在数学上是完整的，但还不是他们希望用来分享的形式。Minzer 对该杂志说：“There is a lot of value in failing and knowing why you failed”（失败并理解自己为什么失败，有很大的价值）。

为什么磁铁始终是磁铁

在磁铁中，原子的微小磁矩，也就是自旋，会朝同一方向排列。量子物理用海森堡模型描述这种行为，任何物理学家都认为，在三维空间中、在低温下，材料会保持磁化。严格证明这一点则是另一回事。该模型的经典版本，以及相邻自旋指向相反方向的量子反铁磁情形，几十年前就已解决。但在那些情形中奏效的技术，并不适用于普通的量子磁铁。1999 年，Elliott Lieb 把它列为一份数学物理未解问题清单中的“Problem A”。

OpenAI 声称已经在三维及以上的所有维度中证明了它。这是一类常被忽视的结果的好例子：它没有改变我们对世界的认识，却把一个物理上的确信变成了一条定理。

一个经典问题，一个出人意料的答案

从一个“自由群”出发，也就是用两个字母及其逆元，或者用三个字母，所能写出的全部单词的集合，可以构造出分析学中一种称为冯·诺依曼因子的对象。这些对象出现在默里和冯·诺依曼的奠基性工作中。这个问题通常归于 Richard Kadison，它问的是：这个对象是否“记得”最初用了几个字母。它被视为该领域最著名的未解问题，大量研究都致力于证明这些对象互不相同。

OpenAI 的说法恰恰相反：用两个字母还是三个字母，得到的是同一个对象。如果得到确认，这将是那种迫使整个领域修正直觉的结果。此外，它也很好地说明了下一节要讨论的问题。

目录中的其余结果

这四个只是样本。下表列出了其他一些顶级结果，以及它们是否有 Lean 形式化证明：

来源：仓库的手稿目录和形式化目录，查阅于 2026 年 10 月 7 日。描述经 Codin 简化。

“已检验”可能有三种不同的含义

与以往的发布相比，这一次的新意在于 Lean。Lean 是一种语言，用它写出的证明详细到可以由程序逐步审查，而不必信任任何人。它依托 Mathlib，这是一个由社区维护的库，收录了已经检验过的定义和定理。一个证明在 Lean 中“编译通过”，意味着每一步都由前面的步骤推出。

但当人们说一个结果已被检验时，最好区分三个问题。

第一：形式化证明是否正确？

这是 Lean 解决的问题，而且可以在 OpenAI 之外重复。仓库为 Comparator 准备了挑战。Comparator 是一种工具，只有当一个证明恰好证明了参考陈述、并且只使用标准公理时，才会接受它。发布后几个小时内，几位 OpenAI 以外的人就在自己的机器上重新编译了 7/8 区域的证明（其一、其二），结果正确。

仓库包含超过 12 万个 Lean 文件，但这个库只覆盖了目录中的一小部分：722 份手稿中，有 162 份的主要结果得到了形式化。

第二：形式化陈述说的是我们以为的内容吗？

Lean 保证证明确实证明了给定的陈述。它并不保证这个陈述的含义与论文所说的一致。这是最依赖人的一层，其难度因结果而异，差别很大。

最好的情况下，陈述短到任何受过一定训练的人都能读懂：

theorem riemannZeta_ne_zero_of_seven_eighths_lt_re
    {s : ℂ} (hs : (7 / 8 : ℝ) < s.re) : riemannZeta s ≠ 0 := by
  sorry

如果定义来自社区，陈述又只有两行，Lean 所提供的可信度就非常高。正因如此，7/8 的无零点区域是目前目录中检验得最充分的结果。

自由群因子的情况则不同。Mathlib 中还没有这些对象，因此 Comparator 挑战从零开始定义它们，而这些定义同样出自 OpenAI。唯一游戏猜想的情况也类似：它的陈述依赖于数千个字符的自定义编码。对一个略有偏差的定义给出完美的证明，证明的就是另一回事。必须有懂这个领域的人去阅读这些定义，确认它们确实刻画了真正的问题。

形式化目录用两个字段把这一点说得很清楚：Lean 证明同样由一个人工智能智能体编写（automation: agent），其审查状态显示为待完成（review: unchecked）。

第三：我们理解了什么？

即使陈述被正确形式化，Lean 通常也只覆盖主定理。就拟黎曼猜想而言，文档本身就提醒，论文中的应用并未包括在内。而这些应用，恰恰是素数专家感兴趣的内容。

其余 560 份手稿，目前只能依靠其自然语言文本和 OpenAI 的内部判断。其中包括霍奇猜想：它是没有遵循自动流程的两个结果之一，也没有形式化。

此外还有任何程序都无法审查的东西：是什么想法让每个证明成立，它是否开辟了新的路径，以及它给该领域带来了什么改变。我们在当证明不再是瓶颈一文中已经讨论过这种转移。这次发布让它变得具体可感：机器让第一层变得容易得多，而人的工作则集中在另外两层。

数学家们的要求，与实际到来的东西

9 月 21 日，OpenAI 介绍了一个由九位数学家组成的独立顾问小组 AGMAI，设在普林斯顿高等研究院。9 月 29 日，也就是发布前一周，该小组根据数学界的 600 多份反馈发布了建议。建议的第一条是一项请求：希望各实验室不再用专有模型测试高级数学问题。下表对比了他们的要求与实际到来的内容：

来源：AGMAI 9 月 29 日的建议、OpenAI 的公告和仓库的 README。对比由 Codin 整理。

没有模型和提示词，就没有人能复现每个结果是如何得到的。这并不妨碍检验一个证明，因为证明本身要么成立，要么不成立。但这确实让人无法知道问题的选择起了多大作用、哪些尝试没有成功，或者那两个例外是否得到了其他结果没有得到的帮助。

同样在 10 月 6 日，AGMAI 发表了一份声明，值得全文阅读。声明说，它的顾问角色不应被解读为对这些结果影响力的评估，也不应被视为对这一过程的背书。它还指出，其建议在多大程度上得到了遵循，应由数学界来判断。声明这样总结：“This release is the beginning, not the completion, of the process”（这次发布是理解和吸收这些结果这一过程的开始，而不是终点）。

数学界在最初几个小时里的反应

截至 10 月 7 日，还没有专家发表对某个具体结果的审查，也没有任何错误得到确认。目前有的，是关于如何解读这份公告的不同立场。

Andrew Sutherland（MIT）在《科学美国人》上呼吁，凡是无法复现的内容都应视为未经验证：“We should ask for receipts”（我们应该要求出示凭据）。Daniel Litt（多伦多大学）在同一篇文章中提出了相反的论点：如果我们想知道答案，要求公司把它们保密就没有意义，而且他认为这对数学会是好事。Mark Braverman（普林斯顿大学）对 Quanta 表示，靠新闻稿推进的数学“不太健康”，但他也承认，这样的证明可能开辟新的研究方向。

与此同时，验证工作已经开始在 OpenAI 之外组织起来。除了 Lean 证明的重新编译，一个由社区维护的未解问题目录导入了数百个结果，每个结果都附有同样的提醒：尚未有独立的数学家审查过。该目录已将其中几个标记为存在争议，因为它们可能与此前发表的结果相冲突。

整体氛围有两面。一面是对规模的惊叹，甚至批评者也不例外。另一面是疲惫：在纳维–斯托克斯的署名争议和菲尔兹奖得主的公开信之后，批评已不再只针对这些系统说了什么，也针对由谁决定节奏，以及成果如何发布。

测试通过，只证明了测试所检查的内容

9 月 29 日，我们曾主张，宣布一百项进展的人，应当为每一项提供足够的信息，让人能够检验它，并在它的基础上继续研究。这次发布提供的内容比上一次多得多：有完整的手稿、任何人都可以运行的形式化库，以及版本历史。不承认这一点是不公平的。但能够复现整个过程的东西仍然缺失，由谁来为审查工作付费也依然不清楚。

在软件领域，我们很熟悉这个案例所揭示的区别。测试通过并不能证明程序做的是正确的事，只能证明它做了测试所检查的事。如果规格说明写错了，代码可以完美地满足它，却依然毫无用处。Lean 把证明的正确性变成了类似自动化测试的东西：快速而可靠。问题因此转移到了规格说明上：形式化陈述是否就是我们关心的那个问题，以及这个证明除了告诉我们结论成立之外，还教会了我们什么。

因此，未来几个月值得关注的数字不是 722。另外三个数字会说明更多问题：

• 有多少形式化陈述经过了该领域研究者的审读，首先是那些依赖自定义定义的陈述。
• 有多少顶级结果得到了专家的审查，尤其是那些没有 Lean 证明的结果，比如霍奇猜想。
• 版本历史中记录了多少修正。 一个如此规模的仓库如果没有任何勘误，反而比有勘误更可疑。

如果这些数字增长，这次发布就会帮助数学界吸收真实的结果。如果它们不增长，我们将拥有数百条定理，而关于它们，我们唯一知道的就是一台机器说它们是对的。

来源

• OpenAI：“Sharing AI progress in mathematics”，2026 年 10 月 6 日。
• openai/math 仓库：README、手稿目录、形式化目录、拟黎曼猜想形式化的范围和 Comparator 挑战。提交 adc7f124，查阅于 2026 年 10 月 7 日。
• AGMAI：2026 年 9 月 29 日的建议和 10 月 6 日的声明。
• Lance Fortnow：“Open No More”，2026 年 10 月 7 日。
• Quanta Magazine：围绕唯一游戏猜想的竞赛，2026 年 10 月 7 日。
• Scientific American：Sutherland 和 Litt 的反应，2026 年 10 月 6 日。
• Elliott Lieb：“Problem A”，数学物理未解问题清单，1999 年。
• 对 7/8 区域的独立重新编译：Zhang-Liao/quasi-riemann 和 davegoldblatt/openai-zeta-proof-check。它们检验的是形式化证明，而不是论文。
• 社区目录 vibemathed：导入 OpenAI 的结果。

编者注：我们没有审核任何结果。数学描述经过简化，面向非专业读者，反映的是 OpenAI 的说法，而不是数学界的共识。