Case study · Mathematics
A map of Mathlib
How is a large formal mathematics library organized by what its theorems say?
The Space
A map of Mathlib
66,154 theorems of Lean's Mathlib (every documented theorem and every one used by at least five others) placed by what their statements say, in 24 areas, with statements, docstrings and usage counts.
Source: Mathlib 4, leanprover-community (Apache-2.0), Mathlib v4.34.1; The mathlib Community, CPP 2020.
66,154 records
Largest clusters in the map sample
- Topology15%
- Commutative algebra & algebraic geometry14%
- Sets, functions & filters13%
- Category theory11%
- Order & lattices10%
- Groups, rings & modules8%
- Measure theory & probability8%
- Real numbers & special functions7%
On the map
What to look for
- Theorems sit by what their statements say, in 24 areas, from order and lattices to category theory.
- Usage counts show which results the rest of the library leans on most.
With Mantis
What to ask
- Which theorems in topology are used most across the library?
- Where do algebra and order theory meet?
- Find documented theorems about commutative rings with no uses yet.
More case studies
- The immune response to severe COVID-19, cell by cellWhich immune cells carry the interferon response in severe COVID-19, and how does it differ from severe influenza?
- Which neurons Alzheimer’s disease takes firstAlong the disease continuum, which cell types are lost earliest in the middle temporal gyrus?
- The human proteome, read by a protein language modelWhich proteins does a protein language model read as alike, and what do they share?
Work with us
Bring representation superintelligence to your team.
Start in the workspace today, or talk to us about your data, your deployment and your questions.