自动形式化技术正被广泛应用于验证数学文本，包括由人工智能生成的内容。例如，OpenAI此前曾宣布利用该技术验证关于纳维-斯托克斯方程解爆破的证明。在此过程中，AI系统将自然语言文本转换为Lean等形式化语言，随后通过机械方式验证形式化论证的正确性。
然而，这一过程未必能为原始的自然语言论证提供可信度保障。核心难点在于实现“语义忠实”的翻译，即准确消除数学自然语言中的歧义。研究指出，解决此类歧义问题的难度在可解性复杂度指数（SCI）层级中处于任意高位（即SCI = ∞）。换言之，提供语义忠实的AI自动形式化，比包括停机问题（SCI = 1）在内的任何计算问题都更为困难。
为展示这一理论结果的实际影响，研究列举了多个AI将自然语言陈述和证明错误翻译为Lean的案例，导致自然语言证明与其Lean“验证”结果出现错位。其中就包括OpenAI宣布的纳维-斯托克斯方程证明：其形式化的Lean证明并未真正对应于该方程解爆破的自然语言证明逻辑。