OpenAI Navier-Stokes 证明与 Lean 验证不符，学者指形式化可偷换定理
ValerioCapraro · x · 2026-10-08
研究者 Valerio Capraro 指出，OpenAI 声称的 Navier–Stokes 解答与其 Lean 形式化验证不匹配，并推荐阅读一篇指出深层问题的论文。
- 核心论点：Lean 验证通过并不自动等于自然语言证明正确，也不保证形式化命题就是原定理；AI 在翻译过程中可以改变假设、弱化命题甚至完全替换论证——Lean 验证的是另一个定理。
- 具体发现：作者检查 OpenAI 的 Navier–Stokes 方案后，发现至少两处书面中间结果与 Lean 对应版本不一致：一处声称 4 阶输入导数估计即可，Lean 版本实际需要 5 阶（更弱的结果）；一处压力通量估计采用了不同的界和不同的论证方式。
- 影响与态度：尚不清楚这些不一致是否使整个证明失效，但作者批评 OpenAI 正在用「革命性突破」淹没公众，而无人能确认这些证明是否正确、是否证明了它声称证明的东西——「大规模的认识论风险」（Epistemia at scale）。
所属事件:剑桥论文质疑 Lean 验证可信度，直指 OpenAI Navier-Stokes 证明(14 条相关)→
「研究」频道最新
- 研究发现 AI 智能体也有性别工资差距,女性智能体报酬更低 — TMWNN · 2026-10-09
- LightOnOCR-3 训练秘辛：用 OCR 参考文本引导逻辑分块 — IgorCarron · 2026-10-09
- LightOnOCR-3 揭示：单一版面模型无法覆盖全部文档类型 — IgorCarron · 2026-10-09
- Text2Sim 用文本生成物理仿真场景，输出可编辑的真物理视频 — erwincoumans · 2026-10-09
- 单张图像重建 3D 场景:Building Rome 项目可见范围外几何也补全 — jonstephens85 · 2026-10-09
- PredActor 用单一扩散策略统一人形机器人运动生成与控制,G1 端侧跑 50Hz — carlosdponx · 2026-10-09