Theorem Prover and Proof Checker

Decidability of the problem
Depending on the underlying logic, the problem of deciding the validity of a theorem varies from trivial to impossible. For the frequent case of propositional logic, the problem is decidable but NP-complete, and hence only exponential-time algorithms are believed to exist for general proof tasks. For a first order predicate calculus, that is having no proper axioms, Gödel's Completeness Theorem states that the theorems are exactly the logically valid well-formed formulas, so identifying theorems is recursively enumerable, i.e., given unbounded resources, any valid theorem can eventually be proven. Invalid statements, i.e. formulas that are not entailed by a given theory, cannot always be recognized. In addition, a consistent formal theory that contains the first-order theory of the natural numbers (having certain proper axioms then), by Gödel's incompleteness theorems, contains a true statement which cannot be proven, in which case a theorem prover trying to prove such a statement ends up in nontermination.
In these cases, a first-order theorem prover may fail to terminate while searching for a proof. Despite these theoretical limits, practical theorem provers can solve many hard problems in these logics.

(1) Theorem proving is recursively enumerable
(2) Proof verification: whether an existing proof for a theorem is certified valid or not. Decidable
(3) Interactive theorem provers require a human user to give hints to the system. Depending on the degree of automation, the prover can essentially be reduced to a proof checker, with the user providing the proof in a formal way, or significant proof tasks can be performed automatically. Hard problems usually requires a proficient user.
(4) Model checking, which is equivalent to brute-force enumeration of many possible states (although the actual implementation of model checkers requires much cleverness, and does not simply reduce to brute force).