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 important 19th century result that motivated the development of modern algebraic number theory. Besides explaining the mathematics behind this result, we analyze in this paper the difficulties we faced in the formalisation process and how we solved them. For example, we had to deal with a diamond about characteristic zero fields and problems arising from multiple nested coercions related to number fields. We also explain how we integrated our work to \emph{mathlib}.

翻译：我们使用\emph{Lean}定理证明器及其数学库\emph{mathlib}，对正则素数情形下费马大定理的第一种情况进行形式化证明。这是19世纪的一项重要成果，推动了现代代数数论的发展。除了阐述该结果背后的数学原理，本文还分析了形式化过程中遇到的困难及解决方法。例如，我们必须处理特征零域中的菱形结构问题，以及与数域相关的多重嵌套强制转换引发的难题。我们还解释了如何将我们的工作集成到\emph{mathlib}中。