Name: MLn Club (ML Reading Group) #13: A Frontier Model for Open-Source Automated Theorem Proving
Start: 2026-08-17T19:00:00.000-04:00
End: 2026-08-17T21:00:00.000-04:00
Location: 201 S Craig St

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: 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?

 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 

—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 

 ("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 

 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.

 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.