第1章 入门 - 深度伴读
本章定位
第1章是”破冰”章节，不涉及真正的证明技巧。核心目标是建立三个心智模型：
- Lean 是什么（类型论证明助手）
- 证明即程序（Prop → 证明项 → tactic）
- 工作流（VS Code + Goal 窗口 + 交互式反馈）
1.1 Getting Started
核心要点
本节讲的是”怎么开始用”，技术性内容不多，但有几个概念需要建立：
形式化 ≈ 编程
Lean 的核心洞见：写证明就像写程序
- 普通程序：输入数据 → 处理 → 输出数据
- Lean 证明：给定命题（类型）→ 构造证据（项）→ Lean 验证类型正确
这个类比贯穿整个学习过程。如果你有编程基础，会更容易理解 Lean 的思维方式。
工作流
VS Code 编辑 .lean 文件
↓
Lean 服务器实时检查
↓
Goal 窗口显示证明状态
↓
鼠标悬停查看反馈
关键习惯
永远盯着 Goal 窗口。它告诉你：
- 当前有哪些假设（context）
- 还需要证明什么（target）
这是你在 Lean 中唯一的”导航仪”。
常见困惑
| 困惑 | 解答 |
|---|---|
#check 和 #eval 有什么区别？ | #check 查看类型，#eval 计算值 |
| 为什么要复制 MIL 文件夹？ | 保留原始文件便于 git pull 更新 |
\R 怎么打出 ℝ？ | 输入 \R 后按空格或 Tab |
1.2 Overview
本节是全书最重要的概念基础
理解本节的三层结构，后面所有章节都是在这个框架下展开的。
核心概念：三层类型系统
Lean 的世界只有三类东西，用 #check 一看便知：
┌─────────────────────────────────────────────────────────┐
│ 第1层：数据（数学对象） │
│ 类型：ℕ, ℝ, ℕ → ℕ, List ℝ ... │
│ 例子：2 + 2, f(x) = x + 3 │
├─────────────────────────────────────────────────────────┤
│ 第2层：命题（数学陈述） │
│ 类型：Prop │
│ 例子：2 + 2 = 4, FermatLastTheorem, ∀ x, x² ≥ 0 │
├─────────────────────────────────────────────────────────┤
│ 第3层：证明（命题的证据） │
│ 类型：P，其中 P : Prop │
│ 例子：rfl : 2 + 2 = 4, sorry : 任何命题（作弊） │
└─────────────────────────────────────────────────────────┘
关键洞见：在 Lean 中，“证明一个命题 P” = “构造一个类型为 P 的项”。
-- 这不是"声明"，这是在"构造证据"
theorem easy : 2 + 2 = 4 := rfl
-- easy 的类型是 "2 + 2 = 4"，它是一个 Prop
-- rfl 是构造这个证据的方法sorry 是什么？
sorry是 Lean 内置的”万能证据”，可以假装证明任何命题。 它的存在是为了让你先搭框架再填充细节。 Lean 知道你在作弊，会在 Goal 窗口用黄色警告。
两种证明风格
这是本章第二个核心概念：
风格1：证明项（Proof Term）
直接写出”证据长什么样”：
-- Even n 表示"n 是偶数"，定义为 ∃ k, n = k + k（即 n = 2k）
-- 所以 Even n 的值是一个对 ⟨k, hk⟩，其中 k 是 witness，hk 是证明 n = k + k
example : ∀ m n : Nat, Even n → Even (m * n) :=
fun m n ⟨k, hk⟩ ↦ ⟨m * k, by rw [hk, mul_add]⟩
-- ↑ 给定 n = k + k，构造 m*n = m*k + m*k，所以 m*n 也是偶数
-- ↑ mul_add : m * (k + k) = m * k + m * k优点：紧凑、精确 缺点：难写、难读
风格2：Tactic 证明
给 Lean 一步步指令来构造证据：
example : ∀ m n : Nat, Even n → Even (m * n) := by
-- rintro = intro + rcases，同时引入变量和解包假设
rintro m n ⟨k, hk⟩ -- m,n : Nat; k : Nat; hk : n = k + k
use m * k -- 提供偶数 witness：m*n = m*k + m*k
rw [hk] -- 把 n 换成 k + k：目标变成 m*(k+k) = m*k + m*k
ring -- 自动用分配律证明优点：交互式、有反馈、易调试 缺点：稍冗长
本书的选择
主要用 Tactic 风格。原因：
- 有即时反馈（Goal 窗口）
- 更接近人类思考方式
- 可以逐步构建，边写边看
Tactic 证明的状态变化
这是你需要建立的核心直觉。每执行一个 tactic，Goal 窗口会变化：
example : ∀ m n : Nat, Even n → Even (m * n) := by
-- 初始状态：
-- ⊢ ∀ (m n : Nat), Even n → Even (m * n)
rintro m n ⟨k, hk⟩
-- 状态变为：
-- m n k : Nat
-- hk : n = k + k
-- ⊢ Even (m * n)
use m * k
-- 状态变为：
-- ⊢ m * n = m * k + m * k
rw [hk]
-- 状态变为：
-- ⊢ m * (k + k) = m * k + m * k
ring
-- 目标解决！学习建议
把光标放在每个 tactic 后面，观察 Goal 窗口的变化。 这是学习 Lean 最重要的练习。
证明项 vs Tactic 的关系
证明项：直接描述"证据是什么"
↕ 可以互相嵌套
Tactic：描述"怎么构造证据"
by 关键字：从 tactic 世界切换到证明项世界
例：⟨m * k, by rw [hk, mul_add]⟩
↑ 证明项中嵌入了一个 tactic 块
自动化的力量
本节展示了 simp 的威力：
example : ∀ m n : Nat, Even n → Even (m * n) := by
intros; simp [*, parity_simps]
-- ↑ 一行搞定！何时用 simp
simp会尝试所有已知的简化规则simp [*, parity_simps]中：*表示使用所有局部假设，parity_simps是 Mathlib 中关于奇偶性的简化规则集合- 适合”显然”的证明，但有时会过度简化导致意外结果
- 对于学习阶段，建议先用
rw手动证明，理解原理后再用simp
本章练习指导
必做练习
#eval "Hello, World!"- 确保环境正常- 类型检查 - 对各种表达式使用
#check，理解类型 - Even 证明 - 手动写一遍 tactic 证明，观察状态变化
可跳过内容
- Acknowledgments 部分（纯致谢）
- Gitpod/Codespaces 部分（如果你本地安装了 Lean）
本章核心概念总结
| 概念 | 含义 | 关键字 |
|---|---|---|
| 类型 (Type) | Lean 中一切皆有类型 | #check |
| Prop | 命题的类型 | Prop |
| 证明项 | 类型为 Prop 的项 | theorem, example |
| Tactic | 构造证明的指令 | by, rw, ring |
| Goal 窗口 | 显示当前证明状态 | ⊢ 符号 |
| sorry | 占位符，假装证明 | sorry |
预告：第2章会学到什么
第2章开始真正的数学证明，核心 tactic：
rw- 重写（替换等式一边）ring- 自动证明代数恒等式calc- 写计算链apply- 应用定理
自测问题
2 + 2的类型是什么？2 + 2 = 4的类型是什么？sorry能证明False吗？为什么这很危险？- tactic 证明中的
by关键字起什么作用？
伴读文档 - 第1章完