Kevin Buzzard's invited talk at CICM arguing that getting undergraduate mathematics formalised in theorem provers is useful and important. Slides at http://wwwf.imperial.ac.uk/~buzzard/one_off_lectures/ug_maths.pdf

creators hope to define objects in a way that’s useful now but flexible enough to accommodate the unanticipated uses mathematicians might have for these objects. with more complicated objects, there are maybe 10 or 20 different ways to formalize it.

Constructing proof is an art, checking them is a science. Making a distinction between the statement of a theorem and the proof is important. It means that if we have a proof of P, we can make a proof of Q. It is a function from the proofs of P to the proofs of Q. It is a function sending an element of P to an element of Q. It is a term of type P → Q. …This is why in the natural number game we use the → symbol to denote implication.