当我们在项目中引入形式化验证工具时，一个最常见的问题摆在面前：应该选择哪一种定理证明器？Lawrence Paulson 在其博客文章《为什么不用 Lean？》中提出的观点值得深思 —— 他作为 Isabelle 的创始人，从历史和工程实践的角度审视了当前主流证明辅助器之间的差异。这篇文章将在其基础上进一步聚焦工程选型的实际考量，为技术团队提供可操作的决策参考。
历史脉络与技术基础
形式化数学机械化的探索可以追溯到上世纪六十年代。NG de Bruijn 于 1968 年创建的 AUTOMATH 系统已经包含了现代证明辅助器的大部分核心要素，尽管其符号表示相当晦涩，且几乎没有任何自动化能力。1977 年，Jutting 使用 AUTOMATH 形式化了 Landau 的《数学基础》，其中涉及有理数等价类的形式化以及实数 Dedekind 完备性的证明 —— 这个成就此后二十年未被超越。
与 AUTOMATH 来自不同方向的 Robert Boyer 和 J Moore 开发了所谓 “计算逻辑”，初衷是验证 LISP 代码而非数学定理。他们的系统后来演变为 ACL2，在硬件验证领域取得了显著成就。这条技术路线说明了一个重要观点：形式化验证的方法并非只有一条道路可走。
Edinburgh LCF 的出现标志着证明辅助器架构的重要突破。其核心思想是使用函数式编程语言（ML）作为元语言，通过抽象数据类型来保护证明内核的安全性。这一设计被后续的 HOL、Coq（现称 Rocq）和 Nuprl 等系统所继承，形成了今天主流证明辅助器的基础架构。
三大系统的核心差异
从工程实践的角度来看，Lean、Coq（Rocq）和 Isabelle/HOL 在以下几个关键维度上存在显著差异。
证明对象的处理方式是最根本性的区别之一。Lean 和 Coq 都采用了 “命题即类型” 的 correspondence，生成庞大的证明对象来记录每一个证明步骤。这些证明对象可能占用数十兆字节的存储空间，却在运行时不产生任何实际价值。Paulson 尖锐地指出，在 “RAMmageddon” 时代，存储这些无用的数据是荒谬的。相比之下，Isabelle 采用了 LCF 架构的变体，依赖 ML 的抽象数据类型来保证证明的正确性，无需生成和存储证明对象。这种设计使得 Isabelle 在处理大型证明时具有明显的内存优势。
自动化能力是另一个关键差异。Isabelle 的 Sledgehammer 子系统可以将证明任务发送给外部自动定理证明器（如 Vampire 和 Z3），然后将返回的证明转换为可读的 Isar 脚本。这种工作流在实践中被证明极为高效 —— 用户只需写出证明的思路大纲，Sledgehammer 能够自动填补技术细节。根据 Paulson 的评价，Sledgehammer 是 “最好的自动化工具，无可比拟”。Lean 的自动化能力虽然也在快速发展，但其设计哲学更强调证明脚本的可读性和交互性。Coq 则提供了强大的自定义策略（Ltac）能力，但编写复杂的自动化脚本通常需要更高的学习成本。
类型系统的复杂性对开发者体验有直接影响。Lean 和 Coq 都依赖依赖类型理论，这意味着开发者需要处理宇宙层级（universe levels）的问题。当类型理论被 “正确实现” 时，类型检查应该是不可判定的，因为相等性的判定是不可判定的。然而，为了让类型检查在实际中可行，主流系统将相等性降级为定义相等性或外延相等性。这导致诸如 T(N+1) 和 T(1+N) 被视为不同类型的情况。虽然这些限制对熟练用户影响不大，但对初学者而言是常见的陷阱。Isabelle/HOL 采用简单类型理论，避免了依赖类型的复杂性，这在 Paulson 看来是一个重要优势 —— 特别是当用户需要处理域扩张、p-adic 数和 Grothendieck 样式的高级数学结构时。
证明可读性对于团队协作和长期维护至关重要。Isabelle 的 Isar 语言被设计为接近自然数学书写风格，proof state 在 IDE 中清晰可见，支持点击式证明构建。Paulson 将可读性列为 Isabelle 的核心优势之一。Lean 近年来也在改进其证明语言的可读性，支持嵌套的证明块，但就目前而言，Isabelle 在这方面仍然保持领先。Coq 的证明脚本往往更加命令式，需要读者理解策略的执行顺序才能把握证明的整体思路。
场景化的选型决策框架
基于上述技术差异，我们可以提炼出一个实用的选型决策框架。
当团队需要快速启动且主要目标是形式化数学时，Lean 是不错的选择。其统一的语言设计使得编程和证明可以使用同一套工具链，VSCode 的良好支持也降低了入门门槛。mathlib 库的丰富程度在持续增长，如果项目所需的基础设施已经存在于 Lean 生态中，迁移成本会很低。
当项目需要工业级验证且依赖已有的大型代码库时，Coq 仍然是可靠的选择。Coq 生态系统拥有经过时间检验的验证组件，包括经过验证的编译器、形式化的高级数学库（如 Mathematical Components）以及成熟的代码提取机制。如果项目需要将证明转换为可执行的程序代码，Coq 的提取功能是目前最成熟的解决方案。
当验证任务涉及复杂数学且对可读性和自动化有较高要求时， Isabelle 值得优先考虑。其强大的自动化能力使得非专业用户也能完成相当复杂的证明，而 Isar 语言的可读性便于团队成员之间的代码审查和知识传递。对于需要处理实分析、数论或复杂代数结构的项目，Isabelle 的数学库提供了良好的支持。
当 AI 辅助证明是核心需求时，Isabelle 的 Sledgehammer 与大语言模型的结合展现出了独特的优势。AI 生成的证明往往冗长且需要整理，但 Isabelle 的自动化工具能够高效地清理和验证这些证明。更进一步，结构化的 Isar 证明易于在不同的证明辅助器之间转换，这意味着团队不必过早锁定单一工具。
面向未来的工程考量
形式化验证领域正在经历 AI 带来的深刻变革。大语言模型能够生成证明草稿，而这些草稿需要通过可靠的证明辅助器进行验证和精化。在这一工作流中，证明工具的可读性和可转化性变得尤为重要。Isabelle 的设计恰好契合这一需求 —— 用户可以使用 AI 生成初步证明，然后通过 Sledgehammer 和手动修改将其转化为清晰的 Isar 脚本。Lean 社区也在积极探索类似的方向，但就目前的工具成熟度而言，Isabelle 在这一领域略有优势。
值得注意的另一个趋势是互操作性的需求正在增长。Paulson 在文章结尾提到，AI 可以轻松地将可读的、结构化的证明在不同证明辅助器之间转换。这暗示了一个可能的未来：工具选择将变得不那么关键，因为证明可以在不同系统之间流动。然而，在那个未来到来之前，团队仍然需要基于当前的技术成熟度和项目需求做出务实的选择。
形式化验证从来不是一条轻松的道路。从 AUTOMATH 的先驱探索，到今天 AI 与证明辅助器的结合，这个领域已经走过近六十年的历程。Paulson 的文章提醒我们，在追逐新热点的同时，不应忘记那些被时间检验过的技术和方法。无论是选择 Lean、Coq 还是 Isabelle，关键在于理解每种工具的设计哲学和工程约束，让技术选择真正服务于项目的实际目标。
参考资料
- Lawrence Paulson，《为什么不用 Lean？》，2026 年 4 月
- Paulson 关于 LCF 架构与命题即类型对应区别的讨论