arXiv 论文质疑 Lean 验证:NLP 歧义翻译难度高于停机问题
RexDouglass · x · 2026-10-08
arXiv 论文（2610.08144，Bastounis、Circelli、Hansen）直指 OpenAI 宣布的 Navier-Stokes 方程解 blow-up 证明所依赖的「AI 自动形式化 + Lean 机械验证」流程存在根本缺陷。要点：- 自动形式化指把自然语言数学文本翻译成 Lean 等形式语言再做机械验证，但这一翻译无法保证语义忠实。- 论文证明：解决数学自然语言文本中的歧义以实现语义忠实的翻译，其难度位于可解性复杂度指数（SCI）层级/算术层级的任意高处（SCI = ∞），形式上难于包括停机问题（SCI = 1）在内的任何计算问题。- 作者给出多个 AI 在实践中把自然语言陈述与证明误译进 Lean 的实例，导致自然语言论证与形式化版本不匹配。结论：Lean 验证通过并不能为原始自然语言证明提供置信度。转发者借此调侃：这是否意味着 gpt-6 修复的是一份原本错误的 Navier-Stokes 证明。
「研究」频道最新
- 以太坊研究员 Justin Drake 呼吁行业转入「地堡模式」应对数学进步风险 — marcvanderchijs · 2026-10-08
- Lean 证明疑与论文不一一对应,GPT 形式化被指对难证引理抄近路 — ctjlewis · 2026-10-08
- Alignment Whack-a-Mole 获 COLM 2026 oral,作者预告对谈节目 — TuhinChakr · 2026-10-08
- OpenAI 疑似证明虚二次域模性猜想,CM 数域椭圆曲线或将全部模性 — soumitrashukla9 · 2026-10-08
- OpenAI 一天发 722 篇数学论文,过半引用自家工作且现引用环 — aran_nayebi · 2026-10-08
- 数学家发现 AI 洞见藏在既有思想的凸包里,其余科学也将在更大规模迎来这一课 — soumitrashukla9 · 2026-10-08