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
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.
