# Lean 4 从入门到精通

> 从第一行代码到形式化证明——依值类型、tactic、Mathlib 与元编程的系统教程。

- 作者：David（道雾轩）
- 最后更新：2026-08-03
- 原文：https://daiw.org/manual/lean4
- 转载与引用：请注明出处并附原文链接（https://daiw.org/about/copyright）

Lean 4 是一个**同时是编程语言和定理证明器**的系统。官方参考手册的定义：

> Lean is an **interactive theorem prover** based on dependent type theory […] that also functions as a pure **functional programming language**.

这个双重身份不是附加功能，而是**同一件事的两面**：在依值类型论里，「程序」与「证明」是同一种东西，「类型」与「命题」是同一种东西。理解了这一点，Lean 的一切设计都会变得自然。

## 版本基准

| 项 | 值 |
| --- | --- |
| 稳定版 | **Lean 4.32.1**（2026-07-22） |
| 最新 rc | 4.33.0-rc1 |
| 参考手册 | [lean-lang.org/doc/reference/latest](https://lean-lang.org/doc/reference/latest/) |
| 社区库 | [Mathlib4](https://github.com/leanprover-community/mathlib4) |
| 快照日期 | 2026-07-30 |

<Callout type="warn">
  **Lean 迭代很快，语法与库 API 会变。** 本专栏所有代码以 4.32.x 为准；遇到与你的版本不符时，以 `lake env lean --version` 显示的版本对应的官方文档为准。

  尤其注意：网上大量 Lean 教程是 **Lean 3** 的，语法差异巨大（`begin...end` vs `by`、`λ x, e` vs `fun x => e`）。**Lean 3 的代码在 Lean 4 里基本一行都跑不了。**
</Callout>

## 这个专栏怎么读

分五个部分，**前三部分必须顺序读**——依值类型与「命题即类型」是后面一切的地基。

- **第 0 部分 · 入门**——它是什么、装上就跑、第一个程序与第一个证明。
- **第 1 部分 · 函数式编程**——类型与项、函数、归纳类型、类型类、Monad 与 `do`。把 Lean 当普通函数式语言用。
- **第 2 部分 · 依值类型与命题**——依值类型、命题即类型、逻辑联结词的类型对应。**全书的转折点**。
- **第 3 部分 · 证明**——tactic 基础、重写、归纳、结构化证明、自动化。
- **第 4 部分 · 工程与进阶**——Mathlib、元编程与宏、Lake 工程组织。
- **第 5 部分 · 实战**——完整例子与收尾。

## 学 Lean 的三个门槛

先说清楚难在哪，好有心理准备：

1. **「证明是一个程序」这个观念的转换。** 从「写代码让机器执行」到「写项让类型检查器接受」，思维方式完全不同。第 2 部分专门处理这个坎。
2. **tactic 的不透明性。** `simp` 成功了你很高兴，失败了你完全不知道为什么。第 3 部分会讲怎么把黑箱打开。
3. **Mathlib 的规模与命名约定。** 几百万行的库，找到你要的那条引理本身就是技能。第 4 部分讲检索方法。

## 读者预设

- 会一门编程语言，**最好接触过函数式**（Haskell/OCaml/F#/Scala 任一即可，不是硬要求）。
- 高中数学水平足够读懂本专栏的例子；**不需要**有形式化数学或逻辑学背景。
- 不需要提前懂类型论——那正是本专栏要教的。

## 与站内其他专栏的关系

Lean 的类型系统与常见语言差别很大，但基本的函数式概念（代数数据类型、模式匹配、类型类、Monad）是相通的。站里的其他编程专栏可作背景，但**不是前置要求**。

准备好了，就从 [Lean 4 是什么](https://daiw.org/manual/lean4/what-is-lean) 开始。

## 本专栏篇目

- [Lean 4 从入门到精通](https://daiw.org/manual/lean4.md): 从第一行代码到形式化证明——依值类型、tactic、Mathlib 与元编程的系统教程。

### 第 0 部分 · 入门

- [Lean 4 是什么](https://daiw.org/manual/lean4/what-is-lean.md): 双重身份、elan 与 lake 工具链、装上就跑，以及与 Coq/Agda/Isabelle 的定位差异。
- [第一个程序与第一个证明](https://daiw.org/manual/lean4/first-steps.md): def/#eval/#check、theorem 与 by、Infoview 读法，以及「错误信息怎么读」。

### 第 1 部分 · 函数式编程

- [类型与项](https://daiw.org/manual/lean4/types-terms.md): 一切皆项、类型宇宙层级、Type 与 Prop 的分工，以及为什么需要宇宙。
- [函数](https://daiw.org/manual/lean4/functions.md): lambda 与 fun、三种参数绑定（显式/隐式/实例）、命名参数与默认值、递归与终止性。
- [归纳类型与结构体](https://daiw.org/manual/lean4/inductive-types.md): inductive 的构造子与递归子、structure 与继承、参数与索引的区别、Nat 与 List 的真实定义。
- [类型类](https://daiw.org/manual/lean4/typeclasses.md): class/instance、实例解析、outParam、Decidable 的桥梁作用与常见解析失败的排查。
- [Monad 与 do 记法](https://daiw.org/manual/lean4/monads.md): Functor/Applicative/Monad 层次、do 记法的脱糖、IO 与 Option/Except，以及 Lean 特有的 do 扩展。

### 第 2 部分 · 依值类型与命题

- [依值类型](https://daiw.org/manual/lean4/dependent-types.md): Pi 类型与 Sigma 类型、类型依赖值的三种典型用法，以及依值模式匹配与「绿色黏液」问题。
- [命题即类型](https://daiw.org/manual/lean4/propositions-as-types.md): Curry-Howard 对应、证明就是程序、Prop 与 Type 的实际差别，以及为什么这让机器检查成为可能。
- [逻辑联结词](https://daiw.org/manual/lean4/logic-connectives.md): And/Or/Iff/Exists 的定义、引入与消去规则、经典逻辑公理，以及每个联结词的证明套路。

### 第 3 部分 · 证明

- [tactic 基础](https://daiw.org/manual/lean4/tactics-basics.md): tactic 是什么、intro/exact/apply/refine 的精确差别、目标管理与 rcases 模式语言。
- [重写与化简](https://daiw.org/manual/lean4/rewriting.md): rw 的方向与位置控制、simp 的工作原理与调试、simp only 与 simp lemma 的选择。
- [归纳证明](https://daiw.org/manual/lean4/induction-proofs.md): induction tactic、归纳假设的使用、泛化技巧、强归纳与良基递归，以及为什么归纳法就是递归。
- [结构化证明](https://daiw.org/manual/lean4/structured-proofs.md): have/suffices/calc/show 写出可读的证明，以及「可维护的证明」应该长什么样。
- [自动化 tactic](https://daiw.org/manual/lean4/automation.md): omega/decide/norm_num/ring/linarith/aesop/grind 各自的适用范围与失败时的替代方案。

### 第 4 部分 · 工程与进阶

- [Mathlib](https://daiw.org/manual/lean4/mathlib.md): 命名约定的解码规则、四种检索手段、代数结构层次，以及如何贡献。
- [元编程与宏](https://daiw.org/manual/lean4/metaprogramming.md): notation/macro/elab 三个层次、语法范畴与卫生性，以及写自定义 tactic 的基本骨架。
- [工程组织](https://daiw.org/manual/lean4/lake-projects.md): lakefile 配置、模块与命名空间、依赖管理与缓存、CI 设置，以及大型形式化项目的组织经验。

### 第 5 部分 · 实战

- [实战：验证过的插入排序](https://daiw.org/manual/lean4/worked-example.md): 从定义到规格到证明的完整流程——把前面所有内容串起来的一个真实例子。
- [收尾复盘](https://daiw.org/manual/lean4/recap.md): 核心观念回顾、tactic 速查、常见卡点索引与继续学习的路径。