Lean 4 交互式中文教程
零基础入门形式化证明 —— 在浏览器里写数学证明，无需安装任何软件。
已学 0 / 18 课全中文界面
怎么使用这个教程？
1.选择一个课程，阅读左侧的知识讲解和证明目标。
2.在右侧编辑器中编写 Lean 证明代码，点击 运行 ▶ 按钮提交。
3.根据反馈修改代码，直到看到 ✅ 证明通过！ 即可进入下一课。
提示：每课编辑器里已经预先写好了部分代码。你需要在
by 后面填入证明策略。不会写？看看左侧的提示和参考解答。第 1 课
欢迎来到 Lean
什么是形式化证明？Lean 能做什么？在浏览器中体验你的第一个证明。
第 2 课
类型与命题
一切皆有类型。理解 Type 和 Prop，学会用 rcases 拆解「且」。
第 3 课
蕴涵与全称量词
学习 intro 处理 ∀ 和 →，掌握最核心的证明策略。
第 4 课
合取与双向蕴涵
学习 constructor、⟨⟩ 构造策略，掌握 ↔ 的证明方法。
第 5 课
归纳法入门
数学归纳法的形式化：induction 策略、rfl 和 rw 重写。
第 6 课
析取：「或」的逻辑
学习 left、right 策略，用 rcases 分情况讨论 ∨。
第 7 课
存在量词：有没有这样的东西？
学习 refine 策略，用「见证」证明 ∃ 命题。
第 8 课
apply：反向推理的艺术
学会从目标反推——apply 把大目标拆成小目标。
第 9 课
simp：让机器帮你化简
用 simp 智能化简等式，巩固归纳法。比手动 rw 更省力。
第 10 课
否定与反证法
理解 ¬ P = P → False。掌握换质换位律和反证法的形式化。
第 11 课
集合的基本操作
进入集合论！学会 Set 类型、∈、⊆，用 intro 展开集合关系。
第 12 课
集合的运算与性质
学习 ∪ 和 ∩，用 ext 策略证明集合相等，证明交集的交换律。
第 13 课
函数与映射
掌握 Injective、Surjective、Bijective 的定义，学会 have 策略。
第 14 课
群的定义与基本性质
进入群论！手动定义群结构，用 calc 块做等式推导，证明逆元的性质。
第 15 课
子群与子群判定
定义 IsSubgroup，学会 refine ⟨?_, ?_⟩ 策略，证明子群的交集仍是子群。
第 16 课
群的更多性质
证明左消去律，体验群论证明的「舞蹈」——插单位元、插逆元、重结合。
第 17 课
环的定义与基本性质
进入环论！两个运算 + 分配律。证明 0 * a = 0 这个看似平凡却关键的结论。
第 18 课
环的更多性质
最后一课！证明 (-a) * b = -(a * b)，完成从命题逻辑到抽象代数的旅程。