In this joint talk we will first present a project by one of us (F.N.) about the formalisation in Lean of the finiteness of the class group for a global field, together with some basic properties of Dedekind Domains. In the second part, R.B. will explain how once the basic properties were in place, it was possible to define regular prime numbers, and to formalise the proof of Fermat’s Last Theorem for regular primes, adapting Kummer’s classical proof. Some time will be spent to discuss the difference between the so-called “first case” and “second case”, and why the second was significantly more difficult to formalise than the first.