Fermat's Last Theorem was proved by Wiles and Taylor in the 1990s, and now there are several known routes to the summit. The question of teaching the proof to a computer proof assistant was raised in the 1990s but back then the technology was not mature enough. I now believe that it is, and in 2024 I will be leading a project to formalise the proof in the Lean proof assistant. In my talk I will explain what the landscape of computer proof assistants looks like in 2024, and I will say something about the route we'll be taking and the practicalities involved in such a large project. The talk will be a general audience talk -- no background in either the theory of proof assistants or the mathematics behind Fermat's last theorem will be assumed.