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=SELTNkOcfVrIE1IppYCsbooOVqen...
Meeting ID: 871 4336 5195
Passcode: 541180