Slightly misleading title- this is the overall blueprint for a large ongoing effort by the Imperial College London to formalize FLT in Lean, not the proof itself (which is huge).

The project webpage has more information about the efforts and how to contribute:

https://imperialcollegelondon.github.io/FLT/

Thank you. I saw the headline and was thinking things had progress surprisingly quickly.

We've updated the title and URL now, thanks!

That’s the title I saw!