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