Proof Atlas / Interactive microscope

Explore the geometry of a Lean proof

← About the projectResearch methods ↗
Whole-proof geometryExpression occurrence forest · measured structure
Open full app ↗
Your browser does not support Canvas.
7,288 expression occurrencesSelect a node to inspect

The graph is a measured, anonymized projection of the SE(2) Lean theorem CrossingData.crossing. The mathematical idea is an editorial interpretation, not an automatically verified compression.