9.1. "学习 Lean"🔗

Lean 4 本身在以下资源中有详细描述：

• Lean 4 定理证明 是一篇使用 Lean 编写证明的教程。

• Lean 4 手册 提供了对语言及其特性的详细描述。

• 怎样用 Lean 证明数学题 是一篇 Lean 支持的配套书籍 怎样证明数学题 的介绍，提供了编写纸笔数学证明的入门。

• Lean 4 元编程 提供了对 Lean 扩展机制的概览，从中缀运算符和记号到宏、自定义策略，甚至完整的自定义嵌入式语言。

• Lean 4 函数式编程 可能对喜欢递归笑话的读者感兴趣。

继续学习 Lean 的最佳方式是开始阅读和编写代码，在遇到困难时查阅文档。此外， Lean Zulip 是结识其他 Lean 用户、寻求帮助和帮助他人的好地方。

9.2. Lean 形式化数学🔗

数学学习资源广泛分布在 社区网站 上。

9.3. 在计算机科学中使用依值类型🔗

Rocq 是一种与 Lean 有许多共同点的语言。对于计算机科学家来说， 《软件基础》系列教材提供了一个很好的介绍， 介绍了 Rocq 在计算机科学中的应用。Lean 和 Rocq 的基本思想非常相似， 编程技巧在两个语言之间是可以相互转换的。

9.4. 使用依值类型编程🔗

对有兴趣学习使用索引族和依值类型来结构化程序的程序员来说，Edwin Brady 的 Type Driven Development with Idris 提供了一个很好的介绍。像 Rocq 一样，Idris 是 Lean 的近亲，尽管它缺乏策略。

9.5. 理解依值类型🔗

The Little Typer 是一本为没有正式学习过逻辑或编程语言理论，但希望理解依值类型论核心思想的程序员准备的书。虽然上述所有资源都旨在实现尽可能的实用，但这本书通过从头开始构建基础，使用仅来自编程的概念来呈现依值类型理论的方法。

免责声明：《Lean 4 函数式编程》的作者也是 The Little Typer 的作者之一。