GPT Navier-Stokes 证明遭质疑：Lean 形式化被指抄近路

针对「GPT-6 是否修复了 Peter Bel 错误的 Navier-Stokes 证明」的讨论，数学家 Elliot Glazer 提出保留意见：他倾向于认为 Lean 形式化证明与英文论文并非一一对应，模型可能对难以证明的引理「抄了近路」。同时一篇 arXiv 论文（2610.08144，Bastounis、Circelli、Hansen）直指 OpenAI 宣布的 Navier-Stokes 解 blow-up 证明所依赖的 Lean 验证存疑，认为将自然语言证明翻译为形式化语言时存在歧义，其难度甚至高于停机问题。

2026-10-08 ~ 2026-10-08 · 2 条相关

• arXiv 论文质疑 Lean 验证:NLP 歧义翻译难度高于停机问题 — RexDouglass · 2026-10-08
• Lean 证明疑与论文不一一对应,GPT 形式化被指对难证引理抄近路 — ctjlewis · 2026-10-08