arXiv·· 12 天前AI 评分37
Navier-Stokes 翻译失真：为何 AI 自动形式化的 Lean 验证不能保证自然语言证明正确
Navier-Stokes lost in translation: Why Lean verification of AI autoformalisation does not guarantee correct natural language proofs
AI 导读
针对 OpenAI 宣称的 Navier-Stokes 方程解爆破证明，该文指出 AI 自动形式化流程存在根本缺陷：AI 将自然语言数学文本翻译为 Lean 形式语言后，Lean 验证只能保证形式化表述本身正确，无法保证原始自然语言论证正确。由于翻译环节存在多重困难，形式化验证通过并不等于原证明成立。
来源：arXiv · arxiv.org