标签
本文论证了用 Lean 对 AI 自动形式化进行验证，并不能保证原始自然语言证明的正确性：语义忠实的翻译在可解性复杂度指数层级中是不可判定的。作者展示了实际存在的 AI 误译案例，其中包括 OpenAI 宣布的 Navier–Stokes 爆炸证明中的一处不一致。