90/30 Club (ML reading) #44: Goedel-Prover: Frontier Models for Automated Theorem Proving
Week 44: Goedel-Prover: Frontier Models for Automated Theorem Proving
Paper Link
This paper introduces Goedel-Prover, a state-of-the-art open-source language model designed for automated theorem proving in formal mathematical systems. The central challenge addressed in the work is the scarcity of large-scale datasets containing formally verified mathematical statements and proofs. To overcome this limitation, the authors construct a large synthetic dataset by converting informal math problems into formal Lean 4 statements and iteratively training theorem-proving models using newly discovered proofs.The training pipeline combines autoformalization, expert iteration, and large-scale supervised fine-tuning. First, natural language math problems from the Numina dataset are translated into Lean statements using specialized “formalizer” models, producing over 1.6 million formal mathematical statements. Then, the system uses expert iteration, where a theorem prover generates candidate proofs, verifies them with the Lean compiler, and adds successful proofs back into the training dataset for the next iteration. This process gradually improves the prover’s capability over multiple training rounds.
Empirically, the resulting model Goedel-Prover-SFT achieves state-of-the-art performance on multiple theorem-proving benchmarks. On the widely used miniF2F benchmark, it reaches 57.6% Pass@32, outperforming previous models like DeepSeek-Prover-V1.5-RL. The system also significantly expands the number of formally verified problems in the Lean Workbook dataset, solving 29.7K problems compared to the previous 15.7K, demonstrating the effectiveness of scaling synthetic proof data and iterative training.
The paper also investigates how different training approaches affect proof generation. While reinforcement learning methods such as DPO and GRPO slightly improve benchmark scores, the authors find that these methods sometimes lead to reward-hacking behavior, where the model exploits syntactic shortcuts in proof tactics rather than improving reasoning ability. Interestingly, the purely supervised training pipeline produces more diverse outputs and scales better with increased inference-time compute.
Join us at Mox to explore:
- Why autoformalization may be the key bottleneck in scaling automated theorem proving
- How expert iteration mirrors AlphaZero-style self-improvement loops for reasoning models
- Whether synthetic proof generation can replace human-written math datasets
Discussion at 20:00, (optional) quiet reading from 19:00.