Fermat's Last Theorem for regular primes
The goal of this project is to prove Fermat's Last Theorem for regular primes in Lean.
The following readme has been shamelessly copied from the Liquid Tensor Experiment.
How to browse this repository
Blueprint
Here are a draft blueprint and dependency graph.
Getting the project
The recommended way of browsing this repository is by using a Lean development environment. Crucially, this will allow you to inspect Lean's "Goal state" during proofs, and easily jump to definitions or otherwise follow paths through the code. Please use the installation instructions to install Lean and a supporting toolchain. After that, download and open a copy of the repository by executing the following command in a terminal:
git clone https://github.com/leanprovercommunity/fltregular.git
cd fltregular
lake exe cache get
lake build
code .
For detailed instructions on how to work with Lean projects, see this.
You can also use gitpod and do everything directly in your browser, without installing anything. Just click on , but beware that everything will be slower than on your computer.
Reading the project
With the project opened in VScode, you are all set to start exploring the code. There are two pieces of functionality that help a lot when browsing through Lean code:
 "Go to definition": if you rightclick on a name of a definition or lemma
(such as
is_regular_number
, orflt_regular_case_one
), then you can choose "Go to definition" from the menu, and you will be taken to the relevant location in the source files. This also works byCtrl
clicking on the name.  "Goal view": in the event that you would like to read a proof, you can step through the proof linebyline, and see the internals of Lean's "brain" in the Goal window. If the Goal window is not open, you can open it by clicking on one of the icons in the top right hand corner.
Organization of the project
 All the Lean code (the juicy stuff) is contained in the directory
FltRegular/
.  The file
FltRegular/FltRegular.lean
contains the statement of Fermat's Last Theorem for regular primes.  The ingredients that go into the theorem statement are defined in several other files.
The most important pieces are:
NumberTheory/RegularPrimes.lean
we give the definition of what a regular number is.NumberTheory/*
are the files we are actively working on.ReadyForMathlib/*
are the files that are (almost) ready to be PRed to mathlib.
Note that we are trying to move all our results to mathlib as fast as possible, so the
folder ReadyForMathlib
changes rapidly. You should also check Mathlib.NumberTheory.Cyclotomic.*
.
Brief note on type theory
Lean is based on type theory, which means that some things work slightly differently from set theory. We highlight two syntactical differences.

Firstly, the elementof relation (
∈
) plays no fundamental role. Instead, there is a typing judgment (:
).This means that we write
x : X
to say that "x
is a term of typeX
" instead of "x
is an element of the setX
". Conveniently, we can writef : X → Y
to mean "f
has typeX → Y
", in other words "f
is a function fromX
toY
". 
Secondly, type theorists use lambdanotation. This means that we can define the square function on the integers via
fun x ↦ x^2
, which translates tox ↦ x^2
in settheoretic notation. For more information aboutλ
(calledfun
in Lean 4), see the Wikipedia page on lambda calculus.
For a more extensive discussion of type theory, see the dedicated page on the perfectoid project website.