Status

This miniproject has been a success: the main results are sorry-free and merged into mathlib (see this PR). As a result there will be no more work on this miniproject in the FLT repo. Below is a fairly detailed sketch of the argument used.

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.