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.
This type of software provides a formal language to write mathematical definitions, executable algorithms and theorems together with an environment for semi-interactive development of machine-checked proofs.
These software tools aid the development of formal proofs by man-machine collaboration. They offer a formal language where mathematical definitions, executable algorithms and theorems co-exist, and an interactive environment keeping the current status of the proof, and updating it according to commands (usually called tactics) issued by the user.
Here’s our verdict captured in a legendary LinuxLinks-style ratings chart. They are all free and open source software.
Let’s explore the 11 proof assistants. For each title we have compiled its own portal page, a full description with an in-depth analysis of its features, a screenshot of the software in action together with links to relevant resources.
| Proof Assistants | |
|---|---|
| Rocq Prover | Formal proof management system |
| Isabelle | Generic proof assistant; express mathematical formulas in a formal language |
| Lean | Programming language and theorem prover |
| Agda | Interactive system for writing and checking proofs |
| F* | Functional language for verified programs with dependent refinement types |
| HOL4 | Interactive higher-order logic environment for rigorous theorem development |
| Aya | Dependently typed language for formalisation and certified programming |
| Lambdapi | Logical framework for defining and checking expressive type systems |
| HOL Light | Lightweight higher-order logic system with a small trusted kernel |
| PVS | Specification and verification suite for analysing complex systems |
| LISA | Scala-based platform for formal mathematics and automated reasoning |
This article has been updated to reflect the changes outlined in our recent announcement.
 Explore our carefully curated directory of recommended free and open source software, covering every major software category.The directory forms part of our extensive collection of articles for Linux enthusiasts. It includes hundreds of detailed reviews, together with free and open source alternatives to proprietary software from companies such as Google, Microsoft, Apple, Adobe, IBM, Cisco, Oracle, and Autodesk. LinuxLinks also covers interesting projects worth exploring, Linux-compatible hardware, free programming books and tutorials, and much more. Know a useful free and open source Linux application that we haven’t covered? Tell us about it using our submission form. |
Please read our Comment Policy before commenting.