Lean 4 · theorem dependency atlas

Fermat’s Last
Theorem Atlas

Explore every proof dependency beneath the final theorem.

/
—theorems / lemmas
—direct dependency edges
—final proof closure

Major proof branches

Mazur · irreducibility
Wiles · modularity
Ribet · level lowering
Modular-curve infrastructure

Drag pan · Wheel zoom · Hover view name · Legend highlight branch · Click pin

Building the dependency layout for 29,511 nodes…