OpenAI称AI智能体88小时给出纳维—斯托克斯方程解法，数学界争议焦点在哪里？

【软盟资讯·新闻导读】OpenAI称，约1万个AI智能体协同运行88小时，针对纳维—斯托克斯方程存在性与光滑性问题提出了解法，并公开论文和Lean验证代码。事件随即引发争议：给出解法、完成形式化验证与获得数学界独立认可，并不是同一件事。

OpenAI公布了一项仍待核验的数学成果

据公开报道，OpenAI当地时间9月8日宣布，其内部系统针对纳维—斯托克斯方程的“存在性与光滑性”问题给出了证明方案。该系统由一个尚未公开、据称强于GPT-6 Astra的下一代模型驱动，组织约1万个AI智能体协同工作，首批智能体启动约88小时后，系统于9月5日得到解法。

OpenAI同时公开了一篇166页论文以及Lean形式化验证代码。按照公开信息，AI智能体阶段完成解答后，Astra又用约17小时将相关内容转化为Lean可以检查的形式。OpenAI方面将这项成果视为通用人工智能进入前沿科学发现的重要信号，但报道同时指出，相关结论仍需要数学界进行独立检验。

这也是事件最容易被标题简化的地方。“AI在88小时内解出千禧年难题”是一种传播性很强的说法，但它至少包含三个需要分别判断的层次：系统是否提出了一个具有数学意义的解法，形式化系统是否检查了这份证明，以及数学家是否确认其满足题目要求、没有遗漏关键条件。这三层不能直接画等号。

纳维—斯托克斯问题究竟难在哪里

纳维—斯托克斯方程是描述流体运动的重要数学模型，相关千禧年难题关注三维情形下，解是否能够始终保持光滑，还是可能在有限时间内出现奇点。所谓奇点，可以简单理解为方程描述的某些量在演化过程中失去原有的良好性质，导致解无法继续以预期方式保持规则。

这个问题的困难不只是计算量大。研究者需要从方程的结构出发，严格处理流体运动中的速度、压力、涡旋以及外力之间的关系，并证明结论适用于题目要求的完整范围。一个看起来合理的物理图像、局部推导或数值实验，都不能自动成为满足数学定义的证明。

公开报道显示，OpenAI此次并没有宣称证明“无外力情况下的解必然光滑”。其选择的是克雷数学研究所题目的C、D方向，即构造一个有限且处处光滑的外力，使得相应的光滑解不能维持到所有时间。报道将这一方案描述为有限时间产生奇点的证明路径。

这一点直接关系到如何理解OpenAI的表述。它并非简单地说“计算机找到了一个答案”，而是声称在千禧年难题允许的方向上构造了满足条件的对象。不过，最终是否完整覆盖题目定义、推理链条是否存在缺口，仍需要熟悉该领域的数学家逐步检查。

“88小时”背后是一套智能体协作流程

从公开披露的过程看，项目并不是让一个模型独立完成一篇证明，而是将研究任务拆分给大量智能体。不同小组获得不同题面，可以读取缓存的互联网资料、运行代码并在组内交流，再由Codex汇总思路、交叉分发给其他智能体继续检验。

报道提到，接近100个智能体先花费约50小时研究无外力欧拉方程的有限时间奇点问题。随后，相关资源转向纳维—斯托克斯方程。整个项目产生约270万条消息，输出约1300亿个Token，项目耗资达到数百万美元的说法也出现在公开报道中。

这套流程的关键，不只是模型本身的推理能力，还包括任务分解、候选方案筛选、代码执行、结果传递和重复检查。传统数学研究通常由少数研究者长期积累并反复讨论，而这次尝试将资料检索、思路生成、计算实验和证明整理组织成了一条大规模流水线。

不过，智能体数量并不等于有效证明数量。大量并行尝试可以提高探索空间，也可能带来重复推理、错误传播和难以追溯的问题。对于数学成果而言，最终需要关注的是证明是否准确、假设是否清楚、每一步是否可复核，而不是参与系统的智能体有多少。

Lean验证能证明什么，又不能证明什么

Lean是一类计算机定理证明器。将数学论证转化为Lean可以检查的形式，意味着形式化系统能够依据预先定义的公理、规则和库，对代码所表达的推理链进行机械检查。与只发布一篇自然语言论文相比，公开验证代码无疑提高了成果的可复核程度。

但“Lean验证通过”并不等于“数学界已经确认问题被解决”。首先，形式化过程需要把自然语言中的概念、假设和结论准确转译到系统中。如果形式化命题与原始问题不完全一致，代码即使通过，也不能替代对研究目标的判断。其次，验证器检查的是输入给它的形式化内容，不能自行判断研究者是否选对了题目方向，也不能自动发现某个关键条件是否在建模阶段被遗漏。

因此，事件中“完成形式化验证”是重要进展，却不应被直接写成“获得独立数学认证”。独立检验还需要其他研究者在不依赖OpenAI内部解释的情况下，阅读论文、运行代码、检查外力构造及其推导，并判断成果是否符合克雷数学研究所对该问题的严格要求。

OpenAI称不会申领该题目悬赏的100万美元奖金。是否申领奖金并不能决定证明真伪，但不申领奖金也不能替代同行评议。对一项可能改变数学研究史的成果，公开材料、可运行代码和外部复核都需要经受时间检验。

争议集中在成果独立性和研究来源

成果公布后，美国纽约大学数学教授特里斯坦·布克马斯特提出质疑。他表示，自己曾与一名Anthropic研究人员在相近方向研究带光滑外力的欧拉方程有限时间奇点，并完成Lean验证。由于相关研究曾使用Codex处理对话，他进一步担心，OpenAI系统是否可能以某种方式接触到相关研究内容。

这使争议从“证明是否正确”扩展到“成果是否独立产生”。如果一个系统在训练或研究过程中接触过正在进行的研究，即使没有直接复制某一段文字，也需要说明信息来源、时间线和研究边界。对于宣称解决长期未决难题的成果，原创性、可追溯性和数据使用范围同样重要。

OpenAI方面回应称，研究人员和AI智能体没有看到对方成果，也没有为解题访问特定用户数据。但公司同时表示，不能完全排除相关产品数据曾以某种方式参与训练，并强调双方研究中的欧拉方程外力设定不同。

双方说法目前并未形成完整的独立结论。需要区分的是，研究方向相近、使用相似工具，并不自动证明存在抄袭；而OpenAI无法完全排除训练数据存在某种关联，也不等于已经确认其系统使用了特定研究成果。真正需要公开核验的，是双方问题设定、时间线、证明结构和代码之间是否存在实质性对应关系。

AI科研突破应当接受怎样的检验

这起事件至少提出了三道检验题。

第一道是数学正确性：论文中的每个定义、引理和推导是否成立，外力是否满足题目要求，奇点结论是否真正对应纳维—斯托克斯方程，而不是只对应一个相近但更弱的问题。

第二道是形式化一致性：公开的Lean代码是否覆盖论文的核心论证，代码依赖的库、前提和定义是否与论文表述一致，其他研究者能否在公开环境下复现检查过程。

第三道是研究独立性：系统是否接触过相关研究者的未公开成果，训练数据和用户数据的边界如何界定，项目团队是否能够解释关键思路的产生过程。对于AI系统而言，这些问题比传统论文中的“作者贡献”更复杂，因为模型可能同时承担资料整理、方案生成和证明重写等多种角色。

在这些问题得到回答之前，比较稳妥的表述应是：OpenAI宣布其AI智能体系统提出了纳维—斯托克斯方程相关问题的解法，并公开了论文和Lean验证代码；成果的数学正确性、形式化覆盖范围以及独立原创性，仍待外部专家检验。把“宣布解决”直接等同于“已经解决”，会跳过最关键的验证环节。

【软盟观察】

这起事件的价值，暂时不应只用“AI是否已经解决千禧年难题”来衡量。更值得观察的是，AI智能体开始尝试把长期数学研究拆分为多个可并行执行的环节：提出假设、寻找相近结果、运行计算、互相审查，再将自然语言推理转化为形式化代码。即便最终证明存在缺陷，这种组织研究工作的方式也可能影响未来的软件开发、科学计算和理论研究。

但科研突破的可信度，不由运行时长、智能体数量或Token规模决定。88小时可以说明系统完成了一次高强度探索，不能说明结论已经通过数学共同体的审查；Lean代码可以提高复核效率，也不能替代对问题定义、研究来源和原创性的判断。尤其当成果与其他团队的研究方向高度接近时，数据治理和研究记录就不再是附属问题，而是成果可信度的一部分。

对大模型和AI智能体行业而言，这次事件也提醒企业减少“先宣布、后解释”的冲动。公开论文、验证代码、实验时间线和数据边界，应当尽可能同步披露，并为独立研究者留下足够的复核空间。对媒体和读者而言，最重要的区分则是三句话：AI给出了一个方案，形式化系统检查了一部分或全部推理，数学界确认这是一份满足原题要求的独立证明。只有第三个层次完成后，才适合把“声称解决”改写成“已经解决”。