Node outline shows whether the item is definition-like or theorem-like.

Border color tracks whether the statement is blocked, ready, or already formalized.

Fill color tracks proof readiness independently from statement progress.

Border treatments flag missing references, missing declarations, or Lean-only nodes without an informal statement.

Line style distinguishes statement dependencies from proof-only dependencies.

Group nodes summarize children instead of showing each declaration separately.

Grouped edges compress many child edges into one aggregate connection.