Proof assistant

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.

For verification in computer science, see formal verification.

A recent effort within this field is making these tools use artificial intelligence to automate the formalization of ordinary mathematics.^[1]

– a programming language, a first-order logical theory, and a theorem prover (with both interactive and automatic modes) in the Boyer–Moore tradition.

ACL2

– 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.

Coq

HOL theorem provers

HOL4

IMPS, An Interactive Mathematical Proof System.

[6]

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.

Isabelle

– Java based.

Jape

Lean

LEGO

– A light system based on the Calculus of Inductive Constructions.

Matita

– A proof assistant based on first-order minimal logic.

MINLOG

– A proof assistant based on first-order logic, in a natural deduction style, and Tarski–Grothendieck set theory.

Mizar

– A proof assistant based on higher-order logic which is eXtensible.

PhoX

(PVS) – a proof language and system based on higher-order logic.

Prototype Verification System

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.

TPS

User interfaces[edit]

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]

Formalization extent[edit]

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]

– Subfield of automated reasoning and mathematical logic

Automated theorem proving

– Mathematical proof at least partially generated by computer

Computer-assisted proof

– Proving or disproving the correctness of certain intended algorithms

Formal verification

– Proposal for a computer-based database of all mathematical knowledge

QED manifesto

– Logical problem studied in computer science

Satisfiability modulo theories

– is an automated theorem prover for first-order and equational logic

Prover9

; Geuvers, Herman (2001). "18. Proof-assistants using Dependent Type Systems" (PDF). In Robinson, Alan J. A.; Voronkov, Andrei (eds.). Handbook of Automated Reasoning. Vol. 2. Elsevier. pp. 1149–. ISBN 978-0-444-50812-6. Archived from the original (PDF) on 2007-07-27.

Barendregt, Henk

. "17. Logical frameworks" (PDF). Handbook vol 2 2001. pp. 1065–1148.

Pfenning, Frank

Pfenning, Frank (1996). "The practice of logical frameworks". In Kirchner, H. (ed.). Trees in Algebra and Programming – CAAP '96. Lecture Notes in Computer Science. Vol. 1059. Springer. pp. 119–134. :10.1007/3-540-61064-2_33. ISBN 3-540-61064-2.

doi

(1998). "X. Types in computer science, philosophy and logic". In Buss, S. R. (ed.). Handbook of Proof Theory. Studies in Logic. Vol. 137. Elsevier. pp. 683–786. ISBN 978-0-08-053318-6.