Lean 4 · Mathlib
Every theorem in Mathlib, on the map.
Mathlib holds more than 300,000 formal declarations of mathematics, checked by Lean. Mathlib Map shows where they are, how they fit together, and what each one rests on.
MapBuilding
Which parts of mathematics are formalized, and how deeply.
A zoomable map of mathematics. Each area is sized by how many Mathlib declarations it holds and colored by how many of its famous theorems are proved.
Open MapStructuresLive
How Mathlib's algebraic and topological structures fit together.
The typeclass hierarchy as one navigable diagram, from Monoid to Field and beyond, with a path finder that shows why a real number is an instance of any class.
Open StructuresTheoremsBuilding
What 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. Structures is live; the Map and Theorems views are next.
Follow the build on GitHub