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.lean-eval-source
Lean Eval Humanize Source
A reproducible snapshot of 226 self-contained Lean Eval workspaces attempted with
the Humanize workflow. Each workspace contains the trusted problem files, the best
available Humanize submission snapshot, and any submission helper modules.
The snapshot contains 152 comparator-accepted submissions and 74 unaccepted or
unverified attempts. An included attempt is not an assertion that its proof is
valid.
[!WARNING]
Every workspace ships a Solution.lean… See the full description on the dataset page: https://huggingface.co/datasets/humanfia-lab/lean-eval-source.Lean-Workbook
Lean Workbook
This dataset is about contest-level math problems formalized in Lean 4.
Our dataset contains 57231 problems in the split of Lean Workbook and 82893 problems in the split of Lean Workbook Plus. We provide the natural language statement, answer, formal statement, and formal proof (if available) for each problem. These data can support autoformalization model training and searching for proofs.
We open-source our code and our data.
Our test environment is based on Lean… See the full description on the dataset page: https://huggingface.co/datasets/internlm/Lean-Workbook.NuminaMath-LEAN
Dataset Card for NuminaMath-LEAN
Dataset Summary
NuminaMath-LEAN is a large-scale dataset of 100K mathematical competition problems formalized in Lean 4. It is derived from a challenging subset of the NuminaMath 1.5 dataset, focusing on problems from prestigious competitions like the IMO and USAMO. It represents the largest collection of human-annotated formal statements and proofs designed for training and evaluating automated theorem provers. This is also the dataset… See the full description on the dataset page: https://huggingface.co/datasets/AI-MO/NuminaMath-LEAN.political-leaning-tweets-100k
🗳️ political-leaning-tweets-100k
Châtelet AI presents a 100,000+ dataset of tweets labelled for political leaning: neutral, liberal, conservative.Labels are machine-generated using a SOTA thinking-enabled LLM. The dataset is intended for research on political language modelling, ideology detection, robustness, and safety evaluation.
📦 Dataset Card
Name: chatelet/political-leaning-tweets-100k
Publisher: Châtelet AI
Licence: MIT with additional restrctions against… See the full description on the dataset page: https://huggingface.co/datasets/chatelet/political-leaning-tweets-100k.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-lean4Fixing the errors in some formal statements and informal proofs of minif2f-lean4.
lean-proofs-v1
Part of the SZL Holdings governed estate — claims are designed to carry checkable receipts. Verification proves integrity & origin, never accuracy or performance.
SZLHOLDINGS/lean-proofs-v1
The complete Lean 4 theorem library for the SZL Holdings Ouroboros Invariant research programme.
Doctrine v10/v11 Canonical Numbers
Metric
Value
Declarations
749
Unique axioms
14 (15 raw, 1 dup)
Sorries
163 (112 baseline + 51 Putnam)… See the full description on the dataset page: https://huggingface.co/datasets/SZLHOLDINGS/lean-proofs-v1.Lean-workbook-proofsThis is the 29.7 solutions of Lean-workbook found by Goedel-Prover-SFT.
Citation
@misc{lin2025goedelproverfrontiermodelopensource,
title={Goedel-Prover: A Frontier Model for Open-Source Automated Theorem Proving},
author={Yong Lin and Shange Tang and Bohan Lyu and Jiayun Wu and Hongzhou Lin and Kaiyu Yang and Jia Li and Mengzhou Xia and Danqi Chen and Sanjeev Arora and Chi Jin},
year={2025},
eprint={2502.07640},
archivePrefix={arXiv}… See the full description on the dataset page: https://huggingface.co/datasets/Goedel-LM/Lean-workbook-proofs.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.GUEThis is a copy of the Genome Understanding Evaluation (GUE) that was presented in
DNABERT-2: Efficient Foundation Model and Benchmark For Multi-Species Genome
Zhihan Zhou and Yanrong Ji and Weijian Li and Pratik Dutta and Ramana Davuluri and Han Liu
and is available to download directly from
https://github.com/MAGICS-LAB/DNABERT_2
If you use this dataset, please cite
@misc{zhou2023dnabert2,
title={DNABERT-2: Efficient Foundation Model and Benchmark For Multi-Species Genome}… See the full description on the dataset page: https://huggingface.co/datasets/leannmlindsey/GUE.lean-rag-indexes
Lean RAG Indexes for BioASQ
Paper: Retrieval-Bound Generation: Lean RAG Pipelines for Biomedical QA — CLEF 2026 Working Notes, BioASQ Task 14b
Code: github.com/lasigeBioTM/BioASQ14Taskb_2026
Prebuilt retrieval indexes for the Lean RAG Pipelines for Biomedical Question Answering project, developed as part of an MSc dissertation at LASIGE, University of Lisbon (in preparation).
These indexes support a hybrid (BM25 + dense retrieval) pipeline evaluated on BioASQ Task 14b.… See the full description on the dataset page: https://huggingface.co/datasets/dantunes6/lean-rag-indexes.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-theorem-tree
Part of the SZL Holdings governed estate — claims are designed to carry checkable receipts. Verification proves integrity & origin, never accuracy or performance.
Lean Theorem Tree — Declaration Manifest Snapshot (269 @ c4d13795)
Doctrine v11 LOCKED. No marketing. Every number resolves to a CI log, a Lean proof, or a Zenodo DOI.
Dependency-graph SNAPSHOT of the Lean 4 declarations in the Ouroboros corpus as of commit c4d13795 (2026-05-29, Lean… See the full description on the dataset page: https://huggingface.co/datasets/SZLHOLDINGS/lean-theorem-tree.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.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.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.jevbench
JevBench
Cases and predictions for JevBench: An Open Evaluation Framework for Typed
Decision Models. The evaluation code is on GitHub: https://github.com/Leanmcp/jevbench JevBench evaluates models that return typed decisions
(a yes/no probability, a distribution over a set of choices, or an expected
level on an ordered rubric) on identical inputs built from public datasets.
Contents
Path
What it holds
cases/
One JSONL file per slice. Each row is the… See the full description on the dataset page: https://huggingface.co/datasets/Leanmcp/jevbench.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.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.LeanWorkbooklean_solutionnl-lean-demo-data
NL-Lean CSN-v2 demo: data bundle
The data needed to run the interactive demo of
padieul/nl-lean (DEMO_README.md) outside the
machine it was built on. Do not download files by hand; the fetch script picks the files,
places them and checks every sha256:
python scripts/demo/fetch_data.py snapshot # recorded answers only, no GPU
python scripts/demo/fetch_data.py full # everything for the live demo
tier
files
size
snapshot
843
24.0 MB
data
123
1.4 GB
index
33… See the full description on the dataset page: https://huggingface.co/datasets/padieul/nl-lean-demo-data.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.lean-math-formal-corpus
Lean Math Formal Corpus
This dataset is a unified, compile-validated collection of Lean mathematical problems/proofs aggregated from multiple public sources.
Configs and Lean versions
Different configs correspond to different Lean adaptation versions.
Available configs:
v4.27.0 -> Lean toolchain target leanprover/lean4:v4.27.0 (primary supported version)
v4.15.0 -> Lean toolchain target leanprover/lean4:v4.15.0
v4.9.0 -> Lean toolchain target leanprover/lean4:v4.9.0… See the full description on the dataset page: https://huggingface.co/datasets/iiis-lean/lean-math-formal-corpus.algoveri-lean
AlgoVeri-Lean
77 classical algorithm verification tasks in Lean 4
What is this?
This is the Lean 4 subset of the AlgoVeri benchmark — a cross-language benchmark for vericoding (generating formally verified code from specifications).
Each task provides a Lean 4 specification that includes:
Preconditions — constraints on valid inputs
Function signature — with a sorry'd implementation to be filled in
Postconditions — formal properties the implementation must… See the full description on the dataset page: https://huggingface.co/datasets/lizn-zn/algoveri-lean.leann-rag-evaluation-data
LEANN-RAG Evaluation Data
This repository contains the necessary data to run the recall evaluation scripts for the LEANN-RAG project.
Dataset Components
This dataset is structured into three main parts:
Pre-built LEANN Indices:
dpr/: A pre-built index for the DPR dataset.
rpj_wiki/: A pre-built index for the RPJ-Wiki dataset.
These indices were created using the leann-core library and are required by the LeannSearcher.
Ground Truth Data:
ground_truth/: Contains the… See the full description on the dataset page: https://huggingface.co/datasets/LEANN-RAG/leann-rag-evaluation-data.LEANDRONE_V1Repository: https://huggingface.co/datasets/Leandro4002/LEANDRONE_V1Download zip: https://public.saraivam.ch/static/LEANDRONE_V1.zipProject using this dataset: https://gitlab.com/Leandro4002/drone-follow-line
Description
The LEANDRONE_V1 dataset is a collection of 500 labelled images triying to mimic the photo taken by the front camera of a Bitcraze AI deck 1.1 mounted on a Crazyflie 2.1 nanodrone.
The camera model is a Himax HM01B0 monochrome with dimension 320×320.
This dataset is… See the full description on the dataset page: https://huggingface.co/datasets/Leandro4002/LEANDRONE_V1.leandojohttps://github.com/lean-dojo/LeanDojo
@article{yang2023leandojo,
title={{LeanDojo}: Theorem Proving with Retrieval-Augmented Language Models},
author={Yang, Kaiyu and Swope, Aidan and Gu, Alex and Chalamala, Rahul and Song, Peiyang and Yu, Shixing and Godil, Saad and Prenger, Ryan and Anandkumar, Anima},
journal={arXiv preprint arXiv:2306.15626},
year={2023}
}