Dependency Graph
Legend
Shape shows declaration kind, border shows statement status, fill shows proof status, and edge style separates statement from proof dependencies.
Shapes
Node outline shows whether the item is definition-like or theorem-like.
DefinitionTheorem / lemma / corollary
Statement Border
Border color tracks whether the statement is blocked, ready, or already formalized.
BlockedReady to formalizeFormalized
Proof Status
Fill color tracks proof readiness independently from statement progress.
not readyready to formalizeLean code incompletelocally formalizedlocally formalized + dependencies complete
Warning Markers
Border treatments flag missing references, missing declarations, or Lean-only nodes without an informal statement.
Unknown referenceLean code, informal statement missingMissing external Lean declaration
Edges
Line style distinguishes statement dependencies from proof-only dependencies.
Solid: statement deps from theorem-like sourcesDashed: statement deps from box-shaped sourcesDotted: proof-only depsThicker solid/dashed: statement + proof deps