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 | Isabelle2021 (February 2021) | Larry Paulson (Cambridge), Tobias Nipkow (München) and Makarius Wenzel | Standard ML, Scala | Yes | No | Yes | Yes | Yes | Yes |
Lean | v4.1.0 (official release) v4.2.0-rc1 (pre-release)[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.05 | 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 Isabelle by Makarius Wenzel,[7] and for Lean 4 by the leanprover developers.[8]
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.[9][10]
The following is a list of notable proofs that have been formalized within proof assistants.
Theorem | Proof assistant | Year |
---|---|---|
Four color theorem[11] | Coq | 2005 |
Feit–Thompson theorem[12] | Coq | 2012 |
Fundamental group of the circle[13] | Coq | 2013 |
Erdős–Graham problem[14][15] | Lean | 2022 |
Polynomial Freiman-Ruzsa conjecture over [16] | Lean | 2023 |