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/