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.
0466
1{2 "snapshot": {3 "mathlib_commit": "534cf0b",4 "snapshot_date": "2026-02-02",5 "lean_version": "leanprover/lean4:v4.28.0-rc1"6 },7 "declaration_graph": {8 "node_count": 308129,9 "edge_count_raw": 8436366,10 "edge_count_no_self_loops": 8431611,11 "self_loops": 4755,12 "explicit_edge_count": 2178534,13 "explicit_edge_ratio": 0.2582,14 "synthesized_edge_ratio": 0.7418,15 "dag_depth": 83,16 "dag_layers": 84,17 "nodes_in_cycles": 5732,18 "louvain_modularity": 0.4778,19 "louvain_num_communities": 89,20 "nmi_namespace_vs_community": 0.3458,21 "power_law_alpha_in": 1.781,22 "power_law_alpha_in_source": "paper appendix-decl.tex table, xmin=20",23 "power_law_alpha_out": 2.936,24 "power_law_alpha_out_source": "paper appendix-decl.tex table"25 },26 "module_graph": {27 "node_count": 7564,28 "edge_count": 20881,29 "dag_depth": 154,30 "dag_layers": 155,31 "louvain_modularity": 0.6101,32 "louvain_num_communities": 15,33 "transitive_redundancy_ratio": 0.175,34 "transitive_redundancy_ratio_source": "paper contribution.tex",35 "median_import_utilization": 0.016,36 "median_import_utilization_source": "paper contribution.tex (per-edge median over all import edges)",37 "critical_path_parallelism_ratio": 22.4,38 "critical_path_parallelism_ratio_source": "paper appendix-module.tex"39 },40 "namespace_graph_k2": {41 "node_count": 10097,42 "edge_count": 332081,43 "dag_depth": 7,44 "dag_layers": 8,45 "dag_note": "namespace graph has cycles; depth computed on condensed SCC graph",46 "louvain_modularity": 0.2703,47 "louvain_num_communities": 13,48 "nmi_namespace_vs_community": 0.2456,49 "cross_namespace_ratio": 0.8581,50 "cross_namespace_ratio_note": "fraction of declaration edges crossing depth-2 namespace boundaries"51 },52 "edge_decompositions": {53 "proof_only_ratio": 0.439,54 "statement_only_ratio": 0.081,55 "mixed_ratio": 0.48,56 "source": "paper contribution.tex (requires Lean extraction not in current dataset)"57 },58 "kind_distribution": {59 "theorem": 243725,60 "definition": 48664,61 "abbrev": 6667,62 "constructor": 4755,63 "inductive": 3813,64 "opaque": 499,65 "quotient": 3,66 "axiom": 367 }68}