开发者用 Rust 从零构建迷你 Lean 4 交互式定理证明器

Lean 4、形式化验证、安全、云安全，从零构建一个迷你 Lean 4：用 Rust 实现一个交互式定理证明器。作者 Hideaki Takahashi，阅读时长 34 分钟，刚刚发布。

如今，人人都在谈论 Lean 4 和 Coq 这类交互式定理证明器。从形式化前沿数学到验证生产代码，社交媒体上的热度让人难以忽视。然而，大多数人仍然把这些工具当作黑箱，很少有人真正了解 Lean 4 在“证明”一个定理时底层发生了什么。

本文通过从零实现一个玩具级的 Lean 4 风格定理证明器来回答这个问题。逐步剖析核心机制，将让你对现代定理证明器实际在做什么、以及为什么我们可以信任它们，有更深入、更自信的理解。

用 Rust 编写的完整源代码可在 https://github.com/h5i-dev/MiniLean4 获取。

从本质上讲，定理证明器只有一项工作：判定一个证明是否有效。由于计算机无法直接验证用自然语言写成的证明，我们需要一座连接数学与代码的形式化桥梁。这座桥就是 Curry–Howard 对应，通常用一句简单的口号概括：命题即类型，证明即程序。

用编程的话来说，把一个数学命题想象成一个类型签名，把它的证明想象成一个满足该签名的程序（或值）。如果我们能写出一个类型为 A 的良类型表达式 t（记作 t : A），那么命题 A 就被证明为真。如果无法构造出这样的程序，该命题就无法被证明。

考虑逻辑蕴含：A → B（A 蕴含 B）。要在数学上证明 A → B，我们假设 A 为真，并用它推导出 B。在编程中，这不过是一个接受类型 A 的参数并返回类型 B 的结果的函数。如果你能实现这个函数，你就证明了该蕴含。

同样的思想自然延伸到全称量化（“对所有 x……”）。假设我们想证明“对类型 A 中的每个 x，性质 B(x) 成立”。和蕴含一样，我们通过编写一个函数来证明它，该函数接受任意输入 x : A 并返回 B(x) 的一个证明。

注意这里的妙处：返回类型 B(x) 实际上会随输入 x 的值而变化。在标准编程语言中，返回类型不能依赖于运行时值，因此我们需要依赖函数类型（或称 Π 类型），写作：

例如，让我们表达“每个命题都蕴含自身”这个陈述。在 Lean 的类型论中，所有命题构成的宇宙写作 Sort 0（或 Prop）。使用依赖类型，我们可以将这个陈述写成：

为了证明它，我们编写一个函数，接受任意命题 P，并返回针对该特定 P 的自反证明：

这就引出了现代定理证明器背后的核心洞见：证明一个定理不过是编写一个类型正确的程序，而验证一个证明不过是对该程序做类型检查。Lean 风格的内核不需要“理解”数学真理，它只需要是一个类型检查器。

要构建我们的最小定理证明器，我们不需要一门庞大的编程语言。事实上，我们的整个核心演算只由五种项构成（稍后我们会再加一种）：

这里，u 是表示宇宙层级的自然数，x 是变量名。让我们逐一拆解每种构造的作用：

#[derive(Clone, Debug, PartialEq, Eq)]
pub enum Term {
    Sort(u64),
    Var(String),
    Pi(String, Box<Term>, Box<Term>),
    Lam(String, Box<Term>, Box<Term>),
    App(Box<Term>, Box<Term>),
}

一切皆项

注意，类型和表达式共享完全相同的语法。没有单独的语法来区分“类型”与“值”，或“证明”与“命题”。一个给定的项 A 是否真的是一个有效类型，由类型检查器动态判定。例如，我们前面那个定理（“每个命题都蕴含自身”）和它的证明，都是由完全相同的构件构造出来的：

结合性与柯里化

与 Haskell、Lean 和 OCaml 等函数式语言一样，函数应用向左结合，而箭头向右结合：

例如，𝜆(𝑎:𝐴). 𝜆(𝑏:𝐵). 𝑎 的类型是 𝐴 → 𝐵 → 𝐴，当应用于 𝑥 : 𝐴 和 𝑦 : 𝐵 时，写作 (𝜆(𝑎:𝐴). 𝜆(𝑏:𝐵). 𝑎) 𝑥 𝑦，即 ((𝜆(𝑎:𝐴). 𝜆(𝑏:𝐵). 𝑎) 𝑥) 𝑦。

现在我们有了语法，内核如何验证一个证明呢？它在上下文 Γ 下检查类型，Γ 是一个有序的假设列表：

它记录作用域中每个变量的类型，我们用 dom(Γ) 表示集合 {𝑥_1, . . . , 𝑥_𝑛}。由于下面的 C-Ext 规则禁止重名，Γ 可以像从名称到类型的字典一样使用，而 T-Var 不过是一次查找。然而，与普通字典不同，顺序很重要：𝐴_𝑖 可能提及 𝑥_1, . . . , 𝑥_𝑖−1，例如 𝑃 : Sort 0, ℎ : 𝑃。我们使用两个判断：

这里，B[x -> a] 表示将 B 中的 x 替换为 a，而 𝐴 ≡ B 表示项 A 与 B 等价（我们稍后会解释等价性的定义）。

要看出这些类型规则与形式逻辑的对应有多直接，可以考虑二阶命题逻辑，其中公式由命题变量 P, 𝑄, . . . 、蕴含 (𝜑 → 𝜓) 以及对命题的全称量化 (∀𝑃 . 𝜑) 构成。

如果我们把每个逻辑公式 𝜑 翻译成对应的类型 𝜑*，将 𝜑 → 𝜓 映射为 𝜑* → 𝜓*，将 ∀𝑃 . 𝜑 映射为 Π(P : Sort 0). 𝜑*，那么自然演绎的标准规则与我们内核的类型规则逐行对应（为便于阅读，省略了良构性前提）：

仔细观察上面两列：如果你把右侧的程序项（h、𝜆、t、f、a）擦除，你就得到了左侧的逻辑演绎规则！逻辑证明的每一步都对应着在我们的编程语言中构造一个语法树节点。

乍一看，把这些规则变成一个类型检查函数似乎几乎微不足道。然而，上面的规则中隐藏着一些微妙的细节：

（原文较长，此处译出前 6000 字，完整内容请点「打开原文」。）