Lean：一个新开源的定理证明器

我通过邮件向 greatzy 请教了一个定理证明器的问题，因为对此我不是特别清楚。greatzy 在邮件中给予了详尽清晰的解释。因为感到这个解释很有价值，特意将此回复公开在这里，希望能对大家也有所帮助。感谢 greatzy 的慷慨大度。

问题：

交互定理证明（ITP）与自动定理证明（ATP）之间的区别到底是什么？

我的困惑是，现有的机器定理证明器，如，Coq，也都具备 ITP 和 ATP 的特性，那么为什么微软研究院发布的 Lean 这个新的实现却要强调，

The Lean Theorem Prover aims to bridge the gap between interactive and automated theorem proving, by situating automated tools and methods in a framework that supports user interaction and the construction of fully specified axiomatic proofs.

回复：

针对不同的应用领域，运用不同的形式演算方法，出现了多种机器定理证明系统，主要分为交互式定理证明器（interactive theorem prover）和自动化定理证明器（automated theorem prover）两大类。

机器定理证明技术的发展经历了从自动到交互,再回到自动的过程。人们最早设计的定理证明系统是自动化的。随着应用的复杂化，如 CUP 验证问题中的大量公式,自动化定理证明系统受到了运行时间和空间上的挑战，于是出现了交互式定理证明系统。

交互式定理证明器以人机交互为基础。在证明定理的过程中，用户先指定每一个证明步骤要做的工作，然后由计算机完成具体的工作细节。部分交互式定理证明器可能带有一个逻辑框架（logical framework），从而具有很强的表达能力，可用于实现非常复杂的形式系统,如 ISabell。交互式定理证明器往往基于有类型的 lambda 演算（Typed lambda calculus）及自然推理，常用的有用于验证硬件和实时系统的 HOL 和 PVS，用于数学形式化的 coq 等。

自动化定理证明则较少需要用户的直接干预，它们应用各种专门的算法、数据结构和优化技术，自动确定每一个推理步骤的工作，具有极高的推理速度,能够证明一些非常复杂的问题。现在已开发出很多高性能的自动化定理证明器，如 Vampire、Otter、SETHEO、PTTP 等。自动化定理证明系统一般限于带等式的一阶谓词逻辑，并且大都依赖于归结原理（resolution）。

我没看过 Lean，也许其在交互式定理证明系统中引入自动化证明策略，这些策略或者采用自动化证明技术实现，或者把定理翻译到专门的自动化定理证明系统中，在后者完成证明后再把其证明合并到前者中。这样既可以获得更高的性能，也可以把原来需要多次交互才能完成的证明变为自动完成。