computer science Computer science is the study of computation, information, and automation. Computer science spans Theoretical computer science, theoretical disciplines (such as algorithms, theory of computation, and information theory) to Applied science, ...

and

mathematical logic Mathematical logic is the study of Logic#Formal logic, formal logic within mathematics. Major subareas include model theory, proof theory, set theory, and recursion theory (also known as computability theory). Research in mathematical logic com ...

, a proof assistant or interactive theorem prover is a software tool to assist with the development of

formal proof In logic and mathematics, a formal proof or derivation is a finite sequence of sentences (known as well-formed formulas when relating to formal language), each of which is an axiom, an assumption, or follows from the preceding sentences in the s ...

s 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 computer is a machine that can be Computer programming, programmed to automatically Execution (computing), carry out sequences of arithmetic or logical operations (''computation''). Modern digital electronic computers can perform generic set ...

. A recent effort within this field is making these tools use

artificial intelligence Artificial intelligence (AI) is the capability of computer, computational systems to perform tasks typically associated with human intelligence, such as learning, reasoning, problem-solving, perception, and decision-making. It is a field of re ...

to automate the formalization of ordinary mathematics.

System comparison

* ACL2 – a programming language, a first-order logical theory, and a theorem prover (with both interactive and automatic modes) in the Boyer–Moore tradition. * Rocq (formerly known as ''Coq'') – Allows the expression of mathematical assertions, mechanically checks proofs of these assertions, helps to find formal proofs, and extracts a certified program from the constructive proof of its formal specification. *

HOL theorem prover HOL (Higher Order Logic) denotes a family of Proof assistant, interactive theorem proving systems using similar Higher-order logic, (higher-order) logics and implementation strategies. Systems in this family follow the LCF (theorem prover), LCF ( ...

s – A family of tools ultimately derived from the LCF theorem prover. In these systems the logical core is a library of their programming language. Theorems represent new elements of the language and can only be introduced via "strategies" which guarantee logical correctness. Strategy composition gives users the ability to produce significant proofs with relatively few interactions with the system. Members of the family include: ** HOL4 – The "primary descendant", still under active development. Support for both Moscow ML and

Poly/ML Standard ML (SML) is a General-purpose programming language, general-purpose, High-level programming language, high-level, Modular programming, modular, Functional programming, functional programming language with compile-time type checking and t ...

. Has a BSD-style license. ** HOL Light – A thriving "minimalist fork".

OCaml OCaml ( , formerly Objective Caml) is a General-purpose programming language, general-purpose, High-level programming language, high-level, Comparison of multi-paradigm programming languages, multi-paradigm programming language which extends the ...

based. **ProofPower – Went proprietary, then returned to open source. Based on

Standard ML Standard ML (SML) is a General-purpose programming language, general-purpose, High-level programming language, high-level, Modular programming, modular, Functional programming, functional programming language with compile-time type checking and t ...

. * IMPS, An Interactive Mathematical Proof System. * Isabelle is an interactive theorem prover, successor of HOL. The main code-base is BSD-licensed, but the Isabelle distribution bundles many add-on tools with different licenses. * Jape – Java based. * Lean *

LEGO Lego (, ; ; stylised as LEGO) is a line of plastic construction toys manufactured by the Lego Group, a privately held company based in Billund, Denmark. Lego consists of variously coloured interlocking plastic bricks made of acrylonitri ...

* Matita – A light system based on the Calculus of Inductive Constructions. * MINLOG – A proof assistant based on first-order minimal logic. * Mizar – A proof assistant based on first-order logic, in a natural deduction style, and Tarski–Grothendieck set theory. * PhoX – A proof assistant based on higher-order logic which is eXtensible. * Prototype Verification System (PVS) – a proof language and system based on higher-order logic. * TPS and ETPS – Interactive theorem provers also based on simply typed lambda calculus, but based on an independent formulation of the logical theory and independent implementation.

User interfaces

A popular front-end for proof assistants is the

Emacs Emacs (), originally named EMACS (an acronym for "Editor Macros"), is a family of text editors that are characterized by their extensibility. The manual for the most widely used variant, GNU Emacs, describes it as "the extensible, customizable, s ...

-based Proof General, developed at the

University of Edinburgh The University of Edinburgh (, ; abbreviated as ''Edin.'' in Post-nominal letters, post-nominals) is a Public university, public research university based in Edinburgh, Scotland. Founded by the City of Edinburgh Council, town council under th ...

. Coq includes CoqIDE, which is based on OCaml/

Gtk GTK (formerly GIMP ToolKit and GTK+) is a free software cross-platform widget toolkit for creating graphical user interfaces (GUIs). It is licensed under the terms of the GNU Lesser General Public License, allowing both Free software, free and ...

. 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, Isabelle by Makarius Wenzel, and for Lean 4 by the leanprover developers.

Formalization extent

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, Rocq, Lean, and Metamath.

Notable formalized proofs

The following is a list of notable proofs that have been formalized within proof assistants.

Notes

References

* * * * *

External links

Theorem Prover Museum

in ''Certified Programming with Dependent Types''.
Introduction to the Coq Proof Assistant
(with a general introduction to interactive theorem proving)

A list of theorem proving tools
; Catalogues

* {{cite web , title=Specific Logical Frameworks and Implementations , url=https://www.cs.cmu.edu/~fp/lfs-impl.html , access-date=15 February 2024 , archive-date=10 April 2022 , archive-url=https://web.archive.org/web/20220410151836/https://www.cs.cmu.edu/~fp/lfs-impl.html , url-status=dead (By Frank Pfenning). * DMOZ
Science: Math: Logic and Foundations: Computational Logic: Logical Frameworks
Argument technology Automated theorem proving de:Maschinengestütztes Beweisen