1 Introduction

Fermat’s Last Theorem is the statement that if \(a,b,c,n\) are positive whole numbers with \(n\geq 3\), then \(a^n+b^n\not=c^n\). It is thus a statement about a family of Diophantine equations (\(a^3+b^3=c^3, a^4+b^4=c^4,\ldots \)). Diophantus was a Greek mathematician who lived around 1800 years ago, and he would have been able to understand the statement of the theorem (he knew about positive integers, addition and multiplication).

Fermat’s Last Theorem was explicitly raised by Fermat in 1637, and was proved by Wiles (with the proof completed in joint work with Taylor) in 1994. There are now several proofs but all of them go broadly in the same direction, using elliptic curves and modular forms.

Explaining a proof of Fermat’s Last Theorem to Lean is in some sense like explaining the proof to Diophantus; for example, the proof starts by observing that before we go any further it’s convenient to first invent/discover zero and negative numbers, and one can point explicitly at places in Lean’s source code here and here where these things happen. However we will adopt a more efficient approach: we will assume all of the theorems both in Lean and in its mathematics library mathlib, and proceed from there. To give some idea of what this entails: mathlib at the time of writing contains most of an undergraduate mathematics degree and parts of several relevant Masters level courses (for example, the definitions and basic properties of elliptic curves and modular forms are in mathlib). Thus our task can be likened to teaching a graduate level course on Fermat’s Last Theorem to a computer.

The proof explained in these notes was constructed by Taylor, taking into account Buzzard’s comments on what would be easy or hard to do in Lean. The proof uses refinements of the original Taylor-Wiles method by Diamond/Fujiwara, Khare-Wintenberger, Skinner-Wiles, Kisin, Taylor and others – one could call it a 21st century proof of the theorem. We shall explain more about the exact path we’re taking in Chapter 4. But before we go into those technical details, we can enjoy some of the more basic arguments at the start of the proof. And the proof starts, as every known proof does, with some basic reductions and the introduction of a certain elliptic curve. We explain this in the next chapter.