Lean 证明能证明什么？Elliot Glazer 厘清形式化验证与真实定理的距离

ctjlewis · x · 2026-10-10

Elliot Glazer 回应 AI 圈热议的问题：什么时候可以由 Lean 形式化证明推断出「我们真正关心的命题（如 Navier-Stokes 解的存在性）」为真。他指出 Lean 证明与数学命题之间取决于形式化过程本身是否忠实，即被验证的形式化陈述必须准确对应非形式的数学意图。

Suhas 的引用评论显示，这一「形式化忠实性」问题正是许多研究者多年来回避 Lean×LLM 方向的原因，如今随着大模型自动形式化的发展再度成为焦点。