本文证明AI将自然语言数学证明自动形式化为Lean等正式语言，无法保证与原论证的语义一致性。作者证明忠实翻译的难度极高（SCI = ∞，超越停机问题），并给出了具体反例，包括指出OpenAI声称的Navier-Stokes方程爆破证明的Lean验证并不对应原文证明。
背景
自动形式化利用AI将自然语言数学转化为Lean等正式证明语言以便机械验证。OpenAI近期宣布使用该方法证明了Navier-Stokes方程解的爆破问题，引发了关于此类方法可靠性的讨论。
- 来源
- Lobsters
- 发布时间
- 2026年10月9日 01:16
- 评分
- 8.0 / 10