四个定理证明器的故事，或：对 Isabelle/HOL、Lean、HOL4 与 Agda 的一份（还算）有主见的比较

# 四个定理证明器的故事，或者：对 Isabelle/HOL、Lean、HOL4 和 Agda 的一份（还算）有主见的对比 来源：https://blueberrywren.dev/blog/primes/ **2026-10-10** 作者：A Wren ## 目录 - [以上这些（哇，标题好长）](https://blueberrywren.dev/blog/primes/#the-above-wow-long-title) - [我们到底在比较什么？](https://blueberrywren.dev/blog/primes/#what-are-we-comparing-anyway) - [比较的基础是什么？](https://blueberrywren.dev/blog/primes/#and-on-what) - [开始比较！](https://blueberrywren.dev/blog/primes/#comparison-time) - [总体上的相似与差异](https://blueberrywren.dev/blog/primes/#overarching-similarities-differences) - [证明对比](https://blueberrywren.dev/blog/primes/#proof-comparisons) - [随性排名](https://blueberrywren.dev/blog/primes/#arbitrary-rankings) - [证明发现的难易程度（越高越好）](https://blueberrywren.dev/blog/primes/#ease-of-proof-discovery-higher-better) - [证明操控的难易程度（越高越好）](https://blueberrywren.dev/blog/primes/#ease-of-proof-manipulation-higher-better) - [愉悦度（越高越好）](https://blueberrywren.dev/blog/primes/#enjoyment-higher-better) - [恼怒指数（越低越好）](https://blueberrywren.dev/blog/primes/#annoyance-factor-lower-better) - [困惑指数（越低越好）](https://blueberrywren.dev/blog/primes/#puzzled-factor-lower-better) - [综合最佳](https://blueberrywren.dev/blog/primes/#overall-best-in-class) - [全部代码](https://blueberrywren.dev/blog/primes/#all-the-code) ## 以上这些（哇，标题好长） 我将对 Lean、Isabelle/HOL、Agda 和 HOL4 进行比较，对"公平性"只给予了些许关注。 ## 我们到底在比较什么？ 以上四个都是定理证明应用；也就是说，它们的目的是将数学在计算机上进行形式化。大致而言，Lean 和 Agda 都是基于依赖类型（dependent types）的系统，利用 Curry-Howard 对应关系通过复杂的类型系统来证明定理；而 Isabelle/HOL 和 HOL4 是 LCF 风格的系统，具有一个包含基本规则（例如 `forall x, x = x`）的小型"证明内核"，所有证明都必须通过它来构建。这两种基础各有利弊，下文会讨论其中一些。 ## 比较的基础是什么？ 我在四个系统中都形式化证明了素数的无穷性；即命题"对于任意数字 n，都存在一个比 n 大的素数"。所形式化的具体证明是欧几里得的"标准"构造，你可以在 Wikipedia 上找到；见 [此处](https://en.wikipedia.org/wiki/Euclid%27s_theorem)。 所有证明的结构看起来都很相似（大部分如此，后面会说到），因此造成差异的是用户体验。坦率地说，在这次实验之前，我最熟悉的是 Isabelle/HOL 和 Agda，并在撰写本文的过程中部分地学习了 HOL4 和 Lean。 ## 开始比较！ 接下来是一堆观点和一些相当随性的分类。请不要期待一篇客观公正的评测。如果你只想看证明对比，请跳到[证明对比](#proof-comparisons)部分；如果你只想看更多观点，请读完下面的部分然后跳到[随性排名](#arbitrary-rankings)部分。观点放在前面。 我不声称以下任何证明是完美的！它们实际上可能相当平庸。 ## 总体上的相似与差异 我们可以从几个类别来对这些定理证明器进行分组。上面已经提到了： - **LCF 风格**：Isabelle/HOL、HOL4 - **依赖类型风格**：Lean、Agda 但还有： ### 交互性 - **高交互性**：Isabelle/HOL、Lean - **低交互性**：HOL4、Agda 原因：Isabelle/HOL 和 Lean 都在你输入时提供"实时更新"，并且它们的结构化证明可以通过按下方向键逐步查看中间步骤。相比之下，完成的 HOL4 和 Agda 证明以完整组装好的项的形式存在，如果你想检查其内部结构，必须手动拆解。当然，HOL4 和 Agda 都可以在任何时候向你显示当前状态和相关信息。 ### 自动化 - **高自动化**：Isabelle/HOL、HOL4 - **中等自动化**：Lean - **低自动化**：Agda Isabelle/HOL 拥有 `sledgehammer`，它可以调用多种外部证明生成方法（SAT/SMT 求解器、各种一阶逻辑求解器等）。对于任何看起来可行但繁琐的目标，`sledgehammer` 有很大概率能够解决——这很好，因为它节省了你的工作量，但它生成的证明也是难以理解的，这或许不太理想。 HOL4 也有一个等价工具叫 HolyHammer，但在我写这篇文章时我都不知道它的存在。算了。 Isabelle/HOL 和 HOL4 都对许多自动简化和证明方法有非常好的支持，例如在处理复杂假设时非常有用。如果不借助简化把所有东西都拆分成小块，可能很难知道如何继续。 Lean 有不错的自动化，但达不到 Isabelle/HOL 或 HOL4 的水平。它的 `simp` 效率远不及前者，而 `grind` 虽然是一个非常好的方法，有时可以与 `sledgehammer` 媲美，但很多时候由于我不太清楚的原因它相当没用。`sledgehammer` 和 `grind` 都是全有或全无的；如果它们不能解决目标，就不会有任何进展。这与三个系统中的 `simp`，或更专业的工具如 `auto`（Isabelle/HOL）或 `gvs`（HOL4）形成对比，后者可以取得一些进展，然后将上下文留在（理想情况下）更好的状态。 Lean 没有同样好的部分自动化能力有点可惜，因为根据我的经验，这才是真正更重要的。值得注意的是，Lean 和 Isabelle/HOL 都有 `try`（在 Isabelle/HOL 中，`try`/`try0` 用于有/无 `sledgehammer` 的情况；在 Lean 中，`try?`/`exact?`/`rw?`），可以用各种自动化方法和直接求解尝试来"试一试"你的目标。据我所知，HOL4 没有等价的工具，这很不幸，因为它相当有用。 Agda 基本上没有任何自动化。你得到的唯一简化是基于函数输入可计算的部分。坦率地说，这有点糟糕。因为有太多手动操作需要考虑，所以很难完成事情。我个人不太喜欢。 ### 基础 Isabelle/HOL 和 HOL4 的基础都极其经典，这意味着它们接受排中律（Law of Excluded Middle，∀ P. ¬P ∨ P），并且都公理化了 Hilbert 的 epsilon，这也导致了选择公理（Axiom of Choice）。 这对自动化求解器似乎有非常积极的影响，因为它们经常依赖双重否定消除（¬¬P ⟶ P）这样的定律，这与排中律等价。 Lean 理论上是构造性的（因此默认没有排中律），但一些"好用的"证明自动化需要排中律，而且使用经典方式似乎是 Lean 的常态，所以我就这么做了。例如 `grind` 就假设你正在使用它。这有一个缺点，就是 Lean 在处理存在量词等方面表现得不太好。 Agda 默认是构造性的，而且在 Agda 世界中保持证明的构造性似乎是常态，所以我也是这样做的。这样做的一个大好处是，在证明了素数有无穷多个之后，我实际上可以生成它们！我可以给我的证明一个数字，它就会输出一个比该数字更大的素数。 缺点是这样做*极其*缓慢： - 0: 2（瞬间） - 1: 3（瞬间） - 2: 7（瞬间） - 3: 5（瞬间） - 4: 11（四分之一秒） - 5: 7（四分之一秒） - 6: 71（3秒） - 7: 61（10秒） - 8: 19（40秒） 如果你看了上面的证明结构，这可能就能理解了；我们考虑 `(n + 1)! + 1`，所以在那个证明内部，它在检查约 360,000 左右的数字的素性；那会有点慢。应该注意的是，这种构造并不是为了速度而设计的，但它也是最自然的一种。 是否值得放弃排中律和良好的证明自动化呢？你来决定。 ### 依赖类型作为基础 vs. LCF 我更倾向于 LCF，因为它似乎更适合自动化，而且我不觉得携带证明项有什么意义（经典逻辑太有用了！）。如果你强烈反对，请发送邮件到 contact AT blueberrywren.dev 给我，如果我觉得你的论点足够好，我会把它发布在这里。 ### 交互模式 Lean 和 Isabelle/HOL 都是交互式使用的。Lean 有其他编辑器的模式，但强烈推荐使用 VSCode，而 Isabelle/HOL 有自己的编辑器（jEdit），实际上也强制使用它。 这*没问题*；我理解他们为什么这样做，因为让交互式开发通用化是相当困难的。它们都能做到。 HOL4 通过 Emacs 模式或 Vim 模式进行交互，还有一些按键绑定可以将文本复制到运行中的 HOL4 REPL 中或从其中复制出来。这听起来很奇怪，确实也确实很奇怪，但效果出乎意料地好。我本来就是 Emacs 用户，所以对我来说没什么变化。 Agda 也是通过 Emacs 模式进行交互的，但一切都在你的文件中发生；你可以使用按键绑定来刷新状态、添加证明目标等。这也很好用。 如上所述，Lean/Isabelle/HOL 方法的优势在于你可以看到正在进行中的证明，这在 Agda 中做不到。 ### 文档 Isabelle/HOL 和 HOL4 都有极好的定理搜索机制；前者有一个编辑器面板加上 `find_theorems`，后者有 `DB.find`/`DB.match`。这些允许按名称和模式搜索定理，所以我可以搜索形如 `_ < SUC _` 的引理。这*非常*方便！很多时候你知道你想要的东西的*形状*，但可能不知道具体的引理。 Lean 有 leansearch 和 loogle，很有意思，但是它们： 1. 不是内置的。 2. 没那么好用。 这有点让人失望。`exact?` 和 `rw?` 作为"这里有些你可能能做的事"存在，但它们远没有那么灵活。 正如预期的那样，Agda 没有等价的工具。你必须成为**禅宗大师**，通过在 Agda 标准库的正确部分中翻找来找到你需要的东西。 ## 证明对比 注意：这并不是任何这些系统的教程，虽然我在开头会做一些解释。这主要是为了读者进行比较，看看类似等价的命题在不同语言中的证明是什么样的。 让我们进入证明！我们将逐段进行，探索证明的各个部分并沿途进行解释。 在此之前，一些大致有趣的统计数据： - **Isabelle/HOL**：117 行代码，包含 19 个证明。 - **Lean**：155 行代码，包含 12 个证明。 - **HOL4**：190 行代码，包含 16 个证明。 - **Agda**：264 行代码，包含 45 个证明（不计算 `where` 块的话是 29 个） 这些完全不能直接比较，但仍然很有趣。 我们从定义整除性开始。在 Agda 中我们偷懒使用了标准库版本，这样我们可以利用关于计算除数的现成证明，而我不太想重新实现它们。 Isabelle/HOL： ``` definition divides :: "nat ⇒ nat ⇒ bool" where "divides n k = (∃j. j * n = k)" ``` Lean： ``` @[grind] def divides (n k : Nat) : Prop := ∃q, k = n * q ``` HOL4： ``` Definition divides_def: divides n k = ∃q. q * n = k End ``` Agda（看起来像是标准库中的）： ``` record _∣_ (m n : N) : Set where constructor divides field quotient : N equality : n ≡ quotient * m ``` 基本上是一样的。然后我们证明了一些关于整除性的引理（`divides k 0`、`divides k k` 等）。我们要展示的一个是 `divides n k ⟹ divides n j ⟹ divides n (k - j)`，它在一些定理证明器中比较有趣。 在下面所有的例子中，乘法/减法引理本质上陈述的是 `a * (b - c) = a * b - a * c`。 Isabelle/HOL： ``` lemma divides_diff: "divides x k ⟹ divides x n ⟹ divides x (k - n)" using divides_def by (metis diff_mult_distrib) ``` 证明搜索过程 `metis` 完成了大部分工作。 Lean： ``` theorem divides_sub (n j k : Nat) (h1 : divides n k) (h2 : divides n j) : divides n (k - j) := by obtain ⟨q1, h1⟩ := h1 obtain ⟨q2, h2⟩ := h2 unfold divides exists (q1 - q2) grind [Nat.mul_sub] ``` 我们做一些解包，然后将 `q1 - q2` 确认为另一个项（使得 `n * (q1 - q2) = k - j`）。然后用适当的引理进行 `grind` 就能到达目标。 HOL4： ``` Theorem divides_sub: divides n k ⇒ divides n j ⇒ divides n (k - j) Proof rpt strip_tac >> metis_tac[RIGHT_SUB_DISTRIB, divides_def] QED ``` 和 Isabelle/HOL 一样，在提供了适当的引理之后，`metis_tac` 直接解决了。 Agda： ``` divides-sub : ∀ {i j k} → i ∣ j → i ∣ k → i ∣ (j ∸ k) divides-sub {i} (divides-refl q1) (divides-refl q2) = divides (q1 ∸ q2) (sym (*-distribr-∸ i q1 q2)) ``` 非常相似。`divides-refl` 是 `divides _ refl` 的缩写，和 Lean 一样，我们必须手动指出 `q1 ∸ q2`。 让我觉得有趣的是，Lean 的证明在某种程度上是如此费劲。尽管 Lean 拥有相当不错的自动化，但那个证明我花了比其他任何证明都多的精力！找到适当的引理也更费劲一些，不过公平地说，那时候我还在琢磨语法。 接下来我们需要定义一个数字列表的乘积，如下所示： Isabelle/HOL： ``` fun prod_list :: "nat list ⇒ nat" where "prod_list [] = 1" | "prod_list (x # xs) = x * prod_list xs" ``` Lean： ``` @[simp, grind] def prod_list (xs : List Nat) : Nat := match xs with | [] => 1 | x :: xs => x * prod_list xs ``` `simp` 和 `grind` 标记是为了帮助自动化证明方法，它们确实起作用了！ HOL4： ``` Definition prod_list_def: (prod_list [] = 1) ∧ (prod_list (x :: xs) = x * prod_list xs) End ``` Agda： ``` prod-list : List Nat → Nat prod-list [] = 1 prod-list (x ∷ xs) = x * prod-list xs ``` 在 HOL4 中定义东西有点有趣，因为你只是把函数体定义为一个证明！这个定义会输出一个定理 `prod_list_def`，它字面上是： ``` val it = ⊢ prod_list [] = 1 ∧ ∀x xs. prod_list (x::xs) = x * prod_list xs: thm ``` \! 在 Agda 证明中，我们还做了一堆工作来设置最终将成为素性判定程序的东西。这是因为我们之后想问"这个数是素数吗？"，而没有排中律来说明"它要么是素数要么不是素数"，我们需要写一个算法来替我们判定。 回到正轨，我们需要证明关于 prod_list 函数的几个引理。其中一个有趣的如下，我们证明列表中的某个数能整除列表的乘积。 Isabelle/HOL： ``` lemma divides_prod_list: "x ∈ set xs ⟹ divides x (prod_list xs)" apply (induct xs) apply simp apply auto apply (case_tac xs; simp add: divides_def) apply (case_tac xs; simp) apply (rule mult_divide_l) by assumption ``` 非常隐式；很难看出发生了什么，但基本结构在那儿。对列表进行归纳，做一些情况分析，应用一个关于 `divides _ (_ * _)` 的引理。 Lean： ``` theorem divides_prod_list : ∀ xs x, x ∈ xs -> divides x (prod_list xs) := by intros xs x mem induction xs with | nil => grind | cons y ys ih => by_cases h : (x = y) · rw [h] simp exists (prod_list ys) · cases mem with | head => grind | tail => rename_i a have ⟨h, hq⟩ := ih a simp at * rw [hq] exists (y * h) grind ``` 相当大。我们必须相当手动地解构成员关系，这有点麻烦。不过这是一个相当直接的证明。 HOL4： ``` Theorem divides_prod_list: x ∈ set xs ⇒ divides x (prod_list xs) Proof Induct_on ‘xs’ >- fs[] >- (fs[] >> rpt strip_tac >- (fs[prod_list_def, divides_def] >> qexists_tac ‘prod_list xs’ >> simp[]) >- (fs[divides_def, prod_list_def] >> qexists_tac ‘h * q’ >> rev_drule EQ_SYM >> strip_tac >> fs[])) QED ``` 也不算疯狂，但如果没有注释（我没写 :P）很难看出确切的结构。这是一个好时机来指出 HOL4 的证明字面上就是 SML 项！没有什么比这更多的了！组合子 `>>` 和 `>-`（分别用于应用后续步骤和处理目标）在 SML 的高阶函数和管道操作中都能找到。