证明助手

证明助手又称交互式定理证明系统，是软件类别而非某个品牌。它提供精确定义对象和命题的语言，并检查证明是否遵守所采用逻辑的规则。数学证明的形式化与软件验证都可使用这种工具：后者先把程序及要求表达为数学对象，再证明相应性质。

一个项目通常先选择逻辑基础和已有库，再定义对象、写出定理、分解子目标，最后完成各步证明。用户不仅要找到推理路线，还要检查形式陈述是否准确表达原意。若把需要证明的条件误写进假设，系统仍可能正确验证一个远比原问题容易的命题。

参考：[1] [2]

以命题P且Q蕴含P为例，先把P、Q声明为命题，并将目标写成(P∧Q)→P。证明时引入假设h:P∧Q，再从h取出第一个分量，就得到P。策略式界面可以把“引入假设”和“拆解合取”变成操作，直接证明式则能写出相应证明对象。

这两种外观可以承载相同的逻辑推导。自动化策略还可能搜索现成引理、化简等式或调用专门的判定程序，但搜索成功的提示不是最终的逻辑依据。系统应按其架构把搜索结果转成可核查的证明，或通过受控的基本推理构造已验证定理。

参考：[1] [2]

许多证明助手把复杂的前端、策略和搜索与较小的检查核心分开。以Lean为例，前端将输入细化为核心语言中的项，内核再进行类型检查；显式证明项也使独立检查器成为可能。策略中的普通错误不应仅凭策略宣称成功就生成一个被核心接受的错误证明。

并非所有系统都以完全相同方式保存证明。Isabelle采用LCF传统，把已证明定理的构造限制在受控推理接口中，同时提供化简、自动推理与外部证明器协作。交互式和自动式因此是分工与使用方式的差别，不是互斥阵营；证明助手可大量自动化，自动证明器也可输出可复核证据。

参考：[2] [3]

可信性仍依赖逻辑、公理和检查实现。加入一个不一致公理，可能使任何结论都可推出，而内核不会凭空知道这个公理不应被接受。库里的定理还可能间接依赖额外公理或未完成证明，因此审查时必须追踪依赖，不能只看当前文件没有明显空缺。

例如Lean的sorry占位会引入可被依赖审计发现的假设，不能当作完成的证明；某些原生计算证明方式还会扩大对编译器的信任。即使形式推导完整，现实系统是否符合模型、术语是否被正确解释以及硬件和工具链是否可靠，仍是另外的问题。证明助手强化的是可检验的推理链，而不是取消所有前提。

参考：[4]