四个定理证明器的对比：Isabelle/HOL、Lean、HOL4 与 Agda
来源：blueberrywren.dev — 2026-10-10
📋 概述
作者用同一道“素数无限多”的欧几里得证明，在 Isabelle/HOL、Lean、HOL4 与 Agda 中各形式化一遍，再按易发现、易操作、愉悦度、烦躁度等主观维度打分。Lean 与 Agda 属依赖类型体系，借 Curry-Howard 对应以类型证定理；Isabelle/HOL 与 HOL4 则是 LCF 风格，一切证明必须经由小证明内核的基规则构造。结论是结构相近，差别全在用户体验。
🔑 核心要点
- 四者都用于把数学计算机形式化，但基础体系分两大流派
- Lean 与 Agda基于依赖类型与 Curry-Howard 对应
- Isabelle/HOL 与 HOL4是 LCF 风格，证明须经由小内核的基规则构造
- 统一使用同一道欧几里得“素数无限多”证明，结构相似，差别在用户体验
- 评分维度包括易发现、易操作、愉悦度、烦躁度与“困惑度”
💡 金句
所有证明在结构上看起来都很相似，因此真正拉开差距的，是使用体验。
👍 0
👎 0
← 返回 Lobsters 首页