Editing Proof assistant (section)

== {{anchor|Comparison}}System comparison ==
{{see also|Dependent type#Comparison|Automated theorem proving#Comparison}}
<!-- Need to add at least [[Automath]], [[PhoX]] -->
{| class=wikitable
|-
! rowspan=2 | Name !! rowspan=2 | Latest version !! rowspan=2 | Developer(s) !! rowspan=2 | Implementation language !! colspan=6 | Features
|-
! [[Higher-order logic]] !! [[Dependent type]]s !! [[de Bruijn criterion|Small kernel]] !! [[Proof automation]] !! [[Proof by reflection]] !! [[Code generation (compiler)|Code generation]]
|-
| [[ACL2]] || 8.3 || [[Matt Kaufmann]] and [[J Strother Moore]] ||  [[Common Lisp]]     || {{no}}  || {{n/a|Untyped}}  || {{no}}  || {{yes}} || {{yes}}<ref>{{cite book|last=Hunt|first=Warren|author2=Matt Kaufmann |author3=Robert Bellarmine Krug |author4=J Moore |author5=Eric W. Smith |title=Theorem Proving in Higher Order Logics|chapter=Meta Reasoning in ACL2|series=Lecture Notes in Computer Science|year=2005|volume=3603|pages=163–178|doi=10.1007/11541868_11|isbn=978-3-540-28372-0|chapter-url=http://www.cs.utexas.edu/~moore/publications/meta-05.pdf}}</ref> || {{n/a|Already executable}}
|-
| [[Agda (programming language)|Agda]] || 2.6.4.3<ref name="github-agda" />
|| Ulf Norell, Nils Anders Danielsson, and Andreas Abel ([[Chalmers University of Technology|Chalmers]] and [[University of Gothenburg|Gothenburg]])<ref name="github-agda" /> ||[[Haskell (programming language)|Haskell]]<ref name="github-agda" /> || {{yes}}<br/>{{Cn|date=July 2024}} || {{yes}}<br/><ref name="agdaWiki" /> || {{yes}}<br/>{{Cn|date=July 2024}} || {{no}}<br/>{{Cn|date=July 2024}} || {{partial}}<br/>{{Cn|date=July 2024}} || {{n/a|Already executable}}<br/>{{Cn|date=July 2024}}
|-
| [[Albatross (programming language)|Albatross]] || 0.4
|| Helmut Brandl ||[[OCaml]]|| {{yes}} || {{no}} || {{yes}} || {{yes}} || {{unknown}} || {{not yet}} Implemented
|-
| [[Rocq (software)|Rocq]] (formerly known as ''Coq'') || 9.0 || [[INRIA]] || [[OCaml]] || {{yes}} || {{yes}} || {{yes}} || {{yes}} || {{yes}} || {{yes}}
|-
| [[F* (programming language)|F*]] || repository || [[Microsoft Research]] and [[INRIA]] || [[F* (programming language)|F*]] || {{yes}} || {{yes}} || {{no}} || {{yes}} || {{yes}}<ref>Search for "proofs by reflection": {{ArXiv|1803.06547}}</ref> || {{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 (programming language)|Idris]] || 2 0.6.0. || Edwin Brady || [[Idris (programming language)|Idris]] || {{yes}} || {{yes}} || {{yes}} || {{unknown}} || {{partial}} || {{yes}}
|-
| [[Isabelle (proof assistant)|Isabelle]] || Isabelle2024 (May 2024) ||[[Larry Paulson]] ([[University of Cambridge|Cambridge]]), [[Tobias Nipkow]] ([[Technische Universität München|München]]) and [[Makarius Wenzel]] ||  [[Standard ML]], [[Scala (programming language)|Scala]]    || {{yes}} || {{no}}  || {{yes}} || {{yes}} || {{yes}} || {{yes}}
|-
|[[Lean (proof assistant)|Lean]]
|v4.7.0<ref>{{Cite web|url=https://github.com/leanprover/lean4/releases|title=Lean 4 Releases Page |website=GitHub |access-date=15 October 2023}}</ref>
|[[Leonardo de Moura]] ([[Microsoft Research]])
|[[C++]], Lean
|{{yes}}
|{{yes}}
|{{yes}}
|{{yes}}
|{{yes}}
|{{yes}}
|-
| [[LEGO (proof assistant)|LEGO]] || 1.3.1 || [[Randy Pollack]] ([[University of Edinburgh|Edinburgh]]) || [[Standard ML]] || {{yes}} || {{yes}} || {{yes}} || {{no}} || {{no}} || {{no}}
|-
| [[Metamath]] || v0.198<ref>{{cite web | url=https://github.com/metamath/metamath-exe/releases/tag/v0.198 | title=Release v0.198 · metamath/Metamath-exe | website=[[GitHub]] }}</ref> || Norman Megill || [[ANSI C]] ||  ||  ||  ||  ||  || 
|-
| [[Mizar system|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}}
|-
| [[Prototype Verification System|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}}
|}

* [[ACL2]]&nbsp;– a programming language, a first-order logical theory, and a theorem prover (with both interactive and automatic modes) in the Boyer–Moore tradition.
* [[Rocq (software)|Rocq]] (formerly known as ''Coq'') &nbsp;– 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]]s&nbsp;– 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]]&nbsp;– The "primary descendant", still under active development. Support for both [[Moscow ML]] and [[Poly/ML]]. Has a [[BSD-style license]].
**[[HOL Light]]&nbsp;– A thriving "minimalist fork". [[OCaml]] based.
**ProofPower&nbsp;– Went proprietary, then returned to open source. Based on [[Standard ML]].
* IMPS, An Interactive Mathematical Proof System.<ref>{{cite journal |last1=Farmer |first1=William M. |last2=Guttman |first2=Joshua D. |last3=Thayer |first3=F. Javier |title=IMPS: An interactive mathematical proof system |journal=Journal of Automated Reasoning |date=1993 |volume=11 |issue=2 |pages=213–248 |doi=10.1007/BF00881906 |s2cid=3084322 |access-date=22 January 2020|url=https://core.ac.uk/display/23376340|url-access=subscription }}</ref>
* [[Isabelle theorem prover|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 (software)|Jape]]&nbsp;– Java based.
* [[Lean (proof assistant)|Lean]]
* [[LEGO (proof assistant)|LEGO]]
* [[Matita]]&nbsp;– A light system based on the Calculus of Inductive Constructions.
* [[MINLOG]]&nbsp;– A proof assistant based on first-order minimal logic.
* [[Mizar system|Mizar]]&nbsp;– A proof assistant based on first-order logic, in a [[natural deduction]] style, and [[Tarski–Grothendieck set theory]].
* [[PhoX]]&nbsp;– A proof assistant based on higher-order logic which is eXtensible.
* [[Prototype Verification System]] (PVS)&nbsp;– a proof language and system based on higher-order logic.
* [[Theorem Proving System|TPS]] and ETPS&nbsp;– Interactive theorem provers also based on simply typed lambda calculus, but based on an independent [[Q0 Logic|formulation]] of the logical theory and independent implementation.