Remarks

The actual blueprint currently also contains a lot of disorganised ideas. Currently these should be disregarded.

Chapter An overview of the proof is an extremely sketchy overview of how the rest of the proof goes. This is currently being expanded and should be ignored right now.

All of the remaining chapters are experiments, and most of them are what I am currently calling “mini-projects”. A mini-project is a bottom-up project, typically at early graduate student level, with a concrete goal. The ultimate goal of many of these projects is to actually get some result into mathlib. We have had one success so far – the Frobenius mini-project is currently being PRed to mathlib by Thomas Browning. Several other mini-projects have been completed in this repo but have not yet been PRed to mathlib. Examples of completed miniproject which are not yet upstreamed include adeles mini-project and the quaternion algebra mini-project. These projects do not logically depend on each other for the most part, and one can pick and choose how one reads them.

There is also an appendix, which is again very sketchy, and comprises mostly of a big list of nontrivial theorems many of which we will be assuming without proof in the FLT project.

The next chapter to read, where the proof begins, is chapter First reductions of the problem.

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.