一时兴起，想尝试翻译一下《Theorem Proving in Lean》。Lean是一个计算机辅助进行数学证明的语言，我接触到了就觉得十分有意思。初学者十分推荐先游玩自然数游戏（虽然没翻译）。本文是Lean语言的入门教程。

• 引言
  • 计算机与定理证明
  • 关于Lean
  • 关于本书
  • 鸣谢

#引言

#计算机与定理证明

形式化验证是一种使用逻辑推理和计算，去推导用精准的数学术语表达的断言的方法。他们可能包括通常的数学定理，也可能并非通常的数学定理，例如声称一块硬件、一份软件、一条网络协议、或是机械系统、混合系统等等的系统满足所需的标准。在实践上，验证一条数学定理和验证系统的正确性之间并没有很尖锐的分隔线——形式化验证需要使用数学术语描述硬件与软件系统，验证它们的正确性在形式上就可以归结为证明一条定理。相反，证明一条数学定理可能需要冗长的计算，验证证明的正确性就需要验证这一计算过程是否做了它应该做的：也就是系统的正确性。

而支持一条断言的黄金法则就是提供一份证明。20世纪以来逻辑学的发展表明，大部分——如果不是全部——传统的证明方法可以被归结为在任何一个形式体系下很少的几条公理与法则。那么，计算机想要在这里辅助，就有两种方法：一是干脆用计算机来寻找定理的证明方式，二是用计算机帮助验证一个所谓的“证明”是否正确。

自动定理证明就专注于“寻找”这一方面。诸如消解式定理证明、tableau定理证明、快速可满足性求解器等等的工具为我们提供了使用命题逻辑和一阶逻辑来证明公式的方法。其他也有许多系统提供了在特定语言或领域内搜索或是决策的流程，例如整数上或是实数上的线性或非线性表达式。像SMT（satisfiability modulo theories，可满足性模理论）一样的架构，结合了通用领域的搜索方法与专用领域的流程。计算机代数系统和特化的数学软件包也为数学计算、建立上下界、或是寻找数学对象提供了工具。当然，数学计算也可以被视为证明的一种，而上面所说的系统，也同样可以帮助建立数学证明。

自动推理系统则争取的是能力与效率，而通常忽略了严谨性。这样的系统可能出错，也很难保证它们的结果是正确的。另一方面，交互式定理证明则专注于“验证”这一方面。它要求每一句断言都伴随着一个正确的、由公理支持的证明。这就给证明设定了很高的标准：每一条推理和每一步计算都要有之前所建立的定义或是定理的支持，直到最基本的公理和规则。事实上，大部分这样的系统都提供了充分建立好的“证明对象”，以建立系统与系统之间的联系，保证不同的系统之间可以独立地检查正确性。通常，建立这样的证明需要用户输入和交互更多的信息，但是它也让我们可以建立更深也更复杂的证明过程。

Lean Theorem Prover的目标则是填补交互性定理证明与自动化定理证明之间的空白。Lean在框架下，提供了一定程度上自动化的工具和方法，来支持用户的交互以及严谨的公理化证明。它的目标是同时支持数学上的推理，以及复杂系统的推理，在这两个领域都可以验证证明的正确性。

Lean的底层逻辑包含计算性的解释，它可以被看做一种编程语言。也就是说，它可以被看做一个使用精确语义来编写程序的系统，同样也是使用程序计算过程中的函数来推理。Lean也有一套机制使得它可以进行它自己的元编程，也就是说可以使用Lean扩展它自己的功能，实施自动化。在Lean中编程则是另一套与本书配套的教程，在那里会有对元编程更详细的说明，虽然这个系统中一部分计算方面的内容在本书中也会出现。

#关于Lean

Lean计划最早由Leonardo de Moura于2013年在Microsoft Research Redmond发起。这是个长程的、进行中的企划，而且其自动化的潜能只能慢慢地被大家所理解。Lean是在Apache 2.0开源协议下发布的。也就是说，它允许其他人自由地使用和拓展Lean的源码以及数学库。

目前，使用Lean有两种方式。第一种是使用Lean在线编辑器。在使用它的时候，你的浏览器会自动下载一个Javascript版本的Lean，一个包含定义和定理的标准库，以及一个编辑器。这提供了一个方便的快速上手的机会。

第二个方式则是将Lean安装到你的电脑上运行。这比在线版要快上许多，而且也更灵活。Visual Studio Code（简称VS Code）和Emacs里的特殊模式为书写和调试证明提供了强有力的帮助，也就更适合严肃的用途。Lean的源码和安装指南可以从这里获取。

本教程描述的是当前版本的Lean，也就是Lean 3。一个老版本Lean 2，对同伦类型论（HoTT）有着特殊支持。在这里你可以找到Lean 2和HoTT库。Lean 2的教程则在这里。 ## 关于本书

本书的目标是教你如何使用Lean来书写和验证证明。本书很多的背景知识都不止局限于Lean。我们会从解释Lean所基于的逻辑系统开始。这是一种版本的依赖类型论，它强大到足够以自然的方式证明几乎所有传统的数学定理。特别地，Lean是基于一个包含递归类型¹的Calculus of Constructions²系统。我们不止会讲解在依赖类型论中如何定义数学对象和描述数学表达式，也会讲解如何作为一种语言来使用它书写证明。

由于详细的公理化证明过于复杂，定理证明的一大挑战则是如何让计算机填补尽可能多的细节。我们会讲解一些方法来支持这一点。例如，我们会讨论项的重写，以及Lean用来自动简化项和表达式的方法。类似地，我们也会讨论细化与类型推导的方法。它们可以用来支持许多自由形式的代数推导。

最后，当然，我们也会讨论Lean特有的特性，包括你与系统之间交流所使用的语言，以及Lean提供的用以管理复杂理论和数据的机制。

环顾上下文，你会发现诸如下面这样的代码示例：

1
2
3
4
5

theorem and_commutative (p q : Prop) : p ∧ q → q ∧ p :=
assume hpq : p ∧ q,
have hp : p, from and.left hpq,
have hq : q, from and.right hpq,
show q ∧ p, from and.intro hq hp

试试！

如果你是在线阅读本书，你会发现一个按钮写着“试试！”。按下这个按钮会跳转到一个Lean的在线编辑器，并且会将这段代码复制过去，以及添加一些上下文以使得它可以正确编译。你可以在编辑器中书写一些东西，修改例子的内容，Lean则会在你的书写过程中检查你的结果并持续的反馈给你意见。我们推荐你在阅读本书的过程中，运行每一段示例，对代码进行一些自己的实验。

#鸣谢

这个教程是在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的贡献，并对那些在不经意间漏掉名字的人们表示歉意。