Informal Friday Seminar: Bauer -- Lean times: 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.