Named proof mapLean source statements · traced direct references
app (application) const (declaration) bvar (bound variable) binder lit (literal)Terminal syntax leaves are not automatically lemmas.
26 named declarationsSelect a node to inspect
PROOF ATLAS · READER
Mathematical explanation
The graph measures the SE(2) Lean theorem CrossingData.crossing. The reader decodes its published type and proof term. The mathematical idea is an editorial interpretation, not an automatically verified compression.