Lean 4 · Mathlib
Every theorem in Mathlib, on the map.
Mathlib is deepest in category theory; homological algebra, order, lattices, ordered algebraic structures, and group theory and generalizations. It has formalized 199 of the 1,200 theorems on the 1000+ list (17%), and touches 44 of the 63 areas of mathematics. The widest gap is dynamical systems and ergodic theory: 0 of its 24 famous theorems are in Mathlib (0%).
The map of formalized mathematics
Each tile is an area of the Mathematics Subject Classification. Areas with no Mathlib declarations are not drawn. Click a tile to zoom in and open its page.
Size: declarations in Mathlib
Every area, ranked by declarations
Which parts of mathematics are formalized, and how deeply.
Every area of mathematics, sized by how many Mathlib declarations it holds and colored by how many of its famous theorems are proved.
Open MapStructuresHow Mathlib's algebraic and topological structures fit together.
The typeclass hierarchy as one navigable diagram, from Monoid to Field and beyond, with a chain finder that shows why a real number is an instance of any class.
Open StructuresTheoremsWhat each theorem cites, who cites it, and what it rests on.
Every declaration with its statement, its dependencies down to the axioms, and the plumbing filtered out so only the mathematics shows.
Open TheoremsThis site is being built in the open. Map and Structures are live; Theorems is next.
Follow the build on GitHub