Datasetpublic

ChristianZ97/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.

sourceHugging Facemitupdated 4mo agoView on Hugging Face

0likes15downloads

Dataset Card

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
`formal_statement`	bare theorem	`import Mathlib\n\n<theorem>` (header baked in)
`uuid`	absent	`sha256(canonical(formal_statement))[:16]` after baking
`split`	`valid` / `test`	`validation` / `test` (matches minif2f-satp naming)
`goal_state`	shipped as `goal`	renamed; value byte-identical

Dropped: informal_prefix (the /-- ... -/ English statement). Mirrors ChristianZ97/minif2f-satp which drops informal* fields. The SATP eval pipeline reads only `formalstatement`.

Dropped from baked header: the per-row open / open scoped / set_option directives. Only import Mathlib is baked in. Same pattern as minif2f-satp. Consumer scripts strip the import preamble then layer their own canonical opens.

Schema

Field	Type	Description
`name`	`str`	Stable identifier, upstream verbatim (e.g. `exercise_1_13a`)
`uuid`	`str`	`sha256(canonical(formal_statement))[:16]`
`split`	`str`	`"validation"` (185 rows) or `"test"` (186 rows)
`formal_statement`	`str`	`import Mathlib\n\n<theorem>`, ends in `:= by`
`goal_state`	`str`	Initial proof goal, byte-identical to DSP V1.5

Citation

bibtex

@inproceedings{azerbayev2023proofnet,
  title={ProofNet: Autoformalizing and Formally Proving
         Undergraduate-Level Mathematics},
  author={Zhangir Azerbayev and Bartosz Piotrowski and Hailey Schoelkopf
          and Edward W. Ayers and Dragomir Radev and Jeremy Avigad},
  booktitle={Proceedings of the 12th International Conference on Learning
             Representations (ICLR)},
  year={2024}
}