THE OMEGA INSTITUTE
Mathematical Atlas.
A map of our shared mathematical library.
Loading published mathematics
Branches share a color · larger nodes support more mathematics · imports flow downward
Verifying the published graphMathematical Atlas
About this map
Explore a knowledge graph of Lean-verified mathematics. Each node is a module of definitions and proofs; connections show how modules depend on one another. Use the color legend to find widely reused knowledge, or select a node to read its mathematics and follow its connections.