COOKIES: By using this website you agree that we can place Google Analytics Cookies on your device for performance monitoring. |

University of Cambridge > Talks.cam > Formalisation of mathematics with interactive theorem provers > How to prove Fermat's Last Theorem

## How to prove Fermat's Last TheoremAdd to your list(s) Download to your calendar using vCal - Professor Kevin Buzzard (Imperial College London)
- Thursday 08 February 2024, 17:00-18:00
- Live-streamed at MR14 Centre for Mathematical Sciences.
If you have a question about this talk, please contact Anand Rao Tadipatri. Online The statement of Fermat’s Last Theorem would have been comprehensible to Diophantus, who lived nearly 2000 years ago. The question was explicitly raised by Fermat in the 1600s, and was resolved by Wiles and Taylor 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. In my talk I’ll start with a history of the problem, and say something about the contributions made by computers in the pre-Wiles era. Without 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 approach (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 infrastructure which I’ll be using in order to run the project as an open source multi-author collaborative experiment. It is probably worth stressing that this talk is suitable for a general audience familiar with the idea of formalisation but with no background in modern number theory, and in particular it will not be a technical explanation of the route we’re taking. —- WATCH ONLINE HERE : https://www.microsoft.com/en-gb/microsoft-teams/join-a-meeting?rtc=1 Meeting ID: 370 771 279 261 Passcode: iCo7a5 This talk is part of the Formalisation of mathematics with interactive theorem provers series. ## This talk is included in these lists:- All CMS events
- All Talks (aka the CURE list)
- CMS Events
- Cambridge talks
- DPMMS Lists
- DPMMS Pure Maths study groups
- DPMMS info aggregator
- DPMMS lists
- Department of Computer Science and Technology talks and seminars
- Formalisation of mathematics with interactive theorem provers
- Hanchen DaDaDash
- Interested Talks
- Live-streamed at MR14 Centre for Mathematical Sciences
- School of Physical Sciences
- School of Technology
- Trust & Technology Initiative - interesting events
- bld31
Note that ex-directory lists are not shown. |
## Other listsThe political economy of AIDS in Africa RECOUP Seminars se456's list## Other talksSeasonal and spatial patterns of henipavirus seroprevalence in Straw-colored Fruit Bats (Eidolon helvum) Serum symmetric dimethylarginine (SDMA) concentrations are not influenced by systemic inflammation in cats Scientific machine learning - opportunities and challenges from an industrial perspective Towards Autoformalization and Mathematical Reasoning using language models The cartographic commissions of John, 2nd Duke of Montagu (1690–1749) Interaction between fast tides and convection |