ESC
AI 1 分钟阅读

OpenAI 发布 Navier–Stokes 与 Euler 方程有限时间爆破结果的 Lean 形式化证明

OpenAI 在 GitHub 开源了 Navier–Stokes 与 Euler 方程有限时间爆破结果的 Lean 4 形式化证明，涵盖三维全域与周期环面上光滑解的破裂，对应克雷数学研究所千禧年大奖难题官方描述中的情形 (C) 与 (D)，并支持独立机器证明检查。

来源：GitHub

Navier–Stokes 与 Euler 方程的有限时间爆破

本仓库包含 OpenAI 论文《Finite time blowup for Navier–Stokes》与《Finite time blowup for the Euler equation》中所得结果的 Lean 4 形式化。

对于每一个正粘性系数，我们证明了两个结果：

  • 全域 $\mathbb{R}^3$： 存在光滑初值与外力，使得不存在动能一致有界的全局光滑解。
  • 周期环面 $\mathbb{R}^3/\mathbb{Z}^3$： 存在光滑周期初值与外力，使得不存在全局光滑解。

这些对应克雷数学研究所千禧年大奖难题中 Navier–Stokes 方程解的存在性与光滑性 官方问题描述 里的 (C) “Navier–Stokes 解在 ℝ³ 上的破裂"与 (D) “Navier–Stokes 解在 ℝ³/ℤ³ 上的破裂"两种情形。

Euler

我们在 $\mathbb{R}^3$ 上构造了光滑、紧支集、无散度的初始速度，其在无外力不可压缩 Euler 方程下的解会在有限时间内发展出奇点。在该时刻附近，速度的 $C^1$ 范数变为无界，且涡量的 $L^\infty$ 范数的时间积分发散。

构建形式化证明

本项目使用 Lean 4.34.0-rc2、Mathlib 与 Lake。安装 elan 后，获取 mathlib 缓存并构建形式化证明：

lake exe cache get
lake build

独立证明检查

关于使用 Comparator 检查形式化证明的说明，请参见 ComparatorChallenges README。