OpenAI数学证明遭学界质疑

OpenAI可能没完全看懂自己的证明

OpenAI关于纳维-斯托克斯方程的候选证明，正在从一场AI数学能力展示变成一次更严格的科研审计。

据IT之家10月17日报道，多组参与审读的数学家认为，OpenAI公开的166页证明与公司最初描述的研究路线并不完全一致。数学家贡萨洛·曹-拉博拉（Gonzalo Cao-Labora）甚至提出一种尖锐判断：OpenAI可能在尚未充分理解证明结构的情况下，就急于对外发布了结果。

这不等于数学界已经判定证明错误，但它暴露了一个比单处推导错误更棘手的问题：当一个大规模AI系统生成了人类难以迅速理解的证明时，研究团队能否准确说明模型解决了什么、借鉴了什么，以及关键想法究竟来自哪里？

**纳维-斯托克斯方程是描述液体和气体运动规律的一组偏微分方程。**它广泛用于天气模拟、航空设计、海洋研究和血流分析，但数学家至今无法证明三维不可压缩流体的光滑解是否会永远存在，或者是否可能在有限时间内形成奇点。

这次证明究竟证明了什么

OpenAI的结果瞄准的是带有光滑外力的有限时间爆破解，而不是通常最受关注的无外力光滑性问题。

**外力项是从流体系统外部施加的驱动力，例如持续推动、拉伸或压缩流体的作用。**OpenAI的构造利用外力让一组涡旋不断向内收缩并沿轴向拉伸，使流速在有限时间内变得无界，同时设法保证外力本身仍然光滑。

这一点决定了该成果既不能被简单说成“与千禧年问题无关”，也不能被概括为“彻底解决了三维纳维-斯托克斯难题”。克雷数学研究所对该问题的正式表述包含多个可选命题，其中部分命题允许引入满足条件的光滑外力，因此带外力爆破在形式上确实可能构成候选解答。

真正的分歧在于数学意义而不是字面资格。多数研究者更关心的是：在没有人为设计外力的情况下，三维流体是否会依靠自身动力学产生奇点。OpenAI目前展示的机制需要精心构造外力，这和证明自然演化的流体会自行失去光滑性不是一回事。

| 对比项目 | OpenAI候选结果 | 更受关注的开放问题 | |---|---|---| | 方程类型 | 三维不可压缩纳维-斯托克斯方程 | 三维不可压缩纳维-斯托克斯方程 | | 是否允许外力 | 允许光滑外力 | 通常聚焦无外力情形 | | 目标 | 构造有限时间内速度无界的解 | 证明解始终光滑，或构造无外力奇点 | | 与克雷表述的关系 | 可能对应允许外力的C、D类命题 | 对应更常被讨论的A、B类命题 | | 当前状态 | 候选证明，仍在审查 | 仍是开放问题 | | 数学界共识 | 尚未形成 | 尚未解决 |

“符合正式题目中的一个选项”和“解决了公众理解中的核心难题”之间存在明显落差。OpenAI发布时如果没有把这层差异讲透，就容易让“AI解决千禧年难题”的传播标题跑在数学结论前面。

Lean验证不是数学意义的自动认证

**Lean是一种交互式定理证明器，它能把定义、公理和推导步骤转换为计算机可检查的形式对象。**OpenAI在生成自然语言证明后，又花费约17小时将相关结果形式化并进行验证，这比只发布一份166页手稿提供了更强的逻辑保障。

Lean能够回答的是“结论是否按照系统内给定的规则从前提推出”，却不能独立回答“这些前提是否准确对应人类原本要研究的问题”。如果形式化命题缩小了原问题、定义与标准表述存在偏差，或者关键困难被放进了未经充分解释的假设中，那么代码全部通过检查，也不意味着千禧年问题已经按数学界理解的方式得到解决。

形式化验证更像一台极其严格的拼装检测设备。它能确认每个齿轮是否按图纸连接，却不能替研究者判断拿到的图纸是不是目标机器的图纸，也不能解释这台机器为什么值得建造。

数学界接下来至少需要完成三层核验：第一层是检查Lean项目能否在独立环境中完整构建；第二层是逐项比对形式化命题与克雷原始问题的定义、边界条件和正则性要求；第三层是把机器可检验的推导还原成数学家能够理解、讨论和迁移的方法。

因此，“Lean通过”应被理解为候选证明进入审查阶段的重要证据，而不是一张自动生效的获奖证书。克雷数学研究所对千禧年难题有独立的发表、等待和学界普遍接受程序，截至目前也没有正式宣布纳维-斯托克斯问题已经解决。

一万个智能体到底做了什么

**AI智能体是能够围绕目标持续执行搜索、推理、调用工具、记录结果并与其他任务单元交换信息的模型实例。**OpenAI披露，约1万个并行智能体运行约88小时后得到候选结果，随后另一阶段又用约17小时完成形式化与验证。

这组数字证明了计算规模，却不能直接证明原创贡献。1万个智能体可能在真正探索1万条独立路线，也可能大量重复相似推导；它们可能提出了核心构造，也可能主要承担文献重组、局部引理补全、错误排查和形式转换。没有更细粒度的过程记录，外界无法仅凭智能体数量判断系统的科研能力。

| 已公开指标 | 数值 | 能说明什么 | 不能说明什么 | |---|---:|---|---| | 并行智能体规模 | 约10,000个 | 搜索和协作规模很大 | 有多少任务产生了独立有效思路 | | 证明搜索时间 | 约88小时 | 系统可进行长时间并行探索 | 核心洞见出现在哪个阶段 | | 形式化时间 | 约17小时 | 结果进入了Lean检查流程 | 形式化命题是否完全等价于原题 | | 论文长度 | 166页 | 论证规模复杂 | 证明是否正确、是否具有原创性 | | 官方成本 | 未完整披露 | 无法得到可靠单次任务价格 | 不能把公开模型价格直接当成内部成本 |

OpenAI的系统更接近一个由模型、调度器、搜索策略、上下文共享机制和形式化工具组成的研究流水线。把结果全部归结为“某个模型思考了88小时”会掩盖人类团队在选择问题、配置资源、提供中间成果、调整方向和筛选答案方面的作用。

真正需要公开的是贡献链，而不只是运行规模。理想的研究记录应说明核心构造首次出现在哪个智能体的哪轮输出中，哪些步骤来自已有论文，哪些方向由人类研究者指定，Codex或其他模型如何汇总中间结果，以及最终证明经历了哪些人工改写。

“西班牙路线”争议触及研究来源

当前争议的关键变化，是越来越多审读者认为OpenAI的证明没有真正沿用公司此前提到的“西班牙路线”。

所谓“西班牙路线”，指的是数学家迭戈·科尔多瓦（Diego Córdoba）和路易斯·马丁内斯-佐罗亚（Luis Martínez-Zoroa）此前探索的一类相关方法。按照最新审读意见，OpenAI证明与这一路线或许共享某些表面特征，但核心构造、技术机制和推导路径可能并不相同。

如果这一判断成立，问题并不是OpenAI少引用了一篇论文那么简单。它意味着发布团队可能根据结果的外观或关键词，为机器生成的证明附会了一条看似合理的学术脉络，却没有真正识别证明内部最重要的数学机制。

证明来源在AI科研中不是附属信息，而是判断原创性的基础设施。传统论文可以通过草稿、通信、研讨会报告和引用网络还原思想演化；大规模智能体系统却可能把数百万次交互压缩成一份干净的最终稿，从而抹去失败路线、提示来源和概念迁移过程。

这也是“AI究竟贡献了什么”难以回答的根本原因。一个结论可能在逻辑上完全正确，但核心想法来自训练数据中的既有工作；也可能由模型独立组合出新机制，却被人类团队错误归因给某条熟悉路线。两种情况对数学史、论文署名和AI能力评估的意义完全不同。

与Anthropic相关研究的边界仍需厘清

研究优先权争议让这次证明的时间线变得更加敏感。

纽约大学数学家特里斯坦·巴克马斯特（Tristan Buckmaster）与Anthropic研究人员Levent Alpöge此前曾推进欧拉方程、Boussinesq方程及不可压缩多孔介质方程的相关结果，并使用过Claude、Codex等模型辅助研究。他们探索的成果与OpenAI最终公开的纳维-斯托克斯命题并不完全相同，但都涉及光滑外力与有限时间奇点等邻近技术主题。

现有公开信息不足以证明OpenAI使用了任何未公开成果，也不足以排除既有研究对模型或研究团队产生过间接影响。严谨的报道必须把“研究方向相邻”“时间线存在竞争”和“具体证明使用了他人成果”分开，后者需要可核验的输入记录、模型版本、数据说明和证明演化轨迹才能成立。

OpenAI现在面临的不是一道单纯的署名题，而是一套AI科研治理题。当模型可能从训练语料、用户交互、公开论文和智能体之间的中间消息中吸收信息时，传统的“作者读过哪篇论文”已经不足以描述知识来源。

这次争议没有否定AI数学的价值

OpenAI的候选证明即使最终被缩小、修正或否定，这套工作流仍展示了AI参与开放数学问题的一种现实形态。

其价值不在于让模型像竞赛选手一样一次性写出答案，而在于把大规模并行搜索、长程任务协作和形式化验证连接起来。人类数学家通常只能同时深入跟踪少数路线，而智能体系统可以快速生成大量局部猜想、寻找反例、尝试参数组合并补全繁琐引理。

其局限也同样清楚：搜索规模不能替代问题定义，机器验证不能替代科学解释，最终答案不能替代来源记录。一个系统能生成正确证明，不等于它能解释证明；一个实验室能解释证明，也不等于它能准确区分模型、人类和既有研究的贡献。

AI科研的下一个基准不应该只是“解出了多少题”，而应该包括证明复现率、关键思想可追溯率、独立审查通过率和人类理解成本。否则，行业可能得到越来越多形式上完整、实际上难以归因和消化的结果。

现在还不能宣布难题已解决

截至2026年10月17日，最准确的表述仍是：OpenAI公开了一份带有Lean形式化支持的纳维-斯托克斯候选证明，但其数学意义、研究路线和AI贡献尚未获得独立共识。

数学界未来需要关注四个可验证节点：

1. 独立团队能否复现并完整检查Lean形式化项目。
2. 形式化命题是否逐条满足克雷问题中相关选项的要求。
3. 166页自然语言证明能否被整理成人类可理解、可复用的方法。
4. OpenAI能否给出足够清晰的时间线、引用关系和智能体贡献记录。

这场争议真正戳中的不是“AI会不会做数学”，而是AI生成的科学成果应当如何被理解和归功。过去，证明的正确性通常是最难的一关；在大规模智能体时代，证明对应什么问题、关键思想从何而来、团队是否理解自己的结果，正在变成同样重要的三道关卡。

参考来源

• IT之家：OpenAI纳维-斯托克斯证明方法被指与官方叙事不符——汇总10月17日数学界对证明路线、结果意义及智能体贡献的最新质疑。
• Reddit相关讨论：OpenAI声称拥有纳维-斯托克斯证明——社区对候选证明、形式化验证和开放问题边界的讨论，仅作为舆论与观点补充。