引言

计算机与定理证明

形式验证涉及使用逻辑和计算方法来建立以确切的数学术语表达的声明。这些声明可以包括普通的数学定理，以及硬件或软件、网络协议、机械和混合系统符合其规范的声明。实际上，验证数学内容和验证系统正确性之间没有明确的界限：形式验证要求用数学术语描述硬件和软件系统，这时验证其正确性就变成了定理证明的一种形式。相反，数学定理的证明可能需要进行漫长的计算，这种情况下验证定理的真实性就需要验证计算是否按照预期进行。

支持数学断言的黄金标准是提供一个证明，在逻辑学的20世纪发展中，表明大多数，如果不是所有传统证明方法都可以归约为若干基础系统中的一小组公理和规则。通过这种归约，计算机可以帮助建立一个声明的两种方式：它可以帮助寻找一个证明，也可以帮助验证一个所谓的证明是正确的。

自动定理证明专注于“寻找”方面。解析定理证明器、表格定理证明器、快速可满足性求解器等提供了在命题和一阶逻辑中建立公式有效性的方法。其他系统提供了针对特定语言和领域的搜索和决策过程，比如整数或实数上的线性或非线性表达式。像SMT（“可满足性模理论”）这样的体系结构结合了领域通用的搜索方法和领域特定的过程。计算机代数系统和专业的数学软件包提供了进行数学计算、建立数学边界或找到数学对象的方法。计算也可以看作是一种证明，这些系统也有助于建立数学断言。

自动推理系统追求强大和高效，常常以可靠性的代价。这些系统可能存在错误，很难确保它们提供的结果是正确的。相反，交互定理证明注重定理证明的“验证”方面，要求每个断言都必须有一个适当公理的证明来支持。这设置了一个非常高的标准：每个推理规则和每个步骤都必须经过证明，否则就无法接受。 为了证明计算的正确性，必须依据先前的定义和定理，一直追溯到基本公理和规则。事实上，大多数这样的系统提供了完整的“证明对象”，可以传递给其他系统进行独立检查。构建这样的证明通常需要用户提供更多的输入和交互，但它允许您获得更深入和更复杂的证明。

Lean 定理证明器旨在弥合交互式和自动化定理证明之间的差距，通过将自动化工具和方法置于支持用户交互和构建完全规范化的公理证明的框架中。其目标是支持数学推理和复杂系统的推理，并验证在这两个领域中的断言。

Lean 的基本逻辑具有计算解释，因此 Lean 可以被看作一种编程语言。更重要的是，它可以被看作是一种具有精确语义的编写程序的系统，以及对程序计算的函数进行推理。Lean 还具有作为其自己的元编程语言的机制，这意味着可以使用 Lean 实现自动化，并使用 Lean 扩展 Lean 的功能。Lean 的这些方面在与本教程相伴的教程中进行了探讨，即在 Lean 4 中编程，尽管该系统的计算方面也会在这里出现。

关于 Lean

Lean 项目由 Leonardo de Moura 在2013年于微软研究院 Redmond 发起。这是一个持续的、长期的努力，其中大部分自动化的潜力只会逐渐实现。Lean 以Apache 2.0 许可证发布，这是一种自由的开源许可证，允许其他人自由使用和扩展代码和数学库。

要在计算机上安装 Lean，请使用快速入门指南。Lean 的源代码和构建 Lean 的说明可在https://github.com/leanprover/lean4/找到。

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

关于本书

本书旨在教你在 Lean 中开发和验证证明。您将获得大部分背景信息， 为了完成这个任务，你需要掌握的知识并不仅限于 Lean 本身。首先，你将学习 Lean 所基于的逻辑系统，它是一个强大到可以证明几乎任何传统数学定理，同时又以自然方式表达这些定理的 依赖类型论 的版本。具体来说，Lean 是基于一个被称为带递归类型的构造演算的版本。Lean 不仅能够定义数学对象并在依赖类型论中表达数学断言，还可以作为写证明的语言。

由于完整的公理证明过程非常复杂，证明定理的挑战在于让计算机尽可能填充尽可能多的细节。你将学习各种支持这一过程的方法，包括依赖类型论中的术语重写、Lean 的自动化方法来简化术语和表达式，以及支持灵活形式的代数推理的规范化和类型推断方法。

最后，你还将学习一些 Lean 特有的功能，包括与系统交互的语言以及 Lean 提供的管理复杂理论和数据的机制。

在整个文本中，你会找到类似下面这样的 Lean 代码示例：

theorem and_commutative (p q : Prop) : p ∧ q → q ∧ p :=
  fun hpq : p ∧ q =>
  have hp : p := And.left hpq
  have hq : q := And.right hpq
  show q ∧ p from And.intro hq hp

如果您在 VS Code 中阅读这本书，您会看到一个名为 "try it!" 的按钮。点击这个按钮会将示例代码复制到编辑器中，并提供足够的上下文使代码正确编译。您可以在编辑器中输入内容并修改示例代码，Lean 会在您输入时持续检查结果并提供反馈。我们建议您在阅读后继章节时运行示例并尝试自己编写代码。您可以使用命令 "Lean 4: Open Documentation View" 在 VS Code 中打开本书。

致谢

本教程是一个在 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 以获取我们杰出贡献者的最新列表。