I am running an EPSRC-funded 5 year project which involves teaching a modern proof of Fermat's Last Theorem to the Lean theorem prover. It has been running for just over 8 months. In the talk I'll explain more about the goals, and give an overview of how it's going and the things that we've learnt so far. Rest assured that I will not be assuming that the audience knows anything about the technicalities of the proof.
