我几乎不是这方面的专家（我只是这些系统的用户；我不必担心它们的内部情况。）这可能只是模糊的部分答案，但是我知道的两种主要方法是：

• 使用Curry-Howard同构的依赖类型系统（例如Coq，Lean，Agda）。语句只是类型，证明是具有该类型的术语，因此检查证明的有效性本质上只是对术语进行类型检查的一种特殊情况。我不想过多地谈论这种方法，因为我对此不太了解，恐怕会出错。温特豪德（ThéoWinterhalter）在上面的评论中链接了一些内容，可能为这种方法提供了更多背景信息。 li证明了LCF式定理（例如Isabelle，HOL Light，HOL 4）。这里的一个定理（大致而言）是实现语言中类型为thm的不透明值。只有相对较小的“证明内核”才能创建这些thm值，并且系统的所有其他部分都与该证明内核交互。内核提供了一个由各种小功能组成的接口，这些接口实现了小的推理步骤，例如 modus ponens （如果您有一个定理A ⟹ B和一个定理A，则可以获得定理B或∀-介绍（如果您对固定变量P x有定理x，则可以得到定理∀x. P x）等。内核还提供了一个定理用于定义新常量的接口。原则上，只要您可以相信这些函数能够忠实地实现基础逻辑的基本推理步骤，就可以相信可以产生的任何thm值确实对应于逻辑中的一个定理。对于LCF风格的证明者，答案很难回答，因为它们通常不建立证明术语（例如Isabelle拥有它们，但是默认情况下它们被禁用并且未被广泛使用）。我认为可以说内核原语的调用方式的历史构成了证明，如果要进行记录，就可以原则上 –在另一系统中重放和检查。 li>

在两种情况下，我们的想法都是拥有一个必须信任的内核（前一种情况下为类型检查器，后一种情况下为推理内核），然后围绕该内核提供了一个庞大的附加程序生态系统更多便利层。但是，由于它们必须与内核交互才能真正生成定理，因此您不必信任该代码。

所有这些不同的系统都在系统的哪些部分位于内核中以及哪些部分不在内核中进行了各种折衷。总的来说，我认为可以这样说：与基于LCF的系统相比，从属类型的系统往往具有更大的内核（例如，HOL Light具有特别小的和简单的内核）。

我认为还有其他一些系统不适合这两个类别（例如Mizar，ACL2，PVS，Metamath，NuPRL），但我对这些系统的实施方式一无所知。

对于LCF，HOL和Isabelle，您将在期刊文章“ From LCF to Isabelle/HOL”中找到有关您问题的广泛答案。 （这是开放访问。）

大多数依赖类型化的系统（例如Coq）也是LCF样式定理证明，如本文和Eberl的回答所述。一个显着的区别是，这种计算包含了完整的证明对象，因此，LCF方法的目标之一（即通过不存储证明来节省空间）被放弃了。但是，稳健性的目标仍然可以实现。