datasets
Training and evaluation data, with the modality, task and licence stated up front. Listed live from the Hugging Face Hub.
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-exportmathlib_const_deps
Mathlib Const Deps
This dataset was generated with lean_scout
from the GitHub repository adamtopaz/mathlib_const_deps at commit ded17d387875019ca8ee4eca1307a07e814fe565.
Source
Source repository: adamtopaz/mathlib_const_deps
Source commit: ded17d387875019ca8ee4eca1307a07e814fe565
Hugging Face dataset repo: adamtopaz/mathlib_const_deps
Dataset URL: https://huggingface.co/datasets/adamtopaz/mathlib_const_deps
Generated at (UTC): 2026-03-27T20:57:40.590929Z
Mathlib commit… See the full description on the dataset page: https://huggingface.co/datasets/adamtopaz/mathlib_const_deps.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.mathlib_handler_benchmark_410This dataset is used in the paper Assisting Mathematical Formalization with A Learning-based Premise Retriever. It contains data for training and evaluating a premise retriever for the Lean theorem prover.
The dataset is described in detail in the GitHub repository. It consists of proof states and corresponding premises from the Mathlib library. The data is designed to train a model to effectively retrieve relevant premises for a given proof state, assisting users in the mathematical… See the full description on the dataset page: https://huggingface.co/datasets/ruc-ai4math/mathlib_handler_benchmark_410.Lean4-Mathlib
Lean4-Mathlib
Structured dataset of mathematical formalizations from the Mathlib4 library for Lean 4.
Source
Repository: https://github.com/leanprover-community/mathlib4
Commit: b9f14353520df73472ae3825fb53f86559a01319
Files: 8170
License: apache-2.0
Schema
Column
Type
Description
statement
string
Declaration signature/claim with the leading keyword removed (verbatim slice); the full declaration minus its proof
proof
string
Verbatim… See the full description on the dataset page: https://huggingface.co/datasets/phanerozoic/Lean4-Mathlib.lean-dojo-mathlib4
Dataset Card for "lean-dojo-mathlib4"
More Information needed
ntp-mathlib-instruct-context
miniCTX: Neural Theorem Proving with (Long-)Contexts
Lean 4 tactic prediction examples extracted from Mathlib.
Examples contain:
prompt:
instruction, preceding file content, proof state
instruction, proof state
completion: tactic
The file content has been truncated to 1024 tokens.
Version
Generated using ntptoolkit's ntp-training-data and instruction_tuning.py.
It used the following config for ntp-training-data:
{
"repo":… See the full description on the dataset page: https://huggingface.co/datasets/l3lab/ntp-mathlib-instruct-context.ntp-mathlib
miniCTX: Neural Theorem Proving with (Long-)Contexts
Lean 4 tactic prediction examples extracted from Mathlib.
These examples have not been formatted for instruction tuning (including data splits).
Please see l3lab/ntp-mathlib-instruct-* for datasets with instruction tuning examples.
Version
Generated using ntptoolkit's ntp-training-data.
It used the following config for ntp-training-data:
{
"repo": "https://github.com/leanprover-community/mathlib4",
"commit":… See the full description on the dataset page: https://huggingface.co/datasets/l3lab/ntp-mathlib.ntp-mathlib-instruct-st
miniCTX: Neural Theorem Proving with (Long-)Contexts
Lean 4 tactic prediction examples extracted from Mathlib.
Examples contain:
prompt:
instruction, proof state
completion: tactic
Version
Generated using ntptoolkit's ntp-training-data and instruction_tuning.py.
It used the following config for ntp-training-data:
{
"repo": "https://github.com/leanprover-community/mathlib4",
"commit": "cf8e23a62939ed7cc530fbb68e83539730f32f86",
"lean":… See the full description on the dataset page: https://huggingface.co/datasets/l3lab/ntp-mathlib-instruct-st.lsv2-mathlib-v4.28.0-rc1-jsonl
LeanSearch v2 — Mathlib v4.28.0-rc1 corpus (JSONL)
One record per Mathlib v4.28.0-rc1 declaration with the LLM-generated informal description used as the embedding input — the raw source from which the companion cuVS index is built.
Code: https://github.com/frenzymath/LeanSearch-v2
Paper: https://arxiv.org/abs/2605.13137
mathlib-cache
mathlib-cache
Cached databases for the local premise selection server of Canonical.
mathlib_informal_v4.16.0
Notes
Names
All names in Lean (names of symbols and modules) are stored as their raw form (list[int | str]) instead of the usual pretty-printed form to avoid problems arising from quoting/unquoting.
For example, instead of "Lean.«binderTerm∉_»" we have ["Lean", "binderTerm∉_"].
test_extract_mathlib_v2leanstral-mathlib-calibration-corpora
Leanstral Mathlib calibration corpora
The sample data comes from the pinned Apache-2.0-licensed
Mathlib source tree. This
repository holds the data and curated methods documentation—but not the
separately developed builder package.
This dataset contains the calibration corpora used to pick a static FP8
activation profile for an MXFP4 W4A8 conversion of Leanstral 1.5 119B-A6B. It
publishes every candidate corpus, their manifests, the shared
iterative-development pack, and the… See the full description on the dataset page: https://huggingface.co/datasets/robbiemu/leanstral-mathlib-calibration-corpora.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/anon-mlib-d3a4/MathlibGraph.lsv2-mathlib-v4.28.0-rc1-cuvs
LeanSearch v2 — Mathlib v4.28.0-rc1 cuVS index
Pre-built cuVS CAGRA index over every Mathlib v4.28.0-rc1 declaration, encoded with Qwen3-Embedding-8B; drops directly into the LeanSearch v2 serving pipeline (cuvs_index.bin + metadata.pkl + texts.pkl).
Code: https://github.com/frenzymath/LeanSearch-v2
Paper: https://arxiv.org/abs/2605.13137
ntp-mathlib-instruct-context-fullproof
miniCTX: Neural Theorem Proving with (Long-)Contexts
Lean 4 full proof generation examples extracted from Mathlib.
Examples contain:
prompt:
instruction, preceding file content
completion: proof
The file content has been truncated to 1024 tokens.
Version
Generated using ntptoolkit's ntp-training-data and instruction_tuning.py.
It used the following config for ntp-training-data:
{
"repo": "https://github.com/leanprover-community/mathlib4",
"commit":… See the full description on the dataset page: https://huggingface.co/datasets/l3lab/ntp-mathlib-instruct-context-fullproof.mathlib4-state-changevalidation-mathlib-mathcompMathlib-Normalized-Sexpr
Mathlib Normalized S-Expressions
Lean 4 proof states from Mathlib, paired with the tactic applied at each
step, in three representations extracted directly from the Lean kernel:
Source-faithful S-expressions of the goal and every hypothesis, as
Lean elaborated them.
Normalized S-expressions of the same state, with stable local-context
indices suitable for model input.
Annotated tactic syntax -- the original tactic's syntax tree with
identifier leaves resolved to the constants… See the full description on the dataset page: https://huggingface.co/datasets/jajostrains/Mathlib-Normalized-Sexpr.lean-mathlib-hashmapmathlib_informal_v4.28.0
mathlib_informal_v4.28.0
Dataset Summary
This dataset contains Lean v4.28.0 mathlib declarations informalized with the repo's
external LeanSearch-based pipeline and published in the retrieval schema used by this
codebase.
What Is Included
mathlib_informal_v4.28.0.jsonl: one JSON object per declaration
dataset_metadata.json: supplemental provenance, schema, and checksum metadata
Cleaning And Normalization
Machine-local paths were removed from the… See the full description on the dataset page: https://huggingface.co/datasets/adeo1/mathlib_informal_v4.28.0.Lean3-Mathlib
Lean3-Mathlib
Declarations from mathlib3, the Lean 3 mathematical library (archived).
Source
Repository: https://github.com/leanprover-community/mathlib
Commit: 65a1391a0106c9204fe45bc73a039f056558cb83
Files: 3220
License: apache-2.0
Schema
Column
Type
Description
statement
string
Declaration signature/claim with the leading keyword removed (verbatim slice); the full declaration minus its proof
proof
string
Verbatim proof/body, empty… See the full description on the dataset page: https://huggingface.co/datasets/phanerozoic/Lean3-Mathlib.mathlib-refactor-history
Mathlib Refactor History
This release is a source-level history of public declarations in
leanprover-community/mathlib4,
pinned to commit e72c1e277f31441626621f7d0c7207862fc25569. It connects a complete
commit index to statement-change scans and lossless before/after bundles for
refactor-shaped historical events.
The package contains 157.7 MiB of compressed/derived data in
17 data files. Exact byte counts and both compressed and
canonical SHA-256 digests are recorded in… See the full description on the dataset page: https://huggingface.co/datasets/princhernwang/mathlib-refactor-history.ax-prover-mathlib-hyde-4b