阅读 Lean 4 定理的漫游指南

你对数学证明的了解比你想象的要多。如果你曾编写过带有类型签名的函数，你实际上就编写了在结构上与形式化证明相同的东西。这一事实源于一个深刻的理论结果，即 Curry-Howard 同构，它是像 Lean 4 这样的证明助手的基础。

考虑这个 TypeScript 函数：

function compose<A, B, C>(f: (b: B) => C, g: (a: A) => B): (a: A) => C {
  return (a) => f(g(a));
}

现在考虑这个 Lean 4 定理：

theorem imply_transitivity {P Q R : Prop} (hpq : P → Q) (hqr : Q → R) : P → R :=
  fun hp => hqr (hpq hp)

这两者是相同的。TypeScript 函数表示“给定 $f: B \to C$ 和 $g: A \to B$，我可以生成 `$A \to C$。”Lean 定理表示“给定一个 $P$ 蕴含 $Q$ 的证明，以及一个 $Q$ 蕴含 $R$ 的证明，我可以生成一个 $P$ 蕴含 $R$ 的证明。”实现是相同的：组合这两个函数。一个类型就是一个命题，而一个该类型的程序就是该命题的证明。当 Lean 的编译器接受你的代码时，它就验证了你的证明——不是通过运行测试或检查示例，而是通过验证你编写的程序确实拥有你所声称的类型。

本文旨在教你像阅读他人的代码一样阅读 Lean 4 证明：通过理解每个步骤背后的词汇、结构和意图。所有示例均来自经过真实验证的项目——AMO-Lean，一个形式化验证的密码学原语优化器，以及 OptiSat，一个经过验证的 e-graph 等价饱和引擎。不需要任何 Lean 或形式化数学背景。如果你能阅读 Python 或 TypeScript，你就能学会阅读 Lean 证明。

罗塞塔石碑

在深入语法之前，建立数学和编程概念之间的转换是有帮助的。形式化数学中的每一个概念都有一个直接的编程对应物。

一个 theorem 是一个带有类型签名的函数。它的 hypotheses 是函数参数，它的 conclusion 是返回类型。proof 是函数体——实现。一个 lemma 是一个辅助函数。$\forall$（对于所有）是一个泛型类型参数。箭头 $\to$ 既表示“蕴含”也表示“从 $A$ 到 $B$ 的函数”。合取 $\wedge$ 是一个元组。析取 $\vee$ 是一个带标签的联合类型。存在 $\exists$ 是一个依赖对。相等 $= 是结构相等。而 QED——kernel 接受证明的那一刻——就是类型检查器说“这可以编译”的那一刻。

在编程中，你相信编译器会拒绝类型错误的程序。在 Lean 中，你相信 kernel——一个最小的、经过良好审计的核心——会拒绝无效的证明。kernel 是你唯一需要信任的东西。其他一切——tactics、自动化、Mathlib 中超过 500,000 行代码——都可能存在 bug，但 kernel 仍然会捕捉到这些工具生成的任何无效证明。这被称为 de Bruijn criterion：验证器独立于证明生成器 (the verifier is independent of the proof generator)。可以将其视为信任 CPU 和 OS kernel，但不信任应用程序代码。在 Lean 中，信任边界甚至更严格。

定理的结构

让我们从最简单开始，解剖真实的定理，并逐步构建出你在经过验证的代码库中会遇到的复杂性。

在 Lean 中你能写的最简单的定理是这样的：

theorem one_plus_one : 1 + 1 = 2 := rfl

作为一个程序员来阅读它：theorem 声明一个命名的、有类型的值，就像 JavaScript 中的 const。one_plus_one 是名称。: 1 + 1 = 2 是声明签名。而 := rfl 是证明，其中 rfl 代表 tactic “自反性”，它是一个向证明器发出的命令，表明两边计算出相同的值。kernel 将 $1 + 1$ 评估为 $2$，将 $2$ 评估为 $2$，确认它们相同，并接受证明。没有运行时检查发生。真相在编译时建立。

当 hypotheses 出现时，事情变得更有趣：

theorem add_pos (a b : Nat) (ha : a > 0) (hb : b > 0) : a + b > 0 := by
  omega

这里 $a b : Nat$ 是两个自然数参数——就像 function add_pos(a: number, b: number)。然后 $(ha : a > 0)$ 是一个 $a$ 为正数的 proof：一个前置条件，一个契约。命名约定在 Lean 代码库中是一致的：$h$ 代表“hypothesis”，后面是它所指的变量，所以 $ha$ 是关于 $a$ 的 hypothesis，$hb$ 是关于 $b$ 的 hypothesis。当几个 hypotheses 涉及同一个变量时，像 $h_1$ 和 $h_2$ 这样的编号变体很常见。你还会看到 $ih$ 表示“inductive hypothesis”，$hne$ 表示非相等，$hlt$ 表示小于，$this$ 表示最近的未命名结果。结论 $: a + b > 0$ 是在满足前置条件的情况下必须为真的东西，而 omega 是一个 tactic——一个用于线性算术的自动化求解器——它自动构造证明项。

花括号引入了 implicit arguments，Lean 版的泛型：

theorem list_append_nil {α : Type} (l : List α) : l ++ [] = l := by
  simp

$\{ \alpha : Type \}$ 告诉 Lean 从上下文中推断 $\alpha$。你从不写 list_append_nil Nat [1, 2, 3]——只写 list_append_nil [1, 2, 3]，Lean 就会推断出 $\alpha = Nat$。这与 TypeScript 的 function appendNil<T>(l: T[]): T[] 的工作方式完全相同：类型参数是被推断出来的，而不是明确指定的。

真实世界的定理结合了所有这些元素。这是 AMO-Lean 的 NTT 验证中的一个定理：

theorem sum_of_powers_zero {ω : F} {n : ℕ} (hn : n > 1)
    (hω : IsPrimitiveRoot ω n) :
    (Finset.range n).sum (fun i => ω ^ i) = 0

不要对密度感到恐慌。逐块解码它：$\{ \omega : F \}$ 是某个域 $F$（一个带有算术的泛型 $T$）的一个 implicit 元素。$\{ n : \mathbb{N} \}$ 是一个 implicit 自然数。$(hn : n > 1)$ 要求 $n > 1$。$(h\omega : \text{IsPrimitiveRoot } \omega n)$ 要求 $\omega$ 是一个 $n$ 次单位本原根——一个结构化的数学属性，断言 $\omega^n = 1$ 且对于 $0 < k < n$ 有 $\omega^k \neq 1$。结论是 $ \omega^0 + \omega^1 + \dots + \omega^{n-1}$ 的和为零。在编程术语中，这是一个在域类型上参数化的泛型函数，接受两个证明作为输入，并返回一个幂和为零的证明。这是 Number Theoretic Transform (数论变换) 的一个基本结果，它是 FFT (快速傅里叶变换) 的密码学友好型近亲。

证明状态：你的调试器

当你在 Lean 中编写 by 时，你就进入了 tactic mode (策略模式)——一个交互式环境，感觉非常像调试器会话。有一个 goal：你需要证明的东西，就像一个失败的断言。有 hypotheses：你已经知道的事实，就像作用域中的变量。每个 tactic 都是一个命令，它转换 goal，让你离完成它更近一步。

符号 $\vdash$（称为“转角符”）将你所知道的与你需要证明的分开。$\vdash$ 上方的一切都在作用域内；下方是你的义务。这是一个证明，每一步都标注了状态：

TODO

theorem add_comm_manual (a b : Nat) : a + b = b + a := by
  -- 状态：a : Nat, b : Nat ⊢ a + b = b + a
  induction a with
  | zero =>
    -- 状态：b : Nat ⊢ 0 + b = b + 0
    simp
  | succ n ih =>
    -- 状态：ih : n + b = b + n ⊢ n + 1 + b = b + (n + 1)
    rw [Nat.succ_add, Nat.add_succ, ih]

这个结构反映了递归编程。induction a 创建了两个子目标——基例 ($a = 0$) 和归纳步 ($a = n + 1$)——其中你免费获得了 $ih$，即 inductive hypothesis。在基例中，simp tactic 通过重写项来“简化”它们，调用一个事实数据库。第二个分支是“recursive call”，其中 $ih$ 是 inductive hypothesis。给定 hypothesis，我们可以重写 (rw) 这些项以满足 goal。kernel 保证终止，因为 $n < n + 1$。如果你曾编写过带有基例和减少问题的步骤的递归函数，你已经完成了归纳。

Tactic 词汇表

Tactics 是构造证明的命令，每一个都有清晰的编程类比。Lean 附带了一个非常方便的 tactics 选择，并且可以开发专门针对数学子领域的新 tactics。你可以在此处查看 tactic 参考。

intro 正在命名函数参数。当目标是 $P \to Q \to R$ 时，写入 intro hp hq 会将 $P$ 和 $Q$ 作为 $hp : P$ 和 $hq : Q$ 移入 hypothesis 上下文，留下 $R$ 作为新目标。它是编写 function(hp, hq) { ... } 的形式化版本。

exact 是 return。它通过提供一个类型完全正确的项来关闭目标。exact $h$ 表示“证明正是 $h$”，就像return h表示“答案正是h`”。

apply 是部分函数应用。如果你有 $hpq : P \to Q$ 并且你的目标是 $Q$，那么 apply $hpq$ 会将目标简化为 $P$。它表示“我知道如何从一个 $P$ 得到一个 $Q$，所以现在只需给我一个 $P$。”这就像调用一个函数，让类型检查器找出还需要哪些参数。

rw 是查找和替换。给定一个方程 $h : a = b$，tactic rw [$h$] 会在目标中将 $a$ 的所有出现替换为 $b$。你可以使用 rw [$\leftarrow h$] 反向重写（将 $b$ 替换为 $a$），并使用 rw [$h$] at $h2$ 在特定 hypotheses 中重写。它是数学表达式的正则表达式替换，只是 kernel 保证它保持真理。

simp 从包含数百个简化引理的数据库中提取，并应用它们直到目标处于范式。simp only [rule1, rule2] 将其限制为特定规则。把它想象成数学表达式的 eslint --fix——例如，它知道 $l ++ [] = l$，$0 + n = n$，以及数千个类似的 S事实。当你在证明中看到 simp 时，作者的意思是“这遵循标准简化规则”。

omega 用于解决 $N$ 或 $Z$ 上的线性算术问题。它决定任何 Nat 或 Int 上的线性不等式系统，处理 $+$、$-$、与常数的乘法、$\le$、$<$、$=$、$\neq$ 和逻辑组合。当证明以 omega 结束时，该语句是一个常规的算术事实。可以将其视为整数片段的 Z3。

cases 是 switch。它解构一个值，并为每个构造器创建一个子目标。对于 Nat，这意味着 zero 和 succ m。对于 Bool，true 和 false。对于自定义枚举，每个变体。当你看到 cases x with | variant1 => ... | variant2 => ... 时，可以将其解读为一个必须处理所有可能情况的 match 表达式。

have 是一个局部 let 绑定。编写 have $h3 : T := \text{proof}$ 会将一个新事实 $h3$，类型为 $T$，通过 proof 引入到上下文中。它恰好是一个局部变量声明：你证明了一些中间的东西，给它命名，然后稍后使用它。它是“提取局部变量”重构，应用于证明。

constructor 构建结构体。对于 $\wedge$（逻辑 AND），它将目标拆分为两个子目标——证明每个合取。对于 $\exists$（存在），它要求你提供一个见证。对于 $\leftrightarrow$（当且仅当），它拆分为正向和反向。$\langle \dots \rangle$ 尖括号是 Lean 的匿名构造器表示法，等同于元组或结构体字面量。

还有两个值得一提。split 通过为每个分支创建子目标来处理目标中的 if/then/else 表达式。而 $<;>$ 组合器 将相同的 tactic 应用于所有待处理的目标——它是证明义务的 .forEach()。

这是核心词汇表。十几个 tactics 涵盖了你将遇到的绝大多数证明。让我们看看它们是如何工作的。

逐步解读真实证明

当定义完成了所有工作时

来自 AMO-Lean 的 NTT butterfly 实现：

def butterfly_fst (a b twiddle : F) : F := a + twiddle * b
def butterfly_snd (a b twiddle : F) : F := a - twiddle * b

theorem butterfly_fst_eq (a b twiddle : F) :
    butterfly_fst a b twiddle = a + twiddle * b := rfl

该定理表示“$butterfly\_fst \ a \ b \ twiddle$ 等于 $a + twiddle * b$”，证明是 rfl。为什么？因为 $butterfly\_fst$ 被 定义 为 $a + twiddle * b$。当 Lean 评估两边时，它们是相同的。证明字面意思是“查看定义”。

这种模式揭示了一个设计原则：当证明是 rfl 时，定义在进行智力工作。 最好的 Lean 代码使有趣的属性自然而然地从定义中产生。如果你发现自己为简单的属性编写冗长的证明，这通常意味着定义需要重新思考。

归纳法反映函数结构

来自 AMO-Lean 的 list 工具：

def evens : List α → List α
  | [] => []
  | [x] => [x]
  | x :: _ :: xs => x :: evens xs

theorem evens_length (l : List α) :
    (evens l).length = (l.length + 1) / 2 := by
  induction l using evens.induct with
  | case1 => simp [evens]
  | case2 x => simp [evens]
  | case3 x y xs ih =>
    simp only [evens, List.length_cons]
    rw [ih]
    omega

函数 evens 从列表中提取偶数索引的元素：$[a,b,c,d,e]$ 变为 $[a,c,e]$。它有三种模式匹配情况——空列表、单元素列表和两个或更多元素的列表。证明有 完全相同的三个情况，因为 induction l using evens.induct 从函数自身的模式匹配生成归纳原理。

基例 (case1 和 case2) 由 simp [evens] 处理——展开定义，简化，完成。有趣的情况是 case3：对于列表 $x :: y :: xs$，我们有 inductive hypothesis $ih : (\text{evens } xs).\text{length} = (xs.\text{length} + 1) / 2$。证明通过 simp only 展开 evens 和 List.length_cons，通过 rw 替换 $ih$，并使用 omega 完成剩余的算术。

要点是：证明结构反映函数结构。 函数中有三个情况，证明中也有三个情况。inductive hypothesis 是递归调用。omega 处理手动处理会很繁琐的算术记账。如果你能阅读函数，你就能阅读证明。

前向和后向：双条件证明

来自 OptiSat 的 utility 库：

theorem le_min_iff (a b c : Nat) : c ≤ Nat.min a b ↔ c ≤ a ∧ c ≤ b := by
  constructor
  · intro h
    exact ⟨Nat.le_trans h (min_le_left a b),
           Nat.le_trans h (min_le_right a b)⟩
  · intro ⟨ha, hb⟩
    simp only [Nat.min_def]
    split <;> omega

目标是 $\leftrightarrow$（当且仅当），所以 constructor 将其拆分为两个方向——就像实现 serialize 和 deserialize。正向假设 $h : c \le \text{Nat.min } a b$ 并使用 $\langle \dots, \dots \rangle$——Lean 的元组字面量——构建合取。每个分量通过 Nat.le_trans 连接两个不等式：从 $c \le \min a b$ 和 $\min a b \le a$，我们得到 $c \le a$。反向将合取解构为 $ha$ 和 $hb$，将 min 展开为其 $if \ a \le b \text{ then } a \text{ else } b$ 定义，然后 split $<;>$ omega 在 if 上进行拆分，并使用算术求解器解决两个分支。

组合保证：健全性三明治

来自 OptiSat 的 rewrite rule verification：

theorem sound_rule_preserves_consistency
    (g : EGraph Op) (rule : SoundRewriteRule Op Expr Val)
    (lhsId rhsId : EClassId)
    (env : Nat → Val) (v : EClassId → Val)
    (hv : ConsistentValuation g env v)
    (hwf : WellFormed g.unionFind)
    (h1 : lhsId < g.unionFind.parent.size)
    (h2 : rhsId < g.unionFind.parent.size)
    (vars : Nat → Expr)
    (h_lhs : v (root g.unionFind lhsId) = rule.eval (rule.lhsExpr vars) env)
    (h_rhs : v (root g.unionFind rhsId) = rule.eval (rule.rhsExpr vars) env) :
    ConsistentValuation (g.merge lhsId rhsId) env v :=
  merge_consistent g lhsId rhsId env v hv hwf h1 h2
    (by rw [h_lhs, h_rhs, rule.soundness env vars])

这个定理有十一个参数。不要被其规模吓倒——它们在逻辑上分解为四组。设置（四个参数）：一个 e-graph，一个重写规则，以及两个类 ID。语义（两个参数）：一个环境和一个将值分配给 e-类的赋值。前置条件（五个参数）：赋值是一致的，union-find 结构良好，两个 ID 都有效，并且规则的 LHS 和 RHS 与赋值匹配。以及结论：合并两个类后，赋值仍然一致。

整个证明是一个函数调用——merge_consistent——带有一个“粘合”参数：by $rw [h\_lhs, h\_rhs, rule.soundness \text{ env vars}]$，它表示“使用两个匹配的 hypotheses 进行重写，然后应用规则自身的健全性保证来证明两边相等。”

大定理不一定难以证明——它们难以表述。 十一个参数精确地捕捉了每一个前置条件。证明本身是函数组合：委托给一个现有引理并提供连接参数。这就是 soundness sandwich (健全性三明治) 模式：精确地陈述前置条件，组合现有保证，让类型完成工作。

自动驾驶的代数：几何级数

来自 AMO-Lean 的单位根：

theorem geom_sum_finset (r : F) (n : ℕ) :
    (1 - r) * (Finset.range n).sum (fun i => r ^ i) = 1 - r ^ n := by
  induction n with
  | zero => simp
  | succ n ih =>
    rw [Finset.sum_range_succ, mul_add, ih]
    ring

该语句是几何级数的封闭形式：$(1 - r) * (1 + r + r^2 + \dots + r^{n-1}) = 1 - r^n$。基例是微不足道的——当 $n = 0$ 时，两边都为零，simp 处理它。inductive step 是三次重写，然后是 ring。Finset.sum_range_succ 分离出最后一项。mul_add 分配乘法。$ih$ 替换 inductive hypothesis。然后 ring——计算机代数系统 tactic——完成剩余的多项式恒等式。

这里人类的工作是建立结构：选择归纳法，应用正确的重写来揭示代数形式。机器的工作是验证代数。这种分工是优秀的 Lean 证明的典型特征：人类提供策略；tactics 提供计算。

高级模式

除了基本词汇之外，一些结构模式在实际代码库中反复出现。

The roundtrip pattern (往返模式) 证明两个操作是互逆的——$deserialize(serialize(x)) = x$ 的形式化版本。来自 AMO-Lean：

theorem interleave_evens_odds (l : List α) :
    interleave (evens l) (odds l) = l := by
  induction l using evens.induct with
  | case1 => simp [evens, odds, interleave]
  | case2 x => simp [evens, odds, interleave]
  | case3 x y xs ih =>
    simp only [evens, odds, interleave]
    rw [ih]

将列表拆分为偶数索引和奇数索引的元素，然后将它们交错回去，你就会得到原始列表。

The fuel pattern (Gas模式) 处理可能不会终止的递归函数。你添加一个 $fuel : \text{Nat}$ 参数，它在每次递归调用时递减，而不是直接证明终止。如果Gas耗尽，函数返回 none。然后，正确性定理会说“如果函数返回 some result（意味着它在Gas预算内完成），那么 result 是正确的。”来自 OptiSat：

theorem extractF_correct (g : EGraph Op) ... :
    ∀ (fuel : Nat) (classId : EClassId) (expr : Expr),
      extractF g classId fuel = some expr →
      EvalExpr.evalExpr expr env = v (root g.unionFind classId) := by
  intro fuel
  induction fuel with
  | zero => intro classId expr h; simp [extractF] at h
  | succ n ih => ...

这是一种务实的工程方法：你避免了最困难的部分——复杂递归函数的终止证明——同时仍然获得了有用的正确性保证。许多现实世界中经过验证的系统都使用这种模式。理想情况下，人们会避免这种技巧，但如果终止证明因其他原因而难以证明，它就可以提供一种方法。

The case split + embedded lemma pattern (案例分割 + 嵌入引理模式) 将 cases、have 和 omega 结合起来处理局部子问题。来自 AMO-Lean：

theorem evens_length_pow2 (l : List α) (k : Nat) (hk : k ≥ 1)
    (hl : l.length = 2^k) :
    (evens l).length = 2^(k-1) := by
  rw [evens_length, hl]
  have h2k : 2^k = 2 * 2^(k-1) := by
    cases k with
    | zero => omega
    | succ n => simp [Nat.pow_succ, Nat.mul_comm]
  omega

$have \ h2k$ 引入了一个局部引理——一个当场证明并立即使用的事实，就像一个局部辅助函数。$h2k : 2^k = 2 * 2^{k-1}$ 是通过对 $k$ 进行 cases 证明的。| zero => omega 情况很有趣：$k = 0$ 与 $hk : k \ge 1$ 矛盾，所以 omega 检测到矛盾并关闭目标。用编程术语来说，这个分支是不可达的，编译器证明了这一点。不要试图一蹴而就。使用 have 来证明中间事实，清晰地命名它们，并进行组合。

编译 Lean 文件时会发生什么

理解 lake build 实际做了什么，可以阐明 Lean 证明为何具有如此重要的分量。

首先是 elaboration (精化)：Lean 的前端将你的高级代码——tactics、implicit arguments、coercions——转换为低级的 proof term (证明项)，一个纯粹的 lambda 演算表达式。

其次是 kernel type-checking (内核类型检查)：kernel，一个独立的最小程序，独立验证证明项是否具有声明的类型。kernel 不信任 tactics、simp 引理数据库或任何自动化工具。它只信任基本的类型理论规则。如果 simp 有一个 bug 导致生成了无效的证明项，kernel 会拒绝它。

第三是 compilation to native code (编译为本地代码)：对于 def 和 #eval，Lean 通过 C 中间层编译为本地机器代码。定理被擦除——它们没有运行时开销。它们只在编译时存在，作为类型检查义务。

重要的一点是，前两个阶段是独立的。第一阶段的 tactics 仅仅是生成证明项的程序。它们可能有 bug。但第二阶段的 kernel 会捕捉任何无效的输出。kernel 保证三件事：logical consistency (逻辑一致性)（定理遵循公理）、well-typedness (类型良好性)（没有类型错误）和 universality (普遍性)（定理对所有满足 hypotheses 的值都成立，而不仅仅是经过测试的示例）。

kernel 不 保证什么同样重要：它不检查定理是否有用、hypotheses 是否可满足、或者定义是否捕捉了预期的语义。你可以形式化地证明你的排序函数返回一个相同长度的列表——但该规范并未说明输出是否已排序。Lean 验证的是你所陈述的，而不是你所意图的。这个空白是人类判断力仍然不可替代的地方。

阅读陌生证明的方法

当你遇到以前从未见过的 Lean 证明时，不要急于从头到尾阅读。从陈述开始，而不是证明。陈述告诉你什么是真实的；证明告诉你为什么。首先阅读什么。

识别花括号中的 implicit 参数——它们设定了数学上下文。识别 explicit hypotheses——这些是前置条件。识别最终冒号后面的结论——这是保证。将陈述翻译成通俗的语言，问自己：“这合理吗？这有趣吗？”

接下来，快速浏览第一个 tactic，以对证明策略进行分类。如果它以 rfl 开头，则定理通过定义为真。如果它以 simp 或 omega 开头，则证明是自动化的——机器处理它。intro 表示 assume-and-show (假设并显示) 参数。induction 意味着递归参数。cases 意味着案例分析。constructor 意味着逐块构建目标。apply 意味着委托给另一个定理。大多数证明都清晰地属于这些类别之一。

然后，如果你关心为什么，通过每个 tactic 跟踪证明状态。存在哪些目标？发生了什么变化？为什么这一步使我们更接近？大多数证明都有一个创造性的见解——“困难的步骤”——其余的都是琐碎的。寻找哪个 rw 或 have 引入了关键方程，哪个 apply 调用了不明显的引理，或者 inductive hypothesis 在哪里被使用。一旦你找到困难的步骤，你就理解了证明。

阅读 Lean 证明是一种技能，就像阅读汇编代码或导航一个陌生的代码库一样。第一次会很慢。第十次，你开始看到模式。到第一百个定理，你阅读证明就像阅读代码一样流利。

回报是真实的，但在你亲身经历之前很难传达。就像 Rust 中的借用检查器需要一些时间来适应一样，学习信任 Lean 提供的东西并接受成本权衡需要一些初步的努力。

当 AMO-Lean 证明其 NTT 实现保留了代数属性，或者当 OptiSat 证明每个 e-graph 重写都保留了语义时，这些不是碰巧通过的测试。它们是经过最小信任 kernel 检查的永久的、普遍的保证。没有遗漏任何边缘情况。没有回归可以破坏它们。证明就是文档，而且它经过机器检查。

下次当你看到 Lean 定理时，试试这个：忽略证明，阅读陈述，然后问自己——“要测试这个需要什么？”答案通常是“无限多的测试。”这就是证明所取代的：无限测试，压缩成一个 kernel 可以验证的有限程序。

证明是程序，程序是证明。你整个职业生涯都在编写证明。现在你知道如何阅读它们了。

本文中所有代码示例均使用 Lean 4 编译，并取自 AMO-Lean 和 OptiSat，这两个是开源的形式化验证优化项目。

• 原文链接： blog.lambdaclass.com/the...
• 登链社区 AI 助手，为大家转译优秀英文文章，如有翻译不通的地方，还请包涵～