kfdong/STP_Lean download history

kfdong/STP_Lean is a text generation dataset on the Hugging Face Hub. In the last 30 days it was downloaded 122 times (12 in the last 7 days), and 3,029 times in total. It ranks #98,693 among datasets by monthly downloads.

This is the final training dataset of Self-play Theorem Prover as described in the paper STP: Self-play LLM Theorem Provers with Iterative Conjecturing and Proving. This dataset includes: Extracted examples from mathlib4, Generated correct proofs of statements in LeanWorkbook, Generated correct pro

Models trained on STP_Lean

1 models list it as training data.

Open kfdong/STP_Lean on Hugging Face

Sister project: Paper Pulse, the upvote history of every Hugging Face Daily Paper.