简介
Lean 是一个基于依值类型论（Dependent Type Theory）的交互式定理证明器。 它最初由微软研究院开发，现在由 Lean FRO 负责开发。 依值类型论将程序和证明的世界统一了起来，因此，Lean 也是一门编程语言。 Lean 认真对待其双重性质，并被设计为适合用作通用编程语言——Lean 甚至是用它自己实现的。 本书旨在介绍如何使用 Lean 编写程序。
作为一门编程语言，Lean 是一种具有依值类型的严格纯函数式语言。 学习使用 Lean 编程很大一部分内容在于学习这些属性是如何影响程序编写方式的， 以及如何像函数式程序员一样思考。
-
严格性（Strictness） 意味着 Lean 中的函数调用与大多数语言中的工作方式类似： 在函数体开始运行之前，参数会被完全计算。
-
纯粹性（Purity） 意味着 Lean 程序除非明确声明，否则无法产生副作用， 例如修改内存中的位置、发送电子邮件或删除文件等。 Lean 是一种 函数式（Functional） 语言，这意味着函数就像任何其他值一样是一等值， 并且执行模型受数学表达式的求值启发。
-
依值类型（Dependent type） 是 Lean 最不寻常的特性，它使类型成为语言的一等部分， 允许类型包含程序，而程序计算类型。
本书面向想要学习 Lean 的程序员，但未必以前使用过函数式编程语言。 读者不需要熟悉 Haskell、OCaml 或 F# 等函数式语言。而另一方面，本书确实假定读者了解循环、 函数和数据结构等大多数编程语言中的常见概念。虽然本书旨在成为一本关于函数式编程的优秀入门书， 但它并不是一本关于一般编程的入门书。
对于将 Lean 作为证明助手的数学家来说，他们可能需要在某个时间点编写自定义的证明自动化工具， 本书也适用于他们。随着这些工具变得越来越复杂，它们也会越来越像函数式语言编写的程序， 但大多数在职数学家接受的是 Python 和 Mathematica 等语言的培训。 本书可以帮助他们弥合这一差距，让更多数学家能够编写可维护且易于理解的证明自动化工具。
本书旨在从头到尾线性阅读。概念一次引入一个，后面的章节会假定读者熟悉前面的章节。 有时，后面的章节会深入探讨一个之前仅简要讨论过的主题。本书的某些章节包含练习。 为了巩固你对该章节的理解，这些练习值得一做。在阅读本书时探索 Lean 也很有用， 可以发现能利用你所学知识的创造性新方法。
获取 Lean
在编写并运行 Lean 所编写的程序之前，你需要在自己的计算机上设置 Lean。Lean 工具包括以下内容：
-
elan：用于管理 Lean 编译器工具链，类似于rustup或ghcup。 -
lake：用于构建 Lean 包及其依赖项，类似于cargo、make或 Gradle。 -
lean：用于对 Lean 文件进行类型检查和编译，并向程序员工具提供当前正在编写的文件的相关信息。 通常，lean是由其他工具而非用户直接调用的。 -
编辑器插件，如 Visual Studio Code 或 Emacs，可与
lean通信并方便地显示其信息。
有关安装 Lean 的最新说明，请参阅 Lean manual。
排版约定
作为 输入 提供给 Lean 的代码示例格式如下：
def add1 (n : Nat) : Nat := n + 1#eval add1 7
上面最后一行（以 #eval 开头）是指示 Lean 计算答案的命令。Lean 的回复格式如下：
Lean 返回的错误消息格式如下：
警告格式如下：
Unicode字符
惯用的 Lean 代码会使用各种不属于 ASCII 的 Unicode 字符。例如，希腊字母（如 α 和 β）
和箭头（→）都出现在本书的第一章中。这使得 Lean 代码更接近于普通的数学记法。
在默认的 Lean 设置中，Visual Studio Code 和 Emacs 都允许使用反斜杠（\）后跟名称来输入这些字符。
例如，要输入 α，请键入 \alpha。要了解如何在 Visual Studio Code 中键入字符，
请将鼠标指向该字符并查看工具提示。在 Emacs 中，将光标置于相关字符上，然后使用 C-c C-k 即可查看提示。
发布历史
2025 年 10 月
本书已更新到最新的稳定 Lean 版本（版本 4.23.0），现在描述了函数归纳和 grind 策略。
2025 年 8 月
这是一个维护版本，用于解决从本书中复制粘贴代码的问题。
2025 年 7 月
本书已更新到 Lean 4.21 版本。
2025 年 6 月
本书已使用 Verso 重新格式化。
2025 年 4 月
本书已 extensively 更新，现在描述 Lean 4.18 版本。
2024 年 1 月
这是一个次要的错误修复版本，修复了示例程序中的一个回归问题。
2023 年 10 月
在此第一个维护版本中，修复了一些小问题，并根据 Lean 的最新版本更新了文本。
2023 年 5 月
本书现已完成！与 4 月的预发布版本相比，许多小细节得到了改进，并修复了小错误。
2023 年 4 月
此版本增加了关于使用策略编写证明的插曲，以及一个结合了性能和成本模型讨论与终止和程序等价证明的最终章节。 这是最终发布之前的最后一个版本。
2023 年 3 月
此版本增加了关于使用依赖类型和索引族编程的章节。
2023 年 1 月
此版本增加了关于单子转换器的章节，其中包括对 do-notation 中可用的命令式功能的描述。
2022 年 12 月
此版本增加了关于应用函子的章节，其中还更详细地描述了结构和类型类。 同时改进了对单子的描述。 由于冬季假期，2022 年 12 月的版本推迟到 2023 年 1 月发布。
2022 年 11 月
此版本增加了关于使用单子编程的章节。此外，强制转换部分中使用 JSON 的示例已更新，包含了完整的代码。
2022 年 10 月
此版本完成了类型类章节。此外，在类型类章节之前添加了一个简短的插曲，介绍了命题、证明和策略，因为对这些概念的少量熟悉有助于理解一些标准库类型类。
2022 年 9 月
此版本增加了类型类章节的前半部分，类型类是 Lean 重载运算符的机制，也是组织代码和构建库的重要手段。此外，第二章已更新，以适应 Lean 流 API 的变化。
2022 年 8 月
第三次公开发布增加了第二章，其中描述了程序的编译和运行以及 Lean 的副作用模型。
2022 年 7 月
第二次公开发布完成了第一章。
2022 年 6 月
这是第一次公开发布，包括引言和第一章的一部分。
关于作者
David Thrane Christiansen 使用函数式语言已有二十年，使用依赖类型已有十年。 他与 Daniel P. Friedman 合著了 The Little Typer，该书介绍了依赖类型理论的核心思想。 他拥有哥本哈根信息技术大学的博士学位。 在学习期间，他是 Idris 语言第一个版本的主要贡献者。 离开学术界后，他曾在俄勒冈州波特兰的 Galois 和丹麦哥本哈根的 Deon Digital 担任软件开发人员，并曾担任 Haskell 基金会的执行董事。 在撰写本书时，他受雇于 Lean Focused Research Organization，全职从事 Lean 的工作。
许可证
This work is licensed under a Creative Commons Attribution 4.0 International License.
本书的原始版本由 David Thrane Christiansen 受微软公司委托撰写，微软公司慷慨地将其以知识共享署名 4.0 国际许可协议发布。 当前版本已由作者在原始版本的基础上进行修改，以适应 Lean 新版本的变化。 有关更改的详细说明，请参阅本书的源代码仓库。