陶哲轩转载 Thomas Hales：Lean 可靠性、声响漏洞之夏与自动形式化风险
陶哲轩博客刊登 Thomas Hales 长文，回顾 2026 年 Lean 内核「声响漏洞之夏」、Con-Leche 核验证，并警告自动形式化与 AI 辅助核审计需人类严格把关。
菲尔兹奖得主陶哲轩在博客以客座帖形式刊登数学家 Thomas Hales 长文，面向同行解释 Lean 定理证明器、自动形式化现状与可靠性问题。文章梳理 Fermat 大定理、Navier–Stokes 等近期超大规模自动形式化，以及 mathlib 规模。
Hales 重点讨论 2026 年春夏被称为「声响漏洞之夏」的多起 Lean 内核缺陷（曾出现非法「证伪 Collatz」等），并指出漏洞多由前沿模型与安全研究者发现后迅速修复。文中介绍 Joachim Breitner 的形式化核 Con-Leche，以及类型论元理论仍待完善的议题（唯一定型、相对一致性等）。
结语引用 Ken Thompson「信任信任」反思：在 AI 可利用软件漏洞的时代，不能盲目信任未经充分人类审计的证明与核验证链条；自动形式化证明仍须核对陈述是否忠实于自然语言命题。