【定理证明工具调研】Coq, Isabelle and Lean.

官网链接

Welcome! | The Coq Proof Assistant (inria.fr)

Isabelle (tum.de)

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) 成立”。

它包括了命题逻辑和一阶谓词逻辑的所有规则，并且增加了新的规则来处理高阶对象。高阶对象可以是函数、谓词等，并且可以像个体对象一样进行量化操作。

特点

强大的表达能力：能够自然地（更符合一般数学思维和逻辑）表达许多复杂的数学概念和逻辑关系。例如，在形式化数学中，可以方便地定义实数、函数空间等抽象概念。以实数的定义为例，通过高阶逻辑可以精确地定义实数的各种性质，如完备性等。

符合传统数学思维：数学家们在进行数学推理和证明时，很多时候的思维方式与高阶逻辑相契合。它使得从传统数学到形式化证明的过渡相对自然，有利于数学家将已有的数学知识和证明方法转换为形式化的证明。

良好的语义基础：具有清晰明确的语义解释，这使得在基于高阶逻辑的证明过程中，每一个逻辑表达式的含义都能够被准确地理解。例如，对于一个关于函数连续性的高阶逻辑命题，其语义可以通过极限的概念等传统数学定义来解释。

证明工具自动化程度分析

Lean

策略建议：通过如 Lean Copilot 等工具，利用 LLM 生成策略建议。
用户输入当前证明目标，它会从 LLM 获取策略候选项，并筛选出无错误的策略供用户选择，这些策略可直接完成证明或作为中间步骤，帮助用户更快地找到证明思路
证明搜索：search_proof 工具将 LLM 生成的目标相关策略与基于规则的证明搜索工具 aesop 结合，增强规则集，更灵活地搜索完整证明，找到从原始目标到可轻松解决目标的路径.
前提选择：借助 LLM 从大量的库中自动检索潜在有用前提，减少用户查找和筛选相关引理等前提的工作量，提高证明效率(如library_search功能)

Isabelle

逻辑特定的自动化：在命题逻辑中，Isabelle 能够在一定程度实现完全自动化的证明。例如，对于简单的逻辑命题 “若 p 则 q，已知 p，证明 q”，Isabelle 可以直接得出结论并完成证明.（对于高阶复杂逻辑就难以直接证明）
自动证明工具：提供了如 sledgehammer 等自动证明工具。它可以搜索已有的定理和引理，尝试找到能够证明当前目标的方法，并自动应用这些方法来完成部分或全部的证明过程。

证明策略的自动应用：根据用户输入的证明目标和当前的证明状态，Isabelle 能够自动选择合适的证明策略并应用。比如在证明数学等式时，它可以自动判断是使用化简、代换还是其他策略来推进证明。

Isabelle 内部包含了丰富的逻辑规则，这些规则是基于命题逻辑、一阶逻辑、高阶逻辑等各种逻辑体系。 
Isabelle 采用了各种证明搜索算法。其中一种常见的是基于深度优先搜索或广度优先搜索的策略变种。 
Isabelle 会考虑类型信息。当前证明所处的理论环境、已经引入的公理和定理等都会影响证明策略的选择。

Coq 的自动化程度一般

证明步骤需手动构建：相对而言，Coq 需要用户手动构建更多的证明步骤。即使是对于一些看似直观的数学定理，用户也需要详细地说明每一步的推理过程，例如证明简单的加法交换律，在 Coq 中需要明确地写出每一步的变换和依据，无法像 Isabelle 在某些简单逻辑下那样自动完成3.
自动化策略的局限性：虽然 Coq 提供了一些自动化策略，如反演、归纳、重写等，但这些策略在面对复杂的证明目标时，往往不能直接得出完整的证明。用户需要对证明目标有深入的理解，并巧妙地组合和应用这些策略，有时还需要自己定义新的引理和策略来辅助证明。（也是Coq的重要优势所在）
缺乏高效的自动搜索机制：在寻找合适的定理、引理和证明方法时，Coq 的自动搜索能力相对较弱。它不像 Isabelle 的 sledgehammer 等工具那样能够广泛而有效地搜索已有的知识来辅助证明，用户往往需

编程语言、接口和对用户的友好性

研究工具所使用的编程语言

Coq ：Gallina 语言

Isabelle ： ML 语言

Lean： Lean语言

接口（如何理解”接口“）

Coq：拥有多种接口，如 Coq_Nvim 插件，它与 Neovim 集成，提供了代码补全、语法高亮、代码导航等功能，支持 Vimscript 和 Lua 双接口配置，用户可自定义快捷键，还实现了类似 VSCode CoqToolbox 的交互模式和功能，方便用户在熟悉的编辑器环境中高效地编写和验证 Coq 证明。此外，还有 Coq-Elpi 等插件，它将 Coq 与 λProlog 融合，提供了一系列广泛的 Coq 原语访问接口，可实现更灵活的命令和策略编写

Lean：其接口简洁明了，在 Lean 的开发环境中，用户可以方便地输入代码、查看错误提示和证明状态。它还提供了与其他工具和编程语言的良好交互接口，如可以与 C++ 等语言进行交互，方便将形式化证明应用于实际的软件开发和验证中。

Isabelle：具有图形化用户界面和命令行界面等多种交互方式。

图形化界面如 Isabelle/jEdit，提供了直观的操作界面，方便用户进行文件管理、定理证明等操作，支持语法高亮、自动补全等功能，有助于提高用户的编写效率。同时，命令行界面则适合于更专业的用户和自动化脚本的编写，用户可以通过命令行输入各种指令来完成复杂的证明任务和系统配置

对用户的友好性评估（入门学习难度&工程应用情况）

Coq：

优势：具有强大的社区支持和丰富的学习资源，包括教材、在线教程、论坛等，方便用户学习和交流。其证明辅助功能强大，能够帮助用户构建严格的形式化证明，对于深入研究数学基础和软件正确性验证的专业人员来说非常有价值。此外，与其他编程语言的交互能力使其在实际应用中具有更广泛的扩展性

劣势：学习曲线较陡峭，需要用户花费一定时间掌握其独特的证明策略、逻辑系统和语法规则。对于初学者来说，可能会在理解和运用 Coq 的复杂概念和证明技巧上遇到困难，编写简单的证明也可能需要较多的代码和步骤

Isabelle：

优势：逻辑框架丰富，支持多种逻辑体系，能够满足不同用户在不同领域的证明需求，具有很强的通用性和灵活性。图形化界面和命令行界面的结合，使得用户可以根据自己的喜好和使用场景选择合适的交互方式。其自动证明工具如 sledgehammer 等，能够帮助用户快速找到证明思路和方法，提高证明效率

劣势：由于其功能的强大和灵活性，导致其系统相对复杂，对于初学者来说可能会感到困惑和难以掌握。在使用过程中，需要用户对各种逻辑概念和证明策略有深入的理解，否则可能会在证明过程中出现错误或无法有效地利用其提供的工具和功能。

Lean：易上手但应用尚不广泛，现成案例相对较少

优势：语法简洁直观，易于理解和编写，能够让用户更快速地入门和上手。它在数学领域的应用较为广泛，提供了丰富的数学库和工具，方便用户进行数学定理的证明和数学概念的形式化建模。同时，其高效的证明引擎和自动化功能也能够提高证明的效率，减少用户的手动工作量。

劣势：在工业界的应用相对 Coq 和 Isabelle 可能不够广泛，相关的案例和实践经验相对较少。此外，虽然其核心功能强大，

但对于一些复杂的、特定领域的证明需求，可能需要用户自行扩展和定制功能，这对用户的编程能力和领域知识要求较高。

客观情况：虽然依赖近似复杂程度的理论基础，但Coq（1989.5发Lean布）相较Lean（2015发布）发展时间更长，学习资源、证明助手等生态更成熟，在实际应用过程中成功案例丰富，行业普及度较高。

性能比较（证明速度&资源占用）

简单定理证明

Lean：在简单的数学定理证明（如基本算术性质、简单逻辑命题）方面，由于其自动化程度较高，往往能够快速地找到证明路径。例如，证明自然数加法的交换律，Lean 可以利用其内置的自动化策略，相对迅速地完成证明。这是因为它能够自动应用一些基本的数学推理规则和引理，减少用户手动搜索和应用规则的时间。

Coq：对于同样简单的定理，Coq 的证明速度可能会稍慢。因为 Coq 通常需要用户更详细地构建证明步骤，即使是简单定理也需要明确地写出每一步的推理依据。例如，在证明加法交换律时，用户可能需要通过归纳法，详细地定义加法运算并逐步推导等式两边相等，这使得证明过程相对繁琐，速度可能不如 Lean。

Isabelle：Isabelle 在简单定理证明上的速度取决于是否能有效利用其自动证明工具（如 sledgehammer）。如果自动工具能够成功找到合适的证明方法，证明速度可以很快。但如果自动工具不能直接给出完整的证明，需要手动干预，那么证明速度可能会下降。例如，在证明一些简单的逻辑等价命题时，自动工具可能快速匹配到已有的定理并完成证明，但对于稍微复杂一点的涉及自定义数据类型的简单定理，可能需要更多的手动操作。

复杂定理证明

Lean：当面对复杂的数学定理（如高等数学中的分析定理、代数结构中的复杂性质）或复杂的计算机科学证明（如大型程序的正确性验证）时，Lean 的证明速度可能会受到影响。尽管它有自动化功能，但复杂问题可能超出其自动化策略的有效范围，需要用户花费时间去引导证明，寻找合适的中间引理等。例如，在证明复杂的算法正确性时，可能需要用户手动定义许多辅助函数和引理来帮助完成证明，这会减慢证明速度。

Coq：在复杂定理证明中，Coq 的灵活性体现出来。虽然它整体证明速度可能不是最快的，但它允许用户根据对问题的深入理解，采用各种复杂的证明策略。对于一些高度复杂、具有特殊逻辑结构的定理，熟练的用户可以通过巧妙地组合归纳法、反证法等策略，逐步攻克证明难题。然而，这种灵活性也意味着证明过程可能会比较漫长，尤其是对于不太熟练的用户，可能会在摸索合适的证明策略上花费大量时间。

Isabelle：对于复杂定理，Isabelle 的自动证明工具会尽力搜索可能的证明路径，但随着问题复杂度的增加，搜索空间呈指数级增长，可能导致自动工具效率降低。不过，Isabelle 的优势在于它有丰富的逻辑框架和已有的定理库，用户可以利用这些资源进行手动调整和辅助证明。例如，在证明复杂的操作系统内核安全性属性时，自动工具可能找到部分证明思路，但完整的证明可能需要结合手动构建的中间定理和模型来完成，整体证明速度会因问题的复杂程度而有较大差异。

总结

Coq

特点2：
基于依赖类型理论(dependent types)：其类型系统强大，支持依赖类型和多态类型，能在编写代码时避免许多常见错误，还可使复杂证明和程序编写更易实现。
交互式证明：用户可通过交互方式逐步构建和验证证明，便于随时检查证明的正确性，利于理解和组织证明过程。
丰富的库和插件系统：提供大量的库和插件，可轻松扩展和定制功能，满足不同用户的特定需求。
优势：
表达能力强：dependent types 的存在让其可以表达复杂的数学概念和逻辑关系，能够处理一些其他工具难以表达的问题.
成熟的生态系统：拥有多种编辑器、IDE、库和插件等，开发者可以根据自己的需求选择合适的工具，提高开发效率.
广泛应用：在数学定理证明、形式化验证、密码学等多个领域都有成熟的应用案例

Isabelle

特点：
基于经典高阶逻辑：采用这种逻辑系统，使证明过程更符合传统数学和逻辑的思维方式1.
ML 语言实现：使用 Standard ML 语言实现，开发者可利用 ML 语言的特性进行灵活编程和定制13.
强大的标准库和扩展库：如 Isabelle/HOL 库提供高阶逻辑支持，Isabelle/Z 库用于形式化系统规约和验证，Isabelle/UTP 库用于形式化软件系统的设计和验证等，可满足不同领域的形式化需求3.
优势：
自动化程度相对较高：其自动化证明工具如 sledgehammer 等在很多情况下能较好地自动找到证明路径，上手相对较快，可减轻使用者的负担1.
可信度高：具有极小化的逻辑核心，证明和形式化验证的结果具有较强可信度1.
广泛的理论支持：对各种数学理论和计算机科学中的形式化语言、逻辑等都有良好的支持，可用于多种领域的定理证明和形式化工作13.

Lean

特点：
基于依赖类型理论：与 Coq 类似，依赖类型理论为其提供了强大的表达能力，但在具体的实现和应用方式上有自身特点.
强调自动化：从设计之初就以自动化为目标，在自动化证明和自动化定理证明方面效率较高.
元编程能力强：支持在类型层次上的计算和编程，为复杂数学定理的证明提供了很大的灵活性.
优势：
高效的自动化证明：能够自动完成大部分证明步骤，极大地提高了证明效率，尤其是在处理大规模复杂问题时更具优势.
活跃的社区：拥有活跃的开发者社区，意味着有更多的资源、支持和合作机会，有助于推动工具的发展和应用.
适合与 AI 结合：如 Lean Copilot 等项目的出现，使其能够更好地与 AI 技术结合，进一步提升自动化证明的能力和效率.

三者的区别

逻辑系统：Coq 使用依赖类型理论，Isabelle 使用经典高阶逻辑，Lean 使用依赖类型理论，但在具体的逻辑实现和应用细节上与 Coq 有所不同
编程语言：Coq 采用 Gallina 语言，Isabelle 使用 ML 语言，Lean 的编程语言则具有自身特点，与 Coq 和 Isabelle 的语言都有所区别
自动化程度：Lean 的自动化程度较高，Coq 的自动化程度相对较低，需要开发者手动进行更多的证明步骤，而 Isabelle 的自动化程度介于两者之间，其 sledgehammer 等工具较为实用
表达能力：Coq 的表达能力强，能够处理复杂的逻辑关系和数学概念，但细节补全的负担较重；Isabelle 的表达力相对有限，但 inner prover 做得好，可减轻使用者负担；Lean 的表达能力也较强，且结合其自动化能力，在处理复杂问题时具有一定优势

如何选用

一看待证明定理的复杂程度，二看熟悉哪种交互语言~

根据具体需求：如果侧重于数学定理的证明，尤其是需要处理复杂的逻辑关系和数学概念，Coq 和 Lean 可能更适合；如果需要对计算机科学中的各种形式化语言、逻辑、程序设计语言等进行研究和验证，Isabelle 则是一个不错的选择
考虑自动化程度：若希望证明过程具有较高的自动化程度，Lean 是较好的选择；如果不介意手动进行一些证明步骤，且需要强大的表达能力和丰富的生态系统支持，Coq 可能更符合需求；而 Isabelle 则在两者之间提供了一种平衡
结合个人背景和团队情况：如果熟悉 OCaml 或 Gallina 语言，Coq 可能更容易上手；若对 ML 语言有一定了解，Isabelle 可能更适合；而对于那些希望参与活跃社区、获取更多资源和支持的用户，Lean 可能更具吸引力.

注意哦：

由于调研过程整体较为依赖大语言模型，部分结果存在一定的不严谨，关键细节需要重新确认。