2026 年 10 月 9 日，Thomas Hales 在《What’s new》发表了一篇关于 Lean 可靠性的客座文章。 最近围绕形式化数学的讨论，大多在问 AI 已经会证明什么、还能证明什么。 Hales 把问题往下追了一层：我们用 Lean 检查证明，又凭什么相信 Lean？

这个问题值得认真回答。尤其是文章提到，Lean 类型论中的一些基本性质仍没有完整证明， 其中甚至包括“一个项的类型在定义相等的意义下唯一”。 对习惯了数学教材写法的人来说，这很难不令人意外：如此基本的事情，怎么会还没有解决？

但如果读完文章，只剩下“Lean 的地基可能有问题”这一印象，也会错过重要的区别。 一份关于类型论的证明有缺口，与已经从类型论的规则推出矛盾，是两回事。 一个检查器有了可靠性证明，与整套抽象理论的所有重要性质都已证明，也不是一回事。 Hales 的文章把这些问题提到了台前；本文想接着往下讲，说明它们各自是什么， 现有结果究竟证明了什么，以及研究者正在怎样补上缺口。
Continue reading →