OpenAI 宣布 AI 攻克纳维-斯托克斯千禧年大奖难题

纳维-斯托克斯方程是描述粘性流体运动的偏微分方程组，广泛应用于气象预报、航空工程、海洋模拟等领域。然而，数学家们长期无法严格证明在三维空间中，该方程的光滑解是否始终存在且唯一——这一缺口不仅是纯数学的遗憾，也对物理模型的理论基础构成挑战。克雷数学研究所于2000年将其列为七大千禧年大奖难题之一，并设立百万美元奖金，此后逾二十年间无人摘得。

OpenAI 此次公布的成果由 AI 系统独立生成，包含两个核心部分：一份面向数学社区的完整解题论文，以及一份用 Lean 定理证明器编写的形式化证明。Lean 是一种计算机辅助证明语言，能够对数学推导进行逐步机器验证，从而大幅降低人为错误的可能性。形式化证明的引入，使得这份解答在可验证性上超越了传统数学论文的标准，为学界审查提供了更为严格的基础。

这一消息在技术社区引发强烈反响。Hacker News 上的相关讨论帖在短时间内累积超过600个赞与440余条评论，讨论涵盖证明的数学严谨性、AI 在高阶推理中的能力边界，以及该成果对学术评审体系的潜在冲击。《华尔街日报》等主流媒体也迅速跟进报道，将其定性为数学史上的重大事件。

从更宏观的视角来看，此次突破是 AI 系统在形式数学领域持续进化的缩影。近年来，DeepMind 的 AlphaProof 等系统已在国际数学奥林匹克竞赛级别的题目上展现出强劲能力，而 OpenAI 此次直接挑战千禧年级别的开放问题，意味着 AI 辅助数学研究正从竞赛题解向前沿未解问题迈进。这一转变对数学研究的组织方式、人才培养路径以及学术发表机制均可能产生深远影响。

目前，数学界对该证明的独立验证工作尚在进行中。由于 Lean 形式化证明本身具备机器可检验的特性，专业社区可以对每一推导步骤进行系统性审查，这与传统同行评审相比效率更高、透明度更强。克雷数学研究所是否认定该解答符合奖项评定标准，将是接下来最受关注的焦点之一。无论最终结论如何，AI 独立完成顶级数学难题这一事实本身，已足以重塑外界对人工智能推理能力上限的认知。

要点

• OpenAI 发布由 AI 生成的纳维-斯托克斯千禧年大奖问题完整解答，附带 Lean 形式化证明，可供机器逐步验证
• 纳维-斯托克斯问题是克雷数学研究所设立的七大百万美元悬赏难题之一，此前逾二十年无人破解
• Lean 形式化证明的引入使结论可验证性超越传统数学论文标准，为学界审查提供更严格基础
• 该成果标志着 AI 数学能力从竞赛题解向顶级未解问题的实质性跨越，或将重塑数学研究范式
• 克雷数学研究所对该解答的正式认定结果，将成为衡量此次突破历史地位的关键节点