Pythagoras-LM/Pythagoras-Prover-32B
Pythagoras-Prover-32B is a 32 billion parameter autoregressive language model developed by Pythagoras-LM, specifically designed for formal theorem proving in Lean 4. It leverages a unique Lean-verified synthetic data pipeline and Augmented Lean Formalisation (ALF) to achieve compute-efficient performance. This model excels at solving mathematical theorems, setting new benchmarks for open-source provers without relying on inference-time self-correction.
Loading preview...
Pythagoras-Prover-32B: Efficient Lean 4 Theorem Proving
Pythagoras-Prover-32B is a 32 billion parameter autoregressive language model from Pythagoras-LM, optimized for formal theorem proving in Lean 4. It is part of a family of models developed using a novel, scalable, Lean-verified synthetic data pipeline, which includes Augmented Lean Formalisation (ALF). ALF expands a verified seed corpus into approximately 2 million formal variants, allowing for robust training without extensive manual verification.
Key Capabilities & Innovations
- State-of-the-Art Performance: Achieves 93.03% on MiniF2F-Test and solves 93 problems on PutnamBench, outperforming larger open-source provers without self-correction or test-time reinforcement learning.
- Compute-Efficient: Designed to close the performance gap between smaller open provers and their larger counterparts through careful data construction rather than raw scale.
- Advanced Training Methodology: Utilizes LoRA-only supervised fine-tuning of Qwen3-32B under an 8K context, combined with a dynamic proof-reasoning filter, a difficulty-ordered curriculum, and reinforcement learning with a Lean-compilation reward.
- Synthetic Data Generation: Employs a structured mutation scheme (ALF) for simplification, generalization, lemma proposal, proof-step decomposition, and reformulation, significantly expanding the training data.
Should I use this for my use case?
- Formal Theorem Proving in Lean 4: This model is specifically engineered for generating and verifying proofs within the Lean 4 theorem prover environment.
- Research in Automated Reasoning: Ideal for researchers exploring compute-efficient methods, synthetic data generation, and advanced training techniques for theorem proving.
- Benchmarking: Useful for evaluating and comparing the performance of theorem provers, especially with the introduction of the MiniF2F-ALF benchmark.