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 automated-theorem-proving tag.
There is a separate Proof Assistants site.
