Formalizing Fermat: an update

Add to your list(s) Download to your calendar using vCal

• Kevin Buzzard (Imperial College London)
• Thursday 01 May 2025, 17:00-18:00
• MR14 Centre for Mathematical Sciences.

If you have a question about this talk, please contact Anand Rao Tadipatri.

I have been “officially” formalizing Fermat’s Last Theorem for 6 months now, and unofficially I’ve been doing so for around a year. In this talk I’ll give you an update on where we are, how it’s going, and what I’ve learnt so far. More precisely, I’ll talk about infrastructure (what we’ve settled on, the problems that we’ve had, and how we solved them). I’ll talk about what the goals of the project are, what we have achieved, and where we’re going. And I’ll talk about what were (to me) some unexpected consequences of the formalization procedure, namely some old mathematics which we’ve poked holes in, and some new mathematics which has come out of the project. Finally I want to stress that I will not be assuming that the audience knows anything at all about the details of the proof! The talk will be suitable for a general scientific audience.

=== Hybrid talk ===

Join Zoom Meeting https://cam-ac-uk.zoom.us/j/87143365195?pwd=SELTNkOcfVrIE1IppYCsbooOVqenzI.1

Meeting ID: 871 4336 5195

Passcode: 541180

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
• 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.