Goedel Prover V2: The Strongest Open Source Theorem Prover to Date 1. Introduction We introduce Goedel Prover V2, an open source language model series that sets a new state of the art in automated formal proof generation. Built on the standard expert iteration and reinforcement learning pipeline, our approach incorporates three key innovations: (1) Scaffolded data synthesis : We generate synthetic proof tasks of increasing difficulty to progressively train the model, enabling it to master increasingly complex theorems; (2) Verifier guided self correction : The model learns to iteratively revise its own proofs by leveraging feedback from Lean’s compiler, closely mimicking how humans refine their work; (3) Model averaging : We combine multiple model checkpoints to improve robustness and overall performance. Our small model, Goedel Prover V2 8B, reaches 83.0% on MiniF2F test set at Pass@32, matching the performance of prior state of the art DeepSeek Prover V2 671B while being nearly 100 times smaller in model size. Our flagship model, Goedel Prover V2 32B, achieves 88.0% on MiniF2F at Pass@32 on standard mode and 90.4% on self correction mode, outperforming prior SOTA DeepSeek Prover…
We use cookies for essential functionality and analytics. You can accept or reject analytics cookies.Cookie policy