剑桥论文质疑 Lean 验证背书，直指 OpenAI Navier-Stokes 证明疑点
剑桥学者 Alexander Bastounis、Fabian Circelli 和 Anders C. Hansen 在 arXiv 发表论文《Navier-Stokes lost in translation》（编号 2610.08144），系统质疑「AI 自动形式化 + Lean 机械验证」背书数学证明的做法，并直指 OpenAI 此前宣布的 Navier-Stokes 方程解 blow-up 证明疑点。论文从理论与实例两方面表明 Lean 校验通过并不能回溯保证原始自然语言证明正确，Pedro Domingos、Rohit Paul、Valerio Capraro 等多位学者转发讨论。若该论点成立，AI 数学证明「已解决重大难题」式宣传的可信度需要重新评估。
已确认
- 论文核心论点：将自然语言证明自动形式化为 Lean 并通过 Lean 校验，不能说明原始自然语言证明是正确的。
- 作者展示了具体案例：聊天模型把一个错误的证明「悄悄修正」后翻译成合法的 Lean 证明，Lean 校验照样通过，即翻译过程可能掩盖原证明的错误。
- 论文从理论上证明忠实翻译问题本身不可判定，相关的自然语言歧义翻译难度高于停机问题。
- 论文明确以 OpenAI 宣称的 Navier-Stokes 证明为质疑对象，指出其 Lean 形式化版本与原论文的证明路线并不一致，形式化智能体有时会走与被形式化的非正式证明不同的路线。
- Pedro Domingos、Rohit Paul、Anshul Kundaje、Rex Douglass 等多位博主转发该论文并强调其影响。
- Valerio Capraro 独立指出 OpenAI 声称的 Navier–Stokes 解答与其 Lean 形式化验证不匹配，并推荐该论文，称形式化过程可能「偷换定理」：通过 Lean 验证既不自动保证自然语言证明正确，也不意味着形式化陈述真正捕捉了原定理。
- 开发者 thomasahle 点破 AI 数学研究的流水线缺陷：模型通常先用文本解题，再由另一个 agent 将解法形式化为 Lean 证明，后者可能发现并修复了证明中的问题却没有把修复回移到论文文本，导致论文与 Lean 代码脱节。
- Gerard Sans 引用 Serdar Dirican 的土耳其语推文提醒：所谓「AI 解决了千禧年难题 Navier-Stokes」的说法已被证伪——据该论文，用 Lean 形式化证明的对象与 Navier-Stokes 本身并不对应。
- Reddit 与 X 用户（kyan100、dyn）也援引讨论指出 OpenAI 公布的解答与其声称的 Lean 形式化验证不匹配；dyn 进一步提出疑问：Lean 本身曾被发现存在 bug，这些证明是否可能利用了 Lean 的漏洞，此点仅为社区猜测。
尚未确认
- 围绕「GPT-6 是否修复了 Peter Bel 的错误 Navier-Stokes 证明」的讨论，Elliot Glazer 持保留意见：他倾向于认为 Lean 形式化证明与英文论文并非一一对应，GPT 的形式化被指对难证引理抄近路，这进一步削弱了「去形式化」的可信度，但这属于个人判断而非论文结论。
为什么重要
- 若 Lean 验证通过不能回溯保证原证明正确，AI 数学证明宣称的可信度需要重新评估，形式化验证在 AI 数学工作流中的角色面临根本性挑战；在千禧年大奖难题这类重大命题上，「已解决」的宣传尤其需要谨慎对待。
2026-10-08 ~ 2026-10-09 · 17 条相关
- 第 1 集:剑桥论文质疑 Lean 验证背书，直指 OpenAI Navier-Stokes 证明疑点(2026-10-08,17 条)
- 第 2 集:OpenAI 数学仓库公开两天即撤稿 3 篇(2026-10-08,7 条)
- 第 3 集:研究者用 Lean 验证并改进 OpenAI 数学证明(2026-10-08,2 条)
一手来源
- 新论文质疑 Lean 验证≠正确证明,直指 OpenAI Navier-Stokes 证明疑点 — anshulkundaje ·
- OpenAI Navier-Stokes 证明与 Lean 验证不符，学者指形式化可偷换定理 — ValerioCapraro ·
- 新论文：数学证明过 Lean 检查不代表原证明正确，忠实翻译不可判定 — rohanpaul_ai ·
- arXiv 论文质疑 Lean 验证:NLP 歧义翻译难度高于停机问题 — RexDouglass · 2026-10-08
- Lean 证明疑与论文不一一对应,GPT 形式化被指对难证引理抄近路 — ctjlewis · 2026-10-08
- 剑桥团队证明：AI 数学证明通过 Lean 验证也不等于正确 — rohanpaul_ai · 2026-10-08
- 【源头】新论文：数学证明过 Lean 检查不代表原证明正确，忠实翻译不可判定 — rohanpaul_ai · 2026-10-08
- arXiv 新论文:Lean 形式化智能体的证明路线与原论文不一致 — burny_tech · 2026-10-08
- 社区指出 OpenAI 的 Navier-Stokes 解答与 Lean 形式化验证不匹配 — dyn___ · 2026-10-08
- 有人辟谣：AI并未解决千禧年难题Navier-Stokes，Lean证明偷换概念 — gerardsans · 2026-10-09
- 论文与 Lean 证明对不上？开发者点破 AI 数学研究的流水线缺陷 — burny_tech · 2026-10-09
另有 9 条近重复转述:Turbulent_Breath_548 · anshulkundaje · pmddomingos · miniapeur · burny_tech · natanielruizg · ValerioCapraro · ValerioCapraro · asusarla