datasets
Training and evaluation data, with the modality, task and licence stated up front. Listed live from the Hugging Face Hub.
LeanTransitionCorpus
LeanTransitionCorpus
LeanTransitionCorpus is a dataset for training and studying automated theorem
proving systems in Lean. Its unit of data is one tactic transition: the proof state
before a tactic, the tactic that was executed, and the resulting state. This makes
it suitable for tactic prediction, proof-state representation learning, premise
selection, retrieval, verification, and trajectory-level training.
Many Lean datasets expose a theorem, tactic, and pretty-printed goal… See the full description on the dataset page: https://huggingface.co/datasets/HyperCactus0/LeanTransitionCorpus.goedel-workbook-lean427
Goedel Workbook Proofs — Lean 4.27
29,750 competition-math proofs from Goedel-LM/Lean-workbook-proofs, migrated from Lean 4.8 to Lean 4.27.0 / Mathlib v4.27.0.
The original proofs were generated by DeepSeek-Prover-V1.5 against the Lean Workbook problem set.
Quick Stats
Metric
Value
Total proofs
29,750
Compiling on Lean 4.27
28,016 (94.1%)
Traced tactic pairs
60,341
Theorems with traced pairs
24,879
Unique tactic heads
73
Median proof depth
1… See the full description on the dataset page: https://huggingface.co/datasets/banach1729/goedel-workbook-lean427.NuminaMath-LEAN-Proof-Artifacts
NuminaMath-LEAN Proof Artifacts
Dataset Summary
This dataset provides proof-analysis artifacts derived from
AI-MO/NuminaMath-LEAN.
It is released with two aligned configs:
lite: dual-track proof validation/extraction artifacts
full: all lite fields plus dual-track main-theorem structural artifacts
Both configs are aligned by sample identity (uuid, original_index) and processing order.
Config Overview
Use lite for overall tactic usage statistics (e.g.… See the full description on the dataset page: https://huggingface.co/datasets/iiis-lean/NuminaMath-LEAN-Proof-Artifacts.NuminaMath-LEAN-Sol
NuminaMath-LEAN Cleaned with NL Solutions
Dataset Summary
This is a cleaned version of the NuminaMath-LEAN dataset, enhanced with natural language (NL) solutions matched from source datasets. The primary goal is to provide paired formal statements/proofs with natural language solutions for proof formalization and theorem proving research.
The dataset matches problems from NuminaMath-LEAN with their corresponding natural language solutions from:
olympiads-ref: A… See the full description on the dataset page: https://huggingface.co/datasets/iiis-lean/NuminaMath-LEAN-Sol.lean-verifier-formalizations
Lean Verifier Formalizations
A dataset of Lean 4 theorem-proving tasks for evaluating agentic coding harnesses. Each row pairs a formal task_statement (with the reference proof body removed) against a real Lean 4 repository, plus the informal_excerpt/informal_source_text describing what the theorem claims, permitted_axioms for the verifier, and provenance fields (repo_url, repo_commit_sha, license) tracing back to the source project.
Sources
Every row is pulled… See the full description on the dataset page: https://huggingface.co/datasets/Pradheep1647/lean-verifier-formalizations.NuminaMath-LEAN-satp-buffer-dspaug-Temp
NuminaMath-LEAN-satp-buffer-dspaug-Temp
Staging buffer for the DSP+ paper-augmentation sweep (2026-04-29). This
is a -Temp variant — lemma_names / lemma_scores are empty and
theorem_uuid is the join key (matches NuminaMath-LEAN-satp.uuid).
Retrieval population + rename-to-uuid happens at the
promote-to-canonical merge step, mirroring the precedent set by
NuminaMath-LEAN-satp-buffer-planf-v1-Temp.
Why this exists
Schema audit on NuminaMath-LEAN-satp-buffer (40,965… See the full description on the dataset page: https://huggingface.co/datasets/ChristianZ97/NuminaMath-LEAN-satp-buffer-dspaug-Temp.lean-proof-compression
LeanPolish: Verified Supervision for Lean Proof Compression
A dataset of Lean 4 proof rewrite pairs produced by LeanPolish,
a kernel-verified proof-shortening tool. Every accepted
(original, replacement) pair was kernel-checked under Lean 4.21.0
with Mathlib v4.21.0 before emission, and the rewritten file was
re-elaborated end-to-end by a separate out-of-process verifier.
The dataset is suitable for training models that learn to compress,
simplify, or select proof tactics, and… See the full description on the dataset page: https://huggingface.co/datasets/leanpolish-anon/lean-proof-compression.NuminaMath-LEAN-satp-v4.27
NuminaMath-LEAN-satp-v4.27
Lean 4 formal-statement + initial proof goal_state pairs over the
NuminaMath-LEAN problem pool, packaged for Lean 4.27.0. This is the main
training set for SATP (Steering Aesop for Theorem Proving) running in a
Lean 4.27 environment.
Every row's formal_statement elaborates cleanly under the pinned toolchain
below, and every goal_state is the pretty-printed goal produced in that
row's own environment — the same rendering the SATP runtime observes at… See the full description on the dataset page: https://huggingface.co/datasets/ChristianZ97/NuminaMath-LEAN-satp-v4.27.craft-benchmark-lean
CRAFT Benchmark Dataset
Trajectory logs from the CRAFT benchmark — a multi-agent evaluation of pragmatic communication in LLMs under strict partial information. - TL;DR
Dataset Structure
Each row is one turn from a CRAFT game, with fields for:
Identity: structure_id, director_model, builder_model, model_type (base/frontier), turn_number
Director responses: D1_thinking, D1_message, D2_thinking, D2_message, D3_thinking, D3_message
Builder: builder_action, builder_block… See the full description on the dataset page: https://huggingface.co/datasets/Abhijnan/craft-benchmark-lean.Lean4-EquationalTheories
Lean4-EquationalTheories
Structured dataset from equational_theories — Terence Tao's magma equations project.
Source
Repository: https://github.com/teorth/equational_theories
Commit: 3f3999d958c5e289c7f5a063479af9dac122a7a8
Files: 1301
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… See the full description on the dataset page: https://huggingface.co/datasets/phanerozoic/Lean4-EquationalTheories.STP_Lean_0320This is an updated version of the final training dataset of Self-play Theorem Prover as described in the paper STP: Self-play LLM Theorem Provers with Iterative Conjecturing and Proving. This dataset includes:
Extracted examples from mathlib4,
Generated correct proofs of statements in LeanWorkbook,
Generated correct proofs of conjectures proposed by our model during self-play training.
Leandata
LEANDATA
A collection of Lean-formalized STEM problem-solving examples across physics, chemistry, calculus, probability, and related domains.
Dataset summary
Dataset page: https://huggingface.co/datasets/anon-ed-2026/Leandata
Total examples: 580
Loading with datasets
from datasets import load_dataset
ds = load_dataset("anon-ed-2026/Leandata", "atkins")
print(ds["train"][0]["problem_id"])
LeanCat
LeanCat: A Lean Dataset for Evaluating Library-Grounded Category-Theoretic Reasoning
This is an anonymized review artifact.
LeanCat is a dataset of 100 statement-level problems in Lean 4 (mathlib), designed to stress-test abstraction-heavy, library-grounded reasoning in formal mathematics. This repository contains Part I: 1-Category Theory.
Overview
LeanCat addresses a critical gap in automated theorem proving evaluation datasets by focusing on category theory - the… See the full description on the dataset page: https://huggingface.co/datasets/scicraft/LeanCat.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.STP_LeanThis is the final training dataset of Self-play Theorem Prover as described in the paper STP: Self-play LLM Theorem Provers with Iterative Conjecturing and Proving. This dataset includes:
Extracted examples from mathlib4,
Generated correct proofs of statements in LeanWorkbook,
Generated correct proofs of conjectures proposed by our model during self-play training.
lean4-stat-learning-theory-novel
A Large-Scale Lean 4 Dataset on Statistical Learning Theory
We present a high-quality, human-verified, large-scale Lean 4 dataset, extracted from our formalization of Statistical Learning Theory (SLT). We present the first comprehensive Lean 4 formalization of SLT grounded in empirical process theory. Our end-to-end formal infrastructure implement the missing contents in latest Lean 4 Mathlib library, including a complete development of Gaussian Lipschitz concentration… See the full description on the dataset page: https://huggingface.co/datasets/yuanhezhang/lean4-stat-learning-theory-novel.lean4-stat-learning-theory-random
A Large-Scale Lean 4 Dataset on Statistical Learning Theory
We present a high-quality, human-verified, large-scale Lean 4 dataset, extracted from our formalization of Statistical Learning Theory (SLT). We present the first comprehensive Lean 4 formalization of SLT grounded in empirical process theory. Our end-to-end formal infrastructure implement the missing contents in latest Lean 4 Mathlib library, including a complete development of Gaussian Lipschitz concentration… See the full description on the dataset page: https://huggingface.co/datasets/yuanhezhang/lean4-stat-learning-theory-random.lean4-stat-learning-theory-corpus
A Large-Scale Lean 4 Dataset on Statistical Learning Theory
We present a high-quality, human-verified, large-scale Lean 4 dataset, extracted from our formalization of Statistical Learning Theory (SLT). We present the first comprehensive Lean 4 formalization of SLT grounded in empirical process theory. Our end-to-end formal infrastructure implement the missing contents in latest Lean 4 Mathlib library, including a complete development of Gaussian Lipschitz concentration… See the full description on the dataset page: https://huggingface.co/datasets/yuanhezhang/lean4-stat-learning-theory-corpus.ai4math-lean
ai4math-lean
21 Lean 4 formal mathematics datasets with machine-verified labels.
Every problem has been verified against lean-server v4.21.0 on UVA's HPC cluster.
Results are embedded in each row as both structured verification JSON and flattened convenience columns.
Quick Start
from datasets import load_dataset
# Load a single dataset
ds = load_dataset("charliemeyer2000/ai4math-lean", "deepseek_prover")
# Load a large dataset with streaming
ds =… See the full description on the dataset page: https://huggingface.co/datasets/charliemeyer2000/ai4math-lean.leandojo-benchmark-4-randomThe random split of LeanDojo Benchmark 4.
Source data: https://zenodo.org/record/12740403/files/leandojo_benchmark_4.tar.gz
Lean4-FormalConjectures
Lean4-FormalConjectures
Structured dataset from formal-conjectures — Google DeepMind formalized conjectures.
Source
Repository: https://github.com/google-deepmind/formal-conjectures
Commit: b9b8aa0fd6170e482798f7c78c163acacd40e083
Files: 896
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… See the full description on the dataset page: https://huggingface.co/datasets/phanerozoic/Lean4-FormalConjectures.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.math-lean-hackable-rollouts
Math Lean Hackable Rollouts
This dataset contains 2,241 labeled multi-turn rollouts from a GRPO run on deliberately
hackable Lean 4 theorem-proving tasks. The policy was
nvidia/NVIDIA-Nemotron-3-Nano-30B-A3B-BF16.
The run's weakened grader accepts proofs containing sorry; the separate oracle restores
Lean's sorry check. hack_detected is true exactly when the weakened grader paid the
rollout but the restored oracle rejected it. Rows without a gradeable final answer were
excluded… See the full description on the dataset page: https://huggingface.co/datasets/AlignmentResearch/math-lean-hackable-rollouts.lean-repository-midtraining-v1
Lean 4 repository midtraining corpus v1
This is a causal language-model corpus curated from pinned Lean 4 repositories. It is
intended for repository midtraining after introductory Lean language SFT and before
verified proof SFT or verifier-guided RL. The rows contain source text, not
instruction/answer conversations.
Dataset
Split
Chunks
Train
18,367
Validation
1,071
Total
19,438
The source-preserving builder estimates 16.71M tokens using four… See the full description on the dataset page: https://huggingface.co/datasets/Pradheep1647/lean-repository-midtraining-v1.Lean-SFT-dataset
Lean Workbook + Goedel Proofs (Merged)
A merged dataset combining
problem statements from internlm/Lean-Workbook with full proofs from Goedel-LM/Lean-workbook-proofs
Human annotated subset from AI-MO/NuminaMath-LEAN
Citation
If you use this dataset, please cite the original sources:
internlm/Lean-Workbook
[Goedel-LM/Lean-workbook-proofs
AI-MO/NuminaMath-LEANLean4-Stdlib
Lean4-Stdlib
Structured dataset of definitions and theorems from the Lean 4 standard library (Init + Std).
Source
Repository: https://github.com/leanprover/lean4
Commit: d265d1ca745e7741a7e7f7366c22ce9c9dda57b6
Files: 1071
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-Stdlib.lean4
💎 Atomic-Lean4-Mathlib: Granular Proofs for Complex Analysis
🚀 Overview
Atomic-Lean4-Mathlib est un dataset de haute fidélité conçu pour le Process Supervision des LLMs de raisonnement (type o1, DeepSeek-R1).
Contrairement aux preuves standard de la Mathlib qui utilisent des tactiques opaques (simp, ring), ce dataset fournit des preuves décomposées à l'atome. Chaque étape logique est explicitée via des blocs calc et des réécritures (rw), permettant aux modèles… See the full description on the dataset page: https://huggingface.co/datasets/7rouz/lean4.PutnamBench-lean4
PutnamBench — Lean 4 (672 problems)
Lean 4 formalizations from PutnamBench,
a benchmark of problems from the William Lowell Putnam Mathematical Competition (1962-2023).
Converted from the official GitHub repository for convenient HuggingFace datasets access.
Citation
@article{tsoukalas2024putnambench,
title={PutnamBench: Evaluating Neural Theorem-Provers on the Putnam Mathematical Competition},
author={George Tsoukalas and Jasper Lee and John Jennings and Jimmy Xin… See the full description on the dataset page: https://huggingface.co/datasets/ChristianZ97/PutnamBench-lean4.lean-expert-optimized-2000
lean-expert-optimized-2000
Dataset Description
Optimized 2000-example dataset for training Lean trading algorithm optimization agents with 94%+ success rate target.
Dataset Statistics
Total Examples: 2,000
Training Examples: 1800
Validation Examples: 200
Target Success Rate: 94%+
Expected Performance: 96% (94-98% range)
Category Distribution
JSON Parsing: 1,333 examples (CRITICAL - 0% → 95% impact)
Optimization Workflows: 182 examples (HIGH… See the full description on the dataset page: https://huggingface.co/datasets/Kronu/lean-expert-optimized-2000.lean-language-docs-sft
Lean Language Docs SFT
Instruction/code examples for learning Lean 4 as a programming language. The examples
are generated from the introductory Getting to Know Lean sections of the official
Functional Programming in Lean book, then filtered and compiled locally.
Data
train rows: 285
validation rows: 34
teachers: deepseek/deepseek-v4-flash-0731 and openai/gpt-oss-120b
source license: CC BY 4.0
output format: messages plus generation and verification metadata
The… See the full description on the dataset page: https://huggingface.co/datasets/Pradheep1647/lean-language-docs-sft.