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.
Automated proof checking is the process of using software for checking proofs for correctness. It is one of the most developed fields in automated reasoning. Automated proof checking differs from automated theorem proving in that automated proof checking simply mechanically checks the formal workings of an existing proof, instead of trying to develop new proofs or theorems itself. Because of this, the task of automated proof verification is much simpler than that of automated theorem proving, allowing automated proof checking software to be much simpler than automated theorem proving software.
Because of this small size, some automated proof checking systems can have less than a thousand lines of core code, and are thus themselves amenable to both hand-checking and automated software verification. The Mizar system, HOL Light, and Metamath are examples of automated proof checking systems. Automated proof checking can be done either as a batch operation, or interactively, as part of an interactive theorem proving system.
In 1956, Newell, Shaw, and Simon developed Logic Theorist, which was the first automated theorem prover and proved 38 out of the first 52 theorems in Whitehead and Russell's Principia Mathematica.
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.
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, Isabelle by Makarius Wenzel, and for Lean 4 by the leanprover developers.
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.
The following is a list of notable proofs that have been formalized within proof assistants.