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-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.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.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.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.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.minif2f-lean4Fixing the errors in some formal statements and informal proofs of minif2f-lean4.
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.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.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.LeanWorkbookleandojohttps://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}
}
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.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.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.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.Lean-GithubWe release Lean-Github and InternLM2-Step-Prover with 29K theorems compiled from 100+ Lean 4 repos and a 7B models fine-tuned on Lean-Github and Lean-Workbook with SOTA performance on MiniF2F-test (54.5%), ProofNet (18.1%), and Putnam (5 problems).
🤗Dataset 🤗Model 📑 Paper 📖 README
Citation and Tech Report
@misc{wu2024leangithubcompilinggithublean,
title={LEAN-GitHub: Compiling GitHub LEAN repositories for a versatile LEAN prover},
author={Zijian Wu and Jiayu… See the full description on the dataset page: https://huggingface.co/datasets/internlm/Lean-Github.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-buffer-pairs-Temp
NuminaMath-LEAN-satp-buffer-pairs-Temp
Staging snapshot of (theorem, succ_config, fail_config) pairs mined from
the local expert_dspaug_*/{successes,failures}_shard_*.jsonl runs of
workspace/scripts/run_dspaug_minimal_chain.sh over the
ChristianZ97/NuminaMath-LEAN-satp train split.
Schema is byte-identical to the main NuminaMath-LEAN-satp-buffer so
rows can be appended directly. See that repo's README for full column
documentation, head layout, and per-row classification semantics.… See the full description on the dataset page: https://huggingface.co/datasets/ChristianZ97/NuminaMath-LEAN-satp-buffer-pairs-Temp.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.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.miniF2F-lean4JurisTCU
JurisTCU: A Brazilian Portuguese Information Retrieval Dataset with Query Relevance Judgments
Overview
JurisTCU is a dataset for Legal Information Retrieval (LIR) in Brazilian Portuguese. It consists of jurisprudence from the Brazilian Federal Court of Accounts (Tribunal de Contas da União – TCU) and provides query relevance judgments (qrels) to support the evaluation and improvement of legal search systems.
The dataset includes:
16,045 legal documents from the… See the full description on the dataset page: https://huggingface.co/datasets/LeandroRibeiro/JurisTCU.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.lean-dojo-mathlib4
Dataset Card for "lean-dojo-mathlib4"
More Information needed
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.
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.NormasTCU
NormasTCU
Overview
NormasTCU iis a dataset for Legal Information Retrieval (LIR) in Brazilian Portuguese composed of normative documents from the Brazilian Federal Court of Accounts (Tribunal de Contas da União - TCU), along with queries and human-annotated relevance judgments.
The dataset includes:
14,469 legal documents (normative acts);
46 queries;
812 judge query-document pairs derived from 3,048 human annotations with 3-level graded relevance.… See the full description on the dataset page: https://huggingface.co/datasets/LeandroRibeiro/NormasTCU.