OpenAI 请外部专家核查其 AI 在数学、计算机科学和物理学领域产出的证明

于是 OpenAI 请来外部专家充当结果的“牧羊人”。根据他们的建议，公司对每个领域的处理方式各不相同。OpenAI 表示，它还把数学和计算机科学领域的证明翻译成了 Lean。

Lean 是一种编程语言，能让计算机逐步检查证明的每一步。但这并不能保证结果没有错误。Lean 只检查证明是否在 Lean 中按所写的方式确立了该命题。专家仍需判断这个命题是否真正抓住了原本要解决的问题。

如果 OpenAI 是对的，计算机科学的一个核心假设就是错的

计算机科学领域的这项结果围绕指数时间假设（ETH）展开。它涉及布尔可满足性问题，即 SAT。SAT 处理的是一个逻辑公式，其变量只能取真或假。问题在于，能否为变量赋值，使整个公式为真。

变量很少时，你只需穷举所有组合。但每增加一个变量，可能性就翻一倍。变量达到 100 个时，你面对的数字已经有 31 位。

简单说，ETH 认为不存在真正的捷径。你可以加快试错，但在最坏情况下，计算时间仍呈指数增长，每增加一个变量就按固定倍数增加。

OpenAI 表示，可满足性问题与P 与 NP 问题密切相关。那是一个著名的未解问题：一个解能被快速验证的问题，是否也能被快速求解？对 SAT 来说，验证很容易，因为只需代入一个候选答案算一算。难的是找到一个可行的答案。

SAT 被视为这类难题的教科书式例子。一旦有了快速求解它的方法，成千上万个其他问题也会立刻变得容易求解。多数专家认为不存在这样的方法。这个信念被简称为“P 不等于 NP”。

ETH 比这个猜想走得更远。它不仅说 SAT 很难，还说明了难到什么程度。即使 ETH 被推翻，P 仍可能不等于 NP，所以难题不会自动变简单。

ETH 此前被广泛接受为真。图论、计算生物学、数据库和计算几何领域的数百篇论文都建立在它之上。例如，它们证明：如果 ETH 成立，某个问题就不可能快于某个特定时间被求解。

现在 OpenAI 称其系统证明了 ETH 是错的。如果证明成立，这些论文就失去了基础。它们的结果不会自动变错，但也不再是被证明的。

OpenAI 表示，这一结果可能帮助研究人员找到更好的算法。不过，要把它转化为实际收益，仍需大量研究。

实际收益尚不明确，但理论上的影响会很大

SAT 在实践中非常重要。被称为 SAT 求解器的专用程序，例如可以检查芯片设计中的错误、测试软件。

它们如今往往已经能处理包含数百万个变量的公式。这是因为现实应用中的公式通常比 ETH 所处理的最坏情况容易得多。只加快最坏情况，并不会自动让这些程序受益。

MIT 教授 Ryan Williams 在 X 上也表达了类似的谨慎态度。有用户问他，普通开发者最先会注意到什么，Williams 说目前没人知道。他表示，按现在的进展速度，实用 SAT 求解在 12 个月内取得实质性进展是有可能的。"也可能什么都不会发生。我真的不知道，"他坦言。

这一结果还会在复杂性理论内部引发连锁反应，尤其是电路研究——电路是由 AND、OR、NOT 等简单逻辑门组成的网络。Williams 表示，如果 OpenAI 的结果成立，那么可以推出某一类极为困难的问题无法用小型电路求解。这里的"小型"是指：当输入长度翻倍时，电路最多只需要大约两倍数量的逻辑门。

提出 ETH 的人正在检验它是否错了

Williams 将与加州大学圣迭戈分校的 Russell Impagliazzo 和 Ramamohan Paturi 一起独立核查并解释这一结果。Impagliazzo 和 Paturi 当年与 Francis Zane 共同提出了 ETH。Williams 写道，这个小组没有签署任何保密协议，是无偿工作，并计划在过程中随时分享阶段性发现。

在一封公开信中，三人也明确表示，他们的参与并不代表认可这一主张。他们写道，如此重大的结果需要审慎、独立的审查。

应这个小组的要求，OpenAI 正在公开全部原始数据，包括书面证明和 Lean 证明。公司还承诺出资举办一场会议，讨论这一结果对该领域的意义。

一个数十年前的波动猜想如今可能在所有维度上都成立

这项数学成果涉及一个关于波的猜想，比如声波、光波或地震波。数学家 Christopher Sogge 于 1991 年提出了它。

波可以聚集在单个点上，就像放大镜焦点处的光一样。该猜想认为，这种极端聚集只会短暂持续。按时间平均来看，波的表现比极端情形所暗示的要更平滑、更均匀。这也是它被称为局部平滑猜想的原因。

在此之前，它只在二维情形下得到证明，即水面这类表面上的波。Guth、Wang 和 Zhang 在 2019 年完成了这一证明。OpenAI 表示，其模型现已给出适用于所有维度的证明，包括空间中的波，以及维度更多的假想空间中的波。

OpenAI 称这一结果的意义不止于波。由于局部平滑猜想是该领域的基础性命题，另外两个著名猜想可由它推出，分别是几何学中的挂谷猜想和傅里叶分析中的 Stein 限制猜想。傅里叶分析把声音之类的信号分解为一个个振荡。证明了局部平滑猜想，也就自动证明了这两个猜想。

挂谷猜想本身就说明了这类衍生结果有多难。Wang 和 Zahl 直到 2025 年才只证明了三维情形。据 OpenAI 称，如今这两个猜想在所有维度上都将得到解决。

与前两项成果不同，没有专门的小组在跟进这份证明。OpenAI 表示，它确实联系了一位外部专家，讨论过这类合作。不过，按照这位人士的建议，公司直接公开了证明文本和 Lean 证明。这样，研究人员可以自行决定如何核查这一结果。

OpenAI 想为量子场论奠定坚实的数学基础

这项物理成果触及粒子物理的根基。物理学家用量子场论描述基本粒子及其之间的作用力，OpenAI 称其为现代理论物理中最重要的框架。它的预测极其精确，但这些理论缺乏严格的数学基础。

于是物理学家转而使用近似方法，比如一块假想的点阵，并不断把它划分得更细。这样做能否产生一个唯一且自洽的理论，也就是理论在数学意义上是否“存在”，目前仍是未解的问题。至于它是否正确描述了自然，则是另一个问题。

OpenAI 表示，其 AI 已证明某些量子场论在四维（三个空间维度加时间）中确实存在。迄今为止，还没有人在粒子之间存在相互作用的理论上，于四维中完成这样的证明。

强相互作用是这一切的核心。它把夸克束缚成质子和中子，进而把原子核维系在一起，传递这种力的粒子是胶子。此次证明涵盖三个层层递进的理论。

最底层是杨-米尔斯理论，它只描述胶子，不包含夸克。该理论与千禧年大奖难题之一相关，每道题由克莱数学研究所悬赏 100 万美元。

这道难题包含两部分。第一是证明杨-米尔斯理论在数学上存在；第二是证明它具有所谓的质量间隙。OpenAI 明确表示，它只解决了存在性部分。这意味着该千禧年难题并未被完全解决。

质量间隙指向一个谜题。在方程中，胶子没有质量，而由无质量粒子传递的力通常作用范围极远，由无质量的光传递的电磁力就是一例。相比之下，强相互作用只在极短距离内起作用，比如原子核内部。物理学家对此的解释是：胶子会聚集成确实具有质量的结构，其中即使最轻的也不是无质量的。零与这个最小可能质量之间的差距，就被称为质量间隙。计算机模拟支持这一点，但还没有人从数学上证明它。

第二步是量子色动力学（QCD），它加入了夸克，完整描述了强相互作用。

OpenAI 称，这两个理论之所以能在数学上存在，主要归功于渐近自由。也就是说，粒子靠得越近，强相互作用就越弱。正因如此，即使点阵划分得越来越细，数学处理依然可控。

第三步通常应是粒子物理标准模型，它描述了四种基本作用力中的三种，唯独不含引力。但据 OpenAI 所说，它无法推广到任意小的距离，因为其中一些力在短距离上反而变强，而不是变弱。

因此，这次证明覆盖的是最简单的大统一理论。它把三种力归结为一种，并包含标准模型中的力粒子和物质粒子。与强相互作用一样，这种统一力在短距离上会变弱。不过，还没有任何实验证实这类理论。

如果证明成立，这三个步骤就都有了数学基础。这不会改变物理学的任何预测。OpenAI 希望它能将量子场论变成一门数学上严谨的学科。

由 David Gross 领衔的小组将负责推进这项工作。Gross 因在渐近自由方面的研究分享了 2004 年诺贝尔物理学奖。该小组还包括 Michael Douglas、Arthur Jaffe、Igor Klebanov 和 Nikita Nekrasov。Jaffe 曾参与撰写关于杨-米尔斯理论的千禧年大奖难题。

OpenAI 表示，它已经把杨-米尔斯证明翻译成了 Lean。不过，与计算机科学小组不同，这个小组目前暂不公开 AI 的材料，并计划自行撰写成果。

OpenAI 的评审流程本身也引发质疑

OpenAI 承认这一流程存在取舍。公司写道，谁先挑选首批评审者，谁就在一定程度上决定了谁先参与进来，而有些人会更早地比其他人知道更多信息。OpenAI 还表示，目前尚不清楚这三种方式中哪一种效果最好。

OpenAI 表示，它并不为这些发现索取科学功劳。功劳应归于解释结果的各个小组。公司似乎是在回应此前纳维-斯托克斯方程公关灾难之后的批评。

OpenAI 还承诺向西蒙斯基金会捐赠 500 万美元，用于资助围绕 AI 成果的研讨会和会议。

Williams 所在的小组还借这封公开信呼吁展开一场超越评审本身的更广泛讨论。核心问题包括：如何验证 AI 突破、谁能获得这些突破，以及功劳该归谁。