A complete formalization of Fermat's Last Theorem for regular primes in Lean. - Riccardo Brasca; Christopher Birkbeck; Eric Rodriguez Boidi; Alex J. Best; Ruben van De Velde; Andrew Yang (CoRR, 2024)