This is a talk by Prof Kevin Buzzard given at Microsoft Research recently. In it, he proposes a program for formalizing the undergraduate mathematics curriculum in Lean. I personally found it fascinating, partly because this goal resonates strongly with me, but also because of the cultural and sociological observations. The overlap between “real mathematicians” and the the theorem proving space is incredibly tiny, so Prof Buzzard has been able to make a significant impact, working with undergraduates, largely because very few other people are doing that kind of work.

        Comments