datasets
Training and evaluation data, with the modality, task and licence stated up front. Listed live from the Hugging Face Hub.
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.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.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.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.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.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.lean-proof-compression
LeanPolish: A Kernel-Verified Dataset and Symbolic Compression Framework for Lean 4 Proofs
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… See the full description on the dataset page: https://huggingface.co/datasets/leanpolish-anon/lean-proof-compression.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.
leandojo-benchmark-4-randomThe random split of LeanDojo Benchmark 4.
Source data: https://zenodo.org/record/12740403/files/leandojo_benchmark_4.tar.gz
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.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.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.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.NuminaMath-LEAN-satp
NuminaMath-LEAN-satp
Lean 4 formal-statement + initial proof goal_state pairs harvested from
the NuminaMath-LEAN problem pool. This is the main training set for
SATP (Steering Aesop for Theorem Proving) and the target distribution
that all sibling datasets in this collection align with byte-for-byte.
Sibling datasets (same uuid scheme so they join cleanly):
NuminaMath-LEAN-satp-gaps — augmented train set with sub-goal (gap) records harvested from verified sketches… See the full description on the dataset page: https://huggingface.co/datasets/ChristianZ97/NuminaMath-LEAN-satp.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.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.NuminaMath-LEAN-cleaned
NuminaMath-LEAN-cleaned
Dataset Description
This is a cleaned and filtered version of AI-MO/NuminaMath-LEAN dataset, optimized for theorem proving training.
Cleaning Process
The dataset has been automatically cleaned with the following improvements:
Removed all comments: Removed /- -/ multi-line and -- single-line commentsRemoved sorry keywords: Cleaned up incomplete proofsStandardized endings: All statements end with := byFiltered declarations: Only kept… See the full description on the dataset page: https://huggingface.co/datasets/ChristianZ97/NuminaMath-LEAN-cleaned.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
💎 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.small-lean
Small Lean Alpaca
Thirty filtered Alpaca-style Lean 4 theorem-proving records derived from
internlm/Lean-Workbook.
Only train.jsonl is a Hub dataset split. The hf_dataset/ directory is a
local datasets.save_to_disk() artifact and must not be interpreted as JSON
training data.
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-quantfinance
Lean 4 Formalized Quantitative Finance & Game Theory
A domain-specific Lean 4 / Mathlib corpus centered on finance and market
mechanisms: 2,074 theorem records + 887 definitions, extracted from a
formalization pipeline and packaged for theorem-proving research (statement,
proof, tactics, premises, kernel-axiom status).
This is a mechanization of largely standard applied mathematics, not new
finance theory. Its value is breadth in under-formalized areas — market
microstructure… See the full description on the dataset page: https://huggingface.co/datasets/seancollins/lean-quantfinance.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.Lean4-PhysLean
Lean4-PhysLean
Structured dataset from PhysLean — Formalization of physics.
Source
Repository: https://github.com/HEPLean/PhysLean
Commit: 01143d7c9702318879b3c86bd9eadcdc60a13cc3
Files: 552
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 if the declaration has… See the full description on the dataset page: https://huggingface.co/datasets/phanerozoic/Lean4-PhysLean.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.lean-six-sigma-qna-360
Lean Six Sigma QnA Dataset
Dataset Description
This dataset contains 360 high-quality question-answer pairs focused on Lean Six Sigma methodologies, business process improvement, and operational optimization across multiple industries. The dataset is designed for fine-tuning instruction-following language models to provide expert-level consulting advice on Lean Six Sigma implementations across diverse business domains.
Dataset Structure
Data Fields… See the full description on the dataset page: https://huggingface.co/datasets/cw18/lean-six-sigma-qna-360.Lean4-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.