官网链接
Welcome! | The Coq Proof Assistant (inria.fr)
Programming Language and Theorem Prover — Lean (lean-lang.org)
逻辑系统支持
基于依赖类型理论的工具：如 Coq 和 Lean
基于经典高阶逻辑的工具：如 Isabelle
依赖类型理论（Dependent Type Theory）
基本概念
依赖类型理论中，类型可以依赖于值。
对比：在普通的类型系统（如简单类型 lambda 演算）中，类型是固定的，例如一个函数的输入类型和输出类型在定义函数时就确定了。但在依赖类型理论中，类型可以根据函数的输入值而变化。例如，一个函数可以接受一个自然数 n 作为输入，并且返回一个长度为 n 的列表类型的值。
这种类型和值之间的依赖关系使得可以在类型层面表达更加复杂的约束和性质。例如，可以定义一个类型，它表示所有小于某个给定自然数的自然数集合，并且这个类型与给定的自然数是相关的。
特点
强大的精细化表达能力：能够精确地描述程序和数学对象的复杂性质。例如，在编写一个计算矩阵乘法的程序时，可以在类型中体现矩阵维度的约束，确保只有维度匹配的矩阵才能进行乘法运算。这种精细化的表达有助于在编译阶段就发现许多潜在的错误。
内在的一致性保证：由于类型和值的紧密关联，依赖类型系统可以提供一种内在的一致性保证。在构建程序或证明时，通过类型检查可以确保所构建的对象满足其预期的性质。例如，在构造一个证明对象时，类型检查可以验证证明步骤的正确性。
与编程紧密结合：不仅可以用于证明定理，还与编程实践紧密相连。可以将程序和证明看作是同一实体的不同方面，通过编写具有依赖类型的程序来同时实现计算任务和证明相关性质。例如，在开发一个密码学算法的程序时，可以同时证明该算法的安全性属性。
经典高阶逻辑（Higher - Order Logic，HOL）
基本概念
经典高阶逻辑是在一阶逻辑的基础上扩展而来的。
一阶逻辑主要处理个体（对象）和个体上的谓词（关系），而高阶逻辑允许对谓词和函数进行量化。（量化：可以被全称/存在量词作用）
例如，在一阶逻辑中可以说 “存在一个整数 x，使得 P (x) 成立”（这里 P 是一个关于整数的谓词）；而在高阶逻辑中可以说 “对于所有的谓词 P，存在一个对象 x，使得 P (x) 成立”。
它包括了命题逻辑和一阶谓词逻辑的所有规则，并且增加了新的规则来处理高阶对象。高阶对象可以是函数、谓词等，并且可以像个体对象一样进行量化操作。
特点
强大的表达能力：能够自然地（更符合一般数学思维和逻辑）表达许多复杂的数学概念和逻辑关系。例如，在形式化数学中，可以方便地定义实数、函数空间等抽象概念。以实数的定义为例，通过高阶逻辑可以精确地定义实数的各种性质，如完备性等。
符合传统数学思维：数学家们在进行数学推理和证明时&#