datasets
Training and evaluation data, with the modality, task and licence stated up front. Listed live from the Hugging Face Hub.
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.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-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-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
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.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∉_"].
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.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.mathlib_informal_v4.19.0mathlibretrieval
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/
mathlib_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.mathlib_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.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.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.mathlib_informal_v4.9.0