ATLAS

83%
Fully proved
37,864 of 45,865 statements
7,957Ready to work onstatements you can state or prove now
4 of 8 source areas split into statements · 2 not yet settled · 2 out of scope What the sources cover
Next up
Morley's categoricity theorem
Everything it uses is in Lean, so its Lean proof can start.
Dependencies

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.