datasets
Training and evaluation data, with the modality, task and licence stated up front. Listed live from the Hugging Face Hub.
proofnetA dataset that evaluates formally proving and autoformalizing undergraduate mathematics.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.minif2f_proofnet_lean_workbook_deepseek_prover_solsminif2f_proofnet_deepseek_prover_solsProofNetVerif
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.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!
proofnet-lean4ProofNet-Verified
ProofNet-Verified
Resource Links:
Paper: https://openreview.net/forum?id=5c0RSYyIWW, https://openreview.net/forum?id=NjgaeXNit3
GitHub: https://github.com/marcusm117/ProofNet-Verified
HuggingFace: https://huggingface.co/datasets/marcusm117/ProofNet-Verified
Visualization: https://marcusm117.github.io/ProofNet-Verified/
ProofNet-Verified (ProofNet-V) is an audited, corrected, and verified version of the ProofNet dataset that is upgraded to be compatible with Lean v4.28.0. A… See the full description on the dataset page: https://huggingface.co/datasets/marcusm117/ProofNet-Verified.less-proofnet-lean4-top1Mawakening-proofnet-runs
Awakening — ProofNet tool-use inference runs
ProofNet (186 Lean 4 problems) inference outputs for the COLM 2026 paper
"Awakening: minimal agentic replay recovers tool use in formal-math fine-tuned LLMs".
These are the runs behind the ProofNet columns of Table 2 (tab:proofnet_main) —
Goedel-Prover-V2-32B before and after post-hoc SFT on 100 / 1K / 18K Lean agentic
traces, sampled 32× per problem with the LeanSearch retrieval tool available.
Companion release: awakening (training… See the full description on the dataset page: https://huggingface.co/datasets/juihuichung/awakening-proofnet-runs.ProofnetTargetSetproofnet_leanproofnet-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.
train_proofnet_Qwen3-1.7B_samplingproofnet-satp-v4.27
ProofNet#-SATP v4.27 — Lean 4 (371 problems)
ProofNet# (corrected reference
formalizations of ProofNet) normalized to the ChristianZ97/putnambench-satp-v4.27
schema for the SATP-DSP-Eval pipeline.
Provenance
Source: PAug/ProofNetSharp
@ a8da405fbd1e348a87445c2e562c747b7e26dc8f (MIT), 371 rows = 185 valid + 186 test.
Introduced in Reliable Evaluation and Benchmarks for Statement Autoformalization
(Poiroux, Weiss, Kunčak, Bosselut; EMNLP 2025 main;… See the full description on the dataset page: https://huggingface.co/datasets/ChristianZ97/proofnet-satp-v4.27.train_proofnet_Qwen3-1.7Btest_proofnet_with_gsm8k_promptDSP1.5RL-proofnet-sampling_16less-proofnet-lean4-rankedproofnet-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!
proofnet-satp
ProofNet-SATP — Lean 4 (371 problems, SATP-normalized)
ProofNet (undergraduate-level mathematics theorem-proving benchmark, 371
problems from Rudin / Munkres / Dummit-Foote / Axler / Herstein /
Ireland-Rosen / Artin) normalized for the SATP-DSP-Eval pipeline.
Upstream: deepseek-ai/DeepSeek-Prover-V1.5
datasets/proofnet.jsonl — the Lean 4 port of
hoskinson-center/proofnet
shipped with DeepSeek-Prover V1.5.
Differences from upstream
Field
Upstream
This repo… See the full description on the dataset page: https://huggingface.co/datasets/ChristianZ97/proofnet-satp.test_proofnet_Qwen3-8B_naturaltest_Proofnettrain_proofnet_Qwen2.5-Math-1.5Btest_gsm8k_with_proofnet_prompttrain_proofnet_Qwen2.5-Math-7Btest_proofnet_large_Qwen3-8B_8_shard_2test_proofnet_Qwen3-1.7Btest_proofnet_large_Qwen3-8B_8_shard_6