Formalizing mathematics in Lean

Speaker: Floris van Doorn
Tuesday 9 November 2021, 11:00, (Salle des Thèses, bâtiment 650)

Abstract: Lean's mathematical library mathlib is a rapidly growing unified library of formalized mathematics. The library contains a large part of an undergraduate math curriculum, many graduate topics, and some projects based on mathlib address more advanced topic I will give an overview of the design decisions in mathlib to make it suitable for formalizing mathematics, and some of the recent milestones in the library.

Slides: here