Pythagoras-LM/Pythagoras-Prover-4B
Pythagoras-Prover-4B is a 4 billion parameter autoregressive language model developed by Pythagoras-LM, specifically designed for formal theorem proving in Lean 4. It is part of a compute-efficient family of provers, distinguished by its scalable, Lean-verified synthetic data pipeline utilizing Augmented Lean Formalisation (ALF). This model excels at formal mathematics, achieving 86.07% on MiniF2F-Test at Pass@32, outperforming significantly larger models without inference-time self-correction.
Loading preview...
Pythagoras-Prover-4B: Efficient Lean 4 Theorem Proving
Pythagoras-Prover-4B is a 4 billion parameter autoregressive language model from Pythagoras-LM, optimized for formal theorem proving in Lean 4. It stands out for its compute efficiency and a novel Lean-verified synthetic data pipeline that leverages Augmented Lean Formalisation (ALF).
Key Capabilities & Innovations
- Augmented Lean Formalisation (ALF): A structured mutation scheme that expands a verified seed corpus into approximately 2 million formal variants, enabling robust self-distillation during training without per-instance Lean compilation.
- Compute-Efficient Performance: Achieves 86.07% on MiniF2F-Test at Pass@32, surpassing DeepSeek-Prover-V2-671B despite being roughly 167 times smaller, and does so without relying on inference-time self-correction or test-time reinforcement learning.
- Specialized Training: Utilizes LoRA-only supervised fine-tuning of Qwen3-4B under an 8K context, combined with a dynamic proof-reasoning filter, a difficulty-ordered curriculum, and reinforcement learning with a Lean-compilation reward.
- New Benchmark: Introduces MiniF2F-ALF, a companion benchmark designed to challenge provers with ALF-mutated problems.
Why Pythagoras-Prover-4B is Different
This model distinguishes itself by demonstrating that careful data construction can significantly close the performance gap between smaller open provers and much larger counterparts. Its unique synthetic data generation and training methodology allow it to achieve high performance in formal theorem proving with a remarkably small parameter count, making it one of the most efficient open-source Lean theorem provers available.