BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//talks.cam.ac.uk//v3//EN
BEGIN:VTIMEZONE
TZID:Europe/London
BEGIN:DAYLIGHT
TZOFFSETFROM:+0000
TZOFFSETTO:+0100
TZNAME:BST
DTSTART:19700329T010000
RRULE:FREQ=YEARLY;BYMONTH=3;BYDAY=-1SU
END:DAYLIGHT
BEGIN:STANDARD
TZOFFSETFROM:+0100
TZOFFSETTO:+0000
TZNAME:GMT
DTSTART:19701025T020000
RRULE:FREQ=YEARLY;BYMONTH=10;BYDAY=-1SU
END:STANDARD
END:VTIMEZONE
BEGIN:VEVENT
CATEGORIES:Formalisation of mathematics with interactive theo
 rem provers 
SUMMARY:How to prove Fermat's Last Theorem - Professor Kev
 in Buzzard (Imperial College London)
DTSTART;TZID=Europe/London:20240208T170000
DTEND;TZID=Europe/London:20240208T180000
UID:TALK210157AThttp://talks.cam.ac.uk
URL:http://talks.cam.ac.uk/talk/index/210157
DESCRIPTION:The statement of Fermat's Last Theorem would have 
 been comprehensible to Diophantus\, who lived near
 ly 2000 years ago. The question was explicitly rai
 sed by Fermat in the 1600s\, and was resolved by W
 iles and Taylor in the 1990s\, when I was a PhD st
 udent of Taylor. In 2023 I got an EPSRC grant to b
 egin formalising the proof in the Lean theorem pro
 ver.\n\nIn my talk I'll start with a history of th
 e problem\, and say something about the contributi
 ons made by computers in the pre-Wiles era. Withou
 t going into details\, I'll then say a little bit 
 about the proof (due to Taylor) which I'm going to
  formalise\, how it differs from Wiles' original a
 pproach (it is broadly but not exactly the same)\,
  and what factors influenced the choice of route t
 o the top. I'll finish by talking about the infras
 tructure which I'll be using in order to run the p
 roject as an open source multi-author collaborativ
 e experiment. \n\nIt is probably worth stressing t
 hat this talk is suitable for a general audience f
 amiliar with the idea of formalisation but with no
  background in modern number theory\, and in parti
 cular it will not be a technical explanation of th
 e route we're taking.\n\n---\n\nWATCH ONLINE HERE 
 : https://www.microsoft.com/en-gb/microsoft-teams/
 join-a-meeting?rtc=1 Meeting ID: 370 771 279 261 P
 asscode: iCo7a5
LOCATION:Live-streamed at MR14 Centre for Mathematical Scie
 nces
CONTACT:Anand Rao Tadipatri
END:VEVENT
END:VCALENDAR