Pythagoras-LM/SFT_Dataset
Pythagoras SFT Dataset Project Page | GitHub | Paper Data Our training dataset consists of approximately 841K problems paired with Lean formal statements, formal proofs, and reasoning chains. We release a partial subset, which consists of 126K instances: 30K easy instances 49K medium instances 47K hard instances Complete data will be released soon. The complete explanation of the synthetic data generation pipeline can be found in Pythagoras-Prover: Advancing… See the full description on the dataset page: https://huggingface.co/datasets/Pythagoras-LM/SFT_Dataset.
| Author / organization | Pythagoras-LM |
|---|---|
| License (as declared) | apache-2.0 |
| Downloads | 130 (as reported by Hugging Face) |
| Likes | 9 |
| Created | 13 June 2026 |
| Last updated at source | 22 June 2026 |
Popularity, last 2 days
130 now (-1 since 2026-10-16). Counts as reported by the source, snapshotted daily by Silytics.
Connected in the knowledge graph
- mradermacher/Pythagoras-Prover-32B-GGUFModel · used to train
- Pythagoras-LM/Pythagoras-Prover-4BModel · used to train
- Pythagoras-Prover: Advancing Efficient Formal Proving via Augmented Lean FormalisationPaper · cites
Related papers
More from Pythagoras-LM
Silytics shows public metadata from Hugging Face and links to the original. Information may be incomplete or out of date. Last refreshed 17 October 2026. Licenses and terms of the original apply to the work itself. Not financial, legal or professional advice.