下一步

本书介绍了 Lean 中函数式编程的基本知识，包括一些互动定理证明的内容。 使用依值类型的函数式语言（如 Lean）是一个深奥的主题，内容丰富。 根据您的兴趣，以下资源可能对学习 Lean 4 有用。

学习 Lean

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

《Lean 4 定理证明》 是一本关于使用 Lean 编写证明的教程。 《Lean 4 手册》 提供了 Lean 语言及其功能的参考资料。虽然在撰写本文时它仍未完成， 但它比本书更详细地描述了 Lean 的许多方面。 《怎样用 Lean 证明数学题》是著名教材 《怎样证明数学题》的 Lean 版伴随读物， 介绍了如何编写纸笔数学证明。 《Lean 4 元编程》概述了 Lean 的扩展机制， 从中缀运算符和符号到宏、自定义策略和完整的自定义嵌入式语言。 《Lean 函数式编程》可能对喜欢递归笑话的读者来说很有趣。 然而，继续学习 Lean 的最佳方式是开始阅读和编写代码，在遇到困难时查阅文档。 此外，Lean Zulip 是结识其他 Lean 用户、 寻求帮助和帮助他人的好地方。

标准库

Lean 自带的库相对较小。Lean 是自托管的，所包含的代码仅够实现 Lean 本身。 对于许多应用来说，需要更大的标准库。

std4 是一个正在开发中的标准库， 包含许多数据结构、策略、类型类实例和函数，这些都超出了 Lean 编译器本身的范围。 要使用 std4，第一步是找到与您使用的 Lean 4 版本兼容的提交记录（即其中的 lean-toolchain 文件与您的项目匹配）。然后，将以下内容添加到您的 lakefile.lean 顶层， 其中 COMMIT_HASH 是适当的版本：

require std from git
  "https://github.com/leanprover/std4/" @ "COMMIT_HASH"

Lean 形式化数学

大多数数学资源是为 Lean 3 编写的。 在社区网站上可以找到许多这样的资源。 要开始在 Lean 4 中进行数学研究，最简单的方法可能是参与将数学库 mathlib 从 Lean 3 迁移到 Lean 4 的过程。 有关更多信息，请参阅 mathlib4 的 README.

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

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

使用依值类型编程

对于有兴趣学习使用索引族和依值类型来构建程序的程序员来说，Edwin Brady 的 《Idris 类型驱动开发》 提供了一个很好的介绍。和 Coq 一样，Idris 是 Lean 的近亲语言，但是它缺乏策略。

理解依值类型

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

免责声明：《Functional Programming in Lean》的作者也是《The Little Typer》的作者之一。