Thomas Hales 解读 Lean 定理证明器：可靠性与 AI 自动形式化

Thomas Hales 在 Terry Tao 博客发表客座文章，评估 Lean 在 AI 自动形式化快速发展后的可靠性。文章称 mathlib 已含近 300000 条定理、100000 多个定义和 250 万行代码，并列举 2026 年费马大定理、Navier-Stokes forced blowup 等自动形式化项目。