如果它能编译，那它就是正确的（几乎）：Lean 4 在 ZK 系统和工程中的介绍

lambdaclass
发布于 19小时前
阅读 39

本文介绍了使用 Lean 4 进行形式化验证的方法，特别是在零知识证明系统中的应用。文章阐述了 Lean 4 的理论基础，包括 Curry-Howard 同构，并通过一个实际案例——验证加法约束——展示了如何利用 Lean 4 保证代码的正确性。文章还介绍了 Lean 4 的代码提取功能，可以将经过验证的 Lean 代码编译成高效的 C 代码。

## 介绍

在 LambdaClass，我们一直在探索 Lean 4，将其作为零知识证明系统中形式化验证的工具，并用于形式化 [Concrete 的内核](https://federicocarrone.com/series/concrete/the-concrete-programming-language-systems-programming-for-formal-reasoning/)。随着 ZK 生态系统的日趋成熟，正确性的重要性也日益提高：zkVM 或证明系统中的一个错误可能会危及价值数十亿美元的资产安全。我们已经多次看到这种情况发生——细微的算术错误、约束系统中的差一错误，以及规避了数千个测试向量的边缘情况。审计会有所帮助，但审计是人为的；它们会遗漏东西。测试告诉你什么**没有**失败；证明告诉你什么**不能**失败。

这项工作是 LambdaClass 将形式化方法引入生产系统的一项更广泛努力的一部分。我们还在开发 Concrete，这是一种系统编程语言，其内核正在 Lean 4 中进行形式化——从一开始就经过精心设计，因此每个设计选择都必须回答这个问题：机器可以对此进行推理吗？我们应用于 Concrete 类型系统的严谨性，同样适用于我们思考 ZK 基础设施的方式：正确性应该被证明，而不是被期望。

为什么要进行形式化验证，又为什么是现在？定理证明器已经存在几十年了，像 Coq 和 Isabelle 这样的系统产生了具有里程碑意义的成果——CompCert、seL4 以及基础数学的形式化。但是，证明定理和发布生产代码之间的差距仍然很大。Lean 4 显着缩小了这一差距：它既是证明助手，又是可以编译为高效 C 代码的现代编程语言。你可以在同一个系统中编写你的规范，证明其正确性，并提取可部署的代码。

时机已经成熟：[Lean 4](https://lean-lang.org/) 在 2023 年实现了其稳定版本，并且 [Mathlib](https://leanprover-community.github.io/mathlib4_docs/)（最大的形式化数学库之一）在 2024 年完成了向 Lean 4 的移植。[以太坊基金会资助了多项计划](https://blog.ethereum.org/2024/04/01/zk-grants-round)来形式化验证 zkVM，他们认识到这些系统的复杂性需要机器检查的证明，而不仅仅是测试和审计。

本文是我们尝试与好奇者和新手分享我们所学到的知识。我们将介绍使 Lean 4 强大的理论基础（Curry-Howard 同构），展示为什么这对编写正确的软件很重要，并以一个实际示例作为结尾：形式化验证 ZK 系统中常见的加法约束。

## Lean 4：从集合到类型

那么，Lean 4 是什么？就像一颗多面体的宝石，答案取决于你如何看待（和持有）它。 Lean 4 可以同时被描述为两件事：第一种是函数式、表达能力强的编程语言，它能够高效编译，并且可以作为第一个近似值进行探索。当然，这当然是正确的，但是我们对 Lean 感兴趣的真正原因是它还有更多。 Lean 也是一种交互式定理证明器，该系统允许对数学推理的正确性进行形式化验证。

Lean 的核心是将两个理论领域融合在一起：**类型论** 和 **Lambda 演算**。

一些具有计算机科学背景的人可能已经熟悉这些术语，但简而言之，对于一般受众，我们可以将类型论表征为提供该语言的类型系统：与集合论（其中对象可以是异质的混合物，如果不加以注意，则容易出现悖论）不同，类型论为数学提供了一个更强大和“类型化”的基础。

更具体地说，朴素集合论中存在一些模糊性，将集合定义为“对象的集合”——而且，对其成员的性质没有任何限制：例如，集合 A 可能包含一个实数、一个三角形以及美国总统姓氏的完整列表。 Lean 4 采用类型论，并将类型的概念作为中心，从而防止了常规集合的行为。这种严格性远非表达上的限制，而是变得非常重要，并且是伟大功能的来源。

> Lean 中的核心概念是 **类型判断**，通常表示为
>
> `t : T`，表示“术语 `t` 的类型是 `T`”。

此外，Lambda 演算提供了关于计算和函数式编程的理论（例如，考虑 Haskell）。通常，作为一种

编程语言，它的行为和提供了任何程序员每天使用的一组常用工具；仅需快速提及一些表面特性，常量通过指定其名称，类型和值来定义。例如

> `def name : Type := term`

Lean 允许类型推断，表达式求值（`#eval`）和类型检查（`#check`）。此外，为了构建复杂的结构，Lean 使用 **构造器**，这些构造器在 C++ 等语言中具有直接的对应关系，例如 `Prod A B` 表示笛卡尔积 $A \times B$：

> `(5, true)` 是类型 `Prod Int Bool` 的一个术语。

等等。目前，有几个在线资源可以检查 Lean 4 的语法和典型语法——鼓励读者在继续阅读时查找这些参考资料进行练习。

## 函数是一等公民

关于 Lean 中的 **函数** 有一些有趣的内容值得一提。 虽然在大多数语言（Python，C++）中，函数是对 CPU 指令序列的抽象，但在 Lean 4（和依赖类型理论）中，**函数是一等公民**。 例如，如果你有一个函数 $f$ 接受一个整数并返回一个布尔值，则其 **类型** 为 $Z \rightarrow Bool$，这在 Lean 的术语中很简单

$f: Z \rightarrow Bool$

将函数视为一等对象有很多优点：

1. **统一性：** 一切都是一种类型的术语。 `5` 的类型是 `Nat`。 `sum` 的类型是 `Nat -> Nat -> Nat`。 `Pythagorean_Theorem` 的类型是 `Prop`，这是一个有意义的，可以证明的语句。 编译器使用此机制来验证你的代码、逻辑和数学。

2. **柯里化（部分应用）：** 在 Lean 中，严格意义上不存在“多参数”函数。
   - 对两个数字求和的函数 `Int -> Int -> Int` 实际上是一个接受 **一个** 数字并**返回另一个等待第二个数字的函数**。

- 这允许通过“固定”参数来创建新函数，而无需额外的代码。

- 同样，这有助于可以机械地推理代码的机制。
3. **依赖类型（皇冠上的明珠）：**
   - 存在许多类型系统，其中一些比其他类型系统更正式，而另一些则比其他类型系统更强大。 在最具表现力的类型系统中，Lean 的类型系统所依据的系统是最强大的。

- 函数的返回类型可以 **依赖于**

输入参数的 **值**。

- **示例：** 函数 `zero_vector (n : Nat)` 返回大小为 `n` 的向量。 结果的 **类型** (`Vector F n`) 会根据 `n` 的值而变化。 这在标准的 Java 或 Rust 中是不可能的。

这种语言背后的真正潜力在于，它建立在一个

数学逻辑之间融合而产生的关键思想之上

和计算理论：**Curry-Howard 同构定理。**

在研究组合逻辑时（1930 年至 1950 年间），Haskell Curry 观察到一种特殊的模式：计算中最基本函数 (**组合子**) 的类型与蕴涵逻辑 (即经典的“如果 A 则 B”) 的公理具有完全相同的代数结构。 他直觉到计算和逻辑演绎是同一枚Coin的两面。

后来，在 1960 年代，William Howard 将这种直觉形式化，证明了 **简化逻辑证明** 过程（自然演绎中的切消除）与 **执行程序** 过程（lambda 演算中的 beta 归约）同构。

**Curry-Howard 定理（或同构）** 确立了逻辑系统和计算系统在结构上是相同的。 这允许将数学证明不视为静态文本，而是视为可执行的算法。

> **命题即类型：** 数学语句 `P` 是一种类型。
>
> **证明即程序：** `P` 的证明只是类型 `P` 的一个术语（程序）。

如果程序编译（类型检查），则证明有效。

## Curry-Howard 同构及其带来的后果

Curry-Howard 同构的应用在命题逻辑和类型论之间架起了一座桥梁。 作为参考，一个简短的概念表如下所示

| **命题逻辑** | **类型论 (Lean)** | **概念** |
| --- | --- | --- |
| 命题 ($P$) | `P : Prop` | 逻辑宇宙中的一种类型。 |
| 证明 ($h$) | `h : P` | 类型 `P` 的一个术语。 |
| 蕴涵 ($P \rightarrow Q$) | `P -> Q` | **函数**：接受 `P` 的证明，返回 `Q` 的证明。 |
| 合取 ($P \land Q$) | `P`×` Q` (Prod) | **乘积**：一对包含 `P` 的证明和 `Q` 的证明。 |
| 析取 ($P \lor Q$) | `P`⊕` Q` (Sum) | **和**：`P` 的证明 **或** `Q` 的证明。 |
| 真 ($\top$) | `Unit` / `True` | **单元**：具有单个值 `()` 的类型。 平凡。 |
| 假 ($\bot$) | `Empty` / `False` | **空**：没有值的类型。 不可能构造。 |
| 否定 ($\lnot P$) | `P -> False` | 从 `P` 导出矛盾的函数。 |

起初这令人震惊，但 Lean 的一大特点是它允许 **更大程度的** 等价：我们可以从“静态”逻辑转移到动态逻辑（即谓词逻辑）。 这是学习 Lean 时最强大的概念转换，它是通过利用 **谓词可以建模为函数的** 这一事实来实现的！

在谓词逻辑中，像 "`x` 是偶数" 这样的语句，在我们知道 `x` 的值之前既不是真也不是假。 在 Lean 中，这被建模为一个 **接受数据并返回命题** 的函数。 当标准数学说 “`P(x)` 是集合 `A` 上的一个谓词” 时，Lean 编写一个接受 A 类型的输入并返回一个逻辑命题 Prop 的函数："`P : A -> Prop`”。

## 一个简单的例子

此示例使用取模运算定义了“可被 2 整除”的属性。

```
-- 谓词定义
-- --------------------

/-
  我们定义一个名为 `is_divisible_by_two` 的函数。

语法分解：
  1. `def`: 用于定义数据或函数的关键字。
  2. `(n : Nat)`: 输入参数。 我们期望一个自然数。
  3. `: Prop`: 返回类型。
     它不返回 `true` 或 `false` (计算),
     它返回一个逻辑语句。
  4. `:=`: 将签名与实现分开。
  5. `n % 2 = 0`: 主体。 这是一个断言余数为零的等式。
-/
def is_divisible_by_two (n : Nat) : Prop :=
  n % 2 = 0

-- 谓词的用法
-- ----------------------

-- 这里我们用数字 4 来评估谓词。
-- Lean 将其简化为命题 "0 = 0"。
#check is_divisible_by_two 4
-- 控制台结果: is_divisible_by_two 4 : Prop

-- 这里我们用 5 来评估。
-- Lean 将其简化为命题 "1 = 0"。
-- 注意: 该命题在语法上是有效的 (类型为 Prop),
-- 即使它在数学意义上是错误的。
#check is_divisible_by_two 5
```

请注意，`Nat -> Prop` 的意思是：“给我一个自然数，我将返回一个关于该数字的逻辑问题。”

此外，还有 **有效性和真值** 之间的区别：定义谓词并不说明对于给定的数字它是真还是假。 它仅定义 **该语句的含义**。 `is_divisible_by_two 5` 是 `Prop` 类型的有效对象； 这只是一个我们无法构造证明的对象。

## 全称量词

证明 “对于所有 `x`，`P(x)` 为真” 意味着什么？ 这意味着如果你给我 **任何** 具体的值 `x`，我都可以返回 `P(x)` 的证明。 但这**正好** 是一个函数！

现在让我们陈述并证明一些涉及全称量词的内容； 将使用谓词 `P(x) : x < x + 1`。 在 Lean 中，“for all" ($\forall$) 的行为类似于一个接受来自域的 **任何** 值的函数。 在这里，我们将使用 `theorem` 而不是 `def`，因为我们的目的是证明一个真理，而不仅仅是定义一个结构。

## 第二个例子

```
import Mathlib.Data.Nat.Basic -- 导入基本的自然数属性

-- 全称定理的定义和证明
-- -------------------------------------------

/-
  定理：对于每个自然数 x，x 严格小于 x + 1。

语法分解：
  1. `theorem`: 表示我们正在创建一个命题的项(一个证明)。
  2. `x_less_than_succ`: 我们给定理起的名字.
  3. `: forall (x : Nat), x < x + 1`: 我们想要证明的命题.
     读作:“对于任何 Nat 类型的 x，x < x + 1 成立”。
  4. `:=`: 证明开始的地方.
-/
theorem x_less_than_succ : forall (x : Nat), x < x + 1 := by
  -- 我们使用关键字 `by` 进入“战术模式”。
  -- 这允许我们逐步地构造证明(函数)。

-- 步骤 1: 引入 (intro)
  -- 目的是要证明 "对于所有 x" 都是真的。
  -- `intro` 策略接受泛型 `x` 并将其放入我们的上下文中。
  -- 这相当于在纸上说:“设 x 为任意自然数……”
  intro x

-- 当前状态 (信息视图):
  -- x : Nat  (我们有一个任意的 x)
  -- |- x < x + 1 (我们的目标是证明对于那个特定的 x这是成立的)

-- 步骤2: 应用公理 (exact / apply)
  -- 我们在 Lean 库中搜索一个确切说明这一点的定理。
  -- 有一个名为 `Nat.lt_succ_self` 的定理，它证明了 `forall n, n < succ n`。
  -- 我们将我们的 `x` 传递给那个函数。
  exact Nat.lt_succ_self x
```

我们可以强调 `intro x`：是从逻辑到编程的直接翻译。 要构造一个适用于 **所有** 输入的函数，我们首先声明一个表示该输入的变量。

## 构造性

然而，谓词逻辑的这种扩展并不是对通常的 **日常** 谓词逻辑的复制。 这里有一个重要的（哲学意义上和重要意义上的）区别：默认情况下，Lean 是构造性的。 这是什么意思？

在构造性的 Lean 中证明像 “$\exists x, P(x)$” 这样的东西需要 **计算** `x` 并将其呈现出来。 证明“不可能不存在”是不够的。 另外，排中律：$P \lor \lnot P$ **不是** Lean 的构造性逻辑中的公理。

LEＭ不是公理这一事实不应被视为令人震惊。 毕竟，代码仍然受到计算机科学边界的约束：在计算中，我们并不总是知道程序是否终止（停机问题），因此我们不能**普遍地**断言 $P \lor \lnot P$。 为了平息一些情绪，如果数学家需要，Lean 允许调用经典逻辑 (`open Classical`)，接受非构造性的公理，但会失去证明的直接“可计算性”。

## 这一切为什么重要？

从程序员的角度来看，从一开始，肯定会有一个问题萦绕在“数学与编程有什么关系？”这个问题附近"。

**让我们首先说明，除了理论之外，Lean 4 解决了复杂系统开发中的地方性问题。** 在像 Rust 或 C++ 这样的工业语言中，编译器可以防止内存管理错误（段错误，数据竞争）。 但是，它对程序的数学“真值”视而不见。 **Lean 提高了标准：它将逻辑错误转换为编译错误。**

例如，想象一个典型的菜鸟（以及不太菜鸟的）错误："环绕错误"（即索引越界）的情况。 想象一下实现 STARK 执行轨迹上的约束。

- **在 Rust 中：** 工程师编写一个循环 `for i in 0..N`，检查 `trace[i+1] == trace[i] + 1`。 在最后一次迭代中，`i+1` 溢出或访问了无效的内存。 Rust 可能会在运行时抛出一个 _panic_，或者更糟糕的是，读取垃圾并接受一个错误的证明。

- **在 Lean 中：** 我们使用像 `Fin n` 这样的依赖类型（严格小于 `n` 的数字）。
  - 如果你试图访问 `trace[i+1]`，但没有首先证明 `i < n-1`，Lean **将无法编译**。

- 编译器会抛出一个类型错误：_"你还没有证明 `i+1` 是一个有效的索引。"_

- 这迫使工程师在设计期间（而不是在调试期间）正确处理约束。

因此，采用 Lean 引入了一个分层的开发架构，将编译错误和执行错误明显区分开来，并提供了 **改进的工作流程。** Lean 的作用是保证 _规范_ 在编写任何一行底层代码之前是正确且一致的。

## 认证的代码提取

Lean 4 不仅仅是一个验证器； 它是一种能够编译为 C 的高效编程语言。 这使得能够进行所谓的 **认证代码提取**：这是 Lean 采用你的数学定义（函数，结构）并将 **它们编译为高效的 C 代码**，从而消除了所有执行不必要的“逻辑开销”（证明）的过程。

由于在 Lean 中编写规范，然后手动在 C 中重写它会引入人为错误的风险，因此你可以在 Lean 中编写关键函数（如 Merkle 路径验证或多项式求值），正式证明其正确性，**然后要求 Lean 自动生成相应的代码。** 结果，你可以获得一个以 C 的速度运行的二进制文件，但具有数学保证，即它是 Lean 中验证的逻辑的忠实表示。 可以说，此功能使 Lean 4 成为行业的“游戏规则改变者”，将其与 Coq 或 Isabelle 等学术前辈区分开来。

为了理解这是如何工作的，我们来看一下 Lean 在编译时做出的一个基本区分：**数据 (`Type`)：** 数字、列表、向量、矩阵等 _是运行程序所必需的_，而 **证明 (`Prop`)：** 定理、引理、类型保证（例如，`i < n`）等*仅对说服编译器是必要的_，但在运行时无用。

但是，我们如何理解“编译的数学证明”呢？ 好吧，这是一个深刻的问题。 下面我们简要列出由 **代码提取** 产生的二进制文件的实际效用，并按这两个不同的观点进行分离。

从软件开发人员的角度来看，生成的二进制文件（例如，

`libfri_verifier.so` 或 `fri_verifier.exe`) 是一个 **生产工件**。 这对于

1. **部署：** 这个二进制文件就是你上传到服务器，

区块链节点或物联网设备的文件。 你可以用新的文件替换你的旧的

`verifier.rs` 库（手动编写且可能存在错误）。 这样做的好处是，你现在拥有一个以本机速度（C/C++）运行的可执行文件，但**永远**不会受到缓冲区的影响

溢出或接受错误的证明。

2. **集成：** 提取的Lean 代码通常会公开一个 C API；

你使用 **FFI (外部函数接口)** 来调用

Lean 二进制文件中的函数。 举个例子，可以想到 “我的 Web 服务器

(Rust) 处理 JSON 和网络，但当关键时刻

需要验证加密证明时，它会将字节传递给

Lean 二进制文件。” 你将关键安全性委托给已验证的

组件，并以速度为代价。 如果用 C 编写，你将以安全性为代价。 你在需要原始速度时使用 Lean 二进制文件

(C)，但又无法承受任何内存或逻辑错误。

然后将二进制文件解释为 **加固的静态/动态库**。 它可以用于执行生产中的关键业务逻辑，而无需担心崩溃或被利用。

从数学家的角度来看，生成的二进制文件是“见证计算器”：存在性定理的 **计算实现**。 例如，此二进制文件的用途通常是

1. **“物化”存在：** 你证明了定理：

$\forall x, \exists y, P(x,y)$（“对于每个输入 `x`，存在一个解 `y`”）。 虽然该定理是抽象的，但二进制文件是具体的。 数学家使用该二进制文件来 **查找** 现实世界中的 `y`——比方说，你将数字

$x = 2^{64} + 13$ 提供给该二进制文件。 该二进制文件执行证明中隐含的算法，并输出数字 $y = 1948...$。 你已将抽象真理转换为具体数据。

2. **进行认证计算：** 有时你想要计算一些困难的东西（例如，第 `n` 个素数或 ZK 执行轨迹）。 现在，该二进制文件充当“真理黑匣子”：如果你使用 Python 脚本并获得结果，你可能会怀疑你是否正确实现了该算法。 通过使用 Lean 二进制文件，你可以获得数学保证，即屏幕上的数字 **是** 根据公理定义正确的那个。 没有逻辑错误的余地。

从数学的角度来看，二进制文件是你的证明的 **可执行实例**。 它可以计算满足你的定理的具体值（见证），从而将数学对象从思想世界带到硬盘驱动器上。

> 这是同一个文件，但有人将其视为 **理论的确认**，
>
> 另一些人则将其视为 **生产工具**。

## 性能

Lean 4 使用了一种名为 [Perceus](https://www.microsoft.com/en-us/research/publication/perceus-garbage-free-reference-counting-with-reuse/) 的引用计数策略，该策略具有激进的重用和唯一性优化。 当编译器检测到某个数据结构是唯一拥有的（引用计数为 1）并且你将要创建一个类似的结构时，Lean 可以就地重用内存，而不是分配新内存并进行复制。

这使得纯粹的函数式代码在许多情况下可以与命令式实现相媲美——Merkle 树或多项式操作的函数式算法可以实现比你从高级函数式语言中所期望的更接近手写 C++ 的性能。

## 实用示例：验证加法约束

让我们通过一个与 ZK 系统直接相关的示例将理论付诸实践。 在 STARK 和其他证明系统中，我们通常需要验证对 32 位整数执行的算术运算是否正确。 由于我们使用字段元素（如素数为 $p = 2^{31} - 2^{27} + 1$ 的 BabyBear 字段），因此我们将 32 位整数分解为较小的“肢体”，并使用进位位来跟踪溢出。

## 设置

考虑将两个 32 位整数 `lhs` 和 `rhs` 相加得到 `res`。 每个整数都分解为两个 16 位肢体：

$lhs = lhs0 + lhs1 \cdot 2^{16}$

$rhs = rhs0 + rhs1 \cdot 2^{16}$

$res = res0 + res1 \cdot 2^{16}$

ZK 电路强制执行的约束方程为：

$lhs0 + rhs0 = res0 + carry0 \cdot 2^{16}$

$lhs1 + rhs1 + carry0 = res1 + carry1 \cdot 2^{16}$

其中 $carry0$ 和 $carry1$ 是位（0 或 1）。

**我们要证明的定理：** 如果满足这些约束并且进位是位，则 $res \equiv lhs + rhs \pmod{2^{32}}$。
**重要提示：** 该定理确定了在约束方程成立时的模算术恒等式。 在实际的 ZK 电路中，你还需要单独的范围约束，以确保每个肢体都在 \[0,2^{16})\[0,2^{16}) 中。 这些范围检查通常由电路中的查找参数或分解约束强制执行——我们在此处证明代数关系。

## Lean 4 证明

```
import Mathlib.Data.ZMod.Basic
import Mathlib.Tactic
-- 定义常量以提高可读性
def LIMB_BASE : Nat := 65536      -- 2^16
def MOD_32 : Nat := 4294967296    -- 2^32
/-
  定理：加法约束的正确性
  如果肢体约束方程成立并且进位是位，
  那么 res ≡ lhs + rhs (mod 2^32)。
  注意：这证明了代数恒等式。 范围约束
  （确保肢体 < 2^16）在电路中单独处理。
-/
theorem add_constraint_mod32
  (lhs0 lhs1 rhs0 rhs1 res0 res1 carry0 carry1 : Nat)
  -- 肢体约束方程
  (h_low : lhs0 + rhs0 = res0 + carry0 * LIMB_BASE)
  (h_high : lhs1 + rhs1 + carry0 = res1 + carry1 * LIMB_BASE)
  -- 进位约束
  (h_c0_bit : carry0 ≤ 1)
  (h_c1_bit : carry1 ≤ 1)
  : (res0 + res1 * LIMB_BASE) % MOD_32 =
    (lhs0 + lhs1 * LIMB_BASE + rhs0 + rhs1 * LIMB_BASE) % MOD_32 := by
  -- 展开常量，以便全称量词可以使用具体数字
  unfold LIMB_BASE MOD_32
  unfold LIMB_BASE at h_low h_high
  -- 我们从约束中推导出：
  --   res + carry1 * 2^32 = lhs + rhs
  -- 全称量词策略自动处理线性算术
  omega
```

## 理解证明

让我们分解一下正在发生的事情：

1. **展开定义** 我们将 `LIMB_BASE` 和 `MOD_32` 展开为它们的

具体值（65536 和 4294967296），以便 `omega` 策略可以

推理它们。

2. **代数运算：** 我们将高位肢体方程乘以

$2^{16}$ 并将其与低位肢体方程组合。 这为我们提供了

完整的 32 位值之间的关系。

3. **核心恒等式：** 关键的见解是，在结合

约束之后：

res+carry1⋅232=lhs+rhsres+carry1⋅232=lhs+rhs

4. **模约简：** 由于 carry\_1⋅232≡0(mod232)carry\_1⋅232≡0(mod232)，

我们得到 res≡lhs+rhs(mod232)res≡lhs+rhs(mod232)。

`omega` 策略自动处理线性算术，使证明非常简洁，同时保持严谨性。

## 具体例子

我们还可以验证具体案例：

```
-- 验证 100 + 200 = 300（没有进位）
example : (300 + 0 * 65536) % 4294967296 =
          (100 + 0 * 65536 + 200 + 0 * 65536) % 4294967296 := by
  native_decide
-- 验证 65535 + 1 = 65536（从低位肢体进位）
-- 65536 = 0 + 1 * 65536
example : (0 + 1 * 65536) % 4294967296 =
          (65535 + 0 * 65536 + 1 + 0 * 65536) % 4294967296 := by
  native_decide
-- 验证 2^32 - 1 + 1 ≡ 0 (mod 2^32)（完全溢出）
example : (0 + 0 * 65536) % 4294967296 =
          (65535 + 65535 * 65536 + 1 + 0 * 65536) % 4294967296 := by
  native_decide
```

这正是 zkVM 中出现的约束验证类型。 通过在 Lean 4 中证明它，我们可以获得机器检查的保证，即我们的约束逻辑是正确的——不仅适用于测试用例，而且适用于所有可能的输入。

## 结论

我们在本文中介绍了很多内容：

- **Curry-Howard 同构** 揭示了证明和程序在

根本上是同一件事。 类型是命题，而术语

（程序）是证明。

- **类型安全即逻辑安全：** Lean 的类型系统不仅可以捕获

运行时错误，还可以捕获逻辑错误。 如果你的代码编译，你的证明

有效。

- **认证代码提取：** Lean 4 不仅仅是一个定理证明器——它可以

编译为高效的 C 代码，让你可以在生产环境中部署经过形式化验证的

软件。

- **实用的 ZK 验证：** 我们演示了 Lean 4 如何验证

零知识中使用的算术约束的正确性

证明系统。

在 LambdaClass，我们将形式化验证视为 ZK 生态系统的重要工具。 随着证明系统变得越来越复杂，“代码有效”和“可证明正确的代码”之间的差距变得越来越重要。 Lean 4 帮助我们弥合了这一差距。

## Lean 4 入门

如果你想尝试本文中的示例：

1. **安装 elan**（Lean 的工具链管理器）：

```bash
curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh
```

2. **使用 [lean4 扩展](https://marketplace.visualstudio.com/items?itemName=leanprover.lean4&ref=blog.lambdaclass.com) 设置 VS Code**

用于交互式证明，并获得实时反馈。

3. **使用 Mathlib 创建项目：**

```bash
lake new my_project math
cd my_project
lake update && lake build
```

4. **将你的证明** 写入 `.lean` 文件中。 VS Code 扩展在你编写时显示

目标状态，并且 `lake build` 验证所有内容是否已编译。

## 学习更多内容的资源

- [Lean 4 手册](https://lean-lang.org/lean4/doc/) — 官方文档
- [Mathematics in Lean](https://leanprover-community.github.io/mathematics_in_lean/) — 数学形式化的教程
- [Mathlib 文档](https://leanprover-community.github.io/mathlib4_docs/) — 综合的数学库
- [Functional Programming in Lean](https://lean-lang.org/functional_programming_in_lean/) — 从编程的角度来看
- [Theorem Proving in Lean 4](https://lean-lang.org/theorem_proving_in_lean4/) — 深入了解证明策略

>- 原文链接： [blog.lambdaclass.com/if-...](https://blog.lambdaclass.com/if-it-compiles-it-is-correct-almost-an-introduction-to-lean-4-for-zk-systems-and-engineering-2)
>- 登链社区 AI 助手，为大家转译优秀英文文章，如有翻译不通的地方，还请包涵～

介绍

在 LambdaClass，我们一直在探索 Lean 4，将其作为零知识证明系统中形式化验证的工具，并用于形式化 Concrete 的内核。随着 ZK 生态系统的日趋成熟，正确性的重要性也日益提高：zkVM 或证明系统中的一个错误可能会危及价值数十亿美元的资产安全。我们已经多次看到这种情况发生——细微的算术错误、约束系统中的差一错误，以及规避了数千个测试向量的边缘情况。审计会有所帮助，但审计是人为的；它们会遗漏东西。测试告诉你什么没有失败；证明告诉你什么不能失败。

时机已经成熟：Lean 4 在 2023 年实现了其稳定版本，并且 Mathlib（最大的形式化数学库之一）在 2024 年完成了向 Lean 4 的移植。以太坊基金会资助了多项计划来形式化验证 zkVM，他们认识到这些系统的复杂性需要机器检查的证明，而不仅仅是测试和审计。

Lean 4：从集合到类型

Lean 的核心是将两个理论领域融合在一起：类型论 和 Lambda 演算。

Lean 中的核心概念是 类型判断，通常表示为

t : T，表示“术语 t 的类型是 T”。

此外，Lambda 演算提供了关于计算和函数式编程的理论（例如，考虑 Haskell）。通常，作为一种

编程语言，它的行为和提供了任何程序员每天使用的一组常用工具；仅需快速提及一些表面特性，常量通过指定其名称，类型和值来定义。例如

def name : Type := term

Lean 允许类型推断，表达式求值（#eval）和类型检查（#check）。此外，为了构建复杂的结构，Lean 使用 构造器，这些构造器在 C++ 等语言中具有直接的对应关系，例如 Prod A B 表示笛卡尔积 $A \times B$：

(5, true) 是类型 Prod Int Bool 的一个术语。

等等。目前，有几个在线资源可以检查 Lean 4 的语法和典型语法——鼓励读者在继续阅读时查找这些参考资料进行练习。

函数是一等公民

关于 Lean 中的函数有一些有趣的内容值得一提。虽然在大多数语言（Python，C++）中，函数是对 CPU 指令序列的抽象，但在 Lean 4（和依赖类型理论）中，函数是一等公民。例如，如果你有一个函数 $f$ 接受一个整数并返回一个布尔值，则其类型为 $Z \rightarrow Bool$，这在 Lean 的术语中很简单

$f: Z \rightarrow Bool$

将函数视为一等对象有很多优点：

统一性： 一切都是一种类型的术语。 5 的类型是 Nat。 sum 的类型是 Nat -> Nat -> Nat。 Pythagorean_Theorem 的类型是 Prop，这是一个有意义的，可以证明的语句。编译器使用此机制来验证你的代码、逻辑和数学。
柯里化（部分应用）： 在 Lean 中，严格意义上不存在“多参数”函数。
- 对两个数字求和的函数 Int -> Int -> Int 实际上是一个接受一个数字并返回另一个等待第二个数字的函数。
- 这允许通过“固定”参数来创建新函数，而无需额外的代码。
- 同样，这有助于可以机械地推理代码的机制。
依赖类型（皇冠上的明珠）：
- 存在许多类型系统，其中一些比其他类型系统更正式，而另一些则比其他类型系统更强大。在最具表现力的类型系统中，Lean 的类型系统所依据的系统是最强大的。
- 函数的返回类型可以 依赖于
  
  输入参数的值。
- 示例： 函数 zero_vector (n : Nat) 返回大小为 n 的向量。结果的类型 (Vector F n) 会根据 n 的值而变化。这在标准的 Java 或 Rust 中是不可能的。

这种语言背后的真正潜力在于，它建立在一个

数学逻辑之间融合而产生的关键思想之上

和计算理论：Curry-Howard 同构定理。

在研究组合逻辑时（1930 年至 1950 年间），Haskell Curry 观察到一种特殊的模式：计算中最基本函数 (组合子) 的类型与蕴涵逻辑 (即经典的“如果 A 则 B”) 的公理具有完全相同的代数结构。他直觉到计算和逻辑演绎是同一枚Coin的两面。

后来，在 1960 年代，William Howard 将这种直觉形式化，证明了 简化逻辑证明 过程（自然演绎中的切消除）与 执行程序 过程（lambda 演算中的 beta 归约）同构。

Curry-Howard 定理（或同构） 确立了逻辑系统和计算系统在结构上是相同的。这允许将数学证明不视为静态文本，而是视为可执行的算法。

命题即类型： 数学语句 P 是一种类型。

证明即程序： P 的证明只是类型 P 的一个术语（程序）。

如果程序编译（类型检查），则证明有效。

Curry-Howard 同构及其带来的后果

Curry-Howard 同构的应用在命题逻辑和类型论之间架起了一座桥梁。作为参考，一个简短的概念表如下所示

命题逻辑	类型论 (Lean)	概念
命题 ($P$)	`P : Prop`	逻辑宇宙中的一种类型。
证明 ($h$)	`h : P`	类型 `P` 的一个术语。
蕴涵 ($P \rightarrow Q$)	`P -> Q`	函数：接受 `P` 的证明，返回 `Q` 的证明。
合取 ($P \land Q$)	`P`×`Q` (Prod)	乘积：一对包含 `P` 的证明和 `Q` 的证明。
析取 ($P \lor Q$)	`P`⊕`Q` (Sum)	和：`P` 的证明或 `Q` 的证明。
真 ($\top$)	`Unit` / `True`	单元：具有单个值 `()` 的类型。平凡。
假 ($\bot$)	`Empty` / `False`	空：没有值的类型。不可能构造。
否定 ($\lnot P$)	`P -> False`	从 `P` 导出矛盾的函数。

起初这令人震惊，但 Lean 的一大特点是它允许 更大程度的 等价：我们可以从“静态”逻辑转移到动态逻辑（即谓词逻辑）。这是学习 Lean 时最强大的概念转换，它是通过利用 谓词可以建模为函数的 这一事实来实现的！

在谓词逻辑中，像 "x 是偶数" 这样的语句，在我们知道 x 的值之前既不是真也不是假。在 Lean 中，这被建模为一个 接受数据并返回命题 的函数。当标准数学说 “P(x) 是集合 A 上的一个谓词” 时，Lean 编写一个接受 A 类型的输入并返回一个逻辑命题 Prop 的函数："P : A -> Prop”。

一个简单的例子

此示例使用取模运算定义了“可被 2 整除”的属性。

-- 谓词定义
-- --------------------

/-
  我们定义一个名为 `is_divisible_by_two` 的函数。

  语法分解：
  1. `def`: 用于定义数据或函数的关键字。
  2. `(n : Nat)`: 输入参数。 我们期望一个自然数。
  3. `: Prop`: 返回类型。
     它不返回 `true` 或 `false` (计算),
     它返回一个逻辑语句。
  4. `:=`: 将签名与实现分开。
  5. `n % 2 = 0`: 主体。 这是一个断言余数为零的等式。
-/
def is_divisible_by_two (n : Nat) : Prop :=
  n % 2 = 0

-- 谓词的用法
-- ----------------------

-- 这里我们用数字 4 来评估谓词。
-- Lean 将其简化为命题 "0 = 0"。
#check is_divisible_by_two 4
-- 控制台结果: is_divisible_by_two 4 : Prop

-- 这里我们用 5 来评估。
-- Lean 将其简化为命题 "1 = 0"。
-- 注意: 该命题在语法上是有效的 (类型为 Prop),
-- 即使它在数学意义上是错误的。
#check is_divisible_by_two 5

请注意，Nat -> Prop 的意思是：“给我一个自然数，我将返回一个关于该数字的逻辑问题。”

此外，还有 有效性和真值 之间的区别：定义谓词并不说明对于给定的数字它是真还是假。它仅定义 该语句的含义。 is_divisible_by_two 5 是 Prop 类型的有效对象；这只是一个我们无法构造证明的对象。

全称量词

证明 “对于所有 x，P(x) 为真” 意味着什么？这意味着如果你给我任何具体的值 x，我都可以返回 P(x) 的证明。但这正好是一个函数！

现在让我们陈述并证明一些涉及全称量词的内容；将使用谓词 P(x) : x < x + 1。在 Lean 中，“for all" ($\forall$) 的行为类似于一个接受来自域的任何值的函数。在这里，我们将使用 theorem 而不是 def，因为我们的目的是证明一个真理，而不仅仅是定义一个结构。

第二个例子

import Mathlib.Data.Nat.Basic -- 导入基本的自然数属性

-- 全称定理的定义和证明
-- -------------------------------------------

/-
  定理：对于每个自然数 x，x 严格小于 x + 1。

  语法分解：
  1. `theorem`: 表示我们正在创建一个命题的项(一个证明)。
  2. `x_less_than_succ`: 我们给定理起的名字.
  3. `: forall (x : Nat), x &lt; x + 1`: 我们想要证明的命题.
     读作:“对于任何 Nat 类型的 x，x &lt; x + 1 成立”。
  4. `:=`: 证明开始的地方.
-/
theorem x_less_than_succ : forall (x : Nat), x &lt; x + 1 := by
  -- 我们使用关键字 `by` 进入“战术模式”。
  -- 这允许我们逐步地构造证明(函数)。

  -- 步骤 1: 引入 (intro)
  -- 目的是要证明 "对于所有 x" 都是真的。
  -- `intro` 策略接受泛型 `x` 并将其放入我们的上下文中。
  -- 这相当于在纸上说:“设 x 为任意自然数……”
  intro x

  -- 当前状态 (信息视图):
  -- x : Nat  (我们有一个任意的 x)
  -- |- x &lt; x + 1 (我们的目标是证明对于那个特定的 x这是成立的)

  -- 步骤2: 应用公理 (exact / apply)
  -- 我们在 Lean 库中搜索一个确切说明这一点的定理。
  -- 有一个名为 `Nat.lt_succ_self` 的定理，它证明了 `forall n, n &lt; succ n`。
  -- 我们将我们的 `x` 传递给那个函数。
  exact Nat.lt_succ_self x

我们可以强调 intro x：是从逻辑到编程的直接翻译。要构造一个适用于所有输入的函数，我们首先声明一个表示该输入的变量。

构造性

然而，谓词逻辑的这种扩展并不是对通常的日常谓词逻辑的复制。这里有一个重要的（哲学意义上和重要意义上的）区别：默认情况下，Lean 是构造性的。这是什么意思？

在构造性的 Lean 中证明像 “$\exists x, P(x)$” 这样的东西需要计算 x 并将其呈现出来。证明“不可能不存在”是不够的。另外，排中律：$P \lor \lnot P$ 不是 Lean 的构造性逻辑中的公理。

LEＭ不是公理这一事实不应被视为令人震惊。毕竟，代码仍然受到计算机科学边界的约束：在计算中，我们并不总是知道程序是否终止（停机问题），因此我们不能普遍地断言 $P \lor \lnot P$。为了平息一些情绪，如果数学家需要，Lean 允许调用经典逻辑 (open Classical)，接受非构造性的公理，但会失去证明的直接“可计算性”。

这一切为什么重要？

从程序员的角度来看，从一开始，肯定会有一个问题萦绕在“数学与编程有什么关系？”这个问题附近"。

让我们首先说明，除了理论之外，Lean 4 解决了复杂系统开发中的地方性问题。 在像 Rust 或 C++ 这样的工业语言中，编译器可以防止内存管理错误（段错误，数据竞争）。但是，它对程序的数学“真值”视而不见。 Lean 提高了标准：它将逻辑错误转换为编译错误。

例如，想象一个典型的菜鸟（以及不太菜鸟的）错误："环绕错误"（即索引越界）的情况。想象一下实现 STARK 执行轨迹上的约束。

在 Rust 中： 工程师编写一个循环 for i in 0..N，检查 trace[i+1] == trace[i] + 1。在最后一次迭代中，i+1 溢出或访问了无效的内存。 Rust 可能会在运行时抛出一个 panic，或者更糟糕的是，读取垃圾并接受一个错误的证明。
在 Lean 中： 我们使用像 Fin n 这样的依赖类型（严格小于 n 的数字）。
- 如果你试图访问 trace[i+1]，但没有首先证明 i < n-1，Lean 将无法编译。
- 编译器会抛出一个类型错误："你还没有证明 i+1 是一个有效的索引。"
- 这迫使工程师在设计期间（而不是在调试期间）正确处理约束。

因此，采用 Lean 引入了一个分层的开发架构，将编译错误和执行错误明显区分开来，并提供了 改进的工作流程。 Lean 的作用是保证规范在编写任何一行底层代码之前是正确且一致的。

认证的代码提取

Lean 4 不仅仅是一个验证器；它是一种能够编译为 C 的高效编程语言。这使得能够进行所谓的 认证代码提取：这是 Lean 采用你的数学定义（函数，结构）并将 它们编译为高效的 C 代码，从而消除了所有执行不必要的“逻辑开销”（证明）的过程。

由于在 Lean 中编写规范，然后手动在 C 中重写它会引入人为错误的风险，因此你可以在 Lean 中编写关键函数（如 Merkle 路径验证或多项式求值），正式证明其正确性，然后要求 Lean 自动生成相应的代码。 结果，你可以获得一个以 C 的速度运行的二进制文件，但具有数学保证，即它是 Lean 中验证的逻辑的忠实表示。可以说，此功能使 Lean 4 成为行业的“游戏规则改变者”，将其与 Coq 或 Isabelle 等学术前辈区分开来。

为了理解这是如何工作的，我们来看一下 Lean 在编译时做出的一个基本区分：数据 (Type)： 数字、列表、向量、矩阵等 是运行程序所必需的，而 证明 (Prop)： 定理、引理、类型保证（例如，i < n）等*仅对说服编译器是必要的_，但在运行时无用。

但是，我们如何理解“编译的数学证明”呢？好吧，这是一个深刻的问题。下面我们简要列出由 代码提取 产生的二进制文件的实际效用，并按这两个不同的观点进行分离。

从软件开发人员的角度来看，生成的二进制文件（例如，

libfri_verifier.so 或 fri_verifier.exe) 是一个 生产工件。这对于

部署： 这个二进制文件就是你上传到服务器，

区块链节点或物联网设备的文件。你可以用新的文件替换你的旧的

verifier.rs 库（手动编写且可能存在错误）。这样做的好处是，你现在拥有一个以本机速度（C/C++）运行的可执行文件，但永远不会受到缓冲区的影响

溢出或接受错误的证明。

集成： 提取的Lean 代码通常会公开一个 C API；

你使用 FFI (外部函数接口) 来调用

Lean 二进制文件中的函数。举个例子，可以想到 “我的 Web 服务器

(Rust) 处理 JSON 和网络，但当关键时刻

需要验证加密证明时，它会将字节传递给

Lean 二进制文件。” 你将关键安全性委托给已验证的

组件，并以速度为代价。如果用 C 编写，你将以安全性为代价。你在需要原始速度时使用 Lean 二进制文件

(C)，但又无法承受任何内存或逻辑错误。

然后将二进制文件解释为 加固的静态/动态库。它可以用于执行生产中的关键业务逻辑，而无需担心崩溃或被利用。

从数学家的角度来看，生成的二进制文件是“见证计算器”：存在性定理的 计算实现。例如，此二进制文件的用途通常是

“物化”存在： 你证明了定理：

$\forall x, \exists y, P(x,y)$（“对于每个输入 x，存在一个解 y”）。虽然该定理是抽象的，但二进制文件是具体的。数学家使用该二进制文件来查找现实世界中的 y——比方说，你将数字

$x = 2^{64} + 13$ 提供给该二进制文件。该二进制文件执行证明中隐含的算法，并输出数字 $y = 1948...$。你已将抽象真理转换为具体数据。

进行认证计算： 有时你想要计算一些困难的东西（例如，第 n 个素数或 ZK 执行轨迹）。现在，该二进制文件充当“真理黑匣子”：如果你使用 Python 脚本并获得结果，你可能会怀疑你是否正确实现了该算法。通过使用 Lean 二进制文件，你可以获得数学保证，即屏幕上的数字是根据公理定义正确的那个。没有逻辑错误的余地。

从数学的角度来看，二进制文件是你的证明的 可执行实例。它可以计算满足你的定理的具体值（见证），从而将数学对象从思想世界带到硬盘驱动器上。

这是同一个文件，但有人将其视为 理论的确认，

另一些人则将其视为 生产工具。

性能

Lean 4 使用了一种名为 Perceus 的引用计数策略，该策略具有激进的重用和唯一性优化。当编译器检测到某个数据结构是唯一拥有的（引用计数为 1）并且你将要创建一个类似的结构时，Lean 可以就地重用内存，而不是分配新内存并进行复制。

实用示例：验证加法约束

让我们通过一个与 ZK 系统直接相关的示例将理论付诸实践。在 STARK 和其他证明系统中，我们通常需要验证对 32 位整数执行的算术运算是否正确。由于我们使用字段元素（如素数为 $p = 2^{31} - 2^{27} + 1$ 的 BabyBear 字段），因此我们将 32 位整数分解为较小的“肢体”，并使用进位位来跟踪溢出。

设置

考虑将两个 32 位整数 lhs 和 rhs 相加得到 res。每个整数都分解为两个 16 位肢体：

$lhs = lhs0 + lhs1 \cdot 2^{16}$

$rhs = rhs0 + rhs1 \cdot 2^{16}$

$res = res0 + res1 \cdot 2^{16}$

ZK 电路强制执行的约束方程为：

$lhs0 + rhs0 = res0 + carry0 \cdot 2^{16}$

$lhs1 + rhs1 + carry0 = res1 + carry1 \cdot 2^{16}$

其中 $carry0$ 和 $carry1$ 是位（0 或 1）。

我们要证明的定理： 如果满足这些约束并且进位是位，则 $res \equiv lhs + rhs \pmod{2^{32}}$。 重要提示： 该定理确定了在约束方程成立时的模算术恒等式。在实际的 ZK 电路中，你还需要单独的范围约束，以确保每个肢体都在 [0,2^{16})[0,2^{16}) 中。这些范围检查通常由电路中的查找参数或分解约束强制执行——我们在此处证明代数关系。

Lean 4 证明

import Mathlib.Data.ZMod.Basic
import Mathlib.Tactic
-- 定义常量以提高可读性
def LIMB_BASE : Nat := 65536      -- 2^16
def MOD_32 : Nat := 4294967296    -- 2^32
/-
  定理：加法约束的正确性
  如果肢体约束方程成立并且进位是位，
  那么 res ≡ lhs + rhs (mod 2^32)。
  注意：这证明了代数恒等式。 范围约束
  （确保肢体 &lt; 2^16）在电路中单独处理。
-/
theorem add_constraint_mod32
  (lhs0 lhs1 rhs0 rhs1 res0 res1 carry0 carry1 : Nat)
  -- 肢体约束方程
  (h_low : lhs0 + rhs0 = res0 + carry0 * LIMB_BASE)
  (h_high : lhs1 + rhs1 + carry0 = res1 + carry1 * LIMB_BASE)
  -- 进位约束
  (h_c0_bit : carry0 ≤ 1)
  (h_c1_bit : carry1 ≤ 1)
  : (res0 + res1 * LIMB_BASE) % MOD_32 =
    (lhs0 + lhs1 * LIMB_BASE + rhs0 + rhs1 * LIMB_BASE) % MOD_32 := by
  -- 展开常量，以便全称量词可以使用具体数字
  unfold LIMB_BASE MOD_32
  unfold LIMB_BASE at h_low h_high
  -- 我们从约束中推导出：
  --   res + carry1 * 2^32 = lhs + rhs
  -- 全称量词策略自动处理线性算术
  omega

理解证明

让我们分解一下正在发生的事情：

展开定义 我们将 LIMB_BASE 和 MOD_32 展开为它们的

具体值（65536 和 4294967296），以便 omega 策略可以

推理它们。

代数运算： 我们将高位肢体方程乘以

$2^{16}$ 并将其与低位肢体方程组合。这为我们提供了

完整的 32 位值之间的关系。

核心恒等式： 关键的见解是，在结合

约束之后：

res+carry1⋅232=lhs+rhsres+carry1⋅232=lhs+rhs

模约简： 由于 carry_1⋅232≡0(mod232)carry_1⋅232≡0(mod232)，

我们得到 res≡lhs+rhs(mod232)res≡lhs+rhs(mod232)。

omega 策略自动处理线性算术，使证明非常简洁，同时保持严谨性。

具体例子

我们还可以验证具体案例：

-- 验证 100 + 200 = 300（没有进位）
example : (300 + 0 * 65536) % 4294967296 =
          (100 + 0 * 65536 + 200 + 0 * 65536) % 4294967296 := by
  native_decide
-- 验证 65535 + 1 = 65536（从低位肢体进位）
-- 65536 = 0 + 1 * 65536
example : (0 + 1 * 65536) % 4294967296 =
          (65535 + 0 * 65536 + 1 + 0 * 65536) % 4294967296 := by
  native_decide
-- 验证 2^32 - 1 + 1 ≡ 0 (mod 2^32)（完全溢出）
example : (0 + 0 * 65536) % 4294967296 =
          (65535 + 65535 * 65536 + 1 + 0 * 65536) % 4294967296 := by
  native_decide

这正是 zkVM 中出现的约束验证类型。通过在 Lean 4 中证明它，我们可以获得机器检查的保证，即我们的约束逻辑是正确的——不仅适用于测试用例，而且适用于所有可能的输入。

结论

我们在本文中介绍了很多内容：

Curry-Howard 同构 揭示了证明和程序在

根本上是同一件事。类型是命题，而术语