This article is missing information about
automated proof checking. (February 2024) |
This article includes a list of general
references, but it lacks sufficient corresponding
inline citations. (November 2018) |
In computer science and mathematical logic, a proof assistant or interactive theorem prover is a software tool to assist with the development of formal proofs by human–machine collaboration. This involves some sort of interactive proof editor, or other interface, with which a human can guide the search for proofs, the details of which are stored in, and some steps provided by, a computer.
A recent effort within this field is making these tools use artificial intelligence to automate the formalization of ordinary mathematics. [1]
Name | Latest version | Developer(s) | Implementation language | Features | |||||
---|---|---|---|---|---|---|---|---|---|
Higher-order logic | Dependent types | Small kernel | Proof automation | Proof by reflection | Code generation | ||||
ACL2 | 8.3 | Matt Kaufmann and J Strother Moore | Common Lisp | No | Untyped | No | Yes | Yes [2] | Already executable |
Agda | 2.6.3 | Ulf Norell, Nils Anders Danielsson, and Andreas Abel ( Chalmers and Gothenburg) | Haskell | Yes | Yes | Yes | No | Partial | Already executable |
Albatross | 0.4 | Helmut Brandl | OCaml | Yes | No | Yes | Yes | Unknown | Not yet Implemented |
Coq | 8.19.0 | INRIA | OCaml | Yes | Yes | Yes | Yes | Yes | Yes |
F* | repository | Microsoft Research and INRIA | F* | Yes | Yes | No | Yes | Yes [3] | Yes |
HOL Light | repository | John Harrison | OCaml | Yes | No | Yes | Yes | No | No |
HOL4 | Kananaskis-13 (or repo) | Michael Norrish, Konrad Slind, and others | Standard ML | Yes | No | Yes | Yes | No | Yes |
Idris | 2 0.6.0. | Edwin Brady | Idris | Yes | Yes | Yes | Unknown | Partial | Yes |
Isabelle | Isabelle2024 (May 2024) | Larry Paulson ( Cambridge), Tobias Nipkow ( München) and Makarius Wenzel | Standard ML, Scala | Yes | No | Yes | Yes | Yes | Yes |
Lean | v4.7.0 [4] | Leonardo de Moura ( Microsoft Research) | C++, Lean | Yes | Yes | Yes | Yes | Yes | Yes |
LEGO (not affiliated with Lego) | 1.3.1 | Randy Pollack ( Edinburgh) | Standard ML | Yes | Yes | Yes | No | No | No |
Metamath | v0.198 [5] | Norman Megill | ANSI C | ||||||
Mizar | 8.1.11 | Białystok University | Free Pascal | Partial | Yes | No | No | No | No |
Nqthm | |||||||||
NuPRL | 5 | Cornell University | Common Lisp | Yes | Yes | Yes | Yes | Unknown | Yes |
PVS | 6.0 | SRI International | Common Lisp | Yes | Yes | No | Yes | No | Unknown |
Twelf | 1.7.1 | Frank Pfenning and Carsten Schürmann | Standard ML | Yes | Yes | Unknown | No | No | Unknown |
A popular front-end for proof assistants is the Emacs-based Proof General, developed at the University of Edinburgh.
Coq includes CoqIDE, which is based on OCaml/ Gtk. Isabelle includes Isabelle/jEdit, which is based on jEdit and the Isabelle/ Scala infrastructure for document-oriented proof processing. More recently, Visual Studio Code extensions have been developed for Coq, [7] Isabelle by Makarius Wenzel, [8] and for Lean 4 by the leanprover developers. [9]
Freek Wiedijk has been keeping a ranking of proof assistants by the amount of formalized theorems out of a list of 100 well-known theorems. As of September 2023, only five systems have formalized proofs of more than 70% of the theorems, namely Isabelle, HOL Light, Coq, Lean, and Metamath. [10] [11]
The following is a list of notable proofs that have been formalized within proof assistants.
Theorem | Proof assistant | Year |
---|---|---|
Four color theorem [12] | Coq | 2005 |
Feit–Thompson theorem [13] | Coq | 2012 |
Fundamental group of the circle [14] | Coq | 2013 |
Erdős–Graham problem [15] [16] | Lean | 2022 |
Polynomial Freiman-Ruzsa conjecture over [17] | Lean | 2023 |
BB(5) = 47,176,870 [18] | Coq | 2024 |
This article's use of
external links may not follow Wikipedia's policies or guidelines. (December 2022) |