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.

Finally, I am concerned about the state of pure mathematics research. More and more, results depend on theorems whose proofs are unpublished or sketchy (or even, in places, incorrect). We rely more and more on unnamed teams of experts who have a sufficiently broad overview of an area to be able to tell us with confidence which papers can be trusted. Fashions change, people desert areas, and I am genuinely scared that we are leaving a mess behind in some areas. There are some theorems whose proofs might be difficult or impossible to reconstruct in 20 years’ time.