证明助手是一种帮助用户构造和验证形式证明的软件系统。它在精确定义的形式系统中表示定义、假设和命题，并检查所提出的论证是否遵循该系统的推理规则。证明助手应用于数学和计算机科学，将人主导的推理与自动化相结合。其用途包括将数学成果形式化，以及确立软件、硬件和编程语言的性质。与非形式化的数学证明不同，由机器检查的形式化成果必须提供足够的细节，使每一步推理都能在所选的基础体系内得到论证。(isabelle.in.tum.de)
逻辑基础
证明助手需要一种用于表达命题的形式语言，以及一套规定如何推导命题的演算规则。不同系统采用不同的基础，包括类型论、高阶逻辑和集合论。这些选择会影响数学对象的表示方式、可用的原理，以及计算与推理如何相互配合。Isabelle 是一个支持多种逻辑的通用框架；其中广泛使用的 Isabelle/HOL 实例提供了经典高阶逻辑。(isabelle.in.tum.de)
在 Lean 和 Rocq 等依赖类型系统中，类型可以依赖于值。通过柯里—霍华德对应，命题可以表示为类型，证明则表示为属于这些类型的项。蕴含对应于一种函数，它将前提成立的证据转换为结论成立的证据。因此，检查这样的证明，就是检查某个项是否具有所要求的类型。Lean 使用一种源自构造演算的依赖类型论，而 Rocq 使用归纳构造演算。(lean-lang.org)
必须区分基础原理与已证明的结果。定理是在给定的定义和假设之下确立的，这些假设也包括任何已声明的公理。检查器接受某个证明，并不能独立地确立每项假设都恰当，也不能保证该命题准确表达了它所要表达的非形式化含义。(lean-lang.org)
交互式证明构造
用户通常先定义对象，并陈述目标命题。界面会显示证明状态，其中包含局部假设和尚未完成的目标。一个证明步骤可以解决某个目标，也可以将其替换为更简单的子目标。例如，证明一个合取命题需要分别证明两个组成部分；证明一个蕴含命题则可以先将其前提引入为假设。(lean-lang.org)
证明策略是执行证明构造步骤的过程。证明策略可以应用已确立的定理、重写表达式、化简公式或进行搜索。用户将它们组合成脚本，而结构更清晰的证明语言则可以让论证呈现出类似数学论述的形式。Isabelle 的 Isar 语言支持这种结构化风格。由先前已检查的定义和引理组成的库，可以减少每个项目都要重新构建初等数学的需要。(lean-lang.org)
交互式证明与自动定理证明之间并没有绝对的界限。例如，Isabelle 通过 Sledgehammer 集成外部证明器，搜索有用的事实，并尝试在 Isabelle 内部重建证明。自动化可以辅助完成特定步骤，而用户仍可提供总体论证和中间命题。(isabelle.in.tum.de)
内核与信任
许多证明助手将复杂的证明构造工具与相对较小的证明内核分离。在 Lean 和 Rocq 中，证明策略生成证明项，再由内核检查。证明策略中的一般错误不一定会损害逻辑正确性：不合规则的结果应当被拒绝，而不是被接受为定理。这种分离使证明自动化工具能够不断演进，而不必要求每种证明策略的实现都值得信任。(lean-lang.org)
一种相关架构源于 LCF 传统。它将定理值的创建限制在基本逻辑操作之内，使高层过程可以组合这些操作，却无法绕过推理规则。HOL 系统继承了这一做法。20 世纪 70 年代初开发的 Edinburgh LCF 是后来交互式定理证明器的重要前身。(cl.cam.ac.uk)
不过，可信计算基的范围并不止于抽象的逻辑演算。对结果的信心取决于检查器的实现以及实际使用的假设。某些加速计算的方法还需要额外信任编译或求值机制。独立的检查器可以减少对单一实现的依赖，但无法解决形式化命题本身的错误。(lean-lang.org)
代表性系统
Lean证明助手将基于依赖类型的定理证明器与编程语言及可扩展的证明自动化相结合，支持数学形式化和软件验证。Rocq 旧称 Coq，同样结合了依赖类型、交互式证明，以及用于规约和开发已验证程序的工具。(lean-lang.org)
Isabelle 提供通用逻辑框架、结构化证明和集成的自动化功能。HOL Light 专注于高阶逻辑，具有小型逻辑核心、可编程的证明工具和数学库。这些系统的基础体系和界面各不相同；不能简单地将它们的定理陈述和证明产物视为可互换的内容。(isabelle.in.tum.de)
应用与局限
数学方面的应用包括在 Rocq 的前身 Coq 中形式化四色定理。Flyspeck 项目使用 HOL Light 和 Isabelle 将开普勒猜想形式化；这一协作证明于 2014 年完成。这些形式化工作在明确的逻辑框架内检查了大量数学论证及其中涉及计算的子命题。(docs.rocq-prover.org)
在形式验证中，证明助手依据形式规约确立计算系统的性质。CompCert 编译器使用机器检查的推理，建立生成代码与源程序行为之间的联系。HOL Light 也被用于验证浮点运算算法，其中包括一个误差界限得到形式化证明的指数函数实现。(arxiv.org)
形式化需要明确的定义、配套的库和详细的论证。由此获得的保证针对的是形式化命题，而不是未经检查的转述，也不是周边物理系统的所有行为。错误的规约、不恰当的假设、可信组件中的实现缺陷，以及尚未完成的形式化工作，仍然是彼此不同的风险来源。证明助手使逻辑依赖关系可以被审查并由机器检查；判断这些依赖关系是否表达了预期问题，仍是一项独立的任务。(lean-lang.org)