研究称 OpenAI 的 Navier-Stokes 证明与 Lean 形式化验证不一致
ValerioCapraro · x · 2026-10-08
一篇新论文提出一个令人担忧的观点：OpenAI 关于 Navier–Stokes 的解与其 Lean 验证并不匹配。核心论点是——通过 Lean 形式化验证的证明，并不能自动保证其自然语言证明的正确性，也不意味着形式化陈述真正捕捉了原定理的意图。
作者 Valerio Capraro 认为这比 OpenAI 发表的 700 篇 AI 生成数学论文更值得读：形式验证与语义意图之间存在深刻缝隙，AI 数学成果的「已验证」标签可能被高估。论文链接见原帖。
所属事件:剑桥论文质疑 Lean 验证可信度，直指 OpenAI Navier-Stokes 证明(14 条相关)→
「模型」频道最新
- LightOnOCR-3 引发热议：文档解析模型被认为「离谱地强」 — IgorCarron · 2026-10-09
- 疑似 Gemini 4「Argon」现身 Google Antigravity CLI，尚待证实 — gaganghotra_ · 2026-10-09
- 传 OpenAI 因越权与汇报失实担忧推迟 GPT-6.1 Astra 十月发布 — johnkwaters · 2026-10-09
- 开发者反馈 GLM-5.3 在 Cursor CLI 中工具调用疑似完全失效 — DanielLockyer · 2026-10-09
- Cohere 开源 3.35B 模型 Tiny Aya L2-Thinker,支持 44 种语言母语推理 — lmoroney · 2026-10-09
- 三天三个常识错误:用户列举 Google AI 搜索持续翻车案例 — Icy_Jelly_315 · 2026-10-09