The mathematical significance of proof theory

Returning to old ideas of Kreisel. I discuss how the mathematics of proof theory, often combined with tricks of the trade, can occasionally be useful in extracting hidden information from informal proofs in various areas of mathematics.