论文精选
论文：AI 将数学证明翻译成 Lean 通过验证不代表原证明正确
精选理由
有人把错误的数学证明喂给 AI 翻译成 Lean，居然编译通过了，因为 AI 悄悄把 bug 修了。做形式化验证的朋友值得看看。
一篇新论文指出，AI 把数学证明翻译成 Lean 形式化语言后，即使 Lean 编译通过，也无法说明原证明是正确的。论文展示了一个聊天机器人把错误证明静默修复后翻译成合法的 Lean 证明。作者进一步证明，判断某个陈述能否被忠实翻译，在计算复杂度上严格难于 Halting problem，因此不存在任何 AI 翻译器能保证总是做到忠实翻译。
原文 · rohanpaul_ai
A new paper shows that when AI translates a math proof into Lean, passing the Lean check says nothing about whether the original proof is right.
They show a chatbot turning a wrong proof into a valid Lean proof by silently fixing the error.
Knowing when a statement can be translated faithfully is provably harder than the Halting problem, so no AI translator can always do it.
