Thomas Hales 撰文谈数学家应了解的 Lean 定理证明器：可靠性与 AI

Thomas Hales 在 Terence Tao 博客发表客座文章，系统介绍 Lean 定理证明器、mathlib 库及 2026 年成为现实的 AI 自动形式化进展，包括 Anthropic 用 11 天生成 1300 万行 Lean 代码完成费马大定理形式化。