The Network Structure of Mathlib

Overview

A multilayer network analysis of Mathlib, examining logical structure, compiler-generated dependencies, and the limits of network centrality as a measure of mathematical relevance.

The MathlibGraph dataset card identifies Mathlib commit 534cf0b (2 February 2026), with Lean v4.28.0-rc1. Check the paper version and dataset snapshot when reproducing an analysis.

Available materials

Paper: Read the preprint and its version history on arXiv.
Code: Explore the analysis repository referenced by the paper. See the repository for usage and licensing.
Dataset: MathlibGraph: declaration, module and namespace dependency layers, with network metrics. The dataset card specifies Apache 2.0.

Citation

@misc{li2026networkstructuremathlib,
  title = {The Network Structure of Mathlib},
  author = {Xinze Li and Nanyun Peng and Simone Severini and Patrick Shafto},
  year = {2026},
  eprint = {2604.24797},
  archivePrefix = {arXiv},
  primaryClass = {cs.LO},
  url = {https://arxiv.org/abs/2604.24797}
}