Hales：Lean 查得出推导错，查不出你问错问题

今年 7 月到 8 月，Lean 的证明检查内核连续出现漏洞。其中一个能让使用者证出 Collatz 猜想的反例——而那个证明是错的。

一、发生了什么

10 月 9 日，Thomas Hales 在陶哲轩的博客上发了一篇客座文章，谈数学家该怎么看待 Lean。开头有陶哲轩的编者按，注明这是 Hales 的客座文章，原稿是另一种文件格式、经 AI 转换；文末致谢也写明作者是 Hales。这篇不是陶哲轩本人写的。

Hales 给出的背景数字是：Lean 2013 年由微软的 Leo de Moura 开源，2017 年有了数学库 mathlib，如今 mathlib 收录近 30 万条定理、超过 10 万个定义、250 万行代码，贡献者超过 700 人。

2026 年自动形式化的进展被他列成一条时间线：1 月有人用两周生成 13 万行形式拓扑；3 月 Math Inc. 完成 24 维球堆积的形式化，约 50 万行；5 月 Meta 的 ATLAS 把 26 本教材的大部分内容形式化；9 月 4 日 Anthropic 宣布费马大定理形式化，11 天产出 1300 万行 Lean 代码；9 月 8 日 OpenAI 公布 Navier-Stokes 爆破解，同时给出形式化版本。

然后是他真正想说的部分。Lean 的证明要经过一个只有数千行 C++ 的内核检查，检查通过才算数。但内核本身会有 bug。2026 年夏天集中爆出的那批漏洞里，一个导致 Collatz 的非法反证，Hales 本人也因为同一个漏洞做出了开普勒猜想的简短错误证明。这些漏洞后来都被修复，mathlib 用修好的内核重新验证过。发现它们的是安全研究人员，用的是前沿 AI 模型。

他给了三条防线。第一条是多内核交叉，社区里已经有约 25 个 Lean 内核实现。第二条是形式化验证内核本身：9 月 10 日，Joachim Breitner 发布了一个经过一致性证明的检查器 Con-Leche，代码和证明由 Claude 生成，Hales 称这是 Lean 历史上最重要的里程碑之一。第三条是补类型论的基础，他明确说，截至 2026 年 10 月，他还不知道有哪份完整公开的、覆盖 Lean 抽象类型论的相对一致性证明。哥德尔第二不完备定理决定了这条路只能做到"相对"。这也是他呼吁更多类型论学者参与的原因。

二、跟你有什么关系

做数学、写论文的。 形式化能帮你排除推导错误，但不能替你确认"这条定理是不是你想证的那条"。Hales 把后者叫陈述保真，必须人工审计。

做形式化工程的。 内核不是一个可以默认可信的黑盒。你需要多内核交叉检查、版本记录，以及检查是否引用了未授权的公理。

把 AI 输出当结论用的。 1300 万行代码听起来很唬人，但它只证明了一件事：从给定的陈述出发，推导能走到终点。陈述错了，一切白搭。

三、怎么判断

1. 先读陈述，再读证明。 打开形式化文件，看 theorem 那一行的量词、假设、边界条件。这一步不能交给模型。
2. 查公理。 Lean 有工具能列出证明依赖了哪些公理。多出一条 sorry 或一个额外假设，结论就不成立。
3. 至少两个内核。 社区里已有约 25 个 Lean 内核实现，交叉验证能挡掉一部分实现错误。但 Hales 提醒，不同内核可能有相同的缺陷，理想情况是独立实现。
4. 记版本。 内核会修 bug，修完之后旧证明要重跑。把 Lean 版本、mathlib 提交号写进论文附录。

四、三个别信的说法

「形式化验证过的证明一定对。」 它保证的是"在内核没有 bug 的前提下，从陈述到结论的推导成立"。2026 年夏天说明，内核有 bug 不是假设，是事实。

「AI 能自动形式化，数学家可以退场了。」 Hales 举的每个案例里都有人介入：定陈述、补定义、处理 AI 卡住的地方。11 天 1300 万行，前提是有人把问题切好。

「内核很小，所以容易审。」 数千行 C++ 的复杂度不在行数。Lean 4 在 2023 年 9 月发布前修过两个漏洞，2025 年 5 月又修了一个溢出问题，2026 年夏天还有一批。小不等于简单。

五、一句话结论

形式化把"推导有没有错"变成了可机器检查的问题，但"你证的是不是你想证的东西"，仍然只能由人回答。

信息来源

• Terence Tao 博客（客座作者 Thomas Hales）：What mathematicians should know about the Lean Theorem Prover（2026 年 10 月 9 日）

功能与价格以官方公告为准。本文写于 2026 年 10 月 18 日。