Pythagoras-Prover: Advancing Efficient Formal Proving via Augmented Lean Formalisation

LLM-based theorem provers have achieved strong performance on various benchmarks, but still require substantial training and inference compute due to scarce verified proof data and generating long reasoning traces. We introduce Pythagoras-Prover, a compute-efficient, open-source family of Lean theorem provers comprising 4B and 32B autoregressive models and a first diffusion-based proof of concept that iteratively refines proofs at inference time. To improve training efficiency, we apply curriculum supervised fine-tuning to a Lean-verified corpus stratified into easy, medium, and hard problems, progressing from simpler proofs to harder ones. Dynamic proof-reasoning filtering further preserves informative traces within an 8K-token context budget. We then introduce Augmented Lean Formalisation (ALF), which generates structured variants of verified statements and populates them through self-distillation, providing additional training signal without requiring every variant to be formally verified and reducing reliance on statement surface forms. Pythagoras-Prover-4B surpasses DeepSeek-Prover-V2-671B at pass@32 on MiniF2F-Test (86.1% versus 82.4%) with roughly 167× fewer parameters. Pythagoras-Prover-32B achieves state-of-the-art performance among open-source neural theorem provers, reaching 93.0% on MiniF2F-Test and solving 93 of 672 PutnamBench problems. We also release MiniF2F-ALF, a contamination-sensitive benchmark of ALF-generated perturbations. Together, these results demonstrate that strong Lean theorem proving is achievable under practical compute budgets without relying exclusively on frontier-scale models.