In a huge mathematical library, you might expect the most important ideas to sit at the busiest crossroads. A famous theorem, perhaps, or a powerful concept used across many fields. But when researchers mapped the dependency network of Mathlib, a machine-checked library of mathematics, one of its biggest hubs was a rule so basic it says, in effect, that a thing equals itself.
That mismatch is the start of a story about two kinds of structure: the way mathematicians organize knowledge, and the way network scientists measure connections. The researchers treated Mathlib not simply as a collection of theorems, but as a vast directed graph. Each declaration—a theorem, definition, or other named fact—became a node. When a proof or statement depended on another declaration, the graph gained an arrow.
The scale is substantial: their snapshot contained 308,129 declarations and 8,436,366 dependency edges, spread across 7,563 modules. The data came from a single Mathlib commit dated February 2, 2026. That matters: this is a map of one moment in a changing project, not a timeless atlas of mathematics.
Network science supplied the researchers with a way to ask questions that ordinary subject labels cannot answer. Which declarations attract the most incoming links? Which groups of results cluster together through their actual dependencies? How closely do those clusters match folders and namespaces labeled “Algebra,” “Analysis,” or “Topology”?
The answer to that last question was: not very closely. File layout and naming conventions resemble each other, but the dependency-based communities diverge from them. At the declaration level, 50.9% of dependency edges cross namespace boundaries. The labels still help people find their way around, but they do not neatly describe where proofs actually lead.
Then comes the surprising hub. A declaration called OfNat.ofNat, which helps Lean interpret numerals, had the most incoming links: 89,936. The reflexivity-of-equality rule, Eq.refl, ranked second, with 69,580. The Chinese Remainder Theorem, by contrast, did not appear among the top 100 declarations by this measure.
That is not a verdict on what mathematicians should care about. A network’s centrality counts connections, not intellectual depth. In Lean, writing a number or checking an equality can trigger references to the language’s underlying machinery. The researchers estimate that 74.2% of dependency edges are synthesized automatically rather than appearing explicitly in source code. Those links are real features of the formal proof system—but they can make technical infrastructure look more central than mathematical ideas.
Here the crossover does its work: tools designed to study networks reveal how a proof assistant’s design shapes the apparent architecture of mathematics. Lean does not just store results. It requires statements and proofs to be expressed in a form a computer can check, making implicit conventions explicit. A mathematician may write a proof using familiar notation; the system may also connect that proof to declarations that make the notation and its rules work.
The map also points to a practical friction. Mathlib is organized into modules, and importing one brings its declarations into scope. Across import links, the median share of an imported module’s declarations directly used by the importing module was just 1.6%. That does not mean the rest is necessarily dead weight: some imports provide transitive access to other modules, and the paper notes that many imports with no direct declaration references serve that purpose. Still, the gap suggests that file-sized imports can be a coarse fit for fine-grained proof dependencies.
Why should anyone outside formal mathematics care? Because a clearer map could help maintainers spot bottlenecks, rethink boundaries, or prioritize changes that trigger broad recompilation. The authors also suggest that dependency structure could help computer systems search for useful premises when building proofs. These are proposed uses of the analysis, not outcomes the study has already demonstrated.
The researchers are careful about what their map cannot show. One snapshot cannot establish whether these patterns are stable or changing, and the authors say that causal claims about how file organization and logical dependencies shape each other need longitudinal or experimental evidence. Even the graph is not a pure picture of mathematical meaning: it reflects human naming habits, software choices, and the proof assistant’s rules.
That is precisely why the network view is revealing. A library can look like a set of tidy shelves while its working structure runs through unexpected back corridors. Mapping those corridors does not tell us which mathematics matters most. It shows how formal mathematics is built—and how much of its hidden architecture comes from the machinery that lets a computer check a proof.
