Why a Trivial Equality Becomes a Giant Hub in Formal Math
A network-science map of Lean’s Mathlib finds proof dependencies diverge from subject labels—and basic equality rules become giant hubs.
proof dependency network
A network-science map of Lean’s Mathlib finds proof dependencies diverge from subject labels—and basic equality rules become giant hubs.