Title: The anatomy of a proof assistant.

Abstract: A proof assistant is a program that helps formalize mathematics by automating construction of formal proofs and verifying their correctness. It employs a collection of programming techniques that seem unfamiliar to a mathematician, but are just implementations of methods that mathematicians use in everyday work, but rarely speak of them or teach them explicitly.

— Andrej Bauer