Proof theory is the branch of mathematical logic that studies formal proofs as syntactic objects — their structure, rules of inference, and the transformations between them — independent of the semantic models that make statements true. It underpins automated theorem proving, type theory, and formal verification, providing the rules by which a machine can check or search for a valid derivation of a conclusion from axioms. Results such as cut-elimination and normalisation are central to its use in computer science.