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-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.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.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.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.mathlib_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.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.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.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∉_"].
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
lean-dojo-mathlib4
Dataset Card for "lean-dojo-mathlib4"
More Information needed
mathlib-traced-tacticsntp-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.Mathlib-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.leanstral-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.test_extract_mathlib_v2subproofs-mathlib-v4.30.0ntp-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.premises-mathlib-v4.30.0mathlib_informal_v4.19.0mathlib_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.mathlib_informal_v4.15.0
mathlib_informal_v4.15.0
Dataset Summary
This dataset contains Lean v4.15.0 mathlib declarations with informal descriptions produced by the Autoprover enrichment pipeline and published in the retrieval schema used by this codebase.
What Is Included
mathlib_informal_v4.15.0.jsonl: one JSON object per declaration
dataset_metadata.json: supplemental provenance, schema, and checksum metadata
Cleaning And Normalization
Machine-local paths were removed… See the full description on the dataset page: https://huggingface.co/datasets/adeo1/mathlib_informal_v4.15.0.mathlib4-v4.26.0-premises
Mathlib v4.26.0 Premise Corpus (via LeanDojo-v2, fully Dockerized)
本仓库包含从 Mathlib v4.26.0(连同其全部依赖:Lean 核心库、Batteries、Aesop 等)中
提取出的全部有效 premises,以 corpus.jsonl 形式存储,可直接用于构建向量召回 / premise
selection 数据库。提取过程完全在 Docker 容器内完成,无需在本机安装 lean4 / elan / lake。
项目
值
来源仓库
leanprover-community/mathlib4
版本 / commit
v4.26.0 / 2df2f0150c275ad53cb3c90f7c98ec15a56a1a67
Lean toolchain
leanprover/lean4:v4.26.0
build_deps
true(含全部依赖)
文件数
9,765
premises 总数
284,372
corpus.jsonl… See the full description on the dataset page: https://huggingface.co/datasets/CHENSEE/mathlib4-v4.26.0-premises.mathlibretrieval
Informalized Mathlib4 Retrieval Dataset
The goal is to retrieve relevant mathlib4 theorems based on informal mathematical queries. Sourced from https://huggingface.co/datasets/hcju/leansearch_bench/
mathlib4-state-changemathlib_informal_v4.24.0
mathlib_informal_v4.24.0
Dataset Summary
This dataset contains Lean v4.24.0 mathlib declarations with informal descriptions produced by the Autoprover enrichment pipeline and published in the retrieval schema used by this codebase.
What Is Included
mathlib_informal_v4.24.0.jsonl: one JSON object per declaration
dataset_metadata.json: supplemental provenance, schema, and checksum metadata
Cleaning And Normalization
Machine-local paths were removed… See the full description on the dataset page: https://huggingface.co/datasets/adeo1/mathlib_informal_v4.24.0.rollout-premises-mathlib-v4.30.0premises-mathlib-v4.31.0mathlib-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.