Datasetpublic

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.

sourceHugging Faceapache-2.0updated 6mo agoView on Hugging Face

0likes368downloads

root.gitattributes

.gitattributes71 linesDownload Raw Back to root

1*.7z filter=lfs diff=lfs merge=lfs -text2*.arrow filter=lfs diff=lfs merge=lfs -text3*.bin filter=lfs diff=lfs merge=lfs -text4*.bz2 filter=lfs diff=lfs merge=lfs -text5*.ckpt filter=lfs diff=lfs merge=lfs -text6*.ftz filter=lfs diff=lfs merge=lfs -text7*.gz filter=lfs diff=lfs merge=lfs -text8*.h5 filter=lfs diff=lfs merge=lfs -text9*.joblib filter=lfs diff=lfs merge=lfs -text10*.lfs.* filter=lfs diff=lfs merge=lfs -text11*.lz4 filter=lfs diff=lfs merge=lfs -text12*.mds filter=lfs diff=lfs merge=lfs -text13*.mlmodel filter=lfs diff=lfs merge=lfs -text14*.model filter=lfs diff=lfs merge=lfs -text15*.msgpack filter=lfs diff=lfs merge=lfs -text16*.npy filter=lfs diff=lfs merge=lfs -text17*.npz filter=lfs diff=lfs merge=lfs -text18*.onnx filter=lfs diff=lfs merge=lfs -text19*.ot filter=lfs diff=lfs merge=lfs -text20*.parquet filter=lfs diff=lfs merge=lfs -text21*.pb filter=lfs diff=lfs merge=lfs -text22*.pickle filter=lfs diff=lfs merge=lfs -text23*.pkl filter=lfs diff=lfs merge=lfs -text24*.pt filter=lfs diff=lfs merge=lfs -text25*.pth filter=lfs diff=lfs merge=lfs -text26*.rar filter=lfs diff=lfs merge=lfs -text27*.safetensors filter=lfs diff=lfs merge=lfs -text28saved_model/**/* filter=lfs diff=lfs merge=lfs -text29*.tar.* filter=lfs diff=lfs merge=lfs -text30*.tar filter=lfs diff=lfs merge=lfs -text31*.tflite filter=lfs diff=lfs merge=lfs -text32*.tgz filter=lfs diff=lfs merge=lfs -text33*.wasm filter=lfs diff=lfs merge=lfs -text34*.xz filter=lfs diff=lfs merge=lfs -text35*.zip filter=lfs diff=lfs merge=lfs -text36*.zst filter=lfs diff=lfs merge=lfs -text37*tfevents* filter=lfs diff=lfs merge=lfs -text38# Audio files - uncompressed39*.pcm filter=lfs diff=lfs merge=lfs -text40*.sam filter=lfs diff=lfs merge=lfs -text41*.raw filter=lfs diff=lfs merge=lfs -text42# Audio files - compressed43*.aac filter=lfs diff=lfs merge=lfs -text44*.flac filter=lfs diff=lfs merge=lfs -text45*.mp3 filter=lfs diff=lfs merge=lfs -text46*.ogg filter=lfs diff=lfs merge=lfs -text47*.wav filter=lfs diff=lfs merge=lfs -text48# Image files - uncompressed49*.bmp filter=lfs diff=lfs merge=lfs -text50*.gif filter=lfs diff=lfs merge=lfs -text51*.png filter=lfs diff=lfs merge=lfs -text52*.tiff filter=lfs diff=lfs merge=lfs -text53# Image files - compressed54*.jpg filter=lfs diff=lfs merge=lfs -text55*.jpeg filter=lfs diff=lfs merge=lfs -text56*.webp filter=lfs diff=lfs merge=lfs -text57# Video files - compressed58*.mp4 filter=lfs diff=lfs merge=lfs -text59*.webm filter=lfs diff=lfs merge=lfs -text60nodes.csv filter=lfs diff=lfs merge=lfs -text61edges.csv filter=lfs diff=lfs merge=lfs -text62mathlib_nodes.csv filter=lfs diff=lfs merge=lfs -text63mathlib_edges.csv filter=lfs diff=lfs merge=lfs -text64tactic_usage.ndjson filter=lfs diff=lfs merge=lfs -text65mechanisms.ndjson filter=lfs diff=lfs merge=lfs -text66v2/mathlib_nodes_enriched.csv filter=lfs diff=lfs merge=lfs -text67v2/mathlib_namespace_edges_k2.csv filter=lfs diff=lfs merge=lfs -text68v2/declaration/nodes.csv filter=lfs diff=lfs merge=lfs -text69v2/namespace/edges.csv filter=lfs diff=lfs merge=lfs -text70v2/declaration/metrics.csv filter=lfs diff=lfs merge=lfs -text71