Kevin Buzzard: “What is the point of Lean’s maths library?“

12th of August, 2021. Part of the Topos Institute Colloquium. ----- Abstract: Lean is a computer proof checker developed by Microsoft Research. Over the last four years I have been part of a team of mathematicians and computer scientists who have got it into their heads that it is somehow “obviously“ a good idea to build a formally verified library of modern mathematics in Lean. You can think of it as a 21st century Bourbaki if you like, although our plans are actually far grander than Bourbaki’s. I will talk about two things: (1) how it’s going and (2) why we’re doing it. No background in computer proof checkers will be necessary to follow the talk.