# 收尾复盘

> 核心观念回顾、tactic 速查、常见卡点索引与继续学习的路径。

- 作者：David（道雾轩）
- 专栏：Lean 4 从入门到精通（https://daiw.org/manual/lean4.md）
- 最后更新：2026-08-02
- 原文：https://daiw.org/manual/lean4/recap
- 转载与引用：请注明出处并附原文链接（https://daiw.org/about/copyright）

## 一条主线

整个专栏只有一个核心观念：

```text
命题 ←→ 类型
证明 ←→ 项
```

由它推出的一切：

- 「证明定理」就是「写函数」。
- `∀` 与 `→` 是同一个东西。
- `¬p` 就是 `p → False`。
- 归纳法与递归是同一条规则（`Nat.rec`）。
- 定理可以被应用、部分应用、当参数传。
- 机器能检查证明，因为那是**类型检查**。
- 可信度来自**小内核**——tactic 出错最多是造不出项，错的项过不了内核。

理解了这条主线，Lean 的所有设计都是它的直接后果，而不是需要背的规则。

## 二十条要点

**语言基础**

1. `Nat` 减法**截断**到 0，涉及减法的命题要小心。
2. `Bool` 与 `Prop` 是不同的东西，靠 `Decidable` 连接。
3. `→` 右结合，多参数函数是柯里化的。
4. `{}` 隐式、`[]` 实例隐式，`@` 关闭隐式。
5. `x.f a` 被解释成 `T.f x a`（广义字段记法）。
6. 模式匹配有**穷尽性检查**——漏 case 会编译失败。
7. 递归必须能证明终止，否则用 `partial def`（但那样不能用于证明）。

**类型系统**

8. 宇宙层级防止 `Type : Type` 导致的不一致。
9. `Prop` 有 proof irrelevance，编译后被**完全擦除**。
10. 参数在 `:` 左边（各构造子相同），索引在右边（可不同）。
11. 依值类型能把不变量编进类型，但**过度使用会陷入 cast 地狱**。

**证明**

12. tactic 只是「帮你写项」的工具，不是另一套系统。
13. `exact` 要完全匹配，`apply` 留下子目标，`refine` 手工留洞。
14. 归纳证明卡住时，先问**归纳假设够不够强**（`generalizing`）。
15. `rw` 是语法替换且会替换所有匹配处。
16. `simp` 探路、`simp?` 固化成 `simp only`。
17. 线性算术给 `omega`，环恒等式给 `ring`，不等式给 `linarith`。
18. `calc` 是让证明可读的第一选择。

**工程**

19. `#print axioms` 确认没有 `sorryAx`。
20. `autoImplicit false` 避免拼写错误被当成隐式参数。

## tactic 速查

**引入/消去**（对应[逻辑联结词](https://daiw.org/manual/lean4/logic-connectives)）

| 目标/假设形状 | 造 | 用 |
| --- | --- | --- |
| `p → q` | `intro h` | `h hp` |
| `p ∧ q` | `constructor` / `⟨_,_⟩` | `h.1` `h.2` / `obtain ⟨_,_⟩` |
| `p ∨ q` | `left` / `right` | `rcases h with h\|h` |
| `p ↔ q` | `constructor` | `h.mp` / `rw [h]` |
| `¬p` | `intro h` | `h hp` |
| `∀ x, P x` | `intro x` | `h a` |
| `∃ x, P x` | `use a` | `obtain ⟨x, hx⟩ := h` |

**自动化**（见[自动化章](https://daiw.org/manual/lean4/automation)）

```text
具体数字算术       → norm_num
Nat/Int 线性算术   → omega
环恒等式           → ring
线性不等式         → linarith
非线性不等式       → nlinarith [提示]
可判定小命题       → decide
纯逻辑             → tauto / aesop
不确定             → grind / exact?
```

**探索**

```text
exact?      找能直接闭合目标的定理
apply?      找能 apply 的定理
rw?         找能重写的等式
simp?       看 simp 用了哪些引理
#check      查类型
#print      看定义
#print axioms  查依赖公理
```

## 常见卡点索引

| 症状 | 去哪查 |
| --- | --- |
| Lean 3 语法报错（`λ x, e`） | [专栏首页的版本说明](https://daiw.org/manual/lean4) |
| `#eval` 报 no `Repr` instance | [加 `deriving Repr`](https://daiw.org/manual/lean4/inductive-types) |
| `Nat` 减法结果不对 | [截断减法](https://daiw.org/manual/lean4/types-terms) |
| `failed to synthesize` | [类型类解析](https://daiw.org/manual/lean4/typeclasses) |
| do 块里类型多一层 | [`←` 与 `:=` 的区别](https://daiw.org/manual/lean4/monads) |
| `motive is not type correct` | [依值重写的困难](https://daiw.org/manual/lean4/rewriting) |
| 归纳假设用不上 | [`generalizing`](https://daiw.org/manual/lean4/induction-proofs) |
| `rw` 之后目标没变 | [语法匹配的局限](https://daiw.org/manual/lean4/rewriting) |
| 目标里一堆 `↑` | [`push_cast` / `norm_cast`](https://daiw.org/manual/lean4/mathlib) |
| 终止性证不出来 | [`termination_by`](https://daiw.org/manual/lean4/functions) |
| 找不到某个定理 | [Loogle / Moogle](https://daiw.org/manual/lean4/mathlib) |
| CI 编译超时 | [`lake exe cache get`](https://daiw.org/manual/lean4/lake-projects) |

## Lean 的取舍

诚实地说说它的代价：

**优势**

- Mathlib 是目前最大最活跃的形式化数学库。
- 元编程用 Lean 自己写，扩展成本低。
- 是真正可用的编程语言，不只是证明器。
- 社区极其活跃，新手提问基本当天有回应。

**代价**

- **变化快**。Lean 3 → 4 是不兼容重写，4 内部也在持续演进。网上教程过期率高。
- **学习曲线陡**。「命题即类型」的观念转换对多数人是硬门槛。
- **自动化不透明**。`simp` 失败时很难知道原因。
- **依值类型容易过度使用**，陷入 cast 与 `HEq` 的泥潭。
- **编译慢**。大型形式化项目的迭代速度远低于普通编程。

**什么时候值得用 Lean**

- 正确性的价值远高于开发成本（密码学、编译器、航天软件）。
- 形式化数学研究。
- 学习类型论与逻辑。
- AI 定理证明研究——Lean 是当前主要目标平台。

**什么时候不值得**

- 普通业务软件。形式化的成本通常是常规开发的数倍到数十倍。
- 需求频繁变动的项目——规格一改，证明全废。

## 继续学习

**入门路径**

1. **Natural Number Game**——游戏化，从零开始重建自然数理论。最推荐的第一站。
2. **Theorem Proving in Lean 4**——官方教程，侧重语言与类型论。
3. **Mathematics in Lean**——形式化数学实战。
4. **Functional Programming in Lean**——把 Lean 当编程语言用。

**参考资料**

- [Lean 语言参考手册](https://lean-lang.org/doc/reference/latest/)——权威定义。
- [Mathlib 文档](https://leanprover-community.github.io/mathlib4_docs/)——全库 API。
- [Loogle](https://loogle.lean-lang.org/)——按类型搜定理。
- [Zulip](https://leanprover.zulipchat.com/)——社区问答。

**练习建议**

从**小而完整**的项目开始：实现一个数据结构并证明它的核心性质。比起「读懂大证明」，自己从头写完一个小证明收获大得多。

卡住时的正确姿势：**先看 Infoview 里的真实状态**，再 `exact?` 搜库，再去 Zulip 问。不要盯着代码硬想——形式化的困难几乎总是「状态与你以为的不同」或「缺一个引理」。

## 版本说明

本专栏基准为 **Lean 4.32.1**（2026-07-22 稳定版），Mathlib 为对应版本。

Lean 迭代很快，读到与你的环境不符时：

```bash
lean --version
```

以该版本对应的[官方文档](https://lean-lang.org/doc/reference/latest/)为准。**本专栏梳理的核心观念（命题即类型、归纳即递归、tactic 只是构造项）是稳定的**，具体的 tactic 名与库 API 才是易变的部分。

回到[专栏首页](https://daiw.org/manual/lean4)可查任意章节。