简介

计算机和定理证明

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

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

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

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

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

Lean 的底层逻辑有一个计算的解释，与此同时 Lean 可以被视为一种编程语言。 更重要的是，它可以被看作是一个编写具有精确语义的程序的系统， 以及对程序所表示的计算功能进行推理。Lean 中也有机制使它能够作为它自己的 元编程语言， 这意味着你可以使用 Lean 本身实现自动化和扩展 Lean 的功能。 Lean 的这些方面将在本教程的配套教程 Lean 4函数式编程中进行探讨，本书只介绍计算方面。

关于 Lean

Lean 项目由微软 Redmond 研究院的 Leonardo de Moura 在 2013 年发起，这是个长期项目， 自动化方法的潜力会在未来逐步被挖掘。Lean 是在 Apache 2.0 许可协议 下发布的， 这是一个允许他人自由使用和扩展代码和数学库的许可性开源许可证。

通常有两种办法来运行Lean。第一个是网页版本： 由 JavaScript 编写，包含标准定义和定理库，编辑器会下载到你的浏览器上运行。 这是个方便快捷的办法。

第二种是本地版本：本地版本远快于网页版本，并且非常灵活。Visual Studio Code 和 Emacs 扩展模块给编写和调试证明提供了有力支撑，因此更适合正式使用。 源代码和安装方法见https://github.com/leanprover/lean4/.

本教程介绍的是 Lean 的当前版本：Lean 4。

关于本书

本书的目的是教你在 Lean 中编写和验证证明，并且不太需要针对 Lean 的基础知识。首先，你将学习 Lean 所基于的逻辑系统，它是 依值类型论（Dependent type theory） 的一个版本，足以证明几乎所有传统的数学定理，并且有足够的表达能力自然地表示数学定理。更具体地说，Lean 是基于具有归纳类型（Inductive type）的构造演算（Calculus of Construction）系统的类型论版本。Lean 不仅可以定义数学对象和表达依值类型论的数学断言，而且还可以作为一种语言来编写证明。

由于完全深入细节的公理证明十分复杂，定理证明的难点在于让计算机尽可能多地填补证明细节。 你将通过依值类型论语言来学习各种方法实现自动证明，例如项重写， 以及 Lean 中的项和表达式的自动简化方法。同样，繁饰（Elaboration） 和 类型推断（Type inference） 的方法，可以用来支持灵活的代数推理。

最后，你会学到 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 证明器和 Lean 社区。