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 Declarations Modules Namespaces (k=2) Nodes 308,129 7,564 10,097 Edges 8,436,366 20,881 332,081 (weighted) DAG depth 83 154 7 (after SCC condensation)… See the full description on the dataset page: https://huggingface.co/datasets/MathNetwork/MathlibGraph.
0368
1# MathFactor Data Summary2 3**Validation**: WARNING - Some edges reference missing nodes4 - Missing sources: 15914 (e.g., ['Set.preimage_add_preimage_subset', 'Left.add_neg_of_neg_of_nonpos', 'Hindman.FS.head'])5 - Missing targets: 12885 (e.g., ['Set.preimage_add_preimage_subset', 'GroupSeminorm.instSupSet._proof_3._to_additive_1', 'dist_sub_eq_dist_add_right'])6 7## Nodes8 9**Total**: 633,36410 11| Kind | Count |12|------|-------|13| theorem | 441,230 |14| definition | 82,962 |15| abbrev | 79,627 |16| constructor | 9,070 |17| opaque | 7,356 |18| recursor | 6,614 |19| inductive | 6,494 |20| axiom | 7 |21| quotient | 4 |22 23## Edges24 25**Total**: 10,889,01126 27| Type | Count |28|------|-------|29| Explicit (*) | 3,248,395 |30| Simplifier (s) | 0 |31| Direct | 7,640,616 |32 33## Top Modules (by node count)34 35| Module | Count |36|--------|-------|37| | 31,302 |38| List | 5,233 |39| Set | 5,065 |40| Finset | 4,954 |41| Nat | 4,566 |42| MeasureTheory | 3,496 |43| CategoryTheory | 3,471 |44| Polynomial | 3,280 |45| Int | 2,929 |46| CategoryTheory.Limits | 2,757 |