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.
Update dataset card with hold-out experiment results
Add hold-out experiment results
Upload README.md with huggingface_hub
Upload v2/module/edges.csv with huggingface_hub
Upload v2/module/metrics.csv with huggingface_hub
Upload v2/declaration/metrics.csv with huggingface_hub
Upload README.md with huggingface_hub
Delete v2/mathlib_namespace_edges_k2.csv with huggingface_hub
Delete v2/mathlib_namespace_nodes_k2.csv with huggingface_hub
Delete v2/mathlib_module_edges.csv with huggingface_hub
Delete v2/mathlib_module_nodes.csv with huggingface_hub
Delete v2/mathlib_summary.json with huggingface_hub
Delete v2/mathlib_namespaces_k2.csv with huggingface_hub
Delete v2/mathlib_modules.csv with huggingface_hub
Delete v2/mathlib_nodes_enriched.csv with huggingface_hub
Upload v2/summary.json with huggingface_hub
Upload v2/declaration/metrics.csv with huggingface_hub
Upload v2/namespace/metrics.csv with huggingface_hub
Upload v2/namespace/edges.csv with huggingface_hub
Upload v2/namespace/nodes.csv with huggingface_hub
Upload v2/module/metrics.csv with huggingface_hub
Upload v2/module/edges.csv with huggingface_hub
Upload v2/module/nodes.csv with huggingface_hub
Upload v2/declaration/nodes.csv with huggingface_hub
Upload README.md with huggingface_hub
Upload v2/mathlib_namespace_edges_k2.csv with huggingface_hub
Upload v2/mathlib_namespace_nodes_k2.csv with huggingface_hub
Upload v2/mathlib_module_edges.csv with huggingface_hub
Upload v2/mathlib_module_nodes.csv with huggingface_hub
Upload README.md with huggingface_hub
Upload README.md with huggingface_hub
Upload README.md with huggingface_hub
Upload v2/mathlib_summary.json with huggingface_hub
Upload v2/mathlib_namespaces_k2.csv with huggingface_hub
Upload v2/mathlib_modules.csv with huggingface_hub
Upload v2/mathlib_nodes_enriched.csv with huggingface_hub
Add Lean mechanism extraction data (typeclasses, attributes, coercions, etc.)
Add per-declaration tactic usage data (235,586 declarations, extracted via jixia)
Upload README.md with huggingface_hub
Remove incorrect arXiv link
Fix statistics: verified row counts and kind breakdown
Rename MathFactor to MathlibGraph
Upload mathlib_edges.csv with huggingface_hub
Upload mathlib_nodes.csv with huggingface_hub
Upload README.md with huggingface_hub
Upload mathlib_edges.csv with huggingface_hub
Upload mathlib_nodes.csv with huggingface_hub
Upload summary.md with huggingface_hub
Upload edges.csv with huggingface_hub
Upload nodes.csv with huggingface_hub