datasets
Training and evaluation data, with the modality, task and licence stated up front. Listed live from the Hugging Face Hub.
minif2f-lean4Fixing the errors in some formal statements and informal proofs of minif2f-lean4.
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.lean4oeis
LOEIS
Formalizing OEIS sequences in Lean 4 + Mathlib. See SPEC.md and OEIS.md
for the design, and AGENTS.md for current project status.
Setup
1. Clone this repository
git clone https://huggingface.co/datasets/formalica/lean4oeis
cd lean4oeis
This gives you the Lean sources and scripts only. The OEIS raw data and the metadata database
are fetched separately (next two steps) so that a plain clone stays small.
2. Install Lean
Install… See the full description on the dataset page: https://huggingface.co/datasets/formalica/lean4oeis.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.proofnet-lean4Lean4-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.miniF2F-test-lean4lean4-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.miniF2F-lean4proofnet-lean4proofnet-v3-lean4
ProofNet Lean4 v3
This dataset is based on proofnet-v2-lean4 but removes any entries
that caused Lean 4 syntax/parse errors. We also introduce a new field
header_no_import that removes "import Mathlib".
Splits: validation and test.
Enjoy!
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.leandojo-lean4-formal-informal-stringslean4-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.minif2f-lean4-normalizedlean4-docker-offline-imageuploaded a lean-mathlib docker image which can be used without network
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.proofnet-v2-lean4
ProofNet Lean4 v2
A Lean 4 version of the ProofNet dataset.We provide two splits: validation and test.
Adds a nl_statement field which is a cleaned version of the original informal_prefix.
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.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.PutnamBench-lean4minif2f-lean4
MiniF2F Lean4
This dataset provides two splits (validation and test) of the MiniF2F dataset adapted for Lean4.
It includes fields such as:
id
split
formal_statement
header
nl_statement
nl_proof
minif2f-lean4
MiniF2F Lean4
This dataset provides two splits (validation and test) of the MiniF2F dataset adapted for Lean4.
It includes fields such as:
id
split
formal_statement
header
nl_statement
nl_proof
rrma-lean4-agent-traces
RRMA Lean 4 Agent Traces
416 multi-agent Lean 4 proof search traces across two Erdős problems, three model tiers, and four difficulty rungs.
v2 (2026-06-10) — label + format correction. The original upload had two defects:
(1) messages was a JSON string, not an array; (2) reward was set to 1.0 if the
text SCORE=1.0 appeared anywhere in the conversation — including the worker prompt
("repeat until SCORE=1.0") and file reads of the oracle script, so almost every trace was
labeled… See the full description on the dataset page: https://huggingface.co/datasets/vincentoh/rrma-lean4-agent-traces.less-proofnet-lean4-top1Mproofnet-v3-lean4
ProofNet Lean4 v3
This dataset is based on proofnet-v2-lean4 but removes any entries
that caused Lean 4 syntax/parse errors. We also introduce a new field
header_no_import that removes "import Mathlib".
Splits: validation and test.
Enjoy!
erdos741ii-lean4-opus-traces
Erdős #741(ii) — Lean 4 Opus Agent Traces
39 Claude Opus agent sessions attempting Erdős problem #741(ii) in Lean 4 (G1 rung: build the proof from an NL construction description).
v2 (2026-06-10) — label correction. The original upload labeled all 39 traces
reward=1.0; the labeler matched the text SCORE=1.0 anywhere in the conversation,
including the worker prompt. Rewards are now anchored to genuine oracle output
(line-anchored SCORE= adjacent to… See the full description on the dataset page: https://huggingface.co/datasets/vincentoh/erdos741ii-lean4-opus-traces.Lean4-Changelog-QA
Lean 4 Changelog Q&A Dataset
Dataset Description
The Lean 4 Changelog Q&A Dataset is derived from the Lean4-Changelog. Each Lean 4 changelog entry (including version, section, pull request number, and description) is converted into a single Q&A pair. This allows for straightforward question-answering tasks reflecting the evolution of Lean 4 features, bug fixes, and language decisions over time.
Dataset Structure
Each record contains the following fields:… See the full description on the dataset page: https://huggingface.co/datasets/phanerozoic/Lean4-Changelog-QA.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.