Teaching mathematicians to formalise

Part of the "Learning Mathematics with Lean-2nd Event" sites.google.c...
Title: Teaching mathematicians to formalise
Speaker: Prof Kevin Buzzard
Abstract: In the last year, I have taught a graduate course and a final year undergraduate course, and the goal of each course was to teach students how to formalise mathematics in Lean. I'll give an overview of how things went.