独立团队内核级复验 OpenAI 纳维-斯托克斯 Lean 证明，四次构建全通过
pvaa · reddit · 2026-09-11
- 背景是 OpenAI 2026 年 9 月 8 日发布的 166 页手稿，声称给出受迫三维 Navier-Stokes 方程有限时间爆破的证明，并附带 Lean 4 项目，但 Lean 部分此前只有自评。
- 作者团队做了彻底的独立内核验证：在两台机器、同一 pinned commit 上跑了四次完整构建，包括一次从零编译全部 8370 个 mathlib 模块（约 3 小时 13 分），四次全部 exit 0、无错误，输出逐字节一致。
- 关键结论：两条导出定理只依赖 propext、Classical.choice、Quot.sound 三条公理，无 sorryAx；树中仅有的 4 个 sorry 都是 Comparator 挑战占位符，不在任何证明的依赖闭包内。
- 进一步用项目自带 comparator 校验了定理陈述与挑战一致，并将整个证明环境回放给两个独立内核（Lean 自带与 Rust 实现的 nanoda），均通过；定义与 Google DeepMind 的独立形式化逐字节吻合（仅 21 处包装差异）。
- 团队还通读论文两次、逐条核账 79 条陈述、沿 58 条主链重推 480 步：引理 4.8 的大部分构造可复现，但其收尾部分在网格可达的 lambda 范围内无法复现——论文渐近分析表明需要 lambda ≤ 3e-4，远超通常绘图的尺度。
- 明确声明未证之事：Lean 陈述严格弱于论文的 Theorem 1.1；绿色内核只证明"Lean 证明证出 Lean 陈述"，不等于 166 页论文本身正确，也不涉及优先权争议。
所属事件:OpenAI 纳维-斯托克斯证明复现通过但遭社区质疑(2 条相关)→
「研究」频道最新
- 研究揭示合成数据最优比例随算力从10%升至32% — heghbalz · 2026-10-26
- FLASH 仿真框架：单卡 RTX 5090 上分钟级学会布料折叠 — ChongZzZhang · 2026-10-26
- LEMON 监控器:从注意力图零样本识别未见过的 LLM 幻觉与越狱 — yoavartzi · 2026-10-26
- EMNLP 主题演讲背后：用语言模型「模拟学习者」生成儿童语言习得新假设 — najoungkim · 2026-10-26
- EMNLP 2026 主题演讲背后的论文：用 bigram 模拟语言习得 — najoungkim · 2026-10-26
- 把 DeepLIFT 重写为独立计算图：输入序列直接输出归因结果 — jmschreiber91 · 2026-10-26