OpenAI 与那 88 小时「证明」：可能根本不算证明

那个标题，并不是标题本身

OpenAI 声称在 88 小时内解决了一个有着 90 年历史的千禧年大奖难题。同时，该公司也在反复强调，它们并不打算申领这笔奖金。这两句话没法安静地共存。前者是产品发布会，后者是危机公关。

真正发生的事情，比标题更有趣，也比 OpenAI 希望你相信的要更加悬而未决。

这项声明

9 月 5 日，OpenAI 宣布，一个由大约 1 万个 AI 智能体（运行在内部未发布模型上的机器人，其能力远超任何公开版本）组成的集群，找到了纳维-斯托克斯存在性与光滑性问题的部分解。该系统交互了近三百万条消息，消耗了 1300 亿输出 token。按 OpenAI 自身的定价，如果外部计费，这笔计算成本约为 1000 万美元。

这一结果解决了国际克莱数学研究所要求完整证明所需的四条陈述中的两条。OpenAI 称，发布这项发现是为了展示其模型的能力。并表示，它们不会追求那 100 万美元的奖金。

在 AI 行业里，这句话读起来像是一份认罪协议。

这项指控

同一天。数小时之前。纽约大学讲师特里斯坦·巴克马斯特（Tristan Buckmaster）发布了一篇详细记录。他与 Anthropic 数学家莱文特·阿尔波格（Levent Alpoge）一直在使用 OpenAI 的 Codex 研究同一问题。巴克马斯特称，9 月 3 日，关于他们进展的信息传到了 OpenAI。第二天，OpenAI 就发布了纳维-斯托克斯的结果。

巴克马斯特的记录包含邮件往来，他在其中挑战 OpenAI 的时间线和研究方法。他的核心不满是程序性的，而非数学性的：OpenAI 是否从其自身平台的用户（无论多么间接）那里获取了工作成果。

OpenAI 的回应是经过精心校准的。公司祝贺了巴克马斯特和阿尔波格的"同步研究"。它表示，在公开发布之前，它从未以任何方式见过他们的工作。它承认了一种可能性——该公司称之为"不太可能"——即从他们对 Codex 的使用中得出的去标识化数据改进了驱动 OpenAI 内部工具的模型。随后它指出，它们的证明大相径庭，甚至所证明的具体结果也不相同。

“去标识化"这个词在这里承担着重任。它是企业承认风险却不接受责任的标配免责声明。如果巴克马斯特与 Codex 的交互影响了内部模型的权重，而该模型随后生成了被派去研究纳维-斯托克斯的智能体，那么 OpenAI 可能在不知情的情况下使用了无偿研究人员的产出。这在刑法意义上不是盗窃。这是商业模式按其设计正常运行，问题在于这个设计有一个道德盲点。

数字究竟说了什么

让我们具体谈谈 1 万个智能体和 1300 亿 token 代表什么。这是披上对话界面的蛮力搜索。智能体之间相互对话。它们提出引理。它们验证步骤。它们回溯。这个过程与 Lean 和 Coq 等系统中已经存在的大规模定理证明方式相仿——只是在工业规模上运行，且没有人类策展人引导证明结构。

四条陈述中的两条只是部分结果。克莱数学研究所不为部分结果颁发奖金。它也不接受由 AI 生成、缺乏人类验证且机器可检查的形式化证明。OpenAI 两者都未提供。因此，该公司的公告并非数学证明。它是对一种能力的展示——如果规模放大并与形式化验证工具配对，这种能力有朝一日可能产生一个证明。

这个区别之所以重要，是因为市场正在按照"这是前者"来为这项公告定价。

真正的问题：验证，而非生成

这一事件暴露了基础模型在真理二元性的领域里的可靠性边界。语言模型可以生成看起来像证明的文本。它也可以生成看起来像证明、却在 200 步中的第 47 步包含微妙错误的文本。唯一能知道的方法是将论证跑过形式化检查器。这很慢。这很昂贵。但这正是证明的全部意义所在。

OpenAI 的 88 小时运行没有包含形式化验证步骤。它生成了一个人类可读的论证，表明完整猜想中的两个子陈述似乎成立。独立数学家尚未审查细节。克莱数学研究所尚未表态。一位认为自己的工作被导入系统的教授正在公开质疑公司的时间线。

这不是一次失败的证明。这是一项未经核实的声明。二者之间的差异就是一切。

谁赢，谁输

OpenAI 赢得了关注。围绕"AI 作为研究者"的股票相关叙事又添一章。公司的内部模型现在有了一个旗舰演示，没有任何公开基准能与之匹敌。这个演示将在未来数月内的融资材料、企业推销和监管证词中被引用。

巴克马斯特和阿尔波格损失了时间。他们的工作进入了一个他们未曾签署资助的系统。该系统是否在法律上有责，取决于他们在开始使用 Codex 时接受的条款。这是否在道德上站得住脚，则是另一个问题，而整个行业尚未给出答案。

更广泛地看，数学界损失了标准。当一个来自未发布模型的部分结果获得了与百年猜想同等规格的头条待遇时，数学传播中的信噪比就降级了。未来的每一项声明都将与这一刻进行比较。有些会更严谨，大多数会更松懈。

接下来会发生什么

三种情景是 plausible 的。

第一种，形式化验证工作在接下来几个月内运行，要么确认部分结果，要么发现漏洞，要么两者兼有。这将是最诚实的路径，也是最慢的路径。

第二种，OpenAI 在证明助手里发布其论证的形式化版本。如果机器检查器接受了它，数学界将认真参与这项工作，无论结果是如何发现的。起源故事次于输出。这是对除感到贡献被占有的研究者之外的所有人而言的最佳结果。

第三种，这项声明退入背景噪音——在一个每周产生一个突破叙事的行业里。智能体回到更便宜的任务。内部模型被部署用于编程助手和客户支持流程。纳维-斯托克斯的结果成为一则附带新闻稿的注脚。

OpenAI 称不想赢得千禧年大奖。但该公司已经让这项声明实现了货币化。这就够了。现在的问题是，数学界会将这件事视为一种方法还是一场营销活动——以及它是否负担得起以这两种方式之一行事而不树立一个奖励速度胜过严谨性的先例。