mathlib
Datasets
All datasets matching “mathlib”mathlib-tactics
Mathlib Tactics
This dataset contains tactic invocations with associated goal states from proofs in Mathlib, the mathematical library for the Lean 4 theorem prover, extracted with lean_scout.
Extracted from the Mathlib commit with the following hash.
5ed2965256430c3649e86755f9576b54eca72435
The dataset follows this schema:
fields:
- type:
datatype: string
nullable: true
name: module
- type:
datatype: struct
children:
- type:
datatype: nat… See the full description on the dataset page: https://huggingface.co/datasets/mathlib-initiative/mathlib-tactics.mathlib-const-dep
Mathlib Constant Dependencies
This dataset contains direct constant dependency information for declarations in Mathlib, the mathematical library for the Lean 4 theorem prover, extracted with lean_scout.
Extracted from the Mathlib commit with the following hash.
0df444a360eaa60ab8c11dca51a86af692955474
The dataset follows this schema:
fields:
- type:
datatype: string
nullable: false
name: name
- type:
datatype: string
nullable: true
name: module
- type:
item:… See the full description on the dataset page: https://huggingface.co/datasets/mathlib-initiative/mathlib-const-dep.mathlib-types
Mathlib Types
This dataset contains information about types defined in Mathlib, the mathematical library for the Lean 4 theorem prover, extracted with lean_scout.
Extracted from the Mathlib commit with the following hash.
0df444a360eaa60ab8c11dca51a86af692955474
The dataset follows this schema:
fields:
- type:
datatype: string
nullable: false
name: name
- type:
datatype: string
nullable: true
name: module
- type:
datatype: string
nullable: false
name:… See the full description on the dataset page: https://huggingface.co/datasets/mathlib-initiative/mathlib-types.MathlibPR
MathlibPR
MathlibPR is built from real Mathlib4 pull request histories and evaluates merge-readiness judgments for build-passing snapshots. Each snapshot has a binary reference label, but evaluated systems may return one of three final verdicts: merge_ready, not_merge_ready, or uncertain.
Dataset Summary
Full benchmark size: 15,895 snapshots
Label distribution: 11,409 merge_ready, 4,486 not_merge_ready
Within-PR pair dataset: 3,687 pairs
Agent subsets: six… See the full description on the dataset page: https://huggingface.co/datasets/MathlibPR/MathlibPR.mathlib4_dependency_graph
MATHLIB4 DEPENDENCY GRAPH
make dependency graph for mathlib4 using jixia
HOW TO
how to make your own mathlib4 graph
Clone the repository at https://github.com/fbundle/mathlib4_dependency_graph
Check out your favorite mathlib version
Use build script to build mathlib and jixia
Extract dependency graph by jixia_export.py
Get symbol file by get_symbol_file.py and get_symbol_db.py
Upload to huggingface using upload_huggingface.py
or just download the prebuilt files… See the full description on the dataset page: https://huggingface.co/datasets/khanh2023/mathlib4_dependency_graph.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)
Louvain… See the full description on the dataset page: https://huggingface.co/datasets/MathNetwork/MathlibGraph.