Fermat's Last Theorem for regular primes

Alex J. Best, Christopher Birkbeck, Riccardo Brasca +1

We formalise the proof of the first case of Fermat's Last Theorem for regular primes using the \emph{Lean} theorem prover and its mathematical library \emph{mathlib}. This is an im…