当机器先给出答案：Navier–Stokes 事件中的正确性、传承与研究伦理

从一个突然出现的答案开始

原始材料与延伸阅读 · 25 位菲尔兹奖得主的联合声明 · Terry Tao 对 Alpöge–Buckmaster 成果的介绍 · OpenAI 的 Navier–Stokes 说明 · Tristan Buckmaster 的公开陈述

Navier–Stokes 方程描述水和空气等流体的运动。三维不可压缩方程的解能否始终保持光滑，是七个千禧年大奖难题之一。问题既属于偏微分方程，也牵连飞机设计、天气预报和血液流动。所谓有限时间奇异性，是指一个从光滑状态开始的解，在有限时间内出现速度发散等现象。黏性通常会抑制这种失控，非线性却可能把能量不断推向更小的尺度；两种作用如何平衡，正是问题长期困难的原因。

2026 年 9 月的第一周，OpenAI 把这道问题带进了一场关于 AI 数学能力的公开竞赛。按照公司的说明，8 月 28 日起，内部训练中的新模型显示出很强的数学能力。9 月 1 日，团队听到两个千禧年问题可能已经被解决的传闻，于是让近一百个智能体并行探索未解问题。约五十小时后，系统先得到无外力 Euler 方程的结果。Euler 方程可以看作忽略黏性的流体模型；这条路线随后把研究资源引向 Navier–Stokes。

OpenAI 说，智能体在 9 月 5 日得到 Navier–Stokes 的解析解答，距离启动约 88 小时。之后，团队累计投入约 17 小时在 Lean 中完成形式化和核验，并于 9 月 8 日公开论文与代码。Lean 是一种交互式定理证明工具；形式化证明以明确的命题、依赖和检查规则呈现，可以由可信内核重复检查。OpenAI 将这项工作描述为在所声明的范围内解决 Navier–Stokes 千禧年问题，同时把它作为模型能力和研究速度的公开记录。

只看这条时间线，新闻的核心很清楚：一个长期未解的问题出现了新的、可以继续检查的结果，而且形式化材料随论文一起公开。争论从另一条研究时间线进入公共记录开始。

同一周，另一条研究线进入公共记录

Tristan Buckmaster 和 Antonin Alpöge 此前已经围绕流体方程工作了很长时间。Buckmaster 的公开陈述说，他们在 8 月 15 日取得了关于带光滑外力的 Boussinesq 方程和 Euler 方程的进展，并把数月的研究对话、提示和材料保存在 Codex 会话中。对普通读者来说，这些会话更像研究过程的工作台：它们记录问题怎样被提出、线索怎样被试探，承担的是过程记录的作用。

9 月 3 日，关于大型语言模型可能解决重大开放问题的传闻开始流传。Buckmaster 随后联系 OpenAI，并在 9 月 6 日的两次通话中询问：内部系统是否访问过他和 Alpöge 在此前两个月留下的未公开研究，或者是否曾把这些材料用于训练。Buckmaster 公布的文书记录了这些问题和通话内容。9 月 7 日，他和 Alpöge 提前公开了不可压缩多孔介质方程、二维 Boussinesq 方程和三维不可压缩 Euler 方程的三个有限时间爆破结果，以及对应的 Lean 形式化。这些结果研究的是相邻方程，属于同一条流体奇异性研究路线；提前公开也让他们的贡献和时间戳进入了同一份公共记录。

公开文书还记载了优先权与署名安排的争议，包括是否应把 Anthropic 的员工 Levent Alpöge 列入联合发布。9 月 10 日，OpenAI 更新说明，称 Buckmaster 之前两个月的 Codex 提示不可能影响内部系统或训练，也称研究人员和智能体在对方成果公开前没有看到这些成果；公司同时表示，完成项目和 Lean 核验后曾希望安排并行发布，并承认对方在带外力 Euler 结果上的优先权。

双方在数据隔离、优先权和署名安排上的公开说法并不相同。要判断这些说法，需要访问日志、训练数据来历、通信记录、版本时间戳和能够由独立方检查的审计材料。争议的焦点因此从证明本身扩展到研究者能否在公平的条件下保存、说明和发表自己的工作。

Tao 的介绍与联合声明把问题带到更大的背景

9 月 7 日，Terry Tao 介绍 Alpöge–Buckmaster 的工作时，称其为令人振奋的新进展，并解释了三个有限时间爆破结果与无外力 Navier–Stokes 之间的关系。他也提到，最初的证明文字非常难读，作者正在把它改写成专业论文；在这个过程中，解题、理解证明结构和提炼可复用的方法并不在同一个时间尺度上。

9 月 11 日，Tao 发布了题为《A Severe Misalignment of AI in Mathematics》的联合声明，初始签署者包括 25 位菲尔兹奖得主。声明把概念理解和数学洞见放在共同体最重视的位置，把解题描述为获得这些理解的工具或代理。它同时批评 AI 公司把著名开放问题当作 benchmark，担心竞赛会把发布速度推到前面，挤压认真写作、方法提炼、先行工作引用和知识整合。

声明发布在 OpenAI 公开论文后三天，因而自然进入同一场讨论。声明文字面上讨论的是更广泛的 AI 数学实践，并没有对某一篇论文作出数学裁定。它提出的中心因果链却与当前事件相连：当一个答案被当作模型能力的公开成绩，速度和轰动性会不会压过解释、归属和共同体吸收结果所需的时间？这使后面的判断必须把数学、传承和研究过程分开。

从三个维度看这场事件

前面的时间线说明了事情怎样发生。接下来需要换一个角度：同一个数学结果进入公共讨论时，会同时呈现出三种状态。把这三种状态分开，才看得清联合声明在谈什么，也看得清这次争议还有哪些问题需要另一套证据。

第一种状态是正确性。它问的是：AI 产生的命题在明确的假设和适用范围内是否成立，证明或形式化对象能否由别人独立检查。这里有一个客观层面，也有一个认识层面。命题可以已经成立，其他人仍然需要时间去读论文、检查依赖、复现实验或形式化代码，才会形成自己的判断。结论的成立与共同体认识它所需的时间，属于同一件事的两个阶段。

第二种状态是知识传承。一个结果被检查过，还需要被写成别人能够阅读、引用、教学和继续发展的知识。传承的过程包括说明问题的来历，交代先行工作，解释证明中真正起作用的结构，标明适用边界，并让后来的研究者知道怎样复用它。它关心的是一个结果能否进入共同的知识体系，以及人类能否从中汲取结构和方法。

第三种状态是伦理。它问的是结果怎样产生、怎样发布，以及过程中是否尊重了研究者和共同规则。未公开资料是否被访问或用于训练，贡献和署名是否准确，优先权如何处理，相关方是否拥有公平的发表机会，都属于这一层。它需要的证据是访问记录、数据来历、通信、时间戳和独立审计，和判断数学命题的证据不同。

联合声明主要触及前两个维度。它把概念理解和数学洞见放在首要位置，并担心把著名开放问题作为 benchmark 会把答案的速度推到知识传承之前。它讨论的是“得到一个答案”和“把答案变成共同知识”之间的关系。当前事件中的数据隔离、优先权与署名争议，则属于第三个维度；它们不能由声明对数学理解的强调直接解决。

按照这三个维度，下面依次讨论 OpenAI 已经公开的论文和形式化材料为正确性提供了什么，知识传承为什么需要自己的时间和工作，以及一次有价值的结果能否与不恰当的研究过程同时存在。

第一问：形式化的结果在什么范围内成立

形式化把自然语言里的命题、变量、假设、依赖和证明写成检查器能够处理的对象。若论文中的主张与形式命题逐项对应，依赖关系公开，内核确实接受证明项，其他人也能按相同条件重现检查，那么结论就在所声明的范围内获得了明确的正确性边界。它有没有揭示新的结构、是否容易阅读、能否进入教材，则需要另一组证据。

SAT 提供了一个很小、但很有力的参照。面对一个固定的布尔实例，求解器可以给出一个满足赋值；若断言实例不可满足，则可以给出一份独立检查器能够验证的证书。证书通过以后，工程系统可以在这个范围内排除一个设计、确认一组约束，或者继续下一步计算。使用者不必先理解求解器搜索过的每一条路径，证书也不必先被提炼成优雅理论，结果才有用。

形式化的 AI 证明沿着同一条逻辑链走得更远：它给出精确命题、证明对象、依赖和内核检查结果。若自然语言和形式命题忠实对应，证明没有隐藏缺口，检查在公开的基础上可以重现，那么这个结果在其范围内就具有可使用的正确性。它还可能需要很长时间才能被人类读懂，结构解释、方法推广和教材化也许要在之后完成；这些工作的延后不改变已经建立的形式证据。

正确性和知识理解，是两种可以并行发展的贡献。不能因为一个形式化结果尚未在几天内变成教材，就把它的科学价值归零。若相同范围、相同形式状态的结果由人类提出，研究共同体会给它数月乃至数年的核查和消化时间；仅仅因为来源是 AI，就要求它在几天内同时交出完整的概念解释，否则不承认结果，这就把来源置于作品之上，形成了双重标准。对形式化不忠实、依赖有缺口、论文难读或归属不准确的批评都可以成立，但批评应当指向这些具体问题。

关于把形式化结论做成可调用、边界清楚的数学组件，我们在另一篇文章中展开讨论，这里只保留它与本节的连接：结果先要有可检查的边界，之后才谈如何被稳定地复用。

关于可调用的形式化数学组件

第二问：知识传承如何发生

联合声明强调认真写作、方法解释、准确归属、教学和后续研究，这些要求确实构成数学共同体的长期基础。一个结果进入文献、课堂和后续工作之后，才会逐步成为别人能够理解和继续发展的共同知识。作者公开结果以后，仍然要为这段路承担责任。

知识传承是独立的贡献，也是结果进入共同知识的过程。它不需要被设成使用正确结果的前置许可。一个经过可靠检查的结论，可以先在清楚的范围内被引用、复现和调用；与此同时，人们再花时间解释它的证明结构、寻找更好的表述、发现可以推广的方法。对于数学来说，留下可传承的知识是一项功能，留下边界清楚、可以可靠复用的组件是另一项功能。两者可以彼此加强，完成的时间也可以不同。

庞加莱猜想提供了一个具体的时间尺度。Perelman 的第一篇相关预印本发表于 2002 年 11 月 11 日，随后两篇材料在 2003 年 3 月和 7 月出现；从第一篇预印本到初始材料基本齐备，已经过去约八个月。此后，Hamilton、Kleiner、Lott、Tian 等人的核查、解说和整理继续推进。到 2006 年，距离第一篇预印本约三年半，这项证明才逐步形成共同体可以公开依靠的理解。它在最初几天没有完成教材化，并没有抹去它当时已经带来的数学内容。

OpenAI 在 9 月 8 日公开论文和形式化材料，到本文 9 月 14 日修订时只有六天。六天足以让读者看到论文和代码，远不足以让共同体完成所有核查、解释和结构提取。我们可以批评发布中的文字是否清楚、相关工作是否完整，也可以要求后续论文把证明写得更容易阅读。尚未完成的传承工作，不能倒过来成为结论没有价值的证明。

如果一个人类作者提交同样的形式化结果，我们会把理解和教材化看作需要时间的后续工作。对 AI 参与的结果也应保留同样的时间尺度。评价应当随着证据推进：先看命题是否成立，再看解释是否可靠，最后看它能否进入更广的数学知识体系。

庞加莱猜想的时间资料 · 庞加莱猜想的时间线 · Perelman 的第一篇预印本

第三问：数学价值与研究过程是否是同一件事

一个结果的数学价值，与它是怎样产生和发布的，是两组不同的问题。模型公司即使带有商业目标，也可能完成科学上有用的工作；动机不会自动抹去结论的价值。反过来，结论即使正确，也不能替过程中的数据使用、署名或优先权问题提供豁免。

就这次事件而言，需要分别追问：未公开的 Codex 材料是否被访问或用于训练；研究者的提示和数据是否与内部系统隔离；贡献和作者名单是否准确；在得知相关研究存在以后，是否仍然提供了公平的并行发布安排；谁掌握了决定公开时间的权力。Buckmaster 的文书与 OpenAI 的更新给出了不同叙述，公开材料可以确认争议存在，却还不足以独立裁定每一项事实。

如果一家公司为了抢先发布而使用了未公开研究，或者让研究者在数据边界和署名上处于明显弱势，即使最后的数学结论正确，也属于研究治理失败。如果日志、训练数据来历、时间戳、通信和独立审计显示系统保持了隔离，研究者仍然有权追问优先权和署名如何被处理。数学证据和过程证据各自回答自己的问题。

因此，判断一个结果有没有价值，和判断一次发布是否恰当，应当分别进行。前者要看论文、形式代码、依赖和复现；后者要看访问日志、数据来历、通信记录、署名安排和可供独立第三方检查的审计。把其中一组证据拿来替代另一组，都会让讨论偏离问题本身。

从结果到共同知识：一条可追溯的科学流程

一个新的机器辅助结果可以沿着一条连续的科学流程前进。流程中的每一步都增加一种可信度，也都留下可以被后来者检查的记录：

这些阶段可以随着工作推进分别完成，不需要等到所有工作结束才开始。形式结果可以先成为可核验、可引用的记录，知识传承随后继续；论文的可读性和外部审评也可以在公开之后不断提高。不同阶段有不同的证据，公开文本应当把已经完成的部分和仍在进行的工作写清楚。

• 先固定命题、适用范围、形式证明、依赖关系、公理状态和可复现的检查方式。
• 再把形式对象写成研究者能够顺畅阅读的论文，交代问题背景、先行工作、例子和证明路线。
• 将论文和代码作为公开预印本发布，接受外部审评，记录问题、修订和更正。
• 让论文、形式代码、版本时间戳、引用和公开讨论保持在同一条可追溯记录上。
• 最后由综述、课堂、教材和后续研究逐步提取结构，让结果既能被理解，也能被可靠复用。

阅读 Proof Engine 研究纲领

让发现、核验与传承各得其时

这场事件让几个常被混在一起的判断重新分开：一个结论是否正确，一个结论是否已经被共同体充分理解，以及一次研究过程是否尊重了参与者和公共规则。它们彼此相关，却各自需要证据，也各自有自己的时间。

我们会继续把每个结果沿着同一条链推进：固定命题和形式边界，完成可重复的内核检查，把证明写成人类能够阅读的论文，公开预印本并接受外部审评，再把修订、解释和后续应用留在可追溯的版本记录中。这样做同时保留了知识的初版，也给它进入共同知识和可靠复用留下道路。

数学成果可以以两种方式长久留下来：成为人类能够理解、教学和传承的知识，也成为边界清楚、能够在后续工作中可靠调用的组件。科学的发展需要这两种时间，也需要让它们在同一份诚实的记录中相遇。新技术改变发现和核验的速度，科学共同体要做的，是把这种速度转化为能够被检查、被解释、被传给后来者的成果。