1.1. 计算机和定理证明🔗

形式验证（Formal Verification） 是指使用逻辑和计算方法来验证用精确的数学术语表达的命题。 这包括普通的数学定理，以及硬件或软件、网络协议、机械和混合系统中的形式命题。 在实践中，验证数学命题和验证系统的正确性之间很类似：形式验证用数学术语描述硬件和软件系统， 在此基础上验证其命题的正确性，这就像定理证明的过程。相反，一个数学定理的证明可能需要冗长的计算， 在这种情况下，验证定理的真实性需要验证计算过程是否出错。

二十世纪的逻辑学发展表明，绝大多数传统证明方法可以化为若干基础系统中的一小套公理和规则。 有了这种简化，计算机能以两种方式帮助建立命题：1）它可以帮助寻找一个证明， 2）可以帮助验证一个所谓的证明是正确的。

自动定理证明（Automated theorem proving） 着眼于“寻找”证明。 归结原理（Resolution） 定理证明器、表格法（tableau） 定理证明器、 快速可满足性求解器（Fast satisfiability solvers） 等提供了在命题逻辑和一阶逻辑中验证公式有效性的方法； 还有些系统为特定的语言和问题提供搜索和决策程序， 例如整数或实数上的线性或非线性表达式； 像 SMT（Satisfiability modulo theories，可满足性模理论） 这样的架构将通用的搜索方法与特定领域的程序相结合； 计算机代数系统和专门的数学软件包提供了进行数学计算或寻找数学对象的手段， 这些系统中的计算也可以被看作是一种证明，而这些系统也可以帮助建立数学命题。

自动推理系统努力追求能力和效率，但往往牺牲稳定性。这样的系统可能会有 bug， 而且很难保证它们所提供的结果是正确的。相比之下，交互式定理证明器（Interactive theorem proving） 侧重于“验证”证明，要求每个命题都有合适的公理基础的证明来支持。 这就设定了非常高的标准：每一条推理规则和每一步计算都必须通过求助于先前的定义和定理来证明， 一直到基本公理和规则。事实上，大多数这样的系统提供了精心设计的“证明对象”， 可以传给其他系统并独立检查。构建这样的证明通常需要用户更多的输入和交互， 但它可以让你获得更深入、更复杂的证明。

Lean 定理证明器 旨在融合交互式和自动定理证明， 它将自动化工具和方法置于一个支持用户交互和构建完整公理化证明的框架中。 它的目标是支持数学推理和复杂系统的推理，并验证这两个领域的命题。

Lean 的底层逻辑具有计算解释，Lean 同样可以被视为一种编程语言。 更重要的是，它可以被视为一个编写具有精确语义的程序的系统， 以及推理程序计算的函数的系统。Lean 还有机制作为其自己的 元编程语言（metaprogramming language）， 这意味着你可以使用 Lean 本身来实现自动化并扩展 Lean 的功能。 Lean 的这些方面在免费在线书籍 Functional Programming in Lean （译本Lean 4 函数式编程）中有描述， 尽管系统的计算方面也会在这里出现。

1.2. 关于 Lean🔗

Lean 项目由 Leonardo de Moura 于 2013 年在微软雷德蒙德研究院启动。 这是一个持续的、长期的工作，许多自动化的潜力只会随着时间的推移逐渐实现。 Lean 在 Apache 2.0 许可证 下发布，这是一个宽松的开源许可证， 允许他人自由使用和扩展代码及数学库。

要在您的计算机上安装 Lean，请考虑使用 快速入门 说明。（中文版见Lean 4 安装指南） Lean 源代码和构建 Lean 的说明可在 https://github.com/leanprover/lean4/ 获得。

本教程描述了 Lean 的当前版本，即 Lean 4。

1.3. 关于本书🔗

本书旨在教您在 Lean 中开发和验证证明。为此所需的大部分背景信息并非 Lean 特有的。 首先，您将学习 Lean 基于的逻辑系统，即 依赖类型理论（dependent type theory） 的一个版本， 它足够强大，可以证明几乎任何传统的数学定理，并且足够富有表现力，可以以自然的方式进行证明。 更具体地说，Lean 基于一种称为带归纳类型的构造演算（Calculus of Constructions with inductive types）的系统。 Lean 不仅可以在依赖类型理论中定义数学对象和表达数学断言，还可以用作编写证明的语言。

因为完全详细的公理化证明非常复杂，定理证明的挑战在于让计算机尽可能多地填充细节。 您将在 依值类型论 中学习支持这一点的各种方法。 例如，项重写，以及 Lean 自动简化项和表达式的自动化方法。 同样，还有 繁饰（elaboration） 和 类型推断（type inference） 的方法， 可用于支持灵活形式的代数推理。

最后，您将了解 Lean 特有的功能，包括您用于与系统通信的语言，以及 Lean 提供的用于管理复杂理论和数据的机制。

在整本书中，您会发现像下面这样的 Lean 代码示例：

在本书中的每个代码示例旁边，您都会看到一个写着“Copy to clipboard”的按钮。 按下该按钮会复制示例以及足够的周围上下文，以使代码正确编译。 您可以将示例代码粘贴到 VS Code 中并修改示例，Lean 将检查结果并在您键入时不断提供反馈。 我们建议您在阅读后续章节时运行示例并自己尝试代码。 您可以使用命令“Lean 4: Docs: Show Documentation Resources”并在打开的选项卡中选择“Theorem Proving in Lean 4”在 VS Code 中打开本书。

1.4. 致谢🔗

本教程是一个在 Github 上维护的开放获取项目。许多人为这项工作做出了贡献，提供了更正、建议、示例和文本。 我们感谢 Ulrik Buchholz, Kevin Buzzard, Mario Carneiro, Nathan Carter, Eduardo Cavazos, Amine Chaieb, Joe Corneli, William DeMeo, Marcus Klaas de Vries, Ben Dyer, Gabriel Ebner, Anthony Hart, Simon Hudon, Sean Leather, Assia Mahboubi, Gihan Marasingha, Patrick Massot, Christopher John Mazey, Sebastian Ullrich, Floris van Doorn, Daniel Velleman, Théo Zimmerman, Paul Chisholm, Chris Lovett, 和 Siddhartha Gadgil 的贡献。 请参阅 lean prover 和 lean community 以获取我们出色的贡献者的最新列表。