We formalize a complete proof of the regular case of Fermat's Last Theorem in the Lean4 theorem prover. Our formalization includes a proof of Kummer's lemma, that is the main obstruction to Fermat's Last Theorem for regular primes. Rather than following the modern proof of Kummer's lemma via class field theory, we prove it by using Hilbert's Theorems 90-94 in a way that is more amenable to formalization.

翻译：我们在Lean4定理证明器中形式化地完成了正则情形下费马大定理的完整证明。我们的形式化工作包含了库默引理的证明，该引理是正则素数情形下费马大定理的主要障碍。不同于通过类域论来证明库默引理的现代方法，我们采用更易于形式化的途径，通过希尔伯特90-94定理完成了其证明。