Imperial College London is leading an open-source project to formalize the proof of Fermat's Last Theorem using the Lean theorem prover. The multi-author effort, funded by EPSRC until 2029 and led by Kevin Buzzard, follows a modern variant of the original Wiles/Taylor-Wiles proof approach planned by Richard Taylor.