学习资源与练习路线
从游戏到 Mathlib，再回到 Hansen
Lean 社区的学习页开宗明义：无论背景，证明助手都难，不能指望一个下午精通；资源很多，但只学 Lean 4，不要再学 Lean 3 (Lean prover community 2025年b)。本页把这些资源排成一条适合已会写计量证明的教师的路径，并说明本栏目以后如何追加实作笔记。
1 四条并行的官方入口
按「先上手、再补基础」而不是「先读完逻辑再写第一行」：
| 资源 | 适合什么 | 链接 |
|---|---|---|
| Natural Number Game（NNG，自然数游戏） | 零安装，用策略证自然数性质 | adam.math.hhu.de；源码 NNG4 |
| Mathematics in Lean（MIL） | 用 Mathlib（Lean 的数学库）、偏策略、有习题文件 | HTML (Avigad 和 Massot 2025年) |
| Theorem Proving in Lean 4（TPIL） | 依赖类型论、项风格、内核与公理 | TPIL4 (Avigad 等 2025年) |
| The Mechanics of Proof | 比 MIL 更缓，本科证明课口吻 | Macbeth |
社区比喻：MIL 是「先按开始键」；TPIL 是「先读完说明书」(Avigad 和 Massot 2025年)。计量教师建议 NNG → MIL 前几章 → 需要时查 TPIL，不要先把 TPIL 当教材从头到尾抄。
补充：
- Glimpse of Lean：四个基础文件后按主题分支（分析 / 拓扑 / 逻辑）。仓库
- 策略速查 PDF：社区 learn 页提供 cheatsheet 入口 (Lean prover community 2025年b)
- Functional Programming in Lean：当 Lean 是编程语言、或要写自定义策略时再读。https://lean-lang.org/functional_programming_in_lean/
- Hitchhiker’s Guide to Logical Verification：偏计算机科学与逻辑基础
2 建议的十二周节奏
可按学期实验课压缩或拉长。目标不是成为 Mathlib 贡献者，而是：能独立读懂一条普通最小二乘（OLS, Ordinary Least Squares）代数形式化，并能写出带 sorry 的 Hansen 陈述骨架。
第 1–2 周：游戏。
打完 NNG 的加法、乘法、不等式若干世界。体会 rw、induction、have。不要同时装 Mathlib。
第 3–5 周：MIL 基础与逻辑。
安装 Lean 4 与 Visual Studio Code（VS Code）/ Cursor 扩展；按官方说明下载 Mathematics in Lean 仓库，复制 MIL 文件夹再做题，以便日后 git pull (Avigad 和 Massot 2025年)。完成计算、代数结构、逻辑量词、集合与函数。
第 6–7 周：线性代数章。
MIL 第 10 章（向量空间、子空间、矩阵）是第 3 章 Hansen 的预科。同步重读本仓库 block-matrix/ 与 part01-reg/chpt03-*.qmd，尝试把一条板书恒等式写成 calc。
第 8–9 周：测度与积分浏览。
MIL 第 13 章 + Mathlib 文档里 condExp 页。不求证完，求能 #check 出条件期望的类型。对照 计量路径。
第 10 周：读别人的对照表。
打开 lean-hansen-econometrics 的 inventory/ch3-inventory.md（或 ch2），只读陈述差异，不求本地构建通过。用 如何解读 的清单做笔记。
第 11–12 周：自己的第一条骨架。
在独立目录 lake new ... math，写一条 Frisch–Waugh–Lovell（FWL）或投影幂等的 theorem ... := by sorry，补到能 lake build。把假设与 Hansen 编号写入本仓库 inventory（定理清单；Lean 目标列填声明名）。仍不把 .lake 提交到 hansenpeer。
每周保留一次 Zulip 提问或旁听。https://leanprover.zulipchat.com/
3 安装清单（学习工程，不是本站）
- 按 https://lean-lang.org/install/ 安装 elan（Lean 工具链管理器）与 Lean 4 扩展。
- 用 VS Code 的
∀菜单打开 / 下载 Mathematics in Lean，或命令行git clone后lake exe cache get(Lean prover community 2025年a)。 - 自建练习项目：
lake +v4.24.0 new my_project math，再lake update与lake exe cache get。版本号以当时文档为准。 - Windows 若
cache get失败，先看社区项目页的杀毒软件说明。
本 Quarto 站点构建不依赖上述步骤。关掉 Lean 扩展也可以渲染本栏目。
4 检索与社区
- Mathlib 文档：https://leanprover-community.github.io/mathlib4_docs/
- Loogle（按类型搜引理）：https://loogle.lean-lang.org/
- 社区学习总页：https://leanprover-community.github.io/learn.html
- 会议录像与 LCM（Lean for the Curious Mathematician，为好奇的数学家准备的 Lean 研讨）：社区 events / YouTube
- 类型论深水：Carneiro (Carneiro 2019年)、同伦类型论（HoTT, Homotopy Type Theory）书第 1 章（忽略单值公理即可入门）——可选
提问时带：工具链版本、最小可复现代码、Infoview（信息视窗）目标。不要只贴「如何证明 Hansen 4.3」。
5 本栏目以后如何生长
后续实作笔记建议仍放 block-lean/，文件名继续编号，例如：
lean-09-nng-notes.qmd：NNG 与课堂归纳法对照lean-10-mil-linalg.qmd：MIL 矩阵习题与第 3 章记号lean-11-fwl-skeleton.qmd：FWL 的 L1 ↔︎ 拟 Lean 签名（仍可不含可构建工程）
L3 源码若出现，使用第三仓库或本仓库平行目录，独立 lakefile.toml，站点只链过去。规则与方法页 明确不做 一致。
6 阅读本栏目的检查表
读完八篇后，应能不看笔记回答：
- L1、L2、L3 各证明什么、不证明什么？
- 为什么
lake build绿了仍可能没证明 Hansen 原句？ sorryAx与Classical.choice对外说法有何不同？- 为什么 OLS 必须先规定奇异时的值？
- 第一条值得做的 Hansen L3 大概是哪条链？
若这五问清楚，技术细节可以边做边查 TPIL 与 Mathlib 文档。形式化是工程，不是一次读完的理论课。