Lean 4 与形式化验证：先证一个

测试告诉你“这几个输入没问题”。证明告诉你“所有输入都没问题”。形式化验证就是让计算机来检查这种证明，Lean 4 是做这件事的一门语言。

先别管这些词。下面这个命题说的是：如果“p 且 q”成立，那么“q 且 p”也成立。你来证，Lean 来查。

动手证把“且”的两边换个位置状态和报错由 Lean 4.35.0 生成

theorem and_swap' (p q : Prop) : p ∧ q → q ∧ p := by
  intro h
  constructor
  exact h.right
  exact h.left

你刚才做的事情，就是这门课的全部：Lean 给你一个目标，你选一步，目标变小，直到没有目标。 选错了，Lean 当场拦住，告诉你为什么。它不会放过任何一步。

上面每一个状态、每一句报错，都是真实的 Lean 输出，不是我们写的。

学完你手里有什么

一个你自己写的、被 Lean 证明为正确的迷你编译器：它把算式翻译成指令，而且你证明了，对任何算式，翻译出来的指令算出的结果都和原算式一样。

不需要数学基础，会一点任何语言的编程就够。

路线

阶段	课	你会做到
起步	形式化验证是什么	说清测试和证明差在哪
	装好 Lean 4	在自己电脑上让 Lean 算出 1 + 1
	第一个证明	写出并读懂一个定理
逻辑	如果……那么……	用 intro、apply、exact
	且和或	拆开和拼出复合命题
	让 Lean 替你算	用 rw、simp、omega、decide
归纳	对自然数做归纳	证明对所有自然数成立的事
	对列表做归纳	证明“反转两次等于没反转”
验证程序	证明一个编译器是对的	完成毕业作品

这门课怎么保证不出错

• 课文里的每一段 Lean 代码，发布前都由 Lean 4.35.0 实际检查。写着“会报错”的例子，也确认过它真的报错。
• “你应该看到”后面的输出，是从 Lean 的真实输出里核对过的。
• 交互练习里的目标状态和报错，由脚本从 Lean 生成。

Lean 更新后如果你看到的和课文不一样，在那一节末尾告诉我们。

下一步

• 我在上面的练习里证完了第一个定理

从形式化验证是什么开始。想直接动手，去装好 Lean 4。