A proof assistant is an application program that helps humans construct machine-checked proofs.

A proof assistant is an application program that helps humans construct machine-checked proofs. Typical proof assistants are based on relatively strong logic calculi, like Higher-Order Logic, Set Theory, or variants of Type Theory. This allows mathematical modeling with a rich formal language, with specifications and proofs similar to pen-and-paper mathematics, but the high assurance provided by mechine-checked proofs.

Some notable proof assistants (in alphabetical order):

  • ACL2

  • Agda

  • Automath (historic)

  • Coq

  • HOL: HOL4, HOL-Light, ProofPower

  • Isabelle: with object-logics Isabelle/HOL, Isabelle/ZF

  • LCF (historic)

  • Mizar

  • NuPRL

  • PVS

Modern proof assistants integrate a range of automated reasoning tools, which occasionally blurs the boundary between Interactive Theorem Proving (ITP) and Automated Theorem Proving (ATP).

Moreover there is often some integration with computation, as part of the logical foundation or as tool support to turn logical theories into program code. This coincidence often blurs the boundary between Programming and Proving.

history | excerpt history