数学家应了解 Lean：可靠性、健全性缺陷与 AI 自动形式化
AI 总结
Thomas Hales 在 Terry Tao 博客发表客座文章，梳理形式化数学与 Lean 定理证明器的现状：2026 年自动形式化已成为现实，里程碑包括 Math Inc. 对 24 维球填充问题的自动形式化、Meta 的 ATLAS 教材项目、Anthropic 用 11 天生成 1300 万行 Lean 代码形式化费马大定理，以及 OpenAI 在公布 Navier-Stokes 结果时附带 Lean 形式化。文章同时讨论 2026 年春夏被称为“健全性缺陷之夏”的一系列 Lean 内核漏洞——其中一个甚至给出 Collatz 猜想的非法反证——这些漏洞由安全研究者使用前沿模型发现并迅速修复，mathlib 已用修复后的内核重新验证。Hales 强调，Lean 证明必须经内核检查，并且还需人工审计以确保命题忠实于原意。
深度见解
如果 AI 能大规模产出形式化证明，那么证明助手内核的可靠性以及对命题含义的人工核对，就成了数学可信度的关键环节。