来源:环球市场播报
OpenAI 公布一份由内部 AI 系统生成的 Navier – Stokes 方程证明,称其构造出三维不可压缩流体在有限时间内形成奇点的情形,从而解决克雷数学研究所列出的千禧年难题之一。证明同时提供 Lean 形式化版本,但尚未经过长期同行审查,也未获得克雷数学研究所正式认可。

证明选择 " 有限时间奇点 " 路径
Navier – Stokes 方程用于描述空气、水等流体的运动,广泛应用于天气预报、航空设计和血流研究。长期未解决的问题是:三维不可压缩流体从光滑初始状态出发后,解是否始终存在并保持光滑,或能否在有限时间内出现速度等物理量无限增大的奇点。
OpenAI 发布的论文《Finite Time Blowup for Navier – Stokes》采取后一条路径。公司称,AI 系统构造出一种从静止状态开始、受到光滑外力作用的流体,其速度在有限时间内变得无界,同时整个演化过程的能量保持有限。
该构造对应千禧年问题官方表述中的 C 和 D 命题,分别适用于三维欧氏空间和三维环面。官方问题允许存在满足规定条件的外力,关键在于外力本身必须保持光滑,奇点不能由人为加入的无限外力直接产生。
论文提出的机制是一组不断向内收缩并沿轴向拉伸的涡旋。随着尺度缩小,流速持续提高;加速度、压力梯度、动量传递和黏性等项分别增大,却以特定方式相互抵消,使外力保持光滑。
约一万个智能体运行 88 小时
OpenAI 表示,公司在获悉其他研究人员可能取得相关进展后,组织内部系统测试多个尚未解决的千禧年难题。执行 Navier – Stokes 任务的是一款仍在训练、能力高于 GPT-6 Astra 的内部模型。
约一万个并行 AI 智能体参与证明搜索,运行 88 小时,智能体之间交换近 500 万条信息。随后,另一模型用约 17 小时将结果形式化为 Lean 证明。OpenAI 研究人员估计,此次计算成本达到数百万美元。
在 Navier – Stokes 证明形成前,该系统还生成了一个有关无黏性 Euler 方程有限时间奇点的证明。OpenAI 称,不同智能体小组分别探索多种路径,随后由 Codex 汇总中间成果,并将 Euler 方程的结果提供给 Navier – Stokes 研究组。
Lean 形式化能够检查推导是否遵循既定逻辑规则,降低长篇证明中隐藏计算或推理错误的风险。不过,数学家仍需确认 Lean 验证的形式化命题与千禧年问题的原始要求完全等价,并审查证明采用的定义、假设和转换。
研究优先权与数据使用引发争议
OpenAI 公布结果前,纽约大学数学家 Tristan Buckmaster 与 Anthropic 研究人员 Levent Alp ö ge 发布了三项相关成果,涉及 Euler、Boussinesq 及不可压缩多孔介质方程。他们使用 Anthropic Claude、OpenAI Codex 等模型,并在早期研究基础上推进 " 光滑外力下形成奇点 " 的技术路线。
Buckmaster 表示,两人的未公开草稿曾输入 Codex;OpenAI 则是在得知相关研究传闻后启动大规模求解。他称自己无法确定其数据是否被使用,也没有直接指控 OpenAI 挪用研究成果,但要求完整说明研究时间线和思想来源。
OpenAI 否认研究团队访问两人的私人材料,并称 Navier – Stokes 证明由内部系统独立完成。公司承认其研究方向受到相关传闻启发,也无法完全排除用户数据曾以去标识化方式参与模型改进。双方对沟通过程及成果署名安排的叙述仍存在差异。
两条研究路径均建立在 Diego C ó rdoba 和 Luis Mart í nez-Zoroa 多年发展的解析方法之上。OpenAI 承认 Buckmaster 与 Alp ö ge 在三维 Euler 方程成果上的优先权,同时主张 Navier – Stokes 结果由其率先完成。
Lean 验证不等同于获得千禧年大奖
克雷数学研究所为七项千禧年难题各设置 100 万美元奖金。根据规则,一份候选解答需要在符合要求的出版渠道发表,发表后至少经过两年严格检验,并获得全球数学界普遍接受,研究所才会启动正式评估程序。
OpenAI 现阶段发布的是一项有论文和机器验证支持的候选解决方案。即使部分数学家初步认为证明可信,也不能据此认定克雷数学研究所已将 Navier – Stokes 问题列为解决。
OpenAI 表示不准备申领 100 万美元奖金。若证明通过独立审查,其产业意义主要体现在 AI 研发能力:模型开始从检索和整理已有知识,进入开放问题求解、长程协作及形式化验证环节。此次任务所需的大规模并行智能体和数百万美元计算投入,也显示这类科研能力短期内仍依赖高成本算力基础设施。


登录后才可以发布评论哦
打开小程序可以发布评论哦