Loading AI tools
Software tool to assist with the development of formal proofs by human–machine collaboration From Wikipedia, the free encyclopedia
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.
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) |
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.4.3[3] | Ulf Norell, Nils Anders Danielsson, and Andreas Abel (Chalmers and Gothenburg)[3] | Haskell[3] | Yes[citation needed] | Yes[4] | Yes[citation needed] | No[citation needed] | Partial[citation needed] | Already executable[citation needed] |
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[5] | 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[6] | 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[7] | 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,[9] Isabelle by Makarius Wenzel,[10] and for Lean 4 by the leanprover developers.[11]
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.[12][13]
The following is a list of notable proofs that have been formalized within proof assistants.
Theorem | Proof assistant | Year |
---|---|---|
Four color theorem[14] | Coq | 2005 |
Feit–Thompson theorem[15] | Coq | 2012 |
Fundamental group of the circle[16] | Coq | 2013 |
Erdős–Graham problem[17][18] | Lean | 2022 |
Polynomial Freiman-Ruzsa conjecture over [19] | Lean | 2023 |
BB(5) = 47,176,870[20] | Coq | 2024 |