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

The Pythagoras-Prover family of Lean theorem provers has been introduced, featuring autoregressive models with 4B and 32B parameters, alongside a proof-of-concept diffusion-based prover at 4B. The models utilize a Lean-verified corpus for curriculum supervised fine-tuning and employ Augmented Lean Formalisation (ALF) to enhance training efficiency by generating variants of formal statements. Notably, the 32B model achieves a new state-of-the-art accuracy of 93.0% on the MiniF2F-Test benchmark, demonstrating significant performance improvements over larger models with fewer parameters, which is crucial for practitioners aiming to optimize formal proof systems under constrained compute budgets.