BEGIN:VCALENDAR
VERSION:2.0
PRODID:researchseminars.org
CALSCALE:GREGORIAN
X-WR-CALNAME:researchseminars.org
BEGIN:VEVENT
SUMMARY:Kevin Buzzard (Imperial College London)
DTSTART:20201023T160000Z
DTEND:20201023T170000Z
DTSTAMP:20260415T223259Z
UID:BMD2020/9
DESCRIPTION:Title: <a href="https://researchseminars.org/talk/BMD2020/9/">
 The Future of Mathematics?</a>\nby Kevin Buzzard (Imperial College London)
  as part of Barcelona Mathematical Days 2020\n\nLecture held in "Edifici d
 e l'Institut d'Estudis Catalans (IEC)". Carrer del Carme\, 47. Barcelona -
  Catalunya.\n\nAbstract\nI will talk about the state of the art of so-call
 ed “proof assistants”\, computer systems which right now are pretty mu
 ch incapable of assisting any mathematician with any serious proof.\nHowev
 er\, these proof assistants can do something. In fact over the last few ye
 ars the Lean proof assistant has been taught a lot of undergraduate and MS
 c algebra\, analysis\, number theory\, geometry and topology. I will give 
 a live demonstration showing what Lean can do now\, and then talk about wh
 at proof assistants might soon be able to do\, and speculate about how the
 y might be useful to mathematicians in the future.\n
LOCATION:https://researchseminars.org/talk/BMD2020/9/
END:VEVENT
END:VCALENDAR