Proof assistant: Difference between revisions

From Wikipedia, the free encyclopedia
Jump to navigation Jump to search
VisualWikitext
imported>OAbot
m Open access bot: url-access updated in citation with #oabot.
 
imported>GhostInTheMachine
Changing short description from "interactive software theorem prover" to "Interactive theorem prover software"
 
Line 1: Line 1:
{{Short description|Software tool to assist with the development of formal proofs by human–machine collaboration}}
{{Short description|Interactive theorem prover software}}
{{for|verification in computer science|formal verification}}
{{hatnote group|
{{for|the academic conference|Interactive Theorem Proving (conference)}}
{{for|verification in computer science|Formal verification}}
}}
{{distinguish|Interactive proof system}}
{{distinguish|Interactive proof system}}
{{missing information|[[automated proof checking]]|date=February 2024}}
{{missing information|[[automated proof checking]]|date=February 2024}}
{{more footnotes|date=November 2018}}
{{more footnotes|date=November 2018}}


[[Image:CoqProofOfDecidablityOfEqualityOnNaturalNumbers.png|thumb|upright=1.7|An interactive proof session in CoqIDE, showing the proof script on the left and the proof state on the right]]
[[Image:CoqProofOfDecidablityOfEqualityOnNaturalNumbers.png|thumb|upright=1.7|An interactive proof session in RocqIDE, showing the proof script on the left and the proof state on the right]]
In [[computer science]] and [[mathematical logic]], a '''proof assistant''' or '''interactive theorem prover''' is a software tool to assist with the development of [[formal proof]]s by human–machine collaboration. This involves some sort of interactive proof editor, or other [[User interface|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]].
In [[computer science]] and [[mathematical logic]], a '''proof assistant''' or '''interactive theorem prover''' is a software tool to assist with the development of [[formal proof]]s by human–machine collaboration. This involves some sort of interactive proof editor, or other [[User interface|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.<ref>{{Cite web |last=Ornes |first=Stephen |date=August 27, 2020 |title=Quanta Magazine – How Close Are Computers to Automating Mathematical Reasoning? |url=https://www.quantamagazine.org/how-close-are-computers-to-automating-mathematical-reasoning-20200827/}}</ref>
A recent effort within this field is making these tools use [[artificial intelligence]] to automate the formalization of ordinary mathematics.<ref>{{Cite web |last=Ornes |first=Stephen |date=August 27, 2020 |title=Quanta Magazine – How Close Are Computers to Automating Mathematical Reasoning? |url=https://www.quantamagazine.org/how-close-are-computers-to-automating-mathematical-reasoning-20200827/}}</ref>
== History ==
{{Expand section|date=December 2025}}
[[Automath]], which was developed by [[Nicolaas Govert de Bruijn]] starting in 1967, is often considered the first proof checker and the first system to utilize the [[Curry–Howard correspondence]] between programs and proofs.<ref>{{Cite journal|url=https://www.cs.ru.nl/~herman/PUBS/proofassistants.pdf|title=Proof Assistants: history, ideas and future|last=Geuvers|first=Herman|date=16 July 2009|journal=[[Sādhanā (journal)|Sādhanā]]|volume=34|pages=3-25}}</ref>


== {{anchor|Comparison}}System comparison ==
== {{anchor|Comparison}}System comparison ==
Line 18: Line 23:
! rowspan=2 | Name !! rowspan=2 | Latest version !! rowspan=2 | Developer(s) !! rowspan=2 | Implementation language !! colspan=6 | Features
! 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]]
! [[Higher-order logic]] !! [[Dependent type]]s !! [[de Bruijn criterion|Small<br/>kernel]] !! [[Proof automation]] !! Proof by<br/>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}}
| [[ACL2]] || 8.3 || [[Matt Kaufmann]], [[J Strother Moore]] || [[Common Lisp]] || {{no}} || {{n/a|Untyped}} || {{no}} || {{yes}} || {{yes}}<ref>{{cite book |last1=Hunt |first1=Warren |last2=Kaufmann |first2=Matt |author2-link=Matt Kaufmann |last3=Krug |first3=Robert Bellarmine |last4=Moore |first4=J. |last5=Smith |first5=Eric W. |year=2005 |title=Theorem Proving in Higher Order Logics |chapter=Meta Reasoning in ACL2|series=Lecture Notes in Computer Science |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" />
| [[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]]<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}}
|| 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
| Albatross || 0.4 || Helmut Brandl || [[OCaml]] || {{yes}} || {{no}} || {{yes}} || {{yes}} || {{unknown}} || {{not yet}} implemented
|| 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}}
| [[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}}
Line 36: Line 37:
| [[HOL4]] || Kananaskis-13 (or repo) || Michael Norrish, Konrad Slind, and others || [[Standard ML]] || {{yes}} || {{no}} || {{yes}} || {{yes}} || {{no}} || {{yes}}
| [[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}}
| [[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}}
| [[Isabelle (proof assistant)|Isabelle]] || Isabelle2025 (March 2025) || [[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]]
|[[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>
|v4.23.0<ref>{{Cite web|url=https://github.com/leanprover/lean4/releases|title=Lean 4 Releases Page |website=GitHub |access-date=22 September 2025}}</ref>
|[[Leonardo de Moura]] ([[Microsoft Research]])
|[[Leonardo de Moura]] ([[Microsoft Research]])
|[[C++]], Lean
|[[C++]], Lean
Line 51: Line 52:
|{{yes}}
|{{yes}}
|-
|-
| [[LEGO (proof assistant)|LEGO]] || 1.3.1 || [[Randy Pollack]] ([[University of Edinburgh|Edinburgh]]) || [[Standard ML]] || {{yes}} || {{yes}} || {{yes}} || {{no}} || {{no}} || {{no}}
| [[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]] || || || || || ||  
| [[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}}
| [[Mizar system|Mizar]] || 8.1.11 || [[Białystok University]] || [[Free Pascal]] || {{partial}} || {{yes}} || {{no}} || {{no}} || {{no}} || {{no}}
|-
|-
| [[Nqthm]] || || || || || || || || ||  
| [[Nqthm]] || || || || || || || || ||  
|-
|-
| [[NuPRL]] || 5 || [[Cornell University]] || [[Common Lisp]] || {{yes}} || {{yes}} || {{yes}} || {{yes}} || {{unknown}} || {{yes}}
| [[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}}
| [[Prototype Verification System|PVS]] || 6.0 || [[SRI International]] || [[Common Lisp]] || {{yes}} || {{yes}} || {{no}} || {{yes}} || {{no}} || {{unknown}}
|-
| [[Rocq]]<!-- Former 'Coq' --> || 9.0 || [[INRIA]] || [[OCaml]] || {{yes}} || {{yes}} || {{yes}} || {{yes}} || {{yes}} || {{yes}}
|-
|-
| [[Twelf]] || 1.7.1     || [[Frank Pfenning]] and [[Carsten Schürmann]] ||     [[Standard ML]]     || {{yes}} || {{yes}} || {{unknown}} || {{no}} || {{no}} || {{unknown}}
| [[Twelf]] || 1.7.1 || [[Frank Pfenning]], 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.
* [[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 (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.
* [[Rocq]] (former name: ''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]]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:
* [[HOL theorem prover]]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]]&nbsp;– The "primary descendant", still under active development. Support for both [[Moscow ML]] and [[Poly/ML]]. Has a [[BSD-style license]].
**[[HOL4]] – 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.
**[[HOL Light]] – A thriving "minimalist fork". [[OCaml]] based.
**ProofPower&nbsp;– Went proprietary, then returned to open source. Based on [[Standard ML]].
**ProofPower – 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>
* 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.
* [[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.
* [[Jape (software)|Jape]] – Java based.
* [[Lean (proof assistant)|Lean]]
* [[Lean (proof assistant)|Lean]]
* [[LEGO (proof assistant)|LEGO]]
* [[LEGO (proof assistant)|LEGO]]
* [[Matita]]&nbsp;– A light system based on the Calculus of Inductive Constructions.
* [[Matita]] – A light system based on the Calculus of Inductive Constructions.
* [[MINLOG]]&nbsp;– A proof assistant based on first-order minimal logic.
* [[MINLOG]] – 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]].
* [[Mizar system|Mizar]] – 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.
* [[PhoX]] – 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.
* [[Prototype Verification System]] (PVS) – 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.
* [[Theorem Proving System]] (TPS) and ETPS – 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.


== User interfaces ==
== User interfaces ==
A popular front-end for proof assistants is the [[Emacs]]-based Proof General, developed at the [[University of Edinburgh]].
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 (programming language)|Scala]] infrastructure for document-oriented proof processing. More recently, [[Visual Studio Code]] extensions have been developed for Coq,<ref>{{Cite web|url=https://github.com/coq-community/vscoq|title=coq-community/vscoq|date=July 29, 2024|via=GitHub}}</ref> Isabelle by Makarius Wenzel,<ref>{{cite web |last1=Wenzel |first1=Makarius |title=Isabelle |url=https://marketplace.visualstudio.com/items?itemName=makarius.isabelle |access-date=2 November 2019}}</ref> and for Lean 4 by the leanprover developers.<ref>{{cite web |title=VS Code Lean 4 |url=https://github.com/leanprover/vscode-lean4 |website=GitHub |access-date=15 October 2023}}</ref>
Rocq includes RocqIDE, which is based on OCaml/[[Gtk]]. Isabelle includes Isabelle/jEdit, which is based on [[jEdit]] and the Isabelle/[[Scala (programming language)|Scala]] infrastructure for document-oriented proof processing. More recently, [[Visual Studio Code]] extensions have been developed for Rocq,<ref>{{Cite web|url=https://github.com/coq-community/vscoq|title=coq-community/vscoq|date=July 29, 2024|via=GitHub}}</ref> Isabelle by Makarius Wenzel,<ref>{{cite web |last1=Wenzel |first1=Makarius |title=Isabelle |url=https://marketplace.visualstudio.com/items?itemName=makarius.isabelle |access-date=2 November 2019}}</ref> and for Lean 4 by the leanprover developers.<ref>{{cite web |title=VS Code Lean 4 |url=https://github.com/leanprover/vscode-lean4 |website=GitHub |access-date=15 October 2023}}</ref>


== Formalization extent ==
== 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.<ref>{{cite web |url=https://www.cs.ru.nl/~freek/100/ |title=Formalizing 100 Theorems |first=Freek |last=Wiedijk |date=15 September 2023 }}</ref><ref>{{cite journal |url=https://www.ias.ac.in/article/fulltext/sadh/034/01/0003-0025 |title=Proof assistants: History, ideas and future |first=Herman |last=Geuvers |journal=Sādhanā |volume=34 |issue=1 |date=February 2009 |pages=3–25 |doi= 10.1007/s12046-009-0001-5|s2cid=14827467 |doi-access=free |hdl=2066/75958 |hdl-access=free }}</ref>
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 2025, only six systems have formalized proofs of more than 70% of the theorems, namely Isabelle, HOL Light, Lean, Rocq, Metamath and Mizar.<ref>{{cite web |url=https://www.cs.ru.nl/~freek/100/ |title=Formalizing 100 Theorems |first=Freek |last=Wiedijk |date=22 September 2025 }}</ref><ref>{{cite journal |url=https://www.ias.ac.in/article/fulltext/sadh/034/01/0003-0025 |title=Proof assistants: History, ideas and future |first=Herman |last=Geuvers |journal=Sādhanā |volume=34 |issue=1 |date=February 2009 |pages=3–25 |doi= 10.1007/s12046-009-0001-5|s2cid=14827467 |doi-access=free |hdl=2066/75958 |hdl-access=free }}</ref>


== Notable formalized proofs ==
== Notable formalized proofs ==
Line 103: Line 106:
! scope="col" | Year
! scope="col" | Year
|-
|-
| [[Four color theorem]]<ref>{{Citation |last=Gonthier |first=Georges |author-link=Georges Gonthier |title=Formal Proof—The Four-Color Theorem |journal=[[Notices of the American Mathematical Society]] |volume=55 |year=2008 |url=https://www.ams.org/notices/200811/tx081101382p.pdf |archive-url=https://web.archive.org/web/20110805094909/http://www.ams.org/notices/200811/tx081101382p.pdf |archive-date=2011-08-05 |url-status=live |issue=11 |pages=1382–1393 |mr=2463991 }}</ref> || Coq || 2005
| [[Four color theorem]]<ref>{{Citation |last=Gonthier |first=Georges |author-link=Georges Gonthier |title=Formal Proof—The Four-Color Theorem |journal=[[Notices of the American Mathematical Society]] |volume=55 |year=2008 |url=https://www.ams.org/notices/200811/tx081101382p.pdf |archive-url=https://web.archive.org/web/20110805094909/http://www.ams.org/notices/200811/tx081101382p.pdf |archive-date=2011-08-05 |url-status=live |issue=11 |pages=1382–1393 |mr=2463991 }}</ref> || Rocq || 2005
|-
|-
| [[Feit–Thompson theorem]]<ref>{{Cite web |date=2016-11-19 |title=Feit thomson proved in coq - Microsoft Research Inria Joint Centre |url=http://www.msr-inria.fr/news/feit-thomson-proved-in-coq/ |access-date=2023-12-07 |archive-url=https://web.archive.org/web/20161119094854/http://www.msr-inria.fr/news/feit-thomson-proved-in-coq/ |archive-date=2016-11-19 }}</ref> || Coq || 2012
| [[Feit–Thompson theorem]]<ref>{{Cite web |date=2016-11-19 |title=Feit thomson proved in coq - Microsoft Research Inria Joint Centre |url=http://www.msr-inria.fr/news/feit-thomson-proved-in-coq/ |access-date=2023-12-07 |archive-url=https://web.archive.org/web/20161119094854/http://www.msr-inria.fr/news/feit-thomson-proved-in-coq/ |archive-date=2016-11-19 }}</ref> || Rocq || 2012
|-
|-
| [[Fundamental group]] of the [[circle]]<ref>{{Cite book |title=2013 28th Annual ACM/IEEE Symposium on Logic in Computer Science |url=https://ieeexplore.ieee.org/document/6571554 |access-date=2023-12-07 |doi=10.1109/lics.2013.28 |date=2013 |last1=Licata |first1=Daniel R. |last2=Shulman |first2=Michael |chapter=Calculating the Fundamental Group of the Circle in Homotopy Type Theory |pages=223–232 |arxiv=1301.3443 |isbn=978-1-4799-0413-6 |s2cid=5661377 }}</ref> || Coq || 2013
| [[Fundamental group]] of the [[circle]]<ref>{{Cite book |title=2013 28th Annual ACM/IEEE Symposium on Logic in Computer Science |doi=10.1109/lics.2013.28 |date=2013 |last1=Licata |first1=Daniel R. |last2=Shulman |first2=Michael |chapter=Calculating the Fundamental Group of the Circle in Homotopy Type Theory |pages=223–232 |arxiv=1301.3443 |isbn=978-1-4799-0413-6 |s2cid=5661377 }}</ref> || Rocq || 2013
|-
|-
|[[Erdős–Graham problem]]<ref>{{Cite web |date=2022-03-11 |title=Math Problem 3,500 Years In The Making Finally Gets A Solution |url=https://www.iflscience.com/math-problem-3500-years-in-the-making-finally-gets-a-solution-62925 |access-date=2024-02-09 |website=IFLScience |language=en}}</ref><ref>{{Cite arXiv |last=Avigad |first=Jeremy |date=2023 |class=math.HO |title=Mathematics and the formal turn |eprint=2311.00007 }}</ref>
|[[Erdős–Graham problem]]<ref>{{Cite web |date=2022-03-11 |title=Math Problem 3,500 Years In The Making Finally Gets A Solution |url=https://www.iflscience.com/math-problem-3500-years-in-the-making-finally-gets-a-solution-62925 |access-date=2024-02-09 |website=IFLScience |language=en}}</ref><ref>{{Cite arXiv |last=Avigad |first=Jeremy |date=2023 |class=math.HO |title=Mathematics and the formal turn |eprint=2311.00007 }}</ref>
Line 116: Line 119:
|-
|-
|[[Busy Beaver|BB(5)]] = 47,176,870<ref>{{Cite web |date=2024-07-02 |title=We have proved "BB(5) = 47,176,870" |url=https://discuss.bbchallenge.org/t/july-2nd-2024-we-have-proved-bb-5-47-176-870/237 |access-date=2024-07-09 |website=The Busy Beaver Challenge |language=en}}</ref>
|[[Busy Beaver|BB(5)]] = 47,176,870<ref>{{Cite web |date=2024-07-02 |title=We have proved "BB(5) = 47,176,870" |url=https://discuss.bbchallenge.org/t/july-2nd-2024-we-have-proved-bb-5-47-176-870/237 |access-date=2024-07-09 |website=The Busy Beaver Challenge |language=en}}</ref>
|Coq
|Rocq
|2024
|2024
|}
|}

Latest revision as of 14:08, 18 December 2025

Template:Short description Template:Hatnote group Script error: No such module "Distinguish". Template:Missing information Template:More footnotes

File:CoqProofOfDecidablityOfEqualityOnNaturalNumbers.png
An interactive proof session in RocqIDE, showing the proof script on the left and the proof state on the right

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]

History

Script error: No such module "Unsubst". Automath, which was developed by Nicolaas Govert de Bruijn starting in 1967, is often considered the first proof checker and the first system to utilize the Curry–Howard correspondence between programs and proofs.[2]

Script error: No such module "anchor".System comparison

Script error: No such module "Labelled list hatnote".

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, J Strother Moore Common Lisp No Untyped No Yes Yes[3] Already executable
Agda 2.6.4.3[4] Ulf Norell, Nils Anders Danielsson, and Andreas Abel (Chalmers and Gothenburg)[4] Haskell[4] Yes
Script error: No such module "Unsubst".		 Yes
[5]		 Yes
Script error: No such module "Unsubst".		 No
Script error: No such module "Unsubst".		 Partial
Script error: No such module "Unsubst".		 Already executable
Script error: No such module "Unsubst".
Albatross 0.4 Helmut Brandl OCaml Yes No Yes Yes Un­known Not yet implemented
F* repository Microsoft Research and INRIA F* Yes Yes No Yes Yes[6] 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 Un­known Partial Yes
Isabelle Isabelle2025 (March 2025) Larry Paulson (Cambridge), Tobias Nipkow (München) and Makarius Wenzel Standard ML, Scala Yes No Yes Yes Yes Yes
Lean v4.23.0[7] Leonardo de Moura (Microsoft Research) C++, Lean Yes Yes Yes Yes Yes Yes
LEGO 1.3.1 Randy Pollack (Edinburgh) Standard ML Yes Yes Yes No No No
Metamath v0.198[8] 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 Un­known Yes
PVS 6.0 SRI International Common Lisp Yes Yes No Yes No Un­known
Rocq 9.0 INRIA OCaml Yes Yes Yes Yes Yes Yes
Twelf 1.7.1 Frank Pfenning, Carsten Schürmann Standard ML Yes Yes Un­known No No Un­known
  • 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 (former name: 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 provers – 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:
  • IMPS, An Interactive Mathematical Proof System.[9]
  • 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
  • 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.
  • Theorem Proving System (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-based Proof General, developed at the University of Edinburgh.

Rocq includes RocqIDE, 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 Rocq,[10] Isabelle by Makarius Wenzel,[11] and for Lean 4 by the leanprover developers.[12]

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 2025, only six systems have formalized proofs of more than 70% of the theorems, namely Isabelle, HOL Light, Lean, Rocq, Metamath and Mizar.[13][14]

Notable formalized proofs

Script error: No such module "Labelled list hatnote".

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

Theorem Proof assistant Year
Four color theorem[15] Rocq 2005
Feit–Thompson theorem[16] Rocq 2012
Fundamental group of the circle[17] Rocq 2013
Erdős–Graham problem[18][19] Lean 2022
Polynomial Freiman-Ruzsa conjecture over 𝔽2[20] Lean 2023
BB(5) = 47,176,870[21] Rocq 2024

See also

Notes

<templatestyles src="Reflist/styles.css" />

  1. ↑ Script error: No such module "citation/CS1".
  2. ↑ Script error: No such module "Citation/CS1".
  3. ↑ Script error: No such module "citation/CS1".
  4. ↑ a b c Script error: No such module "citation/CS1".
  5. ↑ Script error: No such module "citation/CS1".
  6. ↑ Search for "proofs by reflection": arXiv:1803.06547File:Lock-green.svg
  7. ↑ Script error: No such module "citation/CS1".
  8. ↑ Script error: No such module "citation/CS1".
  9. ↑ Script error: No such module "Citation/CS1".
  10. ↑ Script error: No such module "citation/CS1".
  11. ↑ Script error: No such module "citation/CS1".
  12. ↑ Script error: No such module "citation/CS1".
  13. ↑ Script error: No such module "citation/CS1".
  14. ↑ Script error: No such module "Citation/CS1".
  15. ↑ Script error: No such module "citation/CS1".
  16. ↑ Script error: No such module "citation/CS1".
  17. ↑ Script error: No such module "citation/CS1".
  18. ↑ Script error: No such module "citation/CS1".
  19. ↑ Script error: No such module "citation/CS1".
  20. ↑ Script error: No such module "citation/CS1".
  21. ↑ Script error: No such module "citation/CS1".

Script error: No such module "Check for unknown parameters".

References

  • Script error: No such module "citation/CS1".
  • Script error: No such module "citation/CS1".
  • Script error: No such module "citation/CS1".
  • Script error: No such module "citation/CS1".
  • Script error: No such module "citation/CS1".

External links

Script error: No such module "Unsubst".

Catalogues

de:Maschinengestütztes Beweisen

Retrieved from "http://debianws.lexgopc.com/wiki143/index.php?title=Proof_assistant&oldid=5569876"