Automatic proof checkers verify the validity of formal proofs, while proof assistants aid in the construction of formal proofs. Some popular systems: Mizar, Coq, Isabelle. For automated theorem provers use the (automated-theorem-proving) tag

This tag is for questions concerning automated proof checkers and proof assistants.

An automated proof checker (or proof verifier) is a program designed to check the validity of a formal proof.

A proof assistant is a program designed to aid in the construction of a formal proof, and likely includes an interactive proof editor.

Some popular systems: Mizar, Coq, Isabelle. For automated theorem provers, use the tag

history | excerpt history