研究人员在新发表的论文中指出，AI自动形式化系统存在根本性的局限——即使将数学证明成功转换为Lean形式语言并通过机械验证，也无法保证原始自然语言论证的正确性1。Alexander Bastounis等研究者以OpenAI宣称的Navier-Stokes方程吹胀解证明为案例，揭示了形式化Lean证明与原始自然语言证明之间存在的对应偏差1。
论文论证表明，将数学自然语言文本进行语义忠实翻译的难度在可解性复杂性体系中处于最高层级1。研究者采用可解性复杂性指数（SCI）作为度量指标，指出解决数学自然语言歧义的SCI值为无穷大，甚至高于停机问题的SCI值11。这意味着自动形式化过程中的翻译准确性本质上无法得到理论保证，仅靠Lean验证的成功无法弥补这一根本缺陷1。
A new academic paper challenges the reliability of AI-powered formal verification systems, arguing that successful mechanical proof validation in formal languages does not guarantee the correctness of the original mathematical arguments 1. Researchers including Alexander Bastounis contend that translating natural language mathematical proofs into Lean, a formal verification language, can mask fundamental errors in the source material 1.
The paper, submitted on October 6, 2026, demonstrates that resolving semantic ambiguities in mathematical natural language texts ranks at the highest tier of computational complexity—infinite decidability complexity, surpassing even the halting problem 1. The researchers provide concrete examples of mistranslations, including cases from OpenAI's claimed proof of the blow-up solution for the Navier-Stokes equations, where the formalized Lean proof fails to correspond to the original natural language reasoning 1. This finding exposes a critical gap in the automation pipeline: formal verification can validate the syntactic structure of a translated proof without confirming that the translation faithfully preserves the mathematical content or logical validity of the original work 1.
评论
还没有评论，欢迎留下第一条。