What is the point of Lean's maths library?
Kevin Buzzard
12-Aug-2021, 17:00-18:00 (3 years ago)
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.
Computer sciencealgebraic topologycategory theorylogic
Audience: learners
( chat )
Organizers: | Shaowei Lin, Tim Hosgood* |
*contact for this listing |
Export talk to