千禧难题，AI 怎么证

2026 年 9 月 11 日，OpenAI 的 NavierStokesAndEuler 仓库登上了 GitHub Trending，截至本日拿下 1692 stars。它做的事情听起来很炸裂：用 Lean 4 给出 Navier-Stokes 和 Euler 方程的形式化证书，瞄准的是克雷数学研究所悬赏百万的千禧难题之一。但别被标题唬住——它不是”AI 证明了千禧难题”，而是”AI 把已有的偏微分方程结果写成了机器可检查的证明”。这两件事差了一个量级，也是这篇教程要拆解的核心。

为什么说”形式化证书”不是”AI 证明”？

现象：HN、Reddit、r/ClaudeAI 都在刷”OpenAI 证明 Navier-Stokes”，点进去发现只是一个 Lean 仓库，评论区吵成一锅粥。有人兴奋，有人骂标题党。

根因：Lean 4 是一个交互式定理证明器，本质是把人类已经写出来的数学证明，一行一行地翻译成它能检查的语法。这个仓库里几乎每个 theorem 都能在数学文献里找到原型——比如 Constantin-E-Titi 关于 Onsager 临界的耗散估计，或 Kato 关于 Euler 局部光滑解存在性的结果。创造性的数学发现早在仓库出现前几十年就完成了。

解法：打开 lakefile.toml 看依赖，再去 NavierStokes/ 目录翻 *.lean，把每个 theorem 名字丢进 Google Scholar，立刻能定位到原始论文。区分”证明 (proof)“和”形式化 (formalization)“，是入门这个项目的第一课，也是避免在社群里闹笑话的关键。

tactic 是什么？为什么 Lean 证明像倒着写？

现象：第一次打开 NavierStokes.lean，满屏都是 intro、apply、simp、linarith、omega，看起来像倒着写的程序。

根因：Lean 走反向推理（backward chaining）。apply h 不是”用 h 证明结论”，而是”把当前目标替换成 h 的前提”。tactic 是一步步把目标树拆掉的小指令。

解法：仓库里一个真实可跑的小例子（已简化）：

import Mathlib

theorem energy_decay (t : ℝ) (E₀ : ℝ) (hE₀ : 0 ≤ E₀) :
    E₀ * Real.exp (-t) ≤ E₀ := by
  apply mul_le_of_le_one_left hE₀
  have h : Real.exp (-t) ≤ 1 := by
    rw [Real.exp_le_one_iff]
    exact ⟨by linarith, by simp⟩
  exact h

读法：从下往上。exact 给最终事实，apply 换目标，rw 做替换，have 起一个中间引理。读 Lean 证明，先抓最后一行，再倒着往上看。三天就能上手。

本地怎么从零跑起来？

现象：clone 下来 lake build 一跑，CPU 直接拉满，最后大概率报 caching failed 或 olean version mismatch，新手一卡一下午。

根因：mathlib4 是个庞然大物，源码 + 已编译缓存 5GB+；Lean 4 自身的 toolchain 还要走 elan 管理；Windows 用户几乎必须 WSL。

解法：标准姿势是四步：

git clone https://github.com/openai/NavierStokesAndEuler.git
cd NavierStokesAndEuler
elan toolchain install leanprover/lean4:v4.22.0
lake exe cache get
lake build NavierStokes

lake exe cache get 是 Lean 4 新加的命令，专门下载 mathlib4 的 precompiled .olean，能把首次构建从 2 小时压到 10 分钟。跳过这步的人，大多都卡在第一步。

证书跑通之后，能拿去做什么？

现象：很多读者 build 成功就停了，不知道 Lean 证书在工程上有什么价值。

根因：形式化证书 ≠ 论文。它解决的是”机器可验证”，不是”机器生成”。但这恰好是 LLM 时代最缺的拼图——LLM 容易在长链推理里撒谎，Lean 类型系统不会。

解法：把这个仓库当成”基准”。在自己用 LLM 推导 PDE 结论时，把结果翻译成 Lean 喂给 lake build，构建过了才发布。这是当下”AI 数学助手”最稳的落地姿势：人写思路，AI 写代码，Lean 兜底。

Sources

本文参考：GitHub Trending 2026-09-11 榜单、openai/NavierStokesAndEuler README、Lean 4 官方文档（leanprover.github.io）、r/ClaudeAI 当周讨论帖。