MathNetwork/MathlibGraph

1---2license: apache-2.03task_categories:4  - graph-ml5language:6  - en7tags:8  - mathematics9  - lean410  - mathlib11  - dependency-graph12  - formal-verification13  - network-analysis14size_categories:15  - 100K<n<1M16---17 18# MathlibGraph: The Multinetwork of Mathlib19 20Dependency graph of [Mathlib](https://github.com/leanprover-community/mathlib4) (commit [`534cf0b`](https://github.com/leanprover-community/mathlib4/commit/534cf0b), 2 Feb 2026), the largest formal mathematics library for Lean 4 (`v4.28.0-rc1`).21 22Three dependency layers (declarations, modules, namespaces), each with nodes, edges, and precomputed network metrics.23 24## Quick Stats25 26| | Declarations | Modules | Namespaces (k=2) |27|---|---|---|---|28| Nodes | 308,129 | 7,564 | 10,097 |29| Edges | 8,436,366 | 20,881 | 332,081 (weighted) |30| DAG depth | 83 | 154 | 7 (after SCC condensation) |31| Louvain modularity | 0.478 | 0.610 | 0.270 |32| Synthesized edges | 74.2% | — | — |33| In cycles | 5,732 nodes | 0 (DAG) | 6,055 nodes (38 SCCs) |34 35## Files36 37### Raw Data (v1)38 39| File | Rows | Description |40|------|------|-------------|41| `mathlib_edges.csv` | 8,436,366 | Declaration dependency edges |42| `mathlib_nodes.csv` | 317,655 | Declarations before deduplication |43| `nodes.csv` / `edges.csv` | 633K / 10.9M | Full environment (Lean + Std + Mathlib) |44| `mechanisms.ndjson` | — | Lean language mechanism extractions |45| `tactic_usage.ndjson` | — | Per-declaration tactic usage profiles |46 47### Three-Layer Graphs (v2)48 49Each layer has `nodes.csv`, `edges.csv`, and `metrics.csv`:50 51| Folder | Nodes | Edges | Metrics | Description |52|--------|-------|-------|---------|-------------|53| `v2/declaration/` | 308,129 | (use root `mathlib_edges.csv`) | 308,129 x 11 | Theorems, definitions, and other named constants |54| `v2/module/` | 7,564 | 20,881 | 7,564 x 10 | Source files linked by `import` statements |55| `v2/namespace/` | 10,097 | 332,081 | 10,097 x 11 | Depth-2 dotted-name prefixes, weighted edges |56 57`v2/summary.json` contains headline statistics for all three levels.58 59## Quick Start60 61```python62from datasets import load_dataset63 64# Declaration level65decl = load_dataset("MathNetwork/MathlibGraph",66                    data_files="v2/declaration/metrics.csv", split="train").to_pandas()67edges = load_dataset("MathNetwork/MathlibGraph",68                     data_files="mathlib_edges.csv", split="train").to_pandas()69 70# Module level71mod_nodes = load_dataset("MathNetwork/MathlibGraph",72                         data_files="v2/module/nodes.csv", split="train").to_pandas()73mod_edges = load_dataset("MathNetwork/MathlibGraph",74                         data_files="v2/module/edges.csv", split="train").to_pandas()75 76# Namespace level77ns_nodes = load_dataset("MathNetwork/MathlibGraph",78                        data_files="v2/namespace/nodes.csv", split="train").to_pandas()79ns_edges = load_dataset("MathNetwork/MathlibGraph",80                        data_files="v2/namespace/edges.csv", split="train").to_pandas()81```82 83## Schema84 85### v2/declaration/nodes.csv86 87Deduplicated from `mathlib_nodes.csv` (317,655 to 308,129 rows; 9,526 `@[to_additive]` mirrors removed).88 89| Column | Type | Description |90|--------|------|-------------|91| name | str | Fully qualified declaration name |92| kind | str | theorem, definition, abbrev, inductive, constructor, opaque, axiom, or quotient |93| module | str | Parent namespace (null for 30,944 Lean core declarations) |94 95### v2/declaration/metrics.csv96 97All columns from `nodes.csv` plus:98 99| Column | Type | Description |100|--------|------|-------------|101| namespace_depth2 | str | First 2 dot-separated components (e.g., `Mathlib.Algebra`) |102| namespace_depth3 | str | First 3 dot-separated components |103| in_degree | int | Declarations that depend on this one |104| out_degree | int | Declarations this one depends on |105| pagerank | float | PageRank (alpha=0.85) |106| betweenness | float | Betweenness centrality (k=500, seed=42) |107| community_id | int | Louvain community |108| dag_layer | int | Topological depth; -1 for 5,732 nodes in cycles |109| file_module | str | Source file module (from Lean environment, 278K coverage) |110| is_tactic_proof | bool | Whether the proof uses tactics (78,315 declarations) |111| tactic_count | int | Number of tactics used in the proof |112| top_tactic | str | Most frequently used tactic in this proof |113| is_instance | bool | Whether this is a typeclass instance (26,415 declarations) |114| instance_class | str | Which typeclass this instance implements |115| is_coercion | bool | Whether this is a coercion (241 declarations) |116| to_additive_pair | str | Name of the corresponding additive/multiplicative variant |117| def_height | float | Definitional height in the kernel (42,935 declarations) |118 119### v2/module/nodes.csv120 121| Column | Type | Description |122|--------|------|-------------|123| module | str | Dotted module name (e.g., `Mathlib.Algebra.Group.Defs`) |124| decl_count | int | Declarations defined in this source file |125 126### v2/module/edges.csv127 128| Column | Type | Description |129|--------|------|-------------|130| source | str | Importing module |131| target | str | Imported module |132| is_exported | bool | Whether this is a public import (20,699 of 20,881) |133 134### v2/module/metrics.csv135 136| Column | Type | Description |137|--------|------|-------------|138| module | str | Module name |139| decl_count | int | Declarations in this module (full decl_module mapping, 499K coverage) |140| in_degree | int | Modules that import this one |141| out_degree | int | Modules this one imports |142| pagerank | float | PageRank on module import graph |143| betweenness | float | Betweenness centrality (exact) |144| dag_layer | int | Topological depth in module DAG |145| community_id | int | Louvain community |146| cohesion | float | Fraction of declaration edges staying within module |147| import_utilization_median | float | Median fraction of imported declarations used |148 149### v2/namespace/nodes.csv150 151| Column | Type | Description |152|--------|------|-------------|153| namespace | str | Depth-2 namespace (e.g., `Mathlib.Algebra`) |154| decl_count | int | Declarations in this namespace |155| in_cycle | bool | True if this namespace is in a strongly connected component |156| scc_id | int | SCC identifier (-1 if not in a cycle) |157 158### v2/namespace/edges.csv159 160| Column | Type | Description |161|--------|------|-------------|162| source | str | Source namespace |163| target | str | Target namespace |164| weight | int | Number of declaration-level edges between these namespaces |165 166### v2/namespace/metrics.csv167 168| Column | Type | Description |169|--------|------|-------------|170| namespace | str | Depth-2 namespace |171| decl_count | int | Declarations in this namespace |172| in_degree | int | Unweighted in-degree |173| out_degree | int | Unweighted out-degree |174| edge_weight_sum | int | Total declaration edges involving this namespace |175| pagerank | float | Weighted PageRank (alpha=0.85) |176| betweenness | float | Weighted betweenness (k=300, seed=42) |177| community_id | int | Louvain community (weighted undirected) |178| cross_ns_ratio | float | Fraction of edges crossing namespace boundaries |179| in_cycle | bool | In a strongly connected component (6,055 of 10,097) |180| scc_id | int | SCC identifier (-1 if acyclic) |181 182## Methodology183 184- **Extraction**: lean4export (nodes) + lean-training-data (edges) + importGraph (module graph) + jixia (metadata)185- **Deduplication**: by name, 317,655 to 308,129 rows (9,526 `@[to_additive]` mirrors)186- **Self-loops**: 4,755 constructor self-references filtered187- **PageRank**: alpha=0.85, max_iter=100, tol=1e-6188- **Betweenness**: declaration k=500, namespace k=300, module exact; seed=42189- **Communities**: Louvain, resolution=1.0, random_state=42, undirected projection190- **DAG layers**: Kahn's algorithm; cycle nodes get layer=-1; namespace graph condensed via SCC191- **Namespace cycles**: 6,055 of 10,097 namespaces in 38 SCCs (largest: 5,899 nodes)192 193## Hold-Out Experiments194 195We 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.196 197### Edge-level hold-out198- Randomly remove 20% of edges, recompute all features on remaining 80% graph199- Tests whether full-graph feature computation inflates AUC200 201### Declaration-level hold-out202- Split theorems 80/20, remove ALL edges (incoming and outgoing) of test theorems from training graph203- Test theorems have zero degree in training graph204- Simulates the real scenario: predicting premises for a brand new theorem205 206### Results (Split 1, seed=42)207 208| Method | AUC (original) | AUC (edge hold-out) | AUC (decl hold-out) |209|--------|---------------|---------------------|---------------------|210| Random | 0.499 | 0.497 | 0.500 |211| Same module | 0.563 | 0.562 | 0.563 |212| Same namespace | 0.590 | 0.590 | 0.592 |213| Same community | 0.768 | 0.755 | 0.500 |214| Network features | 0.991 | 0.988 | 0.978 |215| All features | 0.994 | 0.992 | 0.984 |216 217The 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.218 219Full 5-split results with mean and std are in `experiments/holdout_decl_level.json` (updated incrementally).220 221### Experiment Files222 223| File | Description |224|------|-------------|225| `experiments/premise_retrieval_results.json` | Original experiment: 6 methods, 4 metrics, 95% CI |226| `experiments/premise_retrieval_hard_negatives.json` | Hard negatives (same-community) variant |227| `experiments/holdout_edge_level.json` | Edge-level hold-out (1 split) |228| `experiments/holdout_decl_level.json` | Declaration-level hold-out (5 splits, incremental) |229 230## License231 232Apache 2.0233