数学家该知道的 Lean 证明器：可靠性与 AI

📋 概述

这篇客座文章由 Thomas Hales 撰写、Terence Tao 的博客发布，主题是形式化与可靠性。形式化证明是在数学基础与逻辑规则层面被穷尽检查的证明，已完成的例子包括四色定理、Feit-Thompson 奇数阶定理、开普勒猜想、球面翻转、8 与 24 维球堆积、Navier-Stokes 强制爆破与费马大定理，后三项都在今年完成，也让形式化的潜力被广泛注意。Lean 由 Leo de Moura 于 2013 年在微软开发并开源，其数学库 mathlib 已有近 30 万条定理、10 万多个定义、250 万行代码与 700 多名贡献者。HN 讨论则追问 Lean 内核是否还会出现可靠性缺陷，以及由 AI 生成的 Lean 证明该如何建立信任。