datasets
Training and evaluation data, with the modality, task and licence stated up front. Listed live from the Hugging Face Hub.
proofwriter
Dataset Card for "proofwriter"
More Information needed
proofwriter_processed_OWANuminaMath-1.5-proofs-only-strict
NuminaMath-1.5-proofs-only-strict
A strictly filtered version of the NuminaMath-1.5-proofs-only dataset, containing ONLY
validated mathematical proof problems.
📊 Filtering Results
Original dataset: Numina1.5 -> filter for proofs -> 110,998 rows
Filters applied:
✓ Kept rows where answer = "proof" (proof problems only)
✓ Kept rows where solution_is_valid = "Yes"
✓ Kept rows where problem_is_valid = "Yes"
✓ Dropped validation columns after filtering
Filtered dataset:… See the full description on the dataset page: https://huggingface.co/datasets/nlile/NuminaMath-1.5-proofs-only-strict.proof-pile-2-fixed
The original EleutherAI/proof-pile-2 dataset uses a custom python script and .jsonl.zst files, which some versions of the datasets library struggle with.
This dataset contains the same data, subsets, and splits as EleutherAI/proof-pile-2, converted into standard parquet format.
Each subset and split was also shuffled so that you can directly train on the data without issue.
Conversion was performed using the following script:
import os
importzstandard as zstd
import json
import pandas as pd… See the full description on the dataset page: https://huggingface.co/datasets/aklein4/proof-pile-2-fixed.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-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.max-of-10-proofsolympiad-proof-problems
Olympiad-Proof-Problems
Dataset Description
This dataset contains mathematical problems and solutions from CSV data.
Dataset Summary
Total Examples: 39764
Format: Problem-solution pairs
Source: olympiad_proof_problems_clean.csv
Language: English
Domain: Mathematics
Data Fields
prompt: The mathematical problem statement
completion: The complete solution (including working steps)
source: Original source identifier
id: Unique identifier for each… See the full description on the dataset page: https://huggingface.co/datasets/TamasSimonds/olympiad-proof-problems.litcoin-proof-of-research
LITCOIN Proof-of-Research Corpus
191,484,662 AI research submissions, produced by 81,224 anonymous contributors and 470 model
variants competing against each other, every row executed in a sandbox and scored.
This is the complete output of the LITCOIN protocol, which ran on Base from March to August 2026.
Autonomous AI agents were paid in a permissionless token to solve real optimization problems across
32 domains. The protocol was discontinued on 20 August 2026. This dataset is… See the full description on the dataset page: https://huggingface.co/datasets/tekkaadan/litcoin-proof-of-research.proofwriter
Dataset Card for "proofwriter"
More Information needed
ProofNetSharp
ProofNet#
ProofNet# is a Lean 4 port of the ProofNet benchmark including fixes.
A comparison with previous Lean 4 ports can be found at:
https://proofnet4-fix.streamlit.app/.
This benchmark is compatible with all Lean versions between v4.7.0 and v4.16.0-rc2.
Original Dataset Summary
ProofNet is a benchmark for autoformalization and formal proving of undergraduate-level mathematics. The ProofNet benchmarks consists of 371 examples, each consisting of a formal theorem… See the full description on the dataset page: https://huggingface.co/datasets/PAug/ProofNetSharp.ProofRank-outputs
ProofRank: Evaluation Outputs
Companion artifact to the NeurIPS 2026 submission "Not All Proofs Are Equal: Evaluating LLM Proof Quality Beyond Correctness".
This dataset contains the complete LLM-judge outputs behind every number reported in the paper, so that all results can be recomputed without re-querying any model. It covers the ten evaluated models (GPT-5.4, Gemini-3.1-Pro, Gemini-3-Flash, GLM-5, DeepSeek-v3.2, Kimi-K2.5-Think, StepFun-3.5-Flash, Qwen3.5-397B… See the full description on the dataset page: https://huggingface.co/datasets/Anon987281293/ProofRank-outputs.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.proofwriter-source
ProofWriter (The Source)
An unmodified copy of AI2's ProofWriter dataset (release V2020.12.3), re-hosted as datasets
configs for convenient loading. The records are faithful to the upstream release — the id-keyed JSON
is preserved as-is; typing and reasoning-graph extraction happen in later stages.
Each config is a {world}-depth-{n} shelf of the synthetic core (OWA/CWA × depths
0/1/2/3/5), split train/dev/test (dev kept as the corpus names it).
Source:… See the full description on the dataset page: https://huggingface.co/datasets/arqa39/proofwriter-source.proofatlas-enriched
ProofAtlas Enriched Dataset v1
ProofAtlas Enriched combines theorem-disjoint Lean retrieval splits with LLM-generated theorem semantic and strategy enrichment. It is designed for premise-retrieval research, theorem-neighborhood retrieval, and qualitative retrieval-evidence analysis.
Source Data
This dataset is derived from erbacher/LeanRank-data, which is distributed under the Apache-2.0 license. The upstream LeanRank data was extracted from mathlib4 using… See the full description on the dataset page: https://huggingface.co/datasets/ZDCSlab/proofatlas-enriched.proofwriter-source
ProofWriter (The Source)
An unmodified copy of AI2's ProofWriter dataset (release V2020.12.3), re-hosted as datasets
configs for convenient loading. The records are faithful to the upstream release — the id-keyed JSON
is preserved as-is; typing and reasoning-graph extraction happen in later stages.
Each config is a {world}-depth-{n} shelf of the synthetic core (OWA/CWA × depths
0/1/2/3/5), split train/dev/test (dev kept as the corpus names it).
Source:… See the full description on the dataset page: https://huggingface.co/datasets/rlhf-and-friends/proofwriter-source.minif2f_proofnet_lean_workbook_deepseek_prover_solsminif2f_proofnet_deepseek_prover_solssmolmo-proofs-cot-sft
SmolMo Proofs CoT SFT
A supervised fine-tuning dataset for teaching small open language models to write and verify rigorous mathematical proofs with chain-of-thought reasoning. It pairs proof-generation data with verification data, so a model trained on it can both solve olympiad-style problems and grade candidate solutions — supporting solve-then-verify inference workflows.
~302K examples · ~6.1B tokens · ~124K unique problems. Every example is a chat conversation [system, user… See the full description on the dataset page: https://huggingface.co/datasets/chankhavu/smolmo-proofs-cot-sft.ProofNetVerif
ProofNetVerif
ProofNetVerif is a benchmark to evaluate both reference-based and reference-free metrics for statement autoformalization introduced in
Improving Autoformalization using Type Checking. This benchmark is compatible with Lean v4.8.0.
Tasks
Reference-based metric evaluation:
Input: lean4_formalization, lean4_prediction
Output: correct
Reference-free metric evaluation:
Input: nl_statement, lean4_prediction
Output: correct
Note: Developing an accurate… See the full description on the dataset page: https://huggingface.co/datasets/PAug/ProofNetVerif.coq-facts-props-proofs-gen0-v1
Dataset Name: Coq Facts, Propositions and Proofs
Dataset Description
The CoqFactsPropsProofs dataset aims to enhance Large Language Models'
(LLMs) proficiency in interpreting and generating Coq code by
providing a comprehensive collection of over 10,000 Coq source
files. It encompasses a wide array of propositions, proofs, and
definitions, enriched with metadata including source references and
licensing information. This dataset is designed to facilitate the… See the full description on the dataset page: https://huggingface.co/datasets/florath/coq-facts-props-proofs-gen0-v1.Herald_proofsThis is the proof part of the Herald dataset, which consists of 45k NL-FL proofs.
Lean version: leanprover--lean4---v4.11.0
Bibtex citation
@inproceedings{
gao2025herald,
title={Herald: A Natural Language Annotated Lean 4 Dataset},
author={Guoxiong Gao and Yutong Wang and Jiedong Jiang and Qi Gao and Zihan Qin and Tianyi Xu and Bin Dong},
booktitle={The Thirteenth International Conference on Learning Representations},
year={2025},
url={https://openreview.net/forum?id=Se6MgCtRhz}
}
Qwen3.5-9B-EquationalTheories-Proof-eval
Qwen3.5-9B on EquationalTheories-Proof: equational internalization evaluation
Model: the pinned base Qwen3.5-9B (no training)
Evaluation of Qwen/Qwen3.5-9B (revision c202236235762e1c871ad0ccb60c8ee5ba337b9a) on the equational internalization
protocol (recipe/equational_internalization/EVALUATION_PROTOCOL.md, environment
EquationalTheories-Proof): closed-book recall of implication/non-implication relationships between the
4,694 equations of the Equational Theories Project… See the full description on the dataset page: https://huggingface.co/datasets/violetxi/Qwen3.5-9B-EquationalTheories-Proof-eval.proofwriter
ProofWriter — structured
A cleaned, structured build of AI2's ProofWriter
for logical entailment with reasoning-graph supervision. Each row is one theory
(facts + Horn-clause rules) with the questions posed against it; the zip's formal string
reps are parsed into typed atoms (subject, relation, object, polarity), and every
question keeps its gold answer and gold derivation as a structured proof graph — so no
natural-language reverse-engineering is needed downstream.… See the full description on the dataset page: https://huggingface.co/datasets/rlhf-and-friends/proofwriter.ProofBench
ProofBench Dataset
ProofBench is a comprehensive benchmark dataset for evaluating AI models on mathematical proof generation and verification. The dataset contains competition-level mathematics problems from prestigious international competitions, along with both AI-generated and reference solutions, expert ratings, and detailed marking schemes.
Dataset Overview
Total Problems: 435
Competitions: PUTNAM, IMO, USAMO, EGMO, APMO, TST
Years Covered: 2022-2025
AI Models:… See the full description on the dataset page: https://huggingface.co/datasets/wenjiema02/ProofBench.Qwen3.5-9B-eq70-1m-EquationalTheories-Proof-eval
Qwen3.5-9B-eq70-1m on EquationalTheories-Proof: equational internalization evaluation
Model: Qwen3.5-9B full SFT (LR 5e-6, two epochs) on 1M loss tokens: 70% WithProof notes (0.70M) + 30% note-conditioned teacher trajectories (0.30M), held-out-first split relationships-v2/ladder v2
Evaluation of Qwen3.5-9B-eq70-1m (revision 1545499d4db014a012dedc6a7b853779ca21d93e) on the equational internalization
protocol (recipe/equational_internalization/EVALUATION_PROTOCOL.md, environment… See the full description on the dataset page: https://huggingface.co/datasets/violetxi/Qwen3.5-9B-eq70-1m-EquationalTheories-Proof-eval.max-of-4-proofsQwen3.5-9B-eq70-3m-EquationalTheories-Proof-eval
Qwen3.5-9B-eq70-3m on EquationalTheories-Proof: equational internalization evaluation
Model: Qwen3.5-9B full SFT on 3M loss tokens: 70% notes (2.10M) + 30% trajectories (0.90M)
Evaluation of Qwen3.5-9B-eq70-3m (revision 14fd1fe253524178b6cdfc819ea8d39c4648d496) on the equational internalization
protocol (recipe/equational_internalization/EVALUATION_PROTOCOL.md, environment
EquationalTheories-Proof): closed-book recall of implication/non-implication relationships between the
4… See the full description on the dataset page: https://huggingface.co/datasets/violetxi/Qwen3.5-9B-eq70-3m-EquationalTheories-Proof-eval.Qwen3.5-9B-eq70-10m-pc10-EquationalTheories-Proof-eval
Qwen3.5-9B-eq70-10m-pc10 on EquationalTheories-Proof: equational internalization evaluation
Model: Qwen3.5-9B full SFT on the 10M 70/30 mixture plus the 304 study proof chats repeated 10 times (0.62M loss tokens, 5.8%)
Evaluation of Qwen3.5-9B-eq70-10m-pc10 (revision 939e9ffc74c5dfaa08f770fa0c91dbbc1b5b0add) on the equational internalization
protocol (recipe/equational_internalization/EVALUATION_PROTOCOL.md, environment
EquationalTheories-Proof): closed-book recall of… See the full description on the dataset page: https://huggingface.co/datasets/violetxi/Qwen3.5-9B-eq70-10m-pc10-EquationalTheories-Proof-eval.proofwriter-mirror
ProofWriter (The Mirror)
A typed, content-faithful mirror of AI2's ProofWriter dataset (release V2020.12.3),
derived from proofwriter-source. The JSON encoding is cleaned up: the id-keyed dicts
(triple1, Q3, …) become lists of structs that keep their id, every atom representation
is parsed into a typed {subject, relation, object, polarity} triple, and the closed enums
(answer, strategy) are typed. The content stays faithful — nothing renamed, no rows
dropped — and the recursive… See the full description on the dataset page: https://huggingface.co/datasets/rlhf-and-friends/proofwriter-mirror.