关于本课程的任何交流，请加群776491665
催更请加群（
因为我自己在学习Lean的过程中，感觉自己的逻辑思维、抽象思维都被重塑了，收获非常大，并且对形式化证明产生了非常浓厚的兴趣。
但是Lean语言十分抽象、需要的基础知识零散，尤其是对于非数学专业（比如我这样计算机专业出身）的人来说，入门存在一定的困难。
官网虽然有几本相当不错的书，但实际上这些书并未覆盖足够多的领域，读完这几本书只能算是入了个门，几乎不能把Lean用于实际问题中。
主要是课程规划、资料汇集、文档、习题。
- 课程规划：建议先学什么，后学什么，有哪些前置的基础知识 等等。
- 资料：包括其他来源的 书、文档、视频 等等等等。
- 文档：我会把部分关键、重要的知识进行整理，方便复习、搜索易错点，以及解答一些常见的疑惑。当然文档可能需要持续的迭代和维护，它未必完整，也未必总是对的。
- 习题：可能是来自于其他书 或各种渠道的问题，进行一定的改编或汇编。
站在程序员的角度，我觉得Lean至少给我带来了这样几方面的变化：
- TDD的范式教会了很多人“面向巧合”编程，很多时候会被误解为 “覆盖率100%就是正确” 。而学Lean的过程可以重新理解什么是“正确”，再一次训练严谨的思考方式。
- 在很多更困难、复杂的工程领域，比如操作系统、数据库、密码安全，“错误没有被发现”是不够安全的，所以采用形式化证明论证“没有错误”是一个非常值得去做的工作。
- 另一方面Lean带着我从另一个角度复习了数学的各个分支领域，让我以代码的方式再次感受到证明的美妙。而且最酷的地方是，如果你做的是对的，编译器会告诉你，而不需要一个老师来帮你检查。如果你做的有遗漏，编译器会帮助你发现。
从实用的角度，今年Lean的关注陡然提升，一个很重要的原因是因为AI的推动。
- 非形式化的数学，一个最大的问题在于 验证一个过程是否正确。 依靠肉眼检查 你只能说“我没发现它的错误”。而且肉眼检查的成本非常高，对专业度的要求也非常高。
- 如果你想借助AI来帮助你完成一些数学工作，尤其是超出你自己能力的数学工作，你怎么知道AI做的是正确的而不是在胡说八道呢？
- Lean（或其他形式化工具）大大降低了验证一个证明的成本——只需要它通过编译。
- 另一方面，交互式证明 或类似的方式，可以给AI创造一个非常有效的“环境”，AI的每一步行动的正确性都可以很容易的被评估，这是一种对强化学习(RL)非常友好的场景
- 我个人相信未来实用化的数学AI，应该是在强化学习的环境中训练出来的。
- 而在所有形式化工具中，Lean是现在生态最好、易用度最好、也是被AI圈广泛使用的（包括DeepSeek-Prover、Project Numina等相当多的AI for math都是基于Lean的）
我正在试图编写一个系统的学习路径。
在此之前，你可以从Theorem Proving in Lean或者它的中文版 开始。
如果一切顺利，并且进度超过我整理学习路径的进度，那么可以继续Mathematics in Lean或它的中文版
我推荐先跳过另一本Functional Programming in Lean，这本书虽然包括了一些和证明有关的内容，但更主要是在讨论函数式编程相关的部分。如果是以学会证明为目标，并不一定要读懂这本书。
如果你打算学习元编程，比如想要自定义tactic 或者做一些其他很酷的事情，那么学习FP是必要的，你可以先读上面这本书，再去读Metaprogramming in Lean 4
你可以关注我课程的更新进度，以及看看我补充的一些信息。
建议的阅读顺序：以章节为单位，先读导读->读原书->做原书习题（如果有）->再读补充阅读->再做补充习题
- 环境配置
- Theorem Proving in Lean 4
- 了解到为什么我们认为形式化了的证明就可以认为是正确的。
- 学习一些基础的证明方法，并尝试用于一些简单逻辑命题的证明。
- 了解到一些在证明过程中也会用到的Lean编程基础，比如枚举类型、结构体等等
- Mathmatics in Lean 4
- 具体领域的定义和定理熟悉
- 必学
- 集合论
- 自然数
- 有理数，实数
- 抽象代数：群、环、域等
- 选学
- 组合数学
- 高等数学
- 数论
- 概率论、测度论
- 几何
- 线性代数
- 多项式
- 计算理论
- 控制论
- 信息论
- 拓扑学
- 图论
- 算法
- （还有一些其他的，后续随更新补充）
- 必学