该论文题为《纳维-斯托克斯方程在翻译中丢失：为什么Lean对AI自动形式化的验证不能保证正确的自然语言证明》，探讨了使用AI将自然语言数学论点翻译成如Lean这样的形式证明语言的应用。文章指出，一旦翻译完成，形式证明可以机械验证，但质疑这种验证是否能让人对原始自然语言论点有信心。作者们将OpenAI宣称的纳维-斯托克斯方程解爆炸的证明作为AI自动形式化的突出例子，并表明形式化的Lean证明与自然语言的爆炸证明不相对应。

作者们认为，核心困难在于消除自然语言数学文本中固有的歧义。他们表明，此问题在可求解性复杂度索引（SCI）层次结构中具有任意高的难度，意味着它比任何计算问题都更难，包括停机问题（其SCI为1）。因此，从自然语言到像Lean这样的形式语言创建语义忠实的翻译在原则上比解决任何算法问题都更难，这意味着不存在能够保证所有数学文本忠实翻译的通用方法。

为了证明这一点，论文提供了几个AI将自然语言陈述和证明错误翻译成Lean的例子，导致自然语言证明与其Lean验证之间出现不匹配。在OpenAI的纳维-斯托克斯证明情况下，形式化的Lean证明与自然语言的爆炸证明不相对应。这意味着尽管Lean证明本身可能是正确的，但它并不能准确代表AI本应形式化的原始自然语言论点，从而削弱了Lean验证对原始NL证明正确性提供的信心。