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.
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.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.miniF2F-lean4minif2f-lean4-normalizedlean4-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-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.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.proofnet-lean4lean4-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.miniF2F-test-lean4lean4oeis
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.proofnet-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!
less-proofnet-lean4-top1Mleandojo-lean4-formal-informal-stringslean4
💎 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.leandojo_benchmark_lean4_17_0minif2f-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
lean4-docker-offline-imageuploaded a lean-mathlib docker image which can be used without network
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.lean4-cot-3kLean4-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.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.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
Lean4-Batteries
Lean4-Batteries
Structured dataset from Lean 4 Batteries - the community standard library extensions.
Source
Repository: https://github.com/leanprover-community/batteries
Commit: 41680f5d84023c7406c841d08ef83bf15a9782a6
Files: 187
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-Batteries.Lean4-Aesop
Lean4-Aesop
Structured dataset from Aesop — White-box proof search automation.
Source
Repository: https://github.com/leanprover-community/aesop
Commit: fafca80479ff95e041d84373dda7122adf1295f2
Files: 250
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… See the full description on the dataset page: https://huggingface.co/datasets/phanerozoic/Lean4-Aesop.