BEGIN:VCALENDAR
VERSION:2.0
PRODID:researchseminars.org
CALSCALE:GREGORIAN
X-WR-CALNAME:researchseminars.org
BEGIN:VEVENT
SUMMARY:Kevin Buzzard
DTSTART:20210812T170000Z
DTEND:20210812T180000Z
DTSTAMP:20260417T095353Z
UID:ToposInstituteColloquium/33
DESCRIPTION:Title: <a href="https://researchseminars.org/talk/ToposInstitu
 teColloquium/33/">What is the point of Lean's maths library?</a>\nby Kevin
  Buzzard as part of Topos Institute Colloquium\n\n\nAbstract\nLean is a co
 mputer proof checker developed by Microsoft Research. Over the last four y
 ears 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 ide
 a 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 plan
 s 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 p
 roof checkers will be necessary to follow the talk.\n
LOCATION:https://researchseminars.org/talk/ToposInstituteColloquium/33/
END:VEVENT
END:VCALENDAR