The Network Structure of the Mathlib Ecosystem

A structural analysis of Mathlib plus its community-project ecosystem, extending the methodology of Li et al. (2026), "The Network Structure of Mathlib" (arXiv:2604.24797v1). The paper measures Mathlib alone at commit 534cf0b (Feb 2026, 308 129 declarations, 8.4 M edges, 7 563 modules) using importGraph, jixia, and lean-training-data.

This report widens the lens. We rebuild the same family of dependency graphs against Corpus V2: Mathlib plus fourteen community projects spanning three Lean toolchains (v4.27.0, v4.28.0, v4.29.0) — including PrimeNumberTheoremAnd, formal-conjectures, Sphere-Packing-Lean, ClassFieldTheory, and ten smaller research projects. Each project is extracted with the typed-edge tool aurasoph/lean-graph, which records six distinct edge kinds (proof, sig, def, field, docref, extends) where the paper's pipeline records one. The result is a single 1.7 GB SQLite graph against which every chart on this page is recomputed.

The takeaways:

1. Scale. Our snapshot is +31% nodes (380 k → 380 k Mathlib alone, 404 k with community projects) and ~+92% edges (8.4 M → 16.2 M unique pairs) vs. the paper. The growth is split between Mathlib drift and our richer extraction: typed sig / field edges that the paper's tooling aggregates away contribute roughly half the gap.
2. Structural friction is larger than reported. Cross-namespace edges reach 78% of all declaration-level edges (paper: 50.9%); same-module edges drop to 8% (paper: 9.6%). The richer edge typing surfaces structural dependencies that don't appear in proof-term-only extraction.
3. Library infrastructure dominates the in-degree tail. OfNat.ofNat, Eq, congrArg, and Membership.mem are the top-cited declarations — none are mathematical content. The paper's "language-infrastructure vs. mathematical content" two-layer hub structure replicates cleanly here.
4. The import wasteland persists. Median scope utilisation is 0.17%; a typical Mathlib file pulls in 600× more declarations than its proofs ever touch.
5. The implication graph is essentially acyclic. 24 small mutual-block SCCs survive in the theorem-implication subgraph; the largest is a 17-node category-theory cluster that collapses entirely once auto-generated structure field projectors are filtered out (§13).
6. The community ecosystem rests on a thin Mathlib core. Across 14 community projects we count ~24 k unique extra declarations, but 1.4 M cross-edges into Mathlib — every new declaration cites Mathlib ~60× on average.

1. Comparative Scale

Both runs use a single static snapshot. Ours is later, larger, and tracks more edge types — so all deltas should be read as a combined growth + extraction-fidelity signal rather than pure library growth.

The 38% leaf-theorem rate falls below the paper's 44.8% — a side effect of richer edge extraction: every additional sig/field edge we record can lift a theorem out of the zero-in-degree bucket. The same mechanism pushes our unique edges / declaration ratio from 27 (paper) to 33.

2. Edge Type Composition

lean-graph decomposes every dependency into one of six edge kinds. The paper's declaration graph collapses these into a single edge per (source, target) pair, losing the layering. We keep them, which lets us track how much of the graph is driven by each Lean mechanism.

proof (proof-term references) accounts for 52% of typed edges; sig (statement-level type references) accounts for 35%. The paper reports a synthesis ratio σ = 74.2% — the share of edges inserted automatically by the elaborator. We do not separate synthesized from explicit at this layer; instead we expose the mechanism (sig, def, field, extends) so the ratio can be recomputed by any combination.

2a. Source–target pair classification

When duplicate (source, target) rows are merged across edge types, every pair falls into one of three buckets — exactly the paper's Statement only / Proof only / Both decomposition (§B.2.2).

The paper reports an 8.1 / 43.9 / 48.0 split for Statement / Proof / Both. We see 33% / 41% / 26%. The extra mass on Statement only is structural overhead our sig/field/extends extraction makes visible: a definition's signature drags in many typeclasses that the elaborator never needs to revisit during proof checking.

3. Declaration Kind Composition

Every node carries a Lean kind. The paper enumerates eight (Table 10); our extractor also records instance and class distinctly because they have different structural roles even though Lean treats them as ordinary definitions.

Theorems are 69% of declarations (paper: 79%). The gap shows up almost entirely as instance (10%) and class (0.6%) — categories the paper folds back into definition. Each instance is an automatically resolved structural witness; treating them as a separate kind is what lets us reproduce the paper's "language infrastructure vs. mathematical content" hub split (§C.2.2) directly from the kind column.

3a. Per-kind degree

The paper's Table 12 finding survives in our richer corpus: axioms still sit at the bottom of the dependency chain (mean in-degree ≈ 4 049, mean out-degree ≈ 1.7), theorems at the top of the production chain (mean out-degree ≈ 49, mean in-degree ≈ 8), and inductive types form structural skeletons (mean in-degree ≈ 441 — even higher than the paper's 273, reflecting the additional sig edges we capture). Theorems retain a heavy long tail: 38% are never cited.

4. Inter-Kind Edge Flow

The kind composition is most informative when read as a flow: which kinds produce edges, and which kinds consume them. The matrix below replicates the paper's Table 11.

Theorems → instances dominates (5.8 M edges), reflecting how often proofs cite typeclass witnesses. Theorem → theorem accounts for only 1.8 M — the paper's Definition B.2.4 prediction that "synthesized" infrastructure dwarfs explicit mathematical citation.

5. Degree Distributions

Both the paper (Figure 28) and our corpus exhibit a heavy in-degree tail with a sharply bounded out-degree.

The in-degree maximum in our corpus is edges (vs. the paper's 89 936 for OfNat.ofNat). The gap reflects more aggressively captured synthesized edges around OfNat, Eq, and congrArg, all of which the elaborator inserts implicitly.

5a. Top-cited declarations

OfNat.ofNat, Eq, congrArg, Membership.mem, DFunLike.coe — the same top-of-list the paper identifies (Table 18). Ranks 1–10 are saturated by language infrastructure, exactly the "language infrastructure vs. mathematical content" two-layer hub structure the paper documents.

5b. Highest out-degree (longest proofs)

Out-degree maxes out at in our snapshot. The paper records 522 — the gap is again the extra edge types we attach to each declaration. The out-degree leaderboard is dominated by combinatorial and analysis files where a single proof unfolds many premises.

6. Boundary Classification

The paper measures (§B.1.6) that 37.1% of module-level edges are inter-directory and (§C.2.2 Table 14) that 50.9% of declaration-level edges are cross-namespace. We measure both, using the first dot-separated segment of each declaration's name as its top-level namespace.

In our corpus, 78% of edges cross a top-level namespace — well above the paper's 50.9%. Two effects compound: (1) deeper extraction surfaces more cross-namespace sig/field edges that the paper's pipeline misses; (2) Mathlib has continued to absorb subdisciplines (e.g., RingTheory → Algebra), inflating the cross-namespace density. Same-module edges drop to 8% (paper: 9.6%).

6a. Heaviest cross-module flows

7. Strongly Connected Structure

Mathlib's declaration graph is almost a DAG, but the moment we keep sig, field, docref, and extends edges, foundational algebra closes a cycle:

Outside the giant 2 980-node "ring core," nearly all SCCs are size 2–8, primarily field ↔ sig pairs introduced by structure projections. The largest non-trivial SCCs beyond the ring core are 317, 114, and 78 nodes — small islands of mutually recursive definitions in category theory and order theory.

7a. The ring core (top 250 hubs)

Edge colour: red = extends, purple = field, blue = sig, grey = mixed/proof. Node radius = degree within the SCC. Drag a node to pin it; scroll to zoom.

8. Module-Level Hubs

Aggregating declaration-level edges to their defining modules reproduces the paper's "infrastructure vs. integrator" axis (Table 6, Figure 26). High in-edge modules are infrastructure; high out-edge modules are integrators.

Init.Prelude, Mathlib.Algebra.Group.Defs, and Mathlib.Algebra.Ring.Defs are the top three by in-edges — exactly the paper's top-3 module ranking transcribed via declarations rather than imports. The points high on the y-axis with low x-axis are foundational; the points along the diagonal are workhorse algebra/topology files that both depend on much and are depended on by much.

9. Import Utilization & the "Wasteland"

Median scope utilization: 0.17%. The paper reports an import-edge utilization median of 1.6% (§B.2.11) — a strictly easier metric, since it is computed per direct import edge rather than per transitive scope. Both metrics agree on the qualitative finding: the typical Mathlib file pulls in two-to-three orders of magnitude more declarations than its proofs ever touch.

10. Zero-Citation Namespaces

Declarations the rest of the corpus never cites form Mathlib's "outer surface." Following Table 13, we group theorems by their first two name components and rank by zero-citation rate.

The paper's pattern repeats: namespaces produced by @[to_additive] mirroring or by generic data-structure libraries (Std.HashSet, Std.TreeSet, Std.ExtTreeSet) are overwhelmingly leaves, while concrete-mathematics namespaces (Std.Internal, Profinite.NobelingProof, Topology.IsInducing) are nearly fully consumed.

11. Community Project Footprint

We measured fourteen community projects spanning three Lean toolchains (v4.27.0, v4.28.0, v4.29.0). Each project is treated as an independent corpus that cites into Mathlib through cross-project edges. Pipelines B (v4.28) and C (v4.27) ran fresh Mathlib clones at the respective revisions so that each project's lean-toolchain matches what we extracted with.

The headline projects in our corpus (ranked by unique-declaration count, i.e. declarations not already in Mathlib):

• PrimeNumberTheoremAnd (v4.28) — 7 693 unique declarations, Tao/Kontorovich's formalisation programme for the Prime Number Theorem.
• formal-conjectures (v4.27) — 4 860 declarations, a Google DeepMind-curated collection of formalised conjectures used as a retrieval benchmark.
• sphere-packing-math-inc (v4.28) — 3 536 declarations, the mathematical-content half of the sphere-packing formalisation.
• combinatorial-games (v4.29) — 2 830 declarations.
• Sphere-Packing-Lean (v4.29) — 1 547 declarations.
• ClassFieldTheory (v4.29) — 1 422 declarations, a deep number-theory formalisation built on Mathlib's algebra and topology stacks.

The much larger raw-extraction footprints of these projects (e.g. Sphere-Packing-Lean produces ~258 k NDJSON rows) collapse to a few thousand unique declarations because the rest are Mathlib declarations the project re-references. See the Glossary for our attribution caveat.

The bars also expose the "Mathlib gravity" of each project — the ratio of cross-edges to own-declarations. A high ratio (e.g. cam-combi at ~48, combinatorial-games at ~32) means a single new declaration typically cites dozens of Mathlib premises: the ecosystem behaves as a dense citation pool, not a thin prelude.

12. Replication Checklist

Where the paper measures only the merged declaration graph (one edge per pair, no type label), our typed-edge extraction lets the same metrics be re-derived per edge kind. Every chart on this page is rebuilt from build_data.py, which queries the v2 corpus DB at formalized_graph_v2/data/generated/corpus_v2_mathlib_plus_v4.27_v4.28_v4.29.db. The exact DB sha256 baked into this build is shown in the Data Provenance footer.

13. The Only Near-Cycle: A mutual Block in Category Theory

In our Mathlib slice (see the verdict table below for exact counts), the theorem → theorem proof graph has a handful of non-trivial strongly-connected components. The largest by a wide margin is a 17-node cluster in Mathlib/CategoryTheory/Presentable/Directed.lean, all members of the mutual block that proves CategoryTheory.IsCardinalFiltered.exists_cardinal_directed.

When we spot-checked the 6-step "longest implication cycle" inside it (see §13b), we found that 5 of the 6 nodes form a real proof chain — but the 6th, Diagram.hP, is a field projector auto-generated by Lean's structure mechanism, not a user-written lemma. The kernel emits projectors with kind = theorem, so they appear in our theorem→theorem subgraph and can close cycles that correspond to "every member of a structure namespace uses that structure's data fields" — not to circular reasoning.

The richer typed-edge corpus surfaces a handful of smaller mutual-block SCCs beyond the 17-node one: 24 total, but every other is size 2–8 — small co-defined helper pairs / triples in algebra and category theory. After filtering field projectors, only a small residue of those small SCCs survives (largest 4 nodes), and the 17-node category-theory SCC collapses entirely. The precise claim is: Mathlib's user-written implication graph is essentially acyclic. The SCCs our extractor surfaces are signatures of mutual blocks plus structural-data dependencies — not circular reasoning.

The graph below shows every edge among the 17 SCC members. Solid red arrows are proof citations (the implication direction we used to find the cycle); blue arrows are sig (signature) references. Click any node to inspect its full statement and LeanSearch summary.

The 17 declarations sit on a ring, ordered by a depth-first walk along proof edges from the highest-in-degree member. Cycles show up as red chords that loop back along the perimeter; structural sig edges (blue) typically jump across the interior. Click any label to load its statement below.

Selected statement

Tiny helper so the html template can splice raw HTML (KaTeX output):

Natural-language summaries for all 17

Each row is the LeanSearch top hit for the corresponding declaration. ✓ = LeanSearch's index has an exact match for this declaration name; ~ = nearest neighbour (LeanSearch doesn't separately index the helper-declarations Lean auto-generates inside a mutual block, so it returns the closest indexed sibling).

All 17 members of the cycle

§13b. Spot-check: walking the longest 6-cycle in plain English

Reading the actual source file alongside the LeanSearch summaries, the 6-node implication cycle decomposes as:

The first five edges form a legitimate proof chain. The sixth edge — the one that closes the cycle back to step 1 — is the field projector for the field hP : P.HasCardinalLT κ declared in

structure Diagram where
  W : MorphismProperty J
  P : ObjectProperty J
  …
  hP : P.HasCardinalLT κ        -- this projector closes the loop

Lean compiles Prop-valued field projectors as theorems, which is why it shows up in our theorem→theorem subgraph. It isn't a proof citation in the way a mathematician would think of it; it's a data reference — the proof of isCardinalFiltered_aux uses a Diagram and therefore touches Diagram.hP, the same way it touches Diagram.W and Diagram.P.

If you skim Directed.lean top-to-bottom you'll find the 5 lemmas in roughly the order above; the "cycle" is the kernel's bookkeeping artefact of them all referring to a common piece of structural data.

Glossary

Terms used across this report, in order of appearance:

Declaration — any named entity in Lean: a theorem, def, structure, class, instance, etc. Mathlib has 380 k declarations across 9 870 modules.

Module — a single .lean source file. Mathlib's import graph is between modules; each module contains many declarations.

Namespace — a dot-separated prefix in a declaration's fully-qualified name. CategoryTheory.IsCardinalFiltered.exists_cardinal_directed.aux has namespace CategoryTheory.IsCardinalFiltered.exists_cardinal_directed. Lean's naming convention is structural, not directory-based: a single file can contribute declarations to many namespaces, and a single namespace can span many files.

Edge type — lean-graph records six categories of dependency between declarations:

• proof — the target appears in the source's proof term (what a mathematician would call a citation).
• sig — the target appears in the source's signature (the statement itself, before the proof).
• def — the target appears in the body of a definition.
• field — the target is a field accessor invoked on a structure value.
• docref — the target is name-checked from a docstring.
• extends — the source structure/class extends the target.

Field projector — when you write structure Foo where bar : T, Lean auto-generates an accessor function Foo.bar : Foo → T. That accessor is a declaration in its own right; it gets emitted into the dependency graph as if you'd written it yourself. For Prop-valued fields (like hP : P.HasCardinalLT κ) the projector is classified with kind theorem, which is why field projectors can show up in a "theorem-only" subgraph and close cycles that don't correspond to any human reasoning step. See §13 for the canonical example.

mutual block — Lean construct for declaring several theorems or definitions together so they can forward-reference each other. The kernel type-checks them as a single unit. Outside a mutual block, declarations must be defined in strict topological order: A can cite B only if B was declared earlier in the file (or in a transitively-imported file).

SCC (strongly connected component) — a maximal set of vertices in a directed graph where every vertex can reach every other along the edges. Any non-trivial (size > 1) SCC indicates a cycle: A → … → B → … → A. The condensation of a graph collapses each SCC to a single super-node and is always a DAG.

DAG (directed acyclic graph) — a directed graph with no cycles. Every SCC has size 1. Lean's module graph and (modulo mutual blocks and projectors) its declaration graph are both DAGs.

Depth / topological layer — for a DAG, the length of the longest directed path. Modules have depth 153, declarations have depth 84 in the paper; we measure 219 on the proof subgraph.

In-degree — number of incoming edges to a node; for a declaration, how many other declarations cite it. Out-degree is the reverse: how many premises a declaration's proof invokes. Mathlib's in-degree is heavy-tailed (89 936 for OfNat.ofNat); its out-degree is bounded by proof complexity (max 522).

Synthesised edges — dependency edges the elaborator inserts automatically (typeclass instances, coercions, OfNat lifts, …). The paper reports a synthesis ratio σ = 74.2%; we expose the underlying mechanism via the sig / field / extends edge labels rather than computing σ directly.

Leaf theorem — a theorem with zero in-degree: no other declaration cites it. These form the "outer surface" of the library; 38% of our theorems and 44.8% of the paper's are leaves.

Centrality — generic term for "how structurally important is this declaration." Three measures are standard: in-degree (vocabulary), PageRank (recursive foundationality), betweenness (bridge role between otherwise-disjoint subfields). They rarely agree, which is why the paper's Figure 26 is so spread out.

Scope utilisation — for a module, the fraction of declarations its transitive import closure brings into scope that the module actually references. Median is 0.17% in our corpus — the "import wasteland" finding.

Cross-namespace edge — a dependency edge whose source and target sit in different top-level namespaces (Algebra, Topology, etc.). 78% of our declaration-level edges cross a namespace boundary; the paper reports 50.9%.

Data provenance

Every chart on this page is generated from a single corpus database via build_data.py. The manifest below records which DB produced this build, when, and which projects were ingested.

To rebuild against a different corpus:

make data DB=/path/to/other_corpus.db TAG=v4.28-2026-06-01
make site
make deploy   # ships to Cloudflare Pages

Citations & Acknowledgments

• Foundational study: Li, Peng, Severini, Shafto (2026), "The Network Structure of Mathlib" (arXiv:2604.24797v1).
• Typed extraction: aurasoph/lean-graph.
• Community-project index: Lean Prover Community Projects.
• Reproduction: make data && make site from this directory regenerates every chart on this page against whichever corpus DB the Makefile points at. The default DB is formalized_graph_v2/data/generated/corpus_v2_mathlib_plus_v4.27_v4.28_v4.29.db; override via make data DB=/path/to/other.db TAG=label.