Theorem Blueprint Graph

Claim boundary manifest evidence graph theorem status preserved not proof-dependency edges

The theorem blueprint graph is a generated evidence graph. It connects theorem ids to Lean declarations, dictionary terms, paper references, and paper reading-order edges.

It is not a formal Lean dependency graph. The manifests do not currently encode which theorem proof depends on which earlier theorem proof.

Artifacts:

Regenerate locally:

make theorem-blueprint

The graph is useful for navigating the corpus: it shows which papers carry the largest theorem spines, which dictionary terms each theorem uses, and which Lean declaration each theorem id claims.