这个仓库用于快速了解 Lean 定理证明的入门介绍。目标是在 2 到 3 小时内感受一下 Lean 的证明过程是什么样的。在阅读 Introduction.lean 文件后，你应该阅读 Basics 文件夹中的解释和练习，然后从 Topics 文件夹中选择一个文件进行学习。当然，如果你有更多的时间，你可以尝试文件夹中的所有文件。
要使用 Lean，可以选择在本地安装，使用 Codespaces 或者 Gitpod。
- 要使用 codespaces，确保已经登录到 Github，点击下面的按钮，选择
4-core，然后按Create codespace。几分钟之后，你的浏览器将打开一个已经配置好 Lean 的编辑器。
- Gitpod 与 Codespaces 非常相似，点击下面的按钮，按
Continue并稍等几分钟。
- 要在本地安装 Lean, 可以按照 这里 的说明进行。
如果你有更多的时间，你应该阅读 Mathematics in Lean 这本书。
此外，https://live.lean-lang.org/ 提供了在线的 Lean 编辑器，可以用来练习 Lean 代码。