逐条核对 Lean 代码库：OpenAI 证的是 Navier–Stokes 命题 (C)

CatAstro_Piyush · x · 2026-09-09

一篇技术博客逐层拆解「OpenAI 解决了 Navier–Stokes」这一说法。作者的第一反应是追问 prompt 是什么，随后先去读了 Fefferman 在 2000 年为 Clay 研究所写的五页官方问题陈述。他的结论是：这句话同时做了三件事——(1) 一个关于带光滑外力的三维 Navier–Stokes 方程的定理被证明，且经证明助手（Lean）检查，这一点目前看属实（作者克隆了 Lean 仓库亲自核对）；(2) 该定理逐条对应官方陈述四个选项中的选项 (C)，经小推广也覆盖 (D)，这点可自行验证；(3) 「这个选项就是人们所说的 Navier–Stokes 问题」——这一步是错的，Fefferman 二十六年前写下四个选项时就已经预见到今天这种歧义。文章的核心是教读者：先读官方定义，再读新闻。