Name: MLn Club (ML Reading Group) #18: Goedel-Prover-V2: Scaling Formal Theorem Proving
Start: 2026-09-20T19:00:00.000-04:00
End: 2026-09-20T21:00:00.000-04:00
Location: Pittsburgh, PA

We meet weekly on Sundays in person to talk about ML papers! Optional quiet reading from 7 pm, discussion starts 8 pm. Come and join the discussion! Open to all. Website: https://czhs.github.io/mln/

MLn Reading Club

Goedel-Prover-V2: Scaling Formal Theorem Proving

How does pairing scaffolded data synthesis with verifier-guided self-correction overcome data scarcity in formal theorem proving?

Can structured compiler feedback and subproblem generation outperform sheer parameter scaling in complex mathematical reasoning?

Goedel-Prover-V2 addresses data scarcity and output homogenization in Lean 4 formal reasoning through three key innovations: scaffolded data synthesis, verifier-guided self-correction, and weight averaging. Rather than relying on brute-force scaling, it extracts unsolved subgoals from failed proofs to build a progressive synthetic curriculum, while using real-time Lean compiler feedback to iteratively repair incorrect proof steps.

Empirically, this framework delivers exceptional sample efficiency. The compact 8B model achieves an 84.6% pass@32 on MiniF2F—matching the 80× larger DeepSeek-Prover-V2-671B—while the 32B model sets a new state-of-the-art with 90.4% on MiniF2F and leads PutnamBench with 86 solved problems. The work reframes formal automated reasoning from a parameter-scaling challenge into an interactive, verifier-guided data problem.

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

📖 Reading Recommendations, Questions, or Comments? Contact us 

People who've been wanting to read up on the latest papers in ML and other fields but just haven't been able to find the time/motivation.