Datasetpublic

UDACA/proofnet-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!

sourceHugging Faceupdated 2y agoView on Hugging Face

1likes68downloads

Dataset Card

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!