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 )


Topos Institute Colloquium

Organizers: Shaowei Lin, Tim Hosgood*
*contact for this listing

Export talk to