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.
d13f23b723b8a846827a245b89c10fc7d3f11612
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-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.
d13f23b723b8a846827a245b89c10fc7d3f11612
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.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.
d13f23b723b8a846827a245b89c10fc7d3f11612
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.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.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.mathlib-export