BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Memento EPFL//
BEGIN:VEVENT
SUMMARY:Interactive theorem provers: can they help mathematicians?
DTSTART:20231129T160000
DTEND:20231129T170000
DTSTAMP:20260407T111213Z
UID:c15872c92a8f8afc5123015d1f2a3e68c5fb9a54bdd3e4852258843a
CATEGORIES:Conferences - Seminars
DESCRIPTION:Professor Kevin Buzzard - Imperial College London\nAssyr Abdul
 le Lecture - Bernoulli Centre\n\nAbstract : An interactive theorem prover
  is\, amongst other things\, a programming language which is sufficiently 
 rich that it can in theory understand modern mathematical research. Two na
 tural questions then arise. First\, can these systems understand modern ma
 thematical research _in practice_\, and secondly\, can they actually help 
 us mathematicians to do it? For many years the answer to both questions wa
 s a resounding "no". But recently things have begun to change. There are s
 everal examples of recently-proved theorems which have been checked by Lea
 n. Furthermore\, interacting with these systems forces you to tidy up your
  ideas and think clearly about abstractions\, which can have unexpected po
 sitive practical consequences. Also\, modern systems are opening up new po
 ssibilities for teaching and communicating mathematics. I will give an ove
 rview of what has been going on recently in this area\, suitable for mathe
 maticians\; no background from computer science will be assumed.\n\nRegist
 ration before November 22\, 2023 is required - thank you\n\n\n\n\n\n\n\n 
LOCATION:SV 1717 https://plan.epfl.ch/?room==SV%201717
STATUS:CONFIRMED
END:VEVENT
END:VCALENDAR