About
A map of formal mathematics, drawn from Mathlib itself.
Mathlib is the largest library of machine-checked mathematics in the world, and it is growing by thousands of results a month. Its shape is hard to see from the inside. Mathlib Map reads the library once a month and draws three views of it.
The three views
Map places every area of mathematics on one page, sized by how many Mathlib declarations it holds and colored by how many of its famous theorems are proved. Every number shows its denominator.
Structures is the typeclass hierarchy: which classes extend which, which concrete types are instances of what, and the chain of instances that connects them.
Theorems gives every declaration a page with its statement, what it cites, what cites it, and what it rests on down to the axioms, with the elaborator plumbing filtered out so that only the mathematics shows.
Where the data comes from
Everything is derived from public data. The current snapshot describes Mathlib v4.33.0 (2026-09).
| Source | Gives | License |
|---|---|---|
| MathNetwork / MathlibGraph | Declaration dependency graph and network metrics | MIT |
| Mathlib Initiative / mathlib-types | Statements and docstrings for every constant | Apache 2.0 |
| Mathlib docs YAML files | The 100 theorems, 1000+ theorems, overview, and undergraduate lists | Apache 2.0 |
| 1000+ theorems project | MSC codes for famous theorems, the coverage denominator | See project |
| Formal Conjectures | Conjecture statements with subject codes | Apache 2.0 |
| MSC2020 | The Mathematics Subject Classification | CC BY-NC-SA |
| Our own Lean extractor | Classes, instances, typeclass assumptions, explicit premises, axioms | MIT |
Each Mathlib file is assigned a subject area by a language model reading the file's own documentation, with hand overrides. Checked against the 1000+ theorems list, the model's area for a theorem's file agrees with the list's area 73% of the time; most disagreements are boundary cases such as a real-analysis theorem proved in a general-topology file. Every area page lists its files and their codes so you can report one that is misplaced.
Derived datasets (the filtered dependency graph, citation counts, the module to subject mapping, and the hierarchy graph) will be published for download here once the first full pipeline run completes.
Independence
An independent project, not affiliated with the Mathlib community or the Lean FRO. The source is public on GitHub. Corrections and ideas are welcome as issues there.
Cite
If the site or its data is useful in your work:
@misc{mathlibmap,
author = {William Zhu},
title = {Mathlib Map: every theorem in Mathlib, on the map},
year = {2026},
url = {https://mathlibmap.com}
}