Lean 4 从入门到精通

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

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

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

版本基准

这个专栏怎么读

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

• 第 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 是什么 开始。