TALK    [MERL Seminar Series 2026] Alex Gu presents talk titled Proving and Improving: Language Models for Theorem Proving and Proof Shortening in Lean

Date & Time:

Wednesday, February 11, 2026; 1:00 PM

Abstract:

Large language models (LLMs) have made steady progress in formal mathematics, achieving near–International Mathematical Olympiad (IMO) performance. This talk presents two complementary advances toward more capable and interpretable formal proving systems. First, we introduce LeanDojo, a foundational open-source toolkit bridging ML and Lean, enabling large-scale data extraction, interactive training, and the development of ReProver, a retrieval-augmented Lean prover. Next, we turn to a critical challenge: proofs produced by LLMs are often unnecessarily long, redundant, and opaque. To mitigate this, we introduce ProofOptimizer, a system that automatically simplifies Lean proofs while preserving correctness. It combines symbolic linting, a fine-tuned 7B model, and iterative refinement, reducing proof length by up to 87% on MiniF2F and 57% on PutnamBench, even halving some IMO-level proofs. Together, these systems demonstrate how AI can make automated proofs not only possible, but also increasingly comprehensible.

Speaker:

Alex Gu
MIT

Alex Gu is a final year PhD student at MIT working with Armando Solar-Lezama. He started his research career in ML theory and later transitioned towards improving the capabilities of language models to reason in domains like math and code. He contributed to several efforts in these fields including ProofOptimizer, CRUXEval, LeanDojo, LiveCodeBench, StarCoder (1&2), and BigCodeBench. He has also done internships at various companies including Meta, Amazon, NVIDIA, Jane Street, and Pony.AI. He received his bachelor's and master's degrees from MIT.

MERL Host:

Pu (Perry) Wang

Research Areas:

Artificial Intelligence, Machine Learning, Optimization