Title: Formalization

Abstract: 
I will begin with some general remarks on why it may make sense to
formalize mathematics, i.e., write proofs in a formal language that can be
understood and checked by a computer program. I will then give a live
demonstration on how such a proof can be put together.