MLn Club (ML Reading Group) #13: A Frontier Model for Open-Source Automated Theorem Proving
Welcome to Week 13: 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?
The Paper Link Here
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.
📖 Reading Recommendations, Questions, or Comments? Contact us here!
🔎 View past meeting notes here.
What's this?
A super warm group of folks discussing their favorite topics!
In the first half, we host an optional quiet reading space
In the second half, we have a discussion where people can talk about what they found interesting about the reading and ask questions about things they didn't understand
When/Where:
CMU AI Safety Initiative's Office, 201 Craig Street, right across the PNC bank. Look for the open door up the stairs.
8pm discussion, 7pm optional quiet reading time.
Here's how it usually goes:
7:00 PM — arrival and settling in
8:00 PM — introductions
8:10 PM — discussion time
9:00 PM — wrap up then open discussion
Who's it for?
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.
Why:
We've been procrastinating too much on our readings, even though we have so much fun doing them. We know we're not alone in this and want to keep others accountable for learning more about what they're passionate about!
We've also met a ton of really fun friends by discussing what we care about!
Rules/guidelines on how to act:
Act like a host, include people in conversations, talk to people even if they're strangers, offer to explain what you know, and keep an open mind! come to read stuff and find super fun friends :)
Bring snacks if you're feeling kind!