Proof assistant vs theorem prover

Two ways to get a trusted proof

An automated theorem prover gets a statement and tries to find a proof without help. A proof assistant, also called an interactive theorem prover, is a program in which a person builds the proof step by step, and the system checks every step against a small trusted core.

The first is about search, the second about certainty and expressiveness. Most proof assistants work in rich logics, such as higher-order logic or dependent type theory, which are more expressive than the first-order logic used by most automatic provers.

Lean, Rocq, Isabelle and HOL Light

The Lean theorem prover, Rocq (formerly known as Coq), Isabelle, HOL Light and Agda are widely used proof assistants. Lean was started by Leonardo de Moura at Microsoft Research and has a large community library for mathematics. Isabelle has a long record in software verification and in formalised mathematics.

Landmark results

Both families have produced results worth knowing. In 1996 the automatic prover EQP settled the Robbins conjecture, a question about algebras that had been open since the 1930s. In 2005 Georges Gonthier completed a machine-checked proof of the four colour theorem in Coq. The Flyspeck project, which formally verified a proof of the Kepler conjecture, was announced complete in 2014 using HOL Light and Isabelle.

Hammers connect them

A hammer is a tool inside a proof assistant that sends the current goal, with selected facts, to external provers and SMT solvers. If one of them finds a proof, the assistant reconstructs it inside its trusted core. Sledgehammer in Isabelle is the best-known example, and it saves a great deal of routine work.

Which to learn first

To understand how search works, read about resolution and run an automatic prover on small TPTP problems. To formalise a mathematical theory or verify software, start with a proof assistant, and learn the hammer when you want to automate the dull steps.