Automated Theorem Proving

Automated theorem proving (ATP) is the use of computer programs to find or verify mathematical proofs without human intervention in the inference steps. ATP systems treat proof construction as a search problem in a vast space of possible logical derivations, using heuristics, decision procedures, and brute-force enumeration to find paths from axioms to target theorems.

The field's greatest successes are in decidable fragments: propositional logic (SAT solvers), first-order logic (resolution provers), and specific theories like linear arithmetic. In these domains, modern ATP systems can solve problems with millions of variables. The frontier lies in combining automated search with human guidance — the interactive theorem proving paradigm — and in extending automation to higher-order logic and proof by induction, where undecidability means that fully automated proofs remain impossible in general.