Jeremy Avigad

2 accepted papers

2026

Premise Selection for a Lean Hammer

Thomas Zhu, Joshua Clune, Jeremy Avigad, Albert Q. Jiang, Sean Welleck

ICLR 2026oral

Neural methods are transforming automated reasoning for proof assistants, yet integrating these advances into practical verification workflows remains challenging. A $\textit{hammer}$ is a tool that integrates premise selection, translation to external automatic theorem provers, and proof reconstruc…

Cited by 0 Source ↗code ↗Scholar ↗

2025

ImProver: Agent-Based Automated Proof Optimization

Riyaz Ahuja, Jeremy Avigad, Prasad Tetali, Sean Welleck

ICLR 2025poster

Large language models (LLMs) have been used to generate formal proofs of mathematical theorems in proofs assistants such as Lean. However, we often want to optimize a formal proof with respect to various criteria, depending on its downstream use. For example, we may want a proof to adhere to a certa…

Cited by 2 Source ↗PDF ↗code ↗Scholar ↗