Thomas Hales 解析 Lean 定理证明器：自动形式化、内核可靠性与 AI 挑战

数学家 Thomas Hales 撰文指出，尽管 AI 推动的数学自动形式化取得重要进展，但 Lean 等定理证明器在内核健全性与类型理论基础上仍面临可靠性挑战。文章梳理了前沿模型发现内核严重漏洞的经过，探讨了多内核交叉验证与 Con-Leche 形式化验证内核等应对方案，并强调在理论基础不完备及对抗性场景下，不能盲目信任缺乏人工严密审查的 AI 形式化系统。