Goedel-Prover: A Frontier Model for Open-Source Automated Theorem Proving

How do we accurately autoformalize natural language mathematics? How can we achieve a state-of-the-art model for theorem proving?

Goedel-Prover introduces an open-source large language model designed for formal mathematical theorem proving in Lean 4. The paper directly tackles the primary bottleneck in automated reasoning—the scarcity of formalized mathematical data—by creating a massive synthetic dataset. The authors first used LLMs to translate over 1.6 million natural language math problems into formal Lean 4 statements, applying automated filtering to verify both syntax correctness and translation accuracy. They then ran an iterative self-improvement loop (“expert iteration”), where successive model versions generated proofs for previously unsolved problems, accumulating over 800,000 machine-verified formal proofs.

Trained on this synthesized dataset, Goedel-Prover achieved state-of-the-art performance among open-source models, outperforming prior leaders like DeepSeek-Prover-V1.5 on the miniF2F benchmark and ranking first on PutnamBench for university-level competition math. The most notable aspect of the work is its commitment to open science: the authors fully open-sourced the model checkpoints, code, and formal datasets (including nearly 30,000 new verified proofs for Lean Workbook problems), providing a strong open-weights foundation for AI-assisted mathematics.

Join us at CASI for discussion at 8 pm, and (optional) quiet reading from 7 pm.