AI 形式化证明的翻译陷阱

OpenAI 此前高调宣布用 AI 证明了 Navier-Stokes 方程的解会 blow up，这篇论文直接戳破了这个叙事的关键漏洞——Lean 验证的是翻译后的形式化陈述，而非数学家原本想表达的内容。翻译过程中语义漂移、条件遗漏、甚至核心假设被悄悄替换，都是难以检测的。

这本质上是一个"信使问题"：形式化验证成了替罪羊，背锅的是自然语言到形式语言的映射环节。做 AI for Math 的团队需要重新设计人机协作的校验流程，比如让数学家反向审阅形式化陈述是否忠实原意，而不是只看最后的 green checkmark。

更值得警惕的是，这种"翻译即验证"的错觉可能被滥用为营销话术，投资人和审稿人需要提高鉴别力。