MathNetwork/MathlibGraph

MathlibGraph: The Multinetwork of Mathlib

Dependency graph of Mathlib (commit `534cf0b`, 2 Feb 2026), the largest formal mathematics library for Lean 4 (v4.28.0-rc1).

Three dependency layers (declarations, modules, namespaces), each with nodes, edges, and precomputed network metrics.

Quick Stats

Files

Raw Data (v1)

Three-Layer Graphs (v2)

Each layer has nodes.csv, edges.csv, and metrics.csv:

v2/summary.json contains headline statistics for all three levels.

Quick Start

from datasets import load_dataset

# Declaration level
decl = load_dataset("MathNetwork/MathlibGraph",
                    data_files="v2/declaration/metrics.csv", split="train").to_pandas()
edges = load_dataset("MathNetwork/MathlibGraph",
                     data_files="mathlib_edges.csv", split="train").to_pandas()

# Module level
mod_nodes = load_dataset("MathNetwork/MathlibGraph",
                         data_files="v2/module/nodes.csv", split="train").to_pandas()
mod_edges = load_dataset("MathNetwork/MathlibGraph",
                         data_files="v2/module/edges.csv", split="train").to_pandas()

# Namespace level
ns_nodes = load_dataset("MathNetwork/MathlibGraph",
                        data_files="v2/namespace/nodes.csv", split="train").to_pandas()
ns_edges = load_dataset("MathNetwork/MathlibGraph",
                        data_files="v2/namespace/edges.csv", split="train").to_pandas()

Schema

v2/declaration/nodes.csv

Deduplicated from mathlib_nodes.csv (317,655 to 308,129 rows; 9,526 @[to_additive] mirrors removed).

v2/declaration/metrics.csv

All columns from nodes.csv plus:

v2/module/nodes.csv

v2/module/edges.csv

v2/module/metrics.csv

v2/namespace/nodes.csv

v2/namespace/edges.csv

v2/namespace/metrics.csv

Methodology

• —Extraction: lean4export (nodes) + lean-training-data (edges) + importGraph (module graph) + jixia (metadata)
• —Deduplication: by name, 317,655 to 308,129 rows (9,526 @[to_additive] mirrors)
• —Self-loops: 4,755 constructor self-references filtered
• —PageRank: alpha=0.85, max_iter=100, tol=1e-6
• —Betweenness: declaration k=500, namespace k=300, module exact; seed=42
• —Communities: Louvain, resolution=1.0, random_state=42, undirected projection
• —DAG layers: Kahn's algorithm; cycle nodes get layer=-1; namespace graph condensed via SCC
• —Namespace cycles: 6,055 of 10,097 namespaces in 38 SCCs (largest: 5,899 nodes)

Hold-Out Experiments

We validate the premise retrieval results with two levels of hold-out experiments to assess information leakage. In the original experiment, all network features (degree, PageRank, betweenness, community, DAG layer) are precomputed on the full graph. Hold-out experiments recompute features on a reduced graph to test whether full-graph computation inflates AUC.

Edge-level hold-out

• —Randomly remove 20% of edges, recompute all features on remaining 80% graph
• —Tests whether full-graph feature computation inflates AUC

Declaration-level hold-out

• —Split theorems 80/20, remove ALL edges (incoming and outgoing) of test theorems from training graph
• —Test theorems have zero degree in training graph
• —Simulates the real scenario: predicting premises for a brand new theorem

Results (Split 1, seed=42)

The community feature drops to random (0.500) in declaration-level hold-out because test declarations become isolated nodes with unique community IDs. Despite this, the combined network feature model retains AUC=0.978, confirming that degree, PageRank, and DAG position carry genuine predictive signal independent of information leakage.

Full 5-split results with mean and std are in experiments/holdout_decl_level.json (updated incrementally).

Experiment Files

License

Apache 2.0