数学家应该了解的Lean定理证明器：可靠性与AI问题
内容提要
数学家Hales撰文讨论Lean形式化数学的可靠性。2026年AI自动形式化取得突破，Fermat大定理等被快速形式化，但同年夏季发现多个Lean内核可靠性漏洞，可证明假命题。应对方案包括多内核交叉验证、形式化验证内核（如Con-Leche）及加强类型论元理论研究。作者警告AI时代不可盲信系统，需人类审计。
延伸解读
自动形式化的突破与隐忧
2026年自动形式化成为现实，AI能在短时间内生成大量Lean代码，如Fermat大定理的形式化仅用11天就产出1300万行。这极大加速了数学形式化进程，但也带来新风险：AI生成的证明可能包含人类难以察觉的错误，且依赖的Lean内核本身可能存在可靠性漏洞。因此，自动形式化虽提高效率，却要求更严格的人类审计和内核验证。
内核可靠性漏洞的警示
2026年夏季，Lean内核被发现多个可靠性漏洞，可证明假命题，甚至导致Collatz猜想的非法反证。这些漏洞由AI安全研究人员发现并修复，表明AI既能引入风险也能帮助检测。但漏洞的存在提醒我们，即使经过内核检查，形式化证明也非绝对可靠，必须结合多内核交叉验证和人类审计，才能确保数学基础的稳固。
应对策略：多内核与形式化验证
为应对内核漏洞，社区提出多内核交叉验证、形式化验证内核（如Con-Leche）及加强类型论元理论研究。Con-Leche用Lean实现并形式化了一致性证明，已通过mathlib检查。然而，交叉验证并非万无一失，不同内核可能共享缺陷。根本解决还需深化对Lean类型论的理解，证明唯一类型性、逻辑一致性等基本性质，这需要更多类型论专家参与。
AI时代的信任与审计
作者引用Ken Thompson的“信任反思”，警告在AI时代不能盲信Lean等系统。AI可能被恶意利用，在内核中植入后门，而人类难以发现。因此，必须采取对抗性视角，加强人类审计，确保形式化数学的可靠性。同时，类型论基础研究不应完全交给AI，而需人类深入参与，以维护数学的严谨性。
Q&A
Lean定理证明器是什么？它为什么受到数学家关注？
Lean是由Leo de Moura于2013年在微软开发的开源定理证明器，基于类型论（CIC）。它拥有庞大的数学库mathlib，包含近30万个定理、超过10万个定义和250万行代码，是数学家最流行的形式化工具。2026年AI自动形式化取得突破，Fermat大定理等被快速形式化，使Lean受到广泛关注。
什么是自动形式化？2026年有哪些重要进展？
自动形式化是指用AI将数学论文自动转换为形式化证明（如Lean代码）。2026年成为现实：Anthropic于9月4日宣布自动形式化Fermat大定理，11天生成1300万行Lean代码；OpenAI于9月8日宣布Navier-Stokes爆破定理并附带Lean形式化；Jared Lichtman于9月8日启动MAP项目，旨在将“所有已知数学转化为形式代码”。
Lean内核的可靠性问题是什么？2026年夏季发生了什么？
Lean内核是几千行C++代码，负责检查证明。2026年夏季被称为“可靠性漏洞之夏”，7月和8月发现多个内核漏洞，可证明假命题（如Collatz猜想的不合法反证和Kepler猜想的非法证明）。这些漏洞由安全研究人员使用前沿AI模型发现，并已迅速修复，mathlib已通过修复后的内核验证。
如何应对Lean内核的可靠性漏洞？有哪些解决方案？
文章提出三种方案：1. 开发多个Lean内核并交叉验证，已有约25个内核，但交叉验证不能消除所有疑虑；2. 形式化验证内核，如Con-Leche项目，它用Lean实现并形式化了一致性证明，已检查mathlib；3. 改进对内核和类型论的理论理解，包括修复Carneiro论文中的错误、研究唯一类型性等未解决问题。
Con-Leche是什么？它如何提高Lean的可靠性？
Con-Leche是由Joachim Breitner开发的经过验证的Lean内核，其实现和一致性证明均在Lean中形式化，代码和证明由Claude生成。一致性证明假设ZF集合论加不可达基数层级，并已通过mathlib检查。它提供了集合论模型下的一致性保证，覆盖了Lean中一些最晦涩的部分，如相互归纳类型。
为什么在AI时代不能盲目信任Lean这样的系统？
文章引用Ken Thompson的“信任反思”，指出不能信任非自己完全创建的代码。AI可能留下后门可靠性漏洞，甚至可能欺骗人类。例如，AI在2026年夏季扫描漏洞时可能植入隐蔽漏洞，若该漏洞被利用，可能破坏关键基础设施。因此，必须进行人类审计，不能盲目信任AI和形式化系统。
