1. Whole project graph
Open the standard Lean blueprint dependency graph. It contains every exported project declaration and the two open conjecture targets. Edges between checked declarations come from their Lean types and proof terms. Click a node to read its statement or open its Lean source. The source pages include Lean hover information.
Download the Graphviz DOT file or the SVG graph.