Goedel-Prover-V2

Goedel-Prover-V2 (paper: August 2025, arXiv 2508.03613) is the open-source state-of-the-art in Lean 4 automated theorem proving, from researchers at Princeton, Shanghai Jiao Tong, and Peking universities. Three innovations drive it: scaffolded synthetic-data synthesis (autoformalizing 1.64M statements), verifier-guided self-correction (feeding Lean compiler errors back for iterative repair), and checkpoint model averaging.

The results are striking: the 8B model matches DeepSeek-Prover-V2-671B on MiniF2F at ~100x smaller size, and the 32B flagship hits 90.4% MiniF2F (self-correction mode) and topped the open PutnamBench leaderboard — the efficiency story of 2025 in formal math. Code, weights, and data are open.

Honest limits: Lean 4 only; whole-proof generation can still fail on hard competition problems where search-based provers grind longer; the GitHub repo has been flagged as missing a LICENSE file — verify licensing before commercial use despite the Apache-2.0 claim; closed systems (ByteDance Seed-Prover) remain ahead on the hardest benchmarks.