证明助手的主要块是什么？
我只是想知道校对的内在逻辑。例如，关于这种助手的图形用户界面的主题我不感兴趣
有人向编译器提出了与我类似的问题：https://softwareengineering.stackexchange.com/questions/165543/how-to-write-a-very-basic-compiler
我关心的是同样的问题，但对于证明检查系统。
我不是这方面的专家(我只是这些系统的用户；我不太担心它们的内部(，这可能只是一个模糊的部分答案，但我知道的两种主要方法是：
- 使用Curry–Howard同构的依赖类型系统(例如Coq、Lean、Agda(。语句只是类型，证明是具有该类型的术语，因此检查证明的有效性本质上只是对术语进行类型检查的特殊情况。我不想对这种方法说太多，因为我对它了解不多，担心我会出错。Théo Winterhalter在上面的评论中联系了一些内容，这些内容可能会为这种方法提供更多的背景
- LCF风格的定理证明者(例如Isabelle，HOL Light，HOL 4(。这里的定理(粗略地说(是实现语言中类型为
thm的不透明值。只有相对较小的"证明内核"才能创建这些thm值，系统的所有其他部分都与该证明内核交互。内核提供了一个由各种小函数组成的接口，这些小函数实现了小的推理步骤，如模块(如果你有定理A ⟹ B和定理A，你可以得到定理B(或∀-引言(如果你对固定变量x有定理P x，你可以获得定理∀x. P x(等。内核还提供了一个用于定义新常量的接口。原则上，只要你能相信这些函数忠实地实现了底层逻辑的基本推理步骤，你就能相信你能产生的任何thm值都真正对应于你逻辑中的一个定理。对于LCF风格的证明者来说，实际证明是什么的答案有点难回答，因为他们通常不会构建证明术语(例如Isabelle有，但默认情况下会禁用，并且没有广泛使用(。我认为可以说，内核基元如何被调用的历史构成了证明，如果要记录它，原则上可以在另一个系统中回放和检查它
在这两种情况下，我们的想法都是，您必须信任一个内核(在前一种情况下是类型检查器，在后一种情况中是推理内核(，然后您有一个由附加过程组成的大型生态系统，以提供更多的便利层。然而，由于它们必须与内核交互才能真正产生定理，因此您不必信任该代码。
所有这些不同的系统都有不同的权衡，即系统的哪些部分在内核中，哪些部分不在内核中。一般来说，我认为可以公平地说，依赖类型的系统往往比基于LCF的系统有更大的内核(例如，HOL Light有一个特别小和简单的内核(。
我认为还有其他系统不属于这两类(例如Mizar、ACL2、PVS、Metamath、NuPRL(，但我对这些系统是如何实现的一无所知。
对于LCF、HOL和Isabelle，您将在期刊文章"从LCF到Isabelle/HOL"中找到您的问题的广泛答案。(这是开放访问。(
大多数依赖类型的系统，如Coq，也是LCF风格的定理证明者，如文章和Eberl的回答中所述。一个显著的区别是，这种演算包含了完整的证明对象，因此LCF方法的目标之一——通过不存储证明来节省空间——被放弃了。然而，健全性的目标仍然得到实现。