Proof assistant

GCL是一些大型项目所选择的实现，包括数学工具Maxima、AXIOM（英语：Axiom (computer algebra system)）、HOL88（英语：HOL (proof assistant)）和ACL2。GCL运行在Linux上的十一种架构下，还有FreeBSD、Solaris、Mac OS X和Microsoft Windows。

所有这些实现都是开源的并可自由的获得。其中多数用SML实现了自身。不再有任何商业SML实现。 证明辅助器HOL4（英语：HOL (proof assistant)）、Isabelle、LEGO（英语：LEGO (proof assistant)）和Twelf（英语：Twelf）是用Standard ML写成。它还用于编译器制作和集成电路设计比如ARM。

Lean是一款在含歸納類型的構造演算基礎上所開發的電腦證明助手（英语：Proof assistant）和函數式編程語言。Lean最初由萊昂納多·德·莫拉（英语：Leonardo de Moura）在微軟研究院下研發，目前以開源合作計劃的形式刊登在GitHub上。2023年成立的非盈利Lean集中研究組織（英語：Lean

Tobias Nipkow, Lawrence C. Paulson, Markus Wenzel: Isabelle/HOL – A Proof Assistant for Higher-Order Logic. Isabelle 的官方网站 （页面存档备份，存于互联网档案馆） 形式化证明存档（The

的类型系统体现了柯里-霍华德同构（Curry-Howard correspondence），因此亦可作为一个构建构造性证明的证明辅助工具（英语：Proof assistant）。它的类型理论基于 Zhaohui Luo 提出的 UTT（unified theory of dependent types），与