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定理完成了证明。