形式化验证是什么

形式化验证，是用数学证明来说明一个程序对所有输入都满足要求，并让计算机检查这个证明的每一步。 它和测试的区别只有一个：测试检查你试过的那些输入，证明覆盖全部。

这一节用一个小函数把这句话落到实处。不用装任何东西，代码看懂就行。

学完你能做什么

• 说出测试和证明各自保证了什么
• 看懂一条 Lean 定理在说什么
• 知道“Lean 检查通过”意味着什么，不意味着什么

一个函数，两种检查

这个函数把 1 到 n 加起来：

def sumTo : Nat → Nat
  | 0 => 0
  | n + 1 => sumTo n + (n + 1)

你记得有个公式：1 加到 n 等于 n × (n + 1) ÷ 2。函数和公式对得上吗？

测试的做法：挑一个数，算一下。

#eval sumTo 100

你应该看到：

5050

100 × 101 ÷ 2 也是 5050，对上了。但这只说明 n = 100 时是对的。n = 101 呢？n = 一亿呢？你可以多测几个，永远测不完。

证明的做法：写下一句对所有 n 都成立的话，然后证明它。

theorem sumTo_formula (n : Nat) : 2 * sumTo n = n * (n + 1) := by
  induction n with
  | zero =>
    rfl
  | succ k ih =>
    simp [sumTo]
    rw [Nat.mul_add, ih]
    simp [Nat.mul_add, Nat.add_mul]
    omega

现在看不懂 by 后面的部分没关系，那是后面几节的内容。只看第一行：

• theorem sumTo_formula：一条定理，名字叫 sumTo_formula。
• (n : Nat)：对任意一个自然数 n。
• 2 * sumTo n = n * (n + 1)：sumTo n 的两倍等于 n × (n + 1)。

Lean 检查通过了这段证明。从此这句话对每一个自然数都成立，不需要再测。

• 我能说出 #eval sumTo 100 和 theorem sumTo_formula 各自保证了什么

写错了会怎样

假如你记错了公式，以为 1 加到 n 等于 n × n：

theorem wrong_formula (n : Nat) : sumTo n = n * n := by
  induction n with
  | zero => rfl
  | succ k ih => simp [sumTo, ih]; omega

Lean 不接受。它的回答以这一句开头：

omega could not prove the goal:

你没法靠“看起来差不多”蒙混过去。一个错的命题，怎么写都证不出来。这就是形式化验证值得信任的原因：检查证明的是程序，不是人的耐心。

考考你你给一个排序函数写了 200 个测试，全部通过。这说明什么？

它不保证什么

Lean 保证的是：你写下的那句话，被证明了。 它不保证你写的那句话就是你真正想要的。

上面的定理说的是“sumTo n 的两倍等于 n × (n + 1)”。如果你本来想要的是别的性质，却写成了这一句，Lean 帮不了你。所以读懂定理的第一行，比读懂证明更重要。证明交给 Lean 查，命题得你自己看。

• 我知道“证明通过”保证的是命题成立，不保证命题写对了需求

检查点

• 我能一句话说清形式化验证：用证明说明程序对所有输入都对，并让计算机检查证明
• 我能说出测试和证明的区别：试过的输入，全部输入
• 我能读出 theorem 名字 (n : Nat) : 命题 各部分的意思
• 我知道一个错的命题在 Lean 里证不出来

常见误会

“形式化验证就是更多的测试。” 不是。测试是运行程序看结果，证明不运行程序，它从定义出发推理，一次覆盖所有情况。

“证明通过了，程序就没有任何问题。” 证明只管你写下的那句话。没写进命题的性质，不在保证之内。

下一节

想亲手让 Lean 检查这些代码，先装好 Lean 4。