Premise Selection for a Lean Hammer

ICLROral2026

Authors: Thomas Zhu, Joshua Clune, Jeremy Avigad, Albert Q. Jiang, Sean Welleck
Affiliation: ByteDance Inc.
Venue: ICLR 2026
Track: Oral

TL;DR

LeanHammer integrates neural premise selection with symbolic reasoning to automate theorem proving in Lean.

Opening excerpt from the authors’ abstract. source

Read the paper

OpenReview

Topics

reasoning

← All ICLR 2026 Oral papers · Browse the whole archive