独立团队内核级复验 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 页论文本身正确，也不涉及优先权争议。
「研究」频道最新
- ECCV 2026 现场报告 LoMa 与 RoMa v2，另有海报展示 — ducha_aiki · 2026-09-11
- UMO 统一框架解锁动作基础模型先验，横扫多种人形动作任务 — Michael_J_Black · 2026-09-11
- 克雷研究所将 Navier-Stokes 方程状态改为 Active,疑有解了? — felpix_ · 2026-09-11
- 首篇AI4AI综述：AI能改进AI，但「组合鸿沟」挡住递归自我改进 — 新智元 · 2026-09-11
- ACL 推出可持续评审新政,Kyunghyun Cho 提议 ScholarCoin 代币经济 — kchonyc · 2026-09-11
- 传 OpenAI、Anthropic 正攻关 P vs NP，构造性证明将颠覆密码学 — MohMayaTyagi · 2026-09-11