datasets
Training and evaluation data, with the modality, task and licence stated up front. Listed live from the Hugging Face Hub.
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!
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_16proofnet-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_6test_proofnet_Apertustest_proofnettest_proofnet_large_Qwen3-8B_8_shard_5test_proofnet_Qwen3-8Btrain_proofnet_Qwen3-8B_samplingtest_proofnet_large_Qwen3-8B