我的博客

Mathematics in Lean 导读

8分钟阅读

Mathematics in Lean 导读

教程简介

Mathematics in Lean 是 Lean 4 + Mathlib 官方数学形式化教程。通过 13 章内容，从零基础到高级主题（拓扑、微积分、测度论），教你用 Lean 证明数学定理。

本仓库的伴读文档是对原教程的深度补充：每章伴读包含核心洞见、完整代码示例、常见陷阱警告、证明模板和学习策略。建议先通读原章节，再读伴读深化理解。

📖 文档使用指南

文档类型内容用法
C##_*.md原教程翻译主体学习内容
##-Chapter*-伴读.md深度伴读查漏补缺、快速回顾、考前复习

高效学习流程

  1. 第一遍：读原教程章节，完成 sorry 练习
  2. 第二遍：读伴读文档，关注「核心洞见」和「常见陷阱」
  3. 复习时：直接看伴读的「核心概念总结表」和「自测问题」

🎯 学习目标

完成本教程后，你将能够：

  • 用 Lean 4 编写数学定义和定理
  • 使用 tactic 系统构造证明
  • 理解依赖类型理论的基础
  • 使用 Mathlib 库中的数学对象和定理

📋 前置要求

要求说明
数学基础高中数学即可起步，大学数学更好
编程经验不需要，但有帮助
Lean 知识零基础

环境准备

  1. 安装 Lean 4 + VS Code：安装指南
  2. 克隆仓库：git clone https://github.com/leanprover-community/mathematics_in_lean
  3. 在 VS Code 中打开，等待 Mathlib 缓存下载

🗺️ 学习路径

第一阶段：入门（1-2 周）

graph LR
    A[Ch1 入门] --> B[Ch2 基础]
    B --> C[Ch3 逻辑]
章节核心内容重点掌握
Ch1 入门Lean 基本概念、#check、#eval理解类型系统、tactic vs 证明项
Ch2 基础代数恒等式证明rw、ring、calc、apply
Ch3 逻辑量词、蕴含、否定intro、apply、exact、constructor

前三章无伴读

Ch1-3 内容较基础，原教程已足够清晰。遇到具体问题时直接查阅即可。

学习建议

  • 必做练习：每节的 sorry 练习是核心，不要跳过
  • 对比答案：完成练习后查看 solutions/ 目录
  • 善用 Goal 窗口：VS Code 的 Lean Goal 窗口会显示当前证明状态

第二阶段：中级（2-3 周）

graph LR
    D[Ch4 集合与函数] --> E[Ch5 数论]
    E --> F[Ch6 离散数学]
章节核心内容重点掌握
Ch4 集合与函数集合运算、函数性质ext、constructor、rcases
Ch5 初等数论整除、素数、归纳induction、omega、decide
Ch6 离散数学有限集合、计数Finset、Fintype、simp

Ch4-6 无伴读

集合论、数论和离散数学章节内容较自洽，原教程讲解充分。

[!warning] 常见卡点

  • Ch4 的 Schroeder-Bernstein 定理证明较难，可先跳过
  • Ch5 的归纳法需要多练习才能熟练

第三阶段：结构化（3-4 周）

graph LR
    G[Ch7 结构] --> H[Ch8 层级]
    H --> I[Ch9 群与环]
章节核心内容伴读重点重点掌握
Ch7 结构结构体定义伴读structure、@[ext]、class/instance、高斯整数
Ch8 层级类型类、继承伴读extends、to_additive、bad diamond、DFunLike
Ch9 群与环代数结构伴读子群构造、商群、中国剩余定理、多项式

核心概念

类型类 (Type Class) 是 Lean 组织数学结构的核心机制。理解 instance 和 extends 是掌握 Mathlib 的关键。

第四阶段：高级（按需学习）

章节核心内容伴读重点适用场景
Ch10 线性代数向量空间、线性映射伴读线性代数相关研究
Ch11 拓扑滤子、度量空间、拓扑空间伴读分析学基础
Ch12 微分学导数、范数空间伴读微积分形式化
Ch13 积分与测度论积分、测度伴读实分析、概率论

📚 伴读文档核心亮点

伴读核心洞见独家内容
Ch7 结构结构体 = 命名元组 + 约束高斯整数完整构造、Subtype vs Sigma、Coercion 机制
Ch8 层级extends 自动解决字段重叠to_additive 原理、bad diamond 详解、DFunLike/SetLike 设计
Ch9 群与环Monoid 是群和环的共同抽象共轭子群构造、中国剩余定理证明策略、多项式求值区别表
Ch10 线性代数V →ₗ[K] W 的 bundled 设计直和/直积泛性质、商空间、toMatrix 换基公式、维数公式
Ch11 拓扑滤子统一 512 种极限Tendsto 的代数证明、拓扑函子性、延拓定理
Ch12 微分学Fréchet 导数 = 最佳线性逼近Banach-Steinhaus、ContDiff 等级、反函数定理
Ch13 积分测度Bochner 积分统一向量值积分控制收敛、Fubini、Haar 测度换元

何时读伴读？

  • 学前：快速浏览「核心洞见」和「自测问题」，建立预期
  • 学中：遇到困惑时查伴读的「常见陷阱」和「学习策略」
  • 学后：用「核心概念总结表」做笔记和复习

🔧 核心 Tactic 速查表

基础 Tactic（Ch1-3）

Tactic用途示例
rw重写目标rw [mul_comm a b]
ring自动证明代数恒等式ring
simp自动简化simp [mul_assoc]
apply应用定理apply mul_le_mul
exact精确匹配exact h
intro引入假设intro x hx
constructor分解合取/双蕴含constructor
rcases模式匹配分解rcases h with ⟨a, b⟩

进阶 Tactic（Ch4+）

Tactic用途示例
ext扩展性证明ext x
induction归纳证明induction n with | zero => ... | succ n ih => ...
omega线性算术omega
decide可判定命题decide
use提供存在见证use 42
obtain提取证明obtain ⟨n, hn⟩ := h

计算 Tactic

Tactic用途
norm_num数值计算
linprog线性规划
polyrith多项式证明

💡 学习技巧

1. 善用 sorry 占位

-- 先写好框架，再逐步填充
theorem my_theorem : ... := by
  intro x
  sorry  -- 先占位，确保类型正确

2. 分步证明

-- 用 have 分解复杂证明
theorem complex : ... := by
  have h1 : ... := by sorry
  have h2 : ... := by sorry
  exact combine h1 h2

3. 查看 Mathlib 文档

  • 在线搜索：Mathlib Docs
  • VS Code 中：Ctrl+Shift+P → Lean 4: Show Documentation Resources

4. 使用 Lean Zulip

遇到问题？Lean Zulip Chat 社区非常友好，随时可以提问。

📚 配套资源

资源链接
在线教程Mathematics in Lean
Mathlib 文档Mathlib4 Docs
定理证明入门Theorem Proving in Lean 4
社区论坛Lean Zulip
GitHub 仓库mathematics_in_lean

⏱️ 推荐学习计划

阶段时间内容每日练习
入门1-2 周Ch1-32-3 个练习
中级2-3 周Ch4-63-4 个练习
结构化3-4 周Ch7-92-3 个练习
高级按需Ch10-13根据兴趣选择

坚持就是胜利

Lean 的学习曲线较陡，但一旦掌握 tactic 系统，你会发现它比手写证明更高效。坚持每天练习，你会很快上手！

最后更新：2026-04-26

关系图谱

反向链接