Application architecture
An independent research tool.
The Explorer has its own extraction pipeline, generated knowledge data, model records, and interactive graph. A visual reskin is planned separately to preserve the existing functionality.
Mathematics made navigable
See the structure
of proof.
Explore mathematical declarations, theorem relationships, source references, dependencies, and Lean proof metadata in the existing interactive research tool.
Explore
Resources & research
Selected public work and source materials.
Interactive
Theorem explorer
Inspect declaration metadata, graph relationships, and proof dependencies.
Open the explorer →Source
Explorer repository
See the rendering application and its extraction inputs.
View code →Foundations
Mathematics program
Return to the staged mathematical study curriculum and reference material.
Explore mathematics →