翻译-TPIL-01-简介

1.1. 计算机和定理证明 Computers and Theorem Proving

形式验证（Formal Verification）涉及到用逻辑和计算方法 去验证那些由精确的数学术语所描述的命题。这些命题既可以是 普通的数学定理，也可以是 那些声称软硬件、网络协议以及机械和混合系统满足某些特定性质的形式命题。 在实践中，验证数学命题与验证系统的正确性似乎并无太多差异： 形式验证用数学术语描述硬件和软件系统并以此为基础确立命题的正确性——正如证明定理一样；相反 一个数学定理的证明可能需要冗长的计算，此时要验证该定理的真实性就需要验证这段计算是否按预期运行。

支撑一个数学命题的“黄金标准”便是提供一个证明；二十世纪的逻辑学进展发现 绝大多数传统的证明方法都可以化简为若干基础系统中的一小套公理和规则。 有了这种化简，计算机便有两种方式来确立一个命题： ①它可以辅助寻找一个证明， ②它可以辅助验证一个所谓的证明是正确的。

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

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

Lean 定理证明器则致力于 弥合交互式定理证明器和自动定理证明系统之间的鸿沟： 实现方式是将自动化工具与方法整合进一个 既支持用户交互， 又允许构造完全形式化的证明的框架之中。 lean 的目标是 同时支持数学/复杂系统的推理， 并且能验证这两个领域的命题。

Lean 的底层逻辑有一个计算性的解释，因此 Lean 也可被视作一种编程语言；具体一点说， Lean 是一个特殊的系统，既可以 编写具有精确语义的程序，又可以 对这些程序所计算的函数进行推理。此外 Lean 还具备某些机制使得其可作为自身的元编程语言—— 这意味着你可以使用 Lean 本身来实现自动化并扩展 Lean 的功能。 诸多特性将在本教程的配套教程《Lean 4 函数式编程》中进行探讨， 而本书只介绍计算方面的内容。

1.2. 关于 Lean About Lean

Lean 项目由微软 Redmond 研究院的 Leonardo de Moura 在 2013 年发起， 这是一个持续进行的长期项目，其自动化的潜力将会在未来被逐步挖掘。 Lean 的发行基于 Apache 2.0 ——这是一个宽松的开源许可证，允许他人自由地使用和扩展代码和数学库的许可性开源许可证。

想在本地电脑上安装 Lean 请见 快速入门说明。 Lean 的源代码以及构建（编译）指南请见 https://github.com/leanprover/lean4/。

这份教程介绍的是 Lean 的当前版本，即 Lean 4。

1.3. 关于本书 About this Book

本书的初衷是教会你如何在 Lean 中编写和验证证明， 而实现这一切并不需要太多 Lean 所特有的前置知识 作为开始，你将学习 Lean 所基于的逻辑系统——一个 依值类型论（Dependent type theory）的变体： 其强大的能力足以证明几乎所有传统意义上的数学定理，而 其丰富的表达力则可使这些证明能以一种自然的方式来实现。 具体来说，Lean 基于一种被称为 带归纳类型的构造演算（Calculus of Constructions with inductive types）的系统变体。 Lean 不仅可以 定义数学对象、 用依值类型论表达数学断言，还可以 作为一种语言来编写证明。

完全展开的公理化证明会十分复杂，因此 定理证明的挑战在于让计算机尽可能多地填补证明细节。 你将学习一系列在依值类型论中实现此目标的方法，如 项重写以及自动化简 Lean 中的项/表达式；此外 用于 繁饰（Elaboration）和 类型推断（*Type inference） 的方法可以允许更灵活的代数推理形式。

最后你会学到 Lean 的一些特性，包括 你与系统交流时所使用的语言，以及 Lean 对复杂理论和数据的管理机制。

贯穿全文你将经常看到如下的 Lean 代码片段：

1
2
3
4
5

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

在每个代码示例旁边你都会看到一个标有“Copy to clipboard”（复制到剪贴板）的图标： 点击按钮后示例代码便会被复制下来，并附带足够的语境信息以使得代码可以被正常编译。 你可以将这些示例代码粘贴到 VS Code 中进行修改， Lean 会在你输入的过程中持续检查代码并提供反馈。 我们建议您在阅读后面的章节时亲自运行示例并试验代码。 你还可以在 VS Code 中打开本书—— 执行命令“Lean 4: Docs: Show Documentation Resources” 然后在弹出的选项卡中选择“Theorem Proving in Lean4”即可。

1.4. 致谢 Acknowledgments

本教程是一项开放源代码项目，在 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 社区。