新论文质疑 Lean 验证≠正确证明,直指 OpenAI Navier-Stokes 证明疑点
anshulkundaje · x · 2026-10-08
剑桥学者 Bastounis 等人在 arXiv 发表论文《Navier-Stokes lost in translation》,质疑用 Lean 形式化验证来背书 AI 生成的数学证明的做法。
- 背景:OpenAI 曾宣称用 AI 自动形式化(将自然语言数学文本翻译为 Lean 等形式语言)证明了 Navier-Stokes 方程解的 blow-up,Lean 通过机器验证即可确保证明正确。
- 核心论点:论文展示该 Lean 形式化证明与原始书面论文中的证明并不对应,即「翻译通过验证」并不能保证原自然语言论证正确。
- 理论结果:消解数学自然语言文本中的歧义(语义忠实翻译的必要条件)在可解性复杂度指数(SCI)层级中处于任意高位(SCI = ∞),这意味着提供语义忠实的 AI 自动形式化比包括停机问题在内的任何计算问题都更难。
- 作者还给出多个 AI 在实践中将自然语言陈述与证明误译为 Lean 的实例,导致两种表述不一致。
结论:AI 自动形式化 + 形式验证这一流程本身,可能对原始自然语言论证的正确性几乎不提供任何置信度。
所属事件:剑桥论文质疑 Lean 验证可信度，直指 OpenAI Navier-Stokes 证明(14 条相关)→
「漫话AGI」频道最新
- 密码学家 matthew_green：公钥加密依赖少数数学难题，人类分析并非金标准 — matthew_d_green · 2026-10-09
- 「思考可以外包，理解不能」：一句话点破 AI 时代的认知边界 — salykova_ · 2026-10-09
- ARK 分析师：推理数据中心测算显示单位能耗 GDP 有清晰上升路径 — skorusARK · 2026-10-09
- ARK 分析师：收入与能耗曲线越陡越高，「没有高收入低能耗国家」 — skorusARK · 2026-10-09
- 安全研究员频频撤离 AI 公司，激进派称留下才能掌舵 — ZeroStateReflex · 2026-10-09
- 开发者放话:不会编程就没资格做游戏，AI 圈吵翻 — AIandDesign · 2026-10-09