Pythagoras SFT Dataset: Formal Proofs and Reasoning Chains for Automated Theorem Proving

A dataset of approximately 126,000 problems paired with Lean formal statements, formal proofs, and reasoning chains, released by Pythagoras-LM. It consists of 30,000 easy, 49,000 medium, and 47,000 hard instances, with a full set of 841,000 problems planned for future release. The data was last updated on June 13, 2026.

Use Cases

• Fine-tuning language models for formal theorem proving based on Lean formal statements.
• Training models to generate step-by-step reasoning chains based on the provided problem-proof pairs.
• Benchmarking the difficulty of automated theorem proving tasks based on the easy, medium, and hard instance labels.
• Developing synthetic data generation pipelines for mathematical reasoning, as referenced in the linked research paper.

Strengths

• Contains 126,000 instances with formal proofs and reasoning chains.
• Problems are categorized by difficulty into 30,000 easy, 49,000 medium, and 47,000 hard instances.
• The full dataset pipeline is documented in an associated research paper, 'Pythagoras-Prover: Advancing Efficient Formal Proving via…'.

Limitations

• Column-level documentation is absent; field semantics must be inferred after download.
• Row count for the full dataset is unknown, which may limit suitability assessment.
• The released data is described as a partial subset, with the complete data pending future release.

Provenance

Source

Pythagoras-LM

Collection Method

Synthetic data generation pipeline, as described in the 'Pythagoras-Prover' paper.

Freshness

Last updated 2026-06-13 14:27:59; freshness should be verified.