Video/Kevin Buzzard: "What is the point of Lean's maths library?"
Buzzard, Kevin (Aug 13, 2021). Kevin Buzzard: "What is the point of Lean's maths library?". local page: Topos Institute.
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.
mathlib
In this talk, Kevin Buzzard also talked about mathlib extensively.