Mathlib explorer is an interactive visualization tool designed for Lean's mathlib library. It visualizes the import relations within mathlib, with carefully thought-out layout and interactions. It is a great visual representation of how math concepts are connected to each other, which can be informative even if you cannot read Lean code.
Related video series (in Chinese):
欢迎关注相关视频系列：《重构数学》on bilibili and YouTube.
Screenshots:
Zoom in view:
The import graph is mapped onto the plane, s.t. if B imports A, B will always be on the right of A. This makes it easy to see how modern math theories are constructed from axioms and definitions.
Supported interactions:
- Scroll to zoom in/out
- Drag to move
- Click on a node to highlight
- its direct neighbors
- its transitive dependents
- its transitive dependencies
- Click on a topic label to highlight
- all nodes in the same topic
- references to the topic
- direct dependencies of the topic
Clone this repo:
git clone https://github.com/Crispher/MathlibExplorer
Go to the binary folder of your platform:
cd MathlibExplorer/release/bin_{YOUR_PLATFORM}
Run the executable:
./MathlibExplorer
Limited testing has been done so far, which is mainly on MacOS (M1).
The underlying mathlib data is a bit outdated. I might update it or publish the scripts to generate the data in the future.
Cross-platform graphics is powered by bgfx.