收尾复盘

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

一条主线

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

命题 ←→ 类型
证明 ←→ 项

由它推出的一切：

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

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

二十条要点

语言基础

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

类型系统

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

证明

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

工程

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

tactic 速查

引入/消去（对应逻辑联结词）

目标/假设形状	造	用
`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`

自动化（见自动化章）

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

探索

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

常见卡点索引

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

Lean 的取舍

诚实地说说它的代价：

优势

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

代价

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

什么时候值得用 Lean

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

什么时候不值得

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

继续学习

入门路径

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

参考资料

Lean 语言参考手册——权威定义。
Mathlib 文档——全库 API。
Loogle——按类型搜定理。
Zulip——社区问答。

练习建议

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

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

版本说明

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

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

lean --version

以该版本对应的官方文档为准。本专栏梳理的核心观念（命题即类型、归纳即递归、tactic 只是构造项）是稳定的，具体的 tactic 名与库 API 才是易变的部分。

回到专栏首页可查任意章节。