BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:How to prove Fermat's Last Theorem - Professor Kevin Buzzard (Impe
 rial College London)
DTSTART:20240208T170000Z
DTEND:20240208T180000Z
UID:TALK210157@talks.cam.ac.uk
CONTACT:Anand Rao Tadipatri
DESCRIPTION:The statement of Fermat's Last Theorem would have been compreh
 ensible to Diophantus\, who lived nearly 2000 years ago. The question was 
 explicitly raised by Fermat in the 1600s\, and was resolved by Wiles and T
 aylor in the 1990s\, when I was a PhD student of Taylor. In 2023 I got an 
 EPSRC grant to begin formalising the proof in the Lean theorem prover.\n\n
 In my talk I'll start with a history of the problem\, and say something ab
 out the contributions made by computers in the pre-Wiles era. Without goin
 g 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 appro
 ach (it is broadly but not exactly the same)\, and what factors influenced
  the choice of route to the top. I'll finish by talking about the infrastr
 ucture which I'll be using in order to run the project as an open source m
 ulti-author collaborative experiment. \n\nIt is probably worth stressing t
 hat this talk is suitable for a general audience familiar with the idea of
  formalisation but with no background in modern number theory\, and in par
 ticular it will not be a technical explanation of the route we're taking.\
 n\n---\n\nWATCH ONLINE HERE : https://www.microsoft.com/en-gb/microsoft-te
 ams/join-a-meeting?rtc=1 Meeting ID: 370 771 279 261 Passcode: iCo7a5
LOCATION:Live-streamed at MR14 Centre for Mathematical Sciences
END:VEVENT
END:VCALENDAR