Premise Selection for a Lean Hammer
Authors: Thomas Zhu
Joshua Clune
Jeremy Avigad
Albert Q. Jiang
Sean Welleck
Venue: ICLR 2026 Oral (2026)
Keywords: premise selection
interactive theorem proving
automated reasoning
contrastive learning
Primary area: neurosymbolic & hybrid AI systems (physics-informed, logic & formal reasoning, etc.)
TL;DR: LeanHammer integrates neural premise selection with symbolic reasoning to automate theorem proving in Lean.

Abstract: 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 reconstruction into one overarching tool to automate tedious reasoning steps. We present LeanPremise, a novel neural premise selection system, and we combine it with existing translation and proof reconstruction components to create LeanHammer, the first end-to-end domain general hammer for the Lean proof assistant. Unlike existing Lean premise selectors, LeanPremise is specifically trained for use with a hammer in dependent type theory. It also dynamically adapts to user-specific contexts, enabling it to effectively recommend premises from libraries outside LeanPremise's training data as well as lemmas defined by the user locally. With comprehensive evaluations, we show that LeanPremise enables LeanHammer to solve 21\% more goals than existing premise selectors and generalizes well to diverse domains. Our work helps bridge the gap between neural retrieval and symbolic reasoning, making formal verification more accessible to researchers and practitioners.

Published as a conference paper at ICLR 2026
PREMISE SELECTION FOR A LEAN HAMMER
Thomas Zhu 1. Joshua Clune Jeremy Avigad",, Albert Q. Jiang" Sean Welleck 'Cameegie Mellon University, Misttal AI "Equal contribution, 'Equal advising {thomaszh, j jelune, avigad, swelleck cwt.erewwwc.....mm cmu. edu, qj2130cam. ac.uk
ABSTRACT
Neural methods are transforming automated reasoning for proof assistants, yet integrating these advances into practical verification workflows remains challeng- ing. A hammer is tool that integrates premise selection, translation external automatic theorem provers, and proof reconstruction into one overarching tool automate tedious reasoning steps. We present LEANPREMISE, a novel neural premise selection system, and we combine it with existing translation and proof reconstruction components to create LEANHAMMER, the first end-to-end domain general hammer for the Lean proof assistant. Unlike existing Lean premise selec- tors, LEANPREMISE is specifically trained for use with hammer in dependent type theory. It also dynamically adapts to user-specific contexts, enabling it to effectively recommend premises from libraries outside LEANPREMISE'S training data well as lemmas defined by the user locally. With comprchensive evalua- tions, we show that LEANPREMISE enables LEANH AMMER to solve 21% more goals than existing premise selectors and generalizes well to diverse domains. Our work helps bridge the gap between neural retrieval and symbolic reasoning, mak- ing formal verification more accessible researchers and practitioners
INTRODUCTION
Interactive proof assistants have long been used to verify the correctness of hardware, software, network protocols, cryptographic protocols, and other computational artifacts. Buoyed by successes like the Liquid Tensor Experiment (Lean Community (0022) and the formalization of the Sphere
Eversion Theorem (van Doorn 2023). mathematicians are increasingly using the technology to
verify mathematical theorems (Tao 2023) and build substantial mathematical libraries (The Mathlib
Community] 2020).
When working with proof assistant, a user describes a proof in an idealized proof language, which programming language that provides sufficient detail for the computer to construct precise formal derivation in the proof assistant's underlying axiomatic system. One of the challenges to formalization is the requirement to spell out what seem like straightforward inferences in painful detail. This problem is exacerbated by the fact that at the most basic level of interaction, users are required to name the required premises (i.c., definitions and lemmas) explicitly to justify an inference step, from library of hundreds of thousands of previously derived facts.
hammer (Meng et al. Paulsonn & Blanchette 2012 Blanchette et al. 2016) is a tool designed to ease the pain of formalization by filling in small inferences automatically. Typically, hammer has three components: given a goal to prove, one first selects a moderate number of premises from the library, project files, current file, and hypotheses that, one hopes, sufficient to prove the goal. This is known as premise selection. Then one translates the premises and the goal into the language of powerful external automated theorem provers like Vampire (Kovács & Voronkov 2013). E (Schulz)
Paulson
et al. 2019), and Zipperposition (Vukmirović et al., (022). or SMT solvers like Z3 (de Moura & Bjørner 2008 and eve5 (Barbosa et al.) 2022). Finally, if the external prover succeeds in proving
!FANPREMMIE is available at http:////////tttooo/////////aaaa selection and LEANN HAMMER is available httpppp///gtaab..c/////sootoooot

---

Published as a conference paper at ICLR 2026
the goal, it reports back the specific premises used, from which a formal proof in the proof assistant is reconstructed.
In this paper, present LEANPREMISE, new premise selection tool for the Lean proof assistant (de Moura & Ullnich 202Tp. We combine it with the DTT-to-HOL (dependent type theory to higher- tactics, order logic) wrnnsattin tool, Lean-auto (Qian et al.] [025 and internal proof-producing
Duper (Clune et al.) 2024) and Aesop (Limperg & From 2023). resulting in LEANHAMMER, the first end-to-end domain general hammer for Lean. Through comprehensive evaluations, we show that LEANHAMMER can hit nails.
Our work, which extends methods of premise selection used by Magnushammer (Mikula et al. 2024) and LeanDojo (Yang et al., 2023). is therefore an auspicious combination of neural premise selection methods with symbolic proof search. For the first time, we specifically design contrastive learning methods for the first end-to-end domain general hammer in Lean. We explain the design choices to make LEANPREMISE performant for LEANHAMMER including new hammer-aware data extraction techniques. An important feature of LEANPREMISE is that it dynamically augments the library of facts with locally defined facts from the user's project, which is essential in practice.
Our core contributions are follows:
We develop LEANPREMISE, a premise selection tool for hammer dependent type theory.
We combine LEANPREMISE with Aesop, Lean-auto, and Duper to make LEANHAMMER, the first domain general hammer in Lean.
We provide an accessible user-facing tactic interface that can dynamically process new premises in the environment.
We conduct comprehensive evaluations of LEANHAMMER'S performance on Mathlib and its abil- ity to generalize to mini CTX-v2 (Hu et al. 2025). Through these evaluations, we show that LEAN- HAMMER solves 21% more goals with LEANPREMISE than with existing premise selectors and that L.ANPREMIIE enables LEANHA MMER to effectively use libraries and premises hasn" 't seen before.
Note that premise selection can be used in other ways, for example, for calling various types of internal automation directly, for presenting suggestions to a user engaged in manual proof, or for use in neural or neurosymbolic search. Although our focus here has been on a hammer, we expect that many the methods we develop carry over to other settings.
RELATED WORK
2.1 HAMMERS IN INTERACTIVE PROOF ASSISTANTS
As explained in the introduction, hammers support interactive proving by completing small infer- ences, called goals. The first and still most successful hammer in use today is Isabelle's Sledge- hammer, developed initially by Meng et al. (2006) and further developed by Paulson & Blanchette (2012) Blanchette et al. (2013). and many others. Since then hammers have been developed for HOL Kaliszyk& & Urban 2013a)) Mizar (Kaliszyk & Urban 2015b). Rocq (Czajka & Kaliszyk 2018 and Metamath (Carneiro et al. 2023). 3,, among others. Of these, only Roeq is based on depen- dent type theory. Despite Lean's popularity, hammer has been developed for Lean.
2.2 NEURAL THROREM PROVING
tools have been developed to prove theorems. A straightfor- ward approach of using neural models is to them generate steps in proofs, notable examples of which include GPT-f (Polu et al., 2023), HTPS (Lample et al., 2022). ReProver (Yang et al.)
Numerous neural-network-
2023 DeepSeek- (Xin et al. 2024a b) for Lean, LISA (Jiang et al. 202I) and Thor (Jiang al. 2022 for Isabelle, and PALM (Lu et al.) 22024). Cobblestone (Kasibatla et al.) 2024 and
Graph2Tac (Blaauwbrock et al. 2024 for Coq/Rocq. Another line of work uses neural models to generate entire proofs proof sketches (Jiang et al.] 2023 Zhao et al.) 2023: Wang et al. [024 First ctt al.] 2023 Lin et al. 2025a Wang et 20.5 Chen et al. 2025). These proof search approaches complementary a hammer, which serves tactic that may be used by neural models.
2

---

Published as a conference paper at ICLR 2026
Hammers embedded in number of neural theorem proving frameworks such Thor and Draft,
Sketch, and Prove (Jiang et al., 2022 Zhao et al. 2023 Jiang et al. 2023] Wang et al. 2024) to fill small gaps in the proofs. It IS worth noticing that all these works use the Isabelle proof
assistant (Nipkow et al. 2002) where the communication infrastructure (Jiang et al. (021) between
neural models and the proof assistant is relatively mature and hammering easy to set up. Our work makes calling a hammer in Lean possible.
Despite a large number of research works, practical tools that a working mathematician has access to without complex setup or prohibitive costs remain scarce. Recent state-of-the-art methods use reinforcement learning on e.g. 7B LLMs with thousands of passes for a single theorem and use infrastructures not callable from Lean (Wu et al. [2244] [in et al. 2025a b Dong & Ma 2025 Chen et al. 2025), so it prohibitive for Lean users to train, test, or use them. Our work brings forward a tool that is packaged as a tactic and can be called straightforvardly from any IDE for Lean with low
computational cost and latency, hence enabling better automation for the masses.
2.3 PREMISE SELECTION
Formalizing mathematics in proof assistants requires users to select relevant premises from libraries of hundreds of thousands of facts. To help facilitate this task, premise selection has been devel- oped for a variety of proof assistants, using both neural and symbolic techniques. MePo (Meng & Paulson! 2009) is a symbolic premise selector which has been widely used in Isabelle's 's Sledge- hammer. Other premise selectors which target hammers but use traditional machine learning tech- niques include MaSh (Kühlwein et al., 2013), k-NN based premise selection for HOL4 (Gauthier & <Kliszyk] 2013), CoqHammer's premise selection (Czajka & Kaliszyk 2018), and random forest based premise selection for Lean (Piotrowski et al.) 2023). LEANPREMISE differs from these by using modern L.M-baeed retrieval methods.
M-)ssd premise selection trained by contrastive learning has also been explored for a variety of use cases. Lean State Search (Tao et al. 2025) recommends relevant premises directly to Lean users. Magnushammer (Mikuta et al.) 2024) generates premises to supply directly to proof recon- struction tactics. ReProver and Lean Copilot Yang et al. [023] Song al.] 2024) retrieve premises to augment neural next-tactic generation. Unlike these, LEANPREMISE specifically designed with hammer integration in mind, which requires specific data extraction and loss formulation, and the resulting selector to be fast and domain general.
3 METHODS
3.1 LEANHAMMER PIPELINE
Hammers broadly consist of three primary components: premise selection, translation to external automatic theorem provers, and proof reconstruction. In traditional hammer pipelines, such Is- abelle's Sledgehammer, these components are composed in a linear fashion, with the premises from premise selection informing the translation to automatic theorem provers and the output from tomatic theorem provers informing proof reconstruction. In other works, such as Magnushammer (Mikuta et al.) 2024) and Lean Copilot (Song al. 2024), premises from premise selection are provided directly to proof reconstruction tactics or language models, without translating and send- ing them to external automatic theorem provers. LEANHAMMER introduces a new, unified hammer pipeline that uses premise selection in both of these ways.
Figure D gives an overview of the LEANHAMMER pipeline. In addition LEANPREMISE itself, LEANHA MMER is built upon Aesop, Lean-auto, and Duper. Aesop is a highly extensible proof search tool that can augmented with new proof search rules and procedures. Lean-auto a translation tool that does not search for proofs itself, but instead translates dependently typed Lean goals into higher-order logic problems which can be solved by external automatic theorem provers such as Zipperposition. Finally, Duper is less powerful but mrof-pprouuiig proof search tool which implements many of the techniques found in automatic theorem provers, and is therefore well suited to rediscovering and verifying proofs found by external automatic theorem provers.
In broad strokes, Acsop is called first and prioritizes finding a proof using its own built-in rules. short proof using only built-in rules is not found quickly, it explores direct premise applications
3

---

Published as a conference paper at ICLR 2026
Lean-auto translation
Zipperposition proof search
Duper proof reconstruction
LeanPremise
Initial goal state
Aesop premise
Aesop
application
Overview of the LEANHAMMER pipeline. Phases that can neither fail nor produce a terminal proof are green. phases that can fail but cannot produce a terminal proof are yellow, and phases that can produce a terminal proof are blue. Black solid arrows indicate control flow, while red dashed arrows indicate the transfer of information between phases.
Figure 1:
using premises recommended by LEANPREMISE and it queries Lean-auto see if subgoals can be closed using premises from the selector When Lean-auto is given a subgoal, it translates that subgoal (along with the premises provided by the selector) to higher-order logic and interfaces with Zipperposition to find a proof. If Zipperposition succeeds, then Duper is provided just the set of premises used by Zipperposition proof from these premises. For an illustrative example of LEANHAMMER pipeline in action, see the extended version of this paper (Zhu et al., 2025 Section B).
solve the translated problem, and Duper attempts to reconstruct
3.2 DATA EXTRACTION
To support LEANPREMISE, we develop data extraction pipeline designed to gather not just in- formation useful for next-tactic generation or human examination, but all of the information that may be helpful for a hammer tasked with discovering dynamically to extract premises that LEAN can retrieve at runtime, including premises or definitions defined by the user locally, and it is used statically to extract (state, premise) pairs for training. As we describe our data extraction pipeline, we note the measures taken to collect data that go beyond what appears explicitly in the source code for the formal proofs.
end-to-end proof. This pipeline is used
3.2. 1 SIGNATURE EXTRACTION
A key aspect of premise selectors is how premises are presented to the model. Previous work YYngg al. 2023) extracts raw strings from the source code, which ignores many details in the full sig- nature (see Section A of the extended version of this paper (Zhu et al. 2025) for an example). We adopt new normalized serialization as follows. For each theorem and definition in each module, we extract the documentation description in the source code (its docstring), if it exists, as well as its kind (theorem or definition), name, arguments, and overall type. Together, these can be composed into a signature of the form docstring? kind name arguments* these signatures into strings, we disable notation pretty printing (e.g. we print N as Nat), and we print every constant with its fully qualified name (e.g. print I as Complex I). This standardizes premise representation, so that it depends only on the type of the premise and does not depend on open namespaces, custom notations, and surface-level syntax, which may change an illustrative example, see Section A of the extended version of this paper (Zhu et al. 2025).
type. When converting
time. For
The signatures extracted in this manner are used form the set of premises P that LEANPREMISE is allowed to retrieve from. This signature extraction pipeline is also used to dynamically extract new premises runtime (Section 3.3.2). To prevent LEANPREMISE from constantly recommending theorems that are technically relevant to the goal but never useful for our hammer's automation, we filter a blacklist of 479 basic logic theorems such as and_ true from P. We also filter out Lean lantu (e.g. metaprogramming! definitions not useful for proofs.
Prremise applications rules added Aesop of the form (add unsafe 20% <premise>) where <premise> is a premise selected hy the premise selector. Leann-auto is added to Aesop rule of the form (add unsafe 10% (by auto [+, <premises>])) where <premises> is list of premises selected by the premise selector.
4

---

Published as a conference paper at ICLR 2026
3.2.2 STATE AND PREMISE EXTRACTION
The next key question is which (state, premise) pairs are extracted from human-written proofs to train the model. Previous premise selectors (Yang et al. 2023 that focus on tactic generation only extract from tactic-style proofs, and only extract explicit premises appearing in the raw source code of only the next tactic. Our hammer-aween we extract from both term-style and tactie-style proofs, significantly increasing training samples especially for short proofs that LEANHA MMER is intended to automate. Second, for multi-tactic proofs, the model is trained to select premises to close the goal (all tactics) rather than to modify the goal (first tactic), because hammers are designed to finish proofs. Third, we extract both implicit and explicit premises from the proof, including ones implicitly called by automation such as simp. Finally, we format states with the same normalized serialization for premises.
data extraction improves upon this in several ways. First,
Specifically, for each theorem in each module, we collect data on the premises used to prove it. Additionally, for each theorem proven via tactic-style proofs, collect data on all intermediate goal states induced by the tactic sequence. For an illustrative example, see Section A of the extended version of this paper (Zhu et al. (022).. Ultimately, all data we extract contains:
proof state obtained either from the beginning of a theorem or from an intermediate step of a tactic-style proof.
The name and signature of the theorem from which the state was extracted.
The set of premises used to prove the theorem")
When theorems are proven via term-style proofs, meaning the theorem's 's proof term is explicitly written in the source code, the set of premises we extract is the set theorems that appear in the proof term. When theorems Lean how to build a proof term, the set of premises we extract contains both the theorems that appear in the proof term constructed by the tactic sequence (so that all implicit premises collected), as well as any theorems and definitions that are explicitly used in rw or simp calls.
proven via tactic-style proofs, meaning automation is invoked to tell
The benefit of collecting explicit theorems and definitions from rw and simp calls relates Lean's dependent type theory. In Lean, terms can be definitionally equal without being syntactically equal, and because of this, tactic-style proofs invoke definitional equalities that do not appear in final proof terms. We therefore collect these definitional equality premises. We experimentally verify that our hammer-ane aware data extraction benefits LEANHAMMER Section
3.3 PREMISE SELECTION
LEANPREMISE uses the standard method of retrieval using textual encoders. In order to retrieve k premises for a state s, we first determine the set Pa of accessible premises at position 8, comprising lemmas and definitions that are imported from other modules or declared earlier in the file. We use an encoder-only transformer model E to embed both the state s and every premise E Pas and the resulting set of premises retrieved is
select_ (allect_premiee((S P.) top-kpep, sim (F((s), F(())
where sim(u, v) = To /l/ u/] |2|(e) u||2 is cosine similarity. In Section 3.3.2 we describe the mechanism
for caching embedding and quick retrieval of the premises.
We do not train separate reranking model in Mikula al. 2024 because did not find it to increase performance in early experiments, especially since a hammer favors recall much more than precision, and we determined the optimal i to be at least 16, which point reranking does not offer much improvement. is also costly to deploy in practice.
3.3.1 MODEL TRAINING
We use modified version of the InfoNCE loss (Oord al.) 2018) to train the encoder model. On a high level, each batch consists of (state, premise) pairs, and contrastive loss is used to let the
We also experimented with pairing states with just the set of premises used to close said states, as opposed to all premises used to prove the overall theorem, but our preliminary experiments showed that this yielded worse results than including all premises.
5

---

Published as a conference paper at ICLR 2026
Premise selector
LM-based
Callable in Lean
New premises
ReProver (Yang et al. 2023)
Lean Copilol (Song el al. (024)
Random forest (Plotrowski et al.
2023
MePo (Meng & Paulson 2009)
X
/
LEANPREMISE
/
Table 1: Usability comparison of existing premise selection tools. Note that this is orthogonal the quantitative performance comparisons (Table 2).
model learn select the correct premise of all premises in this batch. One problem is that there are many premises in the library that do not appear in any proof. This is mitigated by also sampling negative premises in each batch (Mikula al., 2024, Yang et al. (023). Another problem that there are many premises that are shared across many proots, so not all premises in the batch are negative. We use the following masked contrastive loss address these problems.
Specifically, for each training step, we sample batch of B (state, premise) pairs, each consisting of state 8; and premise p. E -P+ where Ptt is the set of ground-truth premises for 8; extracted as in Section 3.2 For each such pair (st. we sample B negative premises {piz}f=1 Pa, P giving B states and ((1 B-) premises in total in each batch. Of these premises, we determine the set N {rr Je U (p,ylay Jay's Pt of negative premises for state 8i, and mask out the positive ones in the loss to avoid mislaheling. The loss is:
B Σ ( = B
cxp(sim E(s;), )(/r))/r)
(2)
exppssi(E(sss
eN; exp (ap(sim(E(()) E(p, ))/r)
where T scalar temperature syper-parameter (set to 0.05 in our experiments).
3.3.2 API INTEGRATION
In order to make LEANPREMISE and LEANHAMMER more accessible for Lean users well as downstream methods, we design our pipeline to maximize usability-ire directly callable in Lean, able to take in new premises, and efficient to run. Our pipeline for premise selection is as follows: when a user invokes premise selection, the client side (Lean) collects all currently defined premises P. defined in the environment and the current proof state and sends them server that hosts the embedding model. The server embeds both the proof state and the list of premises, and then runs FAISS (Douze al., (224) the premises to compute select premises k. Pa). and returns this list of l premises back to the client. Since the typical size of P. is on the scale of 70k, the server also caches the embeddings of premises at fixed versions of Mathlib, and only recomputes embeddings of signatures of new premises uploaded by the user (e.g. when working outside Mathlib or when the user has new premises in the context); the client side also caches the signatures of these new premises computed as in Section 3.2.T
LEANHAMMER is built tactic that can be directly called in Lean. calls LEANPREMISE subprocedure and the retrieved premises are then input to the LEANHAMMER pipeline (Section 3.1 In Mathlib, premise selection usually takes about second amortized on a CPU server (and well under second for single-GPU server). The full LEANHAMMER pipeline on average takes well under seconds (see Section 4.2)
To the best of our knowledge, LEANPREMISE is the first premise selector using language models that can be directly invoked in Lean and can incorporate new user-defined premises. is also efficient to run and requires system setup for the user, because the main computation is only few string embeddings, and done centrally in a server by default. This makes the premise selector itself desirable user-facing tactic for the Lean community. Similarly, the full LEANHAMMER be called straightforwardly in Lean as a tactic. This bridges gap that many previous LM-based retrievers and provers leave. See Table I for comparison.

---

Published as a conference paper at ICLR 2026
3.4 VARIATIONS AND EXTENSIONS
Here, we discuss variations on LEANHAMMER'S design, implemented as settings that can be con- trolled by the user. Note that the pipeline described in Section 3.1 has premises input both to Aesop as premise application rules and to Lean-auto for translation to the external prover. We consider variants that disable either one:
1. aesop: This setting only inputs LEANPREMISE'S premises to Aesop as premise applications, omitting calls to Lean-auto or the external prover.
auto: This setting inputs L. L.FANPREMIS'S premises directly to the external prover through Lean- auto without Aesop normalization premise application.
3. aesop+auto: This setting keeps both Aesop and Lcan-auto, but does not use premise applica- tions as Aesop rules.
4. full: This default setting is the full pipeline described in Section 3.1
These variants are appealing because they offer cheaper computational cost while still preserving much of LEANHAMMER'S 's ability. Experiments offer insight to the ability of each part the pipeline (see Section 4.2). We observe that the first three variants may prove theorems that full does not, so we also consider cumul, which tries all four variants.
We note that other common domain domain-general automation tactics that take premises inputs, such as simp_all, may be roughly considered a subcase of aesop (which we verify in preliminary experi- ments), do not consider them. We also tried using second-stage model to predict simp_all all "whther a premise should be supplied to s simp_all for preprocessing, and whether should be applied in reverse direction, but the performance did not increase. We remark that ad- ditional automated reasoning tactics in the future may be easily added to our pipeline as a rule of Aesop, similarly to how Lean-auto is added.
EXPERIMENTS
4.1
EXPERIMENTAL SETUP
We extract theorem proofs from Mathlib, and premises from Mathlib, Batteries, and Lean core. In to- tal, we extract 469,965 states from 206,005 theorem proofs, and extract 265,348 (filtered) premises. For each state, there are on average 12.45 relevant premises, giving 5,817,740 (state, premise) pairs in the training set. We randomly hold out 500/500 theorems valid/test sets, respectively.
We train the model from three base models that were pre-trained for general natural language em- bedding tasks (Reimers Gurevych) 2019). These are small with layers and hidden size 384 trained from MiniLM-L6, medi with 12 and 384 from MiniLM-L12,, and large [ with 6 and 768 from DistiRo respectively. We train our models with learning rate 2 B = 256, and B 3, found by hyperparameter sweep. Training the large model requires 6.5 A6000-days.
We test LEANHAMMER on proving theorems in (1) our hold-out sets extracted from Mathlib, and (2) the Mon-Mathlib splits of minicTX-- -TTt-tttest (Hu et al. 2025). We impose a001110000 10-second time constraint for each call to Zipperposition, and for each theorem a 300-sccond wall-clock time-out and Lean's 's default heartbeat limit of 200,000. We tuned the value of i Mathlib-valid (see Section D.3 of the extended version of this paper (Zhu et al.) 2025)). and full uses the highest performing combination, which is k; = 16 premises supplied
Lean-auto (with Aesop priority 10%) and k2 = 32 premises for premise application rules (with Aesop priority 20%). Similarly, we use k 16 for auto and aesoptauto, and & 32 for aesop.
For all experiments and data extraction tasks, we use Lean version v4. 14.06.0. We run a maximum of 16 parallel tests on 16 CPUs with 512GB total memory, so CPU and 32GB are allocated per test theorem. In practice, the actual memory used rarely exceeds 4GB, Each CPU is AMD EPYC 9354 (3.8GHz, 32 cores, 64 threads) or similar.
"htrss//huggingfacccoosssmt wraaeeerrrnnstoorsallliiiiiii
"https//huggingfaaccco wttp:aaaccccccccaaaeeeeeeeeeeeee https//hugginggffcc..m caleentenne--mmstfomrrealllllded
7

---

Published as a conference paper at ICLR 2026
Premise selector
Model size
Recall (%)
Proof rate (%)
@ 16
@:2
aеहop
auto
aesop=auto
full
cumil
None
0.0
16.9
16.9
16.9
Random forest*
22.1
22.3
19.1
11.9
19.1
19.1
MePo
38.4
42.1
23.3
14.5
26.3
27.5
ReProver
218M
35.1
38.7
11.4
12.9
20.5
12.0
22.3
LEANPREMISE (small)
23M
59.2
23.9
19.1
27.9
31.9
LEANPREMISE (medium)
33M
23.1
20.1
28.5
30.7
LEANPREMISE (large)
82M
63.5
72.7
24.1
21.3
28.5
30.1
33.3
LEANPREMISE (Iarge) MePo
28.9
23.9
30.3
35.9
37.6
LEAN (cumulative)
27.5
25.5
31.1
34.5
37.3
LEANPREMISE (cumulative) U MePo
30.3
27.1
32.3
38.2
39.6
Ground truth
27.7
33.1
37.8
41.0
43.0
PPerformance upper bound, excluding errons.
"Our detinition is slightly different from
Yang et al.
2023
See Section C' the extended
version of this puper Zhu al.
2025
Table 2: Performance of LEANHAMMER with different premise selectors Mathlib-test.
Premise selector
Proof rate using full (%)
Carleson
ConNF
FLT
Foundation
HepLean
Seymour
Average
None LEANPREMISE (large)
0.0
10.0
27.3
38.0
8.0
6.0
14.9
0.0
16.0
36.4
38.0
10.0
24.0
20.7
Ground truth
7.1
16.0
39.4
40.0
20.0
34.0
26.1
Table 3: Out-of-Mathlib performance of LEANHAMMER on miniCTX-v2-tesx: (Hu et al. 2025) using the large model trained on Mathlib. For other settings than full, Table 5 of the extended version of this paper (Zhu et al. 2025).
4.2 RESULTS
For each theorem, record the average percentage of ground-truth premises retrieved in the top-k premises (recall@ k), and the percentage of theorems proven (proof rute), shown in Tables[aam We favor recall over metries like precision, because hammer can tolerate irrelevant premises much more than missing important ones.
LEANHAMMER proves significant number of theorems. As shown in Table 2 find that LEANHAMMER proves a significant proportion of test theorems, with 33.3% proved by the large model in the cumul setting, and 37.3% when accumulated over model sizes. We also test giving ground-truth premises (those that appear in the human-written proof) to LEANHAMMER, which theoretical best-case scenario of how LEANHAMMER would perform if the models achieved 100% recall, and this proves 43.0% of the theorems. Compared to previous work, LEAN- HAMMER approaches this limit in the settings considered.
Performance scales with model size and accumulation. In Table (and Figure 2a of the extended version of this paper (Zhu et al. 2025 as we increase our model size, for most settings the recall and proof rates also correspondingly increase (e.g., recall @ 32 increases from 67. 87.8% to 72.7% and full proof rate increases from 27.9% 30.1%). We also observe that by accumulating across different model sizes or taking the union of neural (our model) and symbolic (MePo) approaches, the proof rate increases much more than scaling the model alone (e.g., full proof rate increases to 34.5% when accumulated), meaning different selectors prove different sets of theorems. More effective methods ensembling models may be explored in future work.
LEANHAMMER settings offer different abilities at different costs. For the settings auto, aesop. ausop auto, and full, the proof rate roughly increases in this order for all models. This shows aesop*
that each part of the full pipeline incrementally contributes to the final proof rate. Their mean run times on Mathlib-test are 4.3s, 0.92s, 4.9s, and 6.6s respectively, so the non-full variants are computationally appealing alternatives that recover some of the full performance. We also note
8

---

Published as a conference paper at ICLR 2026
that cumul achieves higher proof rates than full, some cases benefit from a partial pipeline (e.g. the full pipeline does not terminate).
LEANHAMMER shows robust out-of- generalization. As shown in Table 3 the perfor- mance on miniCTX-v2-tee (Hu et al., 2025) is comparable to the performance on Mathlib the proportion of theorems proven by LEANHAMMER with the large selector, out of theorems proven with the ground-truth premises (i.e. the best-case scenario), is 73.5% on Mathlib and 79.4% on miniCTX with the full pipeline, showing that performance does not decrease (the other settings also have comparable numbers; see Table 5 of the extended version of this paper (Zhu et al. 2025 ). We also confirm in the table that if no premises are supplied. the performance much worse (ex- cept for the Foundation split), which indicates that the LEANHAMMER is not just proving trivial theorems.
Across all benchmarks, there are a handful of common patterns characterizing problems that LEAN- HAMMER fails solve. Some problems are not solved because LEANPREMISE fails to retrieve necessary lemmas, as can be seen from the fact that the ground truth outperforms all other premise selectors in Tables 2 auto's translation procedure, which can occur when the problem in question contains features from dependent type theory not easily translated to higher-order logic. And some problems are not solved because the solutions require forms of reasoning not supported by Acsop, Zipperposition, or Duper (e.g. induction or arithmetic). Comparatively, it is rare for LEANHAMMER to succeed at proof search with Zipperposition but fail at the proof reconstruction stage with Duper. See Sections D.4 and D.5 of the extended version of this paper (Zhu et al. 2025) for additional analysis.
and 3 Some problems are not solved because they are out of scope for Lean-
4.3 COMPARISONS
We compare LEANPREMISE against the following existing work: non-LM methods MePo Meng & Paulson 2009) and Piotrowski et al. (2023), and LM-based ReProver (Yang et al. 2023 ). We use recent adaptation of MePo from isabelle to Lean (implemented by Kim Morrison), tune its parameters and с on our evaluation recall@k, and apply our premise blacklist. For Piotrowski et al. (2023), select their random forest model with highest reported performance; in order to overcome errors, we modified its training and evaluation in a way that only gives them unfair advan- tage, so the reported performance is an upper bound. (See Section C of the extended version of this paper (Zhu et af.) 2025) for details of both methods.) We find that LEANPREMISE clearly outper- forms either method- for the large model, our recall @ 32 is 73% higher relative to MePo and our cumul proof rate is 21% higher (Table 2). Meanwhile, the union of theorems our models and MePo can solve is much higher than each method separately, indicating that symbolic and neural methods have complementary strengths. We believe effective combinations of neural and symbolic methods warrant future investigation.
We retrain ReProver using their training and retrieval scripts, but on our train/valid/test splits and an updated Mathlib version (Zhu et al. 2025] Section C). LeANPREMISE clearly outperforms ReProver (Yang et al. 2023) in terms of recall and proof rate--LaAAHAAAAA LEANHAMMER using our large model (82M parameters) proves 150% more theorems relative to using ReProver (218M) in the full setting and 50% more in the cumul setting. We attribute the performance gap to two main factors. First, ReProver focuses on premises used in the next tactic for tactic generation, while LEANPREMISE focuses finishing the entire proof, the definitions of ground-truth premises are different (Sec- tion 3.2.2). Second, LEANHAMMES uses techniques such as term-style proof extraction, extraction of implicit premises, and better premise signature formatting (Section 3.2). ReProver also uses an (² loss on the cosine similarity for training, rather than our contrastive loss, and we suspect this also contributes to our better performance.
4.4 ABLATIONS
Table shows the performance of LEANHAMMER on Mathlib-valid with some components re- moved: (1) we use naive data extraction script that (a) uses default pretty-printin
options, (b) disables our premise blacklist, and (c) disables collection of premises from s simp or rw calls; (2) we do not sample negative premises during training (B 0); and (3) we disable masking positive in-batch premises in the contrastive loss, i.e. the denominator of Equation (2) being simply the sum over all B11 + B- premises in batch. We observe these changes clearly degrade performance.

---

Published as a conference paper at ICLR 2026
Premise selector
Recall (%)
Proof rate (%)
@ 16
@ @32
aesop
aesop+auto
full
cumul
LEANPREMISE (medium)
61.1
71.9
29.8
22.6
30.2
34.6
37.6
naive data
57.5
66.8
29.3
20.0
28.5
33.1
35.2
negatives
51.8
59.5
28.6
20.0
28.4
33.0
36.8
loss mask
59.1
69.6
29.4
21.2
29.0
34.1
38.4
Ground truth naive data
30.8
32.0
38.4
41.2
43.6
31.2
30.0
37.0
39.8
42.4
Table 4: Ablation study of LEANHAMMER with different training settings on Mathlib-valid.
Specifically, our data extraction (Section 3.2 is specifically designed with Lean-auto translation in mind, and we observe that settings with Lean-auto have lower performance with naive data extraction script. We observe that randomly sampling negative premises and the loss mask (Sec- tion 3.3.1) improve performance. (Although the cumul proof rate of LEANHAMMER without the loss mask is higher, we strongly believe this due to random noise, because all individual settings give lower performances, the recall lower, and proof rate has higher variance than recall.)
CONCLUSION
We developed LEANPREMISE, novel premise selection tool for hammer in dependent type the- ory, and combined neural premise selection with symbolic automation build LEANHAMMER, the first comainngeneers hammer in Lean. With comprehensive experiments,
show that LEAN- HAMMER is performant on Mathlib compared to baselines, and generalizes well to miniCTX-v2 LEANPREMISE and LEANHAMMER designed with accessibility for Lean users in mind, and lay down groundwork for future hammer-hased neural theorem proving in Lean.
ACKNOWLEDGMENT
We would like to thank Kim Morrison for early discussions about premise selection and implement- ing a premise selection API and the MePo selector in Lean core, Jasmin Blanchette for proofreading the paper and giving suggestions, Yicheng Qian for discussions about premise selection and building and improving Lean-auto, and Jannis Limperg, Mac Malone, and Joachim Breitner for answering our technical questions. Work partially supported by NSF Grant DMS- 24346444 and a gift from Convergent Research.
REPRODUCIBILITY STATEMENT
We make all code for data extraction, model training, evaluation, and API integration publicly available with an open-source license. Data extraction is open source at /https: com/ training script is at hhtpp:://gt htt.:/bb.ttbb...mm/ www//hnwwwhzuuuuuuoooo/ao Leannanmer--traininng premise selection server is at hhtpp::/// h/t::h/bg.b.......m thub. wwt.coom/aaaaae hhom/hhnwwezhu/ Lean-prremise-servee and the Lean premise selection API is partly in Lean core and partly at https://github. wttp://woccchoo/eeeeee www.w/wwwwwwuuuoeeeeeeeeeae http://eemiieeeeeeeeee sereee-selltiiooo We open source both LEANPREMISE
and LEANHAMMER tactics in Lean https:: http:::///gtttt com/ WOomm/OSHHC.NN/LLanniioa also release the extracted data and all trained models and baselines.
We
REFERENCES
Haniel Barbosa, Clark Barrett, Martin Brain, Gereon Kremer, Hanna Lachnitt, Makai Mann, Ab- dairhman Mohamed, Mudathir Mohamed, Aina Niemetz, Andres Nötzli, Alex Ozdemir, Mathias Preiner, Andrew Reynolds, Ying Sheng, Cesare Tinelli, and Yoni Zohar. cve5: A versatile and industrial-streengh SMT solver. In Dana Fisman and Grigore Rosu (eds.). Tools and Algorithms for the Construction and Analysis of Systems, pp. 415 442, Cham, 2022. Springer International Publishing. doi: 00000998---000-9554444 24.
10

---

Published as a conference paper at ICLR 2026
Lasse Blaauwbroek, Mirek Olsák, Jason Rute, Fidel Ivan Schaposnik Massolo, Jelle Piepenbrock, and Vasily Pestun. Graph2tac: Online representation learning of formal math concepts. In Forty- first International Conference Machine Learning, ICML 2024, Vienna, Austria, July 21-27, 2024. OpenReview.net, 2024. URI.tttss: paattps://openreviiee http:p/s///pppueeeeeeeeee//eeeea
Jasmin Christian Blanchette, Sascha Böhme, and Lawrence C. Paulson. Extending sledgehammer with SMT solvers. J. Autom. Reason., 51(1):109-128, 2013. doi: 10.1007/510817-0133922222
Jasmin Christian Blanchette, Cezary Kaliszyk, Lawrence C Paulson, and Josef Urban. Hammering towards qed. Journal of Formalized Reasoning, (1):1011-44, 2016.
Mario Carneiro, Chad E. Brown, and Josef Urban. Automated Theorem Proving for Metamath. In
Adam Naumowiez and René Thiemann (eds.), Interactive Theorem Proving (ITP), pp. 9:1-9:19, Dagstuhl, Germany, 2023. Schloss Dagstuhl Leibniz-7enttrum für Informatik. doi: 10.4230/
IIP.22..TP.
Luoxin Chen, Jimming Gu, Liankai Huang, Wenhao Huang, Zhicheng Jiang, Allan Jie, Xiaoran Jin, Xing Jin, Chenggang Li, Kaijing Ma, et al. Seed-prover: Deep and broad reasoning for automated theorem proving. arXiv preprint arXiv:2507.22:: 2025.
Joshua Clune, Yicheng Qian, Alexander Bentkamp, and Jeremy Avigad. Duper: A Proof- Producing Superposition Theorem Prover for Dependent Type Theory. In Yves Bertot, Temur Kutsia, and Michael Norrish (eds.), Interactive Theorem Proving (ITP), volume 309, pp. 10:1- 10:20, Dagstuhl, Germany, 2024. Schloss Dagstuhl Leibniz-Zentrum für Informatik. doi: 10.4230/LIPIcc.1T...00...
Lukasz Czajka and C. Kaliszyk. Hammer for Coq: Automation for dependent type theory. Journal of Automated Reasoning, 61:423 453, 2018. URL htttts:t/pppp..../ www.aticschooool........... /RLLAtpp:///ppeeeeeattttcccaaaad org/
CorpusID: 11060917
Leonardo de Moura and Nikolaj Björner. Z3:
An efficient SMT solver. C. R. Ramakrishnan and Jakob Rehof (eds.). Tools and Algorithms for the Construction and Analysis of Systems, pp. 337- 340, Berlin, Heidelberg, 2008. Springer Berlin Heidelberg. doi: 10.1007/978-3 3-540--880000000 2_24.
Leonardo de Moura and Sebastian Ullrich. The Lean 4 theorem prover and programming language. In André Platzer and Geoff Sutcliffe (eds.), Conference On Automated Deduction (CADE), pp- 625-66 635. Springer, 2021. doi: 10.1007/978-3-0 000-000077755
Kefan Dong and Tengyu Ma. Beyond limited data: Self-play I1m theorem provers with iterative conjecturing and proving. arXiv preprint arXiv:2502.0m 00212, 2025.
Matthijs Douze, Alexandr Guzhva, Chengqi Deng, Jeff Johnson, Gergely Szilvasy, Pierre- Emmanuel Mazaré, Maria Lomeli, Lucas Hosseini, and Hervé Jégou. The faiss library. arXiv preprint 20x::24401.08811, 2024.
Emily First, Markus N. Rabe, Talia Ringer, and Yuriy Brun. Baldur: Whole-proo generation and repair with large language models. In Satish Chandra, Kelly Blincoe, and Paolo Tonella (eds.), Proceedings of the 31st ACM Joint European Software Engineering Conference and Sympo- sium on the Foundations of Software Engineering, ESEC/FSE 2023, San Francisco, CA, USA, December 3-9, 2023, pp. 1229 1241. ACM, 2023. doi: 10.1145/361 164333316333 URL https://doi. org/ 1145/111116640 36162433
Thibault Gauthier and Cezary Kaliszyk. Premise selection and external provers for HOL4, In Proceedings of the 2015 Conference Certified Programs and Proofs, New York, NY, USA, January 2015. ACM.
Jiewen Hu, Thomas Zhu, and Sean Welleck. miniCTX: Neural theorem proving with (long- Jcontexts. In The Thirteenth International Conference on Learning Representations, 2025. URL https::/oppenrvviee
Albert Q. Jiang, Wenda Li, Jesse Michael Han, and Yuhuai Wu. Lisa: Language models of isabelle proofs. In 6th Conference Artificial Intelligence and Theorem Proving, pp. 378-392, 2021.
11

---

Published as a conference paper at ICLR 2026
Albert Q. Jiang. Wenda Li, Szymon Tworkowski, Konrad Czechowski, Tomasz Odrzygózdz, Piotr Milos, Yuhuai Wu, and Mateja Jamnik. Thor: Wielding hammers to integrate language models and automated theorem provers. In Sanmi Koyejo, S. Mohamed, A. Agarwal, Danielle Bel- grave, K. Cho, and A. Oh (eds.), Advances in Neural Information Processing Systems 35: Anmual Conference on Neural Information Processing Systems 2022, NeurlPS 2022, New Orleans, LA, USA, November 28- December 9, 2022, 2022. URL htRp:/tt:://pppeee nips cc/paper paper_fieees_e//////ppppp files/ 7a2ps77000022hs31555662226222222 -atpre/ets---bbtrratt-oooooooee cenntraactt-oofeeenne.tttttt
Albert Qiaochu Jiang, Sean Welleck, Jin Peng Zhou, Timothée Lacroix, Jiacheng Liu, Wenda Li, Mateja Jamnik, Guillaume Lample, and Yuhuai Wu. Draft, sketch, and prove: Guiding formal theorem provers with informal proofs. In International Conference on Learning Representations (ICLR). OpenReview.net, 2023. URL
Cezary Kaliszyk and Josef Urban. Hol(y)hammen Online ATP service for HOL light. Mathematics in Computer Science, 9(1):5-22, 2015a. doi: 178007/11188-0004-08882222
Cezary Kaliszyk and Josef Urban. Mizar 40 for mizar 40. Journal of Automated Reasoning, 55(3): 245-256, 2015b. doi:
Saketh Ram Kasibatla, Arpan Agarwal, Yuriy Brun, Sorin Lerner, Talia Ringer, and Emily First. Cobblestone: Iterative automation for formal verification. CoRR. abs/2410. 19940, 2024. doi: 10.48555/ARXIV.241000
URL https:////// org/10. 10. 48550/ arxiv 19940
Laura Kováes and Andrei Voronkov. First-order theorem proving and Vampire. In Natasha Shary- gina and Helmut Veith (eds.), Computer Aided Verification (CAV), pp. 1-35, Berlin, Heidelberg, 2013. Springer.
Daniel Kühlwein, Jasmin Christian Blanchette, Cezary Kaliszyk. and Josef Urban. Mash: machine learning for sledgehammer. In Interactive Theorem Proving: 4th International Conference, ITP 2013, Rennes, France, July 22-26, 2013, Proceedings 4, pp. 35-50. Springer, 2013.
Guillaume Lample. Timothée Lacroix, Marie-Anne Lachaux, Aurélien Rodriguez, Amaury Hayat, Thibaut Lavril, Gabriel Ebner, and Xavier Martinet. Hypertree proof search for neural theorem proving. In Sanmi Koyejo, S. Mohamed, A. Agarwal, Danielle Belgrave, K. Cho, and A. Oh (eds.), Advances in Neural Information Processing Systems 35: Annual Conference Neural Information Processing Systems 2022, NeurlPS 2022, New Orleans, LA, USA, November 28 December 9, 2022, 2022. URL http: http://aapprs.eeee www.:errsnnissccccceoeee wwtppppppppppppeeectccceeeeeeeep files/ paaees//ppper/22//aallll .hmml
Lean Community. Completion of the liquid tensor experiment. blog post, 2022. URL https:
//1eanprover-comee cow.rntcoomiitttycm cow.muuit...gg.......//////ottte
Jannis Limperg and Asta Halkjær From. Aesop: White-box best-first proof search for lean. In Proceedings of the 12th ACM SIGPLAN International Conference on Certified Programs and Proofs, pp. 253-266, 2023.
Yong Lin, Shange Tang, Bohan Lyu, Jiayun Wu, Hongzhou Lin, Kaiyu Yang, Jia Li, Mengzhou Xia, Danqi Chen, Sanjeev Arora, et al. Goedel-prover. A frontier model for open-source automated theorem proving. arXiv preprint wrXiv:2502.07641 2025a.
Yong Lin, Shange Tang, Bohan Lyu, Ziran Yang, Jui-Hui Chung, Haoyu Zhao, Lai Jiang, Yihan Geng, Jiawei Ge, Jingruo Sun, al. poover-:: Scaling formal theorem proving with scaffolded data synthesis and self-correction. arXiv preprint arXiv:2508.03613. 2025b.
Minghai Lu, Benjamin Delaware, and Tianyi Zhang. Proof automation with large language models. In Vladimir Filkov, Baishakhi Ray, and Minghui Zhou (eds.), Proceedings of the 39th IEEE/ACM International Conference Automated Software Engineering, ASE 2024, Sacramento, CA, USA, October 27 November 1, 2024. pp. 1509-1520. ACM, 2024. doi: 10. (0.1145/3691220.3695555 URL http::ttt: httt:::://oai.ooo 1ttp///....0rr111..111.1//////10 1145/3691620 3695521
Jia Meng and Lawrence Paulson. Lightweight relevance filtering for machine -ecebine-geeerttedd resolution problems. Journal of Applied Logic, 711):41-57, 2009.
12

---

Published as a conference paper at ICLR 2026
Jia Meng, Claire Quigley, and Lawrence C. Paulson. Automation for interactive proof: First proto- type. Information and Computation, 204(10):1555- 1596, 2006. doi: https///bbiorg//1..110.... 2005.05.010.
Maciej Mikula, Szymon Tworkowski, Szymon Antoniak, Bartosz Piotrowski, Albert Q. Jiang, Jin Peng Zhou, Christian Szegedy, Lukasz Kuciñski, Piotr Mitos, and Yuhuai Wu. Mag- nushammer: A transformer-based approach to premise selection. In The Twelfth International Conference Learning Representations, 2024. URL http://///ppeeeeeeeneeteeeeeeeee oYjPkkmqAV
Tobias Nipkow, Lawrence C. Paulson, and Markus Wenzel. Isabelle/HOI. A Proof Assistant for Higher-Orles Logic. Springer, 2002. doi: 10. 00.1007/3-540455999..
Aaron van den Oord, Yazhe Li, and Oriol Vinyals. Representation learning with contrastive predic- tive coding. arXiv preprint 180.003887 2018.
Lawrence Charles Paulson and Jasmin Christian Blanchette. Three years of experience with Sledge- hammer, a practical link between automatic and interactive theorem provers. In /WIL LPAR, 2012. https//t:://ppp httpptpppppppp..ssaaaitscccoooot wwwantccscooolrr
org/ wrtg/orpussDDDDD :
Bartosz Piotrowski, Ramon Fernández Mir, and Edward Ayers. Machine-learned premise selee- tion for lean. In International Conference on Automated Reasoning with Analytic Tableaux and Related Methods, pp. 175-186. Springer, 2023.
Stanislas Polu, Jesse Michael Han, Kunhao Zheng, Mantas Baksys, Igor Babuschkin, and Ilya Sutskever. Formal mathematics statement curriculum learning. The Eleventh International Conference Learning Representattinns ICLR 2023, Kigali, Rwanda, May 1-5, 2023. OpenRe- view.net, 2023. URL
net wttprriiwwwee/fffroe wwt/tooumiide--Paaa... 8dmSh4
Yicheng Qian, Joshua Clune, Clark Barrett, and Jeremy Avigad. Lean-auto: An interface between lean 4 and automated theorem provers. In Lecture Notes in Computer Science, Lecture notes in computer science, pp. 175-196. Springer Nature Switzerland, Cham, 2025.
Nils Reimers and Iryna Gurevych. Sentence-bert: Sentence embeddings using siamese bert- networks. In Proceedings of the 2019 Conference Empirical Methods in Natural Language Processing. Association for Computational Linguistics, 11 2019. URL https://arxiv..or abs/1908. 10084
Stephan Schulz, Simon Cruanes, and Petar Vukmirović. Faster, higher, stronger: E 2.3. In Pascal Fontaine (ed.), Conference on Automated Deduction (CADE), pp. 495-507. Springer, 2019.
Peiyang Song, Kaiyu Yang, and Anima Anandkumar. Lean copilot: Large language models as copilots for theorem proving lean. arXiv preprini arXiv:2404. 12534, 2024.
Terence Tao. tour. blog post, 2023. URL https:: wordpress o http://rrsssoooo//////////////// wieiiiinnnttteereeee
Formalizing the proof of pfr in lean4 using blueprint: a short
Yicheng Tao, Haotian Liu, Shanwen Wang, and Hongteng Xu. Assisting mathematical formalization with a learning-based premise retriever. arXiv preprint arXiv:2501.1395) 2025.
The Mathlib Community. The lean mathematical library. In Jasmin Blanchette and Catalin Hriteu (eds.), Certified Programs and Proofs (CPP), pp. 367-381. ACM, 2020. doi: 10.134533372885. 3373824.
Floris van Doom, Patrick Massot, and Oliver Nash. Formalising the h-principle and sphere eversion. In Robbert Krebbers, Dmitriy Traytel, Brigitte Pientka, and Steve Zdancewic (eds.). Certified Programs and Proofs (CPP), pp. 121-134. ACM, 2023. doi: 10. 145/3573105.35556688
Petar Vukmirović, Alexander Bentkamp, Jasmin Blanchette, Simon Cruanes, Visa Nummelin, and Sophie Tourret. Making higher- superposition work. Journal of Automated Reasoning, 66: 541-564, 2022. doi: 10. 10010077118817--2--666661
13

---

Published as a conference paper at ICLR 2026
Haiming Wang, Huajian Xin, Chuanyang Zheng. Zhengying Liu, Qingxing Cao, Yinya Huang, Jing Xiong. Han Shi, Enze Xie, Jian Yin, Zhenguo Li, and Xiaodan Liang. Lego-prover: Neural theorem proving with growing libraries. In The Twelfth International Conference Learning Representations, ICIR 2024, Vienna, Austria, May 7-11, 2024. OpenReview.net, 2024. URL htttps://openreviex.. wwtp:e/eooooomdddddnllla...
Haiming Wang, Mert Unsal, Xiaohan Lin, Mantas Baksys, Junqi Liu, Marco Dos Santos, Flood Sung, Marina Vinyes, Zhenzhe Ying, Zekai Zhu, et al. Kimina-prov proverr preview: Towards large formal reasoning models with reinforcement learning. arXiv preprint arXiv:2504. 1354, 2025.
Zijian Wu, Suozhi Huang, Zhejian Zhou, Huaiyuan Ying, Jiayu Wang, Dahua Lin, and Kai Chen. Intern1m2. Internlm22.5sseeprrovee Advancing automated theorem proving via expert iteration large-scale lean problems. arXiv preprint arXiv:2410.15700 2024.
Huajian Xin, Daya Guo, Zhihong Shao, Zhizhou Ren, Qihao Zhu, Bo Liu, Chong Ruan, Wenda Li, and Xiaodan Liang. prepseek-prover: Advancing theorem proving in Ilms through large- scale synthetic data. CoRR. abs/2405. 14333, 2024a. doi: 0048850/ARXXI..445..4333 URL
https://doi. org/10 10. 48540/ arwiv 2405 14333
Huajian Xin, Z. Z. Ren, Junxiao Song. Zhihong Shao, Wanjia Zhao, Haocheng Wang, Bo Liu, Liyue Zhang, Xuan Lu, Qiushi Du, Wenjun Gao, Qihao Zhu, Dejian Yang, Zhibin Gou, Z. F. Wu, Fuli Luo, and Chong Ruan. Deepseck-prover-vv/ for reinforcement learning and monte-carlo tree search. CoRR. 0ww.22488.015522 2024b. doi: 10.48550/RRXI..2408.00 08152. URL (ttttss:::///oi org/10. 48111..5.0/11.1111 arXiv 2408 08152
Harnessing proof assistant feedback
Kaiyu Yang, Aidan Swope, Alex Gu, Rahul Chalamala, Peiyang Song, Shixing Yu, Saad Godil, Ryan Prenger, and Anima Anandkumar. LeanDojo: Theorem proving with eetrieval-augmennt language models. In Neural Information Processing Systems (NeurIPS), 2023.
Xueliang Zhao, Wenda Li, and Lingpeng Kong. Decomposing the enigma: Subgoal-based demon- stration learning for formal theorem proving. CoRR, abs/2305, 16366, 2023. doi: 10.48550/ ARXIV.2305.16366 https://:///do org/10. 48550/8r5iii 2305. 16366
Thomas Zhu, Joshua Clune, Jeremy Avigad, Albert Qiaochu Jiang, and Sean Welleck. Premise selection for a lean hammer, 2025. URL (ttpsttss:// www.iv.oog.................. wbs/abs/////oooooogo..ggo/..aaea abs 220.//5500.777777
14


Reviews:
[{"review_id": "SC32Q9pDXl", "reviewer": "Reviewer_cvrg", "summary": "The paper introduces LEANPREMISE, an LM-based premise selector tailored for use with a hammer in Lean’s dependent type theory, and integrates it with Aesop, Lean-auto (DTT to HOL translation to external ATPs), and Duper to build LEANHAMMER, \"the first end-to-end domain-general hammer for Lean.\" The selector standardizes premise/state serialization, trains with a masked contrastive objective, and dynamically incorporates user/local premises. On Mathlib and miniCTX-v2, the system improves proof rates over prior premise selectors and shows complementary behavior with MePo. The authors provide ablations and claim open-sourced code, data, and trained models.", "questions": "1. While “domain-general” within Lean, it’s unclear how easily the approach ports to other proof assistants like Rocq or Isabelle. A cross-assistant pilot (even small-scale or case-by-case) would strengthen the generality claim and offer insights for future work to extend the approach.\n\n2. In the “ground-truth premises” oracle runs, how many of those premises are actually required for the found proof vs. incidental? Could a minimal-premise oracle raise the theoretical ceiling?\n\n3. When users work in private libraries with heavy custom notations (even if you print fully-qualified constants), how often do premise embeddings drift enough to harm retrieval? Any quantitative OOD tests beyond miniCTX-v2?", "limitations": "", "rating": 6, "confidence": 4, "soundness": 3, "presentation": 3, "contribution": 2, "strengths": "1. Positions premise selection explicitly for a Lean hammer, not just for next-tactic generation, with hammer-aware data extraction (term + tactic proofs; collecting implicit simp/rw premises; signature normalization that avoids notation brittleness). This is a concrete, useful framing that, as far as I know, prior Lean premise selectors did not target.\n\n2. Dynamic augmentation with project-local premises and server-side caching for low-latency retrieval is practically novel for Lean users.\n\n3. Clear methodology for training: masked InfoNCE with explicit negatives; ablation shows each training choice (negatives, loss mask, data extraction) matters.\n\n4. If robust, first domain-general hammer for Lean is a meaningful community contribution, potentially changing day-to-day Lean workflows and enabling downstream NTP systems to \"call a hammer\" in Lean.", "weaknesses": "1. The paper retrains/ports baselines (e.g., MePo to Lean; ReProver on the authors’ splits) and changes data extraction relative to next-tactic systems; while understandable, this complicates strict novelty/efficacy attribution. It would be good to expand baseline re-implementation details and release scripts to reproduce exact comparison settings (hyperparameters, filters, blacklists) and the exact evaluation splits.\n\n2. Success depends on Lean-auto translation quality and Duper reconstruction once Zipperposition returns premises. It would be good to have more failure analyses, for example to provide breakdowns of (a) external ATP success vs. Duper reconstruction failure, (b) cases where Aesop premise applications alone succeed vs. Lean-auto is essential, and (c) how often missing implicit vs. explicit premises is the root cause.\n\n3. Filtering 479 \"basic logic\" theorems and aggressive fully-qualified, notation-free signatures are sensible, but please quantify how each filter/format affects recall, ATP success, and end-to-end proofs on a held-out set (beyond the aggregate ablation), and whether performance is brittle to Mathlib version changes.\n\n4. The reported metrics could be richer. For example, consider reporting proof length, number of premises used, and time-to-first-proof distributions, to understand proof mechanics, as well as the effect of k (and of per-step dynamic k) across problem difficulty buckets, etc.", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "", "claims_and_evidence": "", "methods_and_evaluation_criteria": "", "theoretical_claims": "", "experimental_designs_or_analyses": "", "relation_to_broader_scientific_literature": "", "essential_references_not_discussed": "", "other_strengths_and_weaknesses": "", "other_comments_or_suggestions": "", "questions_for_authors": "", "summary_of_paper": "", "summary_of_recommendation": "", "technical_quality": "", "clarity_of_presentation": "", "potential_impact": "", "robotics_focus": "", "quality_of_limitations": "", "questions_for_rebuttal": "", "reasons_to_accept": "", "reasons_to_reject": "", "questions_to_authors": "", "extra_scores": {}}, {"review_id": "C9eKODLkY1", "reviewer": "Reviewer_u2zP", "summary": "This paper introduces a novel premise selector, LeanPremise, tailored for premise selection for hammer use.\nThe authors fine-tune a textual encoder on carefully extracted (state, premise) data pairs with an InfoNCE-like loss, and rank premises based on embedding similarity. \nBy integrating LeanPremise with Aesop, Lean-auto and Duper, they also build a LeanHammer, which improves the accumulate proof rate from 27.5% (baseline, using MePo as the premise selector) to 33.3% on Mathlib-test. Notably, LeanHammer is currently accessible by simply using the corresponding tactic in Lean.", "questions": "1. I am most curious about whether implementing such a hammer to make use of external ATP/SMT solvers can help with LLM theorem provers. I will appreciate if the authors can provide some examples where the current open-weights SOTA models such as Goedel-Prover-V2-32B fail in pass@k(k=32 or so), but LeanHammer can help the model find a proof.\n\n2. Have you tried to add automation tactics other than simp_all, such as linarith, omega, native_decide, etc. into the pipeline? My experience is that these tactics can usually help solve goals that Aesop, simp_all and external ATPs cannot solve. I agree with that simp_all can not help improve further from Aesop.", "limitations": "", "rating": 4, "confidence": 3, "soundness": 3, "presentation": 2, "contribution": 2, "strengths": "Significance: This work fills the blank that there is no hammer tool (premise selection + translate to external language for ATP/SMT solver application + translate back) in Lean. The proposed LeanHammer tool is practical. It has been built as a tactic in Lean, and I personally have been using it for daily hands-on proofs.\n\nClarity: The pipelines of LeanHammer and LeanPremise are clearly stated. Details such as how to handle the signature are enough covered. \n\nQuality: The performance of LeanPremise is verified extensively on multiple datasets and various experimental settings, compared with many previous methods as baselines.\n\nOriginality: (1)The data extraction pipeline is tailored for hammer use in many details, such as using all premises for the current goal rather than only for the next tactic. (2)  The use of InfoNCE loss for training the LeanPremise encoder, instead of binary-class MSE loss used by ReProver, is quite reasonable. (3) The LeanHammer pipeline not only makes use of current strong tools such as Aesop and external theorem provers like Zipperposition, and also alllows for adding additional automation tactics in the future as a rule of Aesop.", "weaknesses": "1. The conceptual novelty of this work is limited. The overall design of LeanHammer mainly follows that of the Sledgehammer in Isabelle, and the LeanPremise is a standard embedding similarity based retrieval method, similar to what ReProver does. The contribution is mainly engineering rather than methodological.\n2. The writing of the paper should be further checked. There are typos and confusing statements that could harm the understanding of the paper. For example, on page 6, $p_{i}^{+}$ should be changed to $p_{i}^{-}$ in the sum for negative premises in the denominator in the loss function expression, and the definition $$\\mathcal{N}_{i}=\\{p_{i}^{+}\\}_{i}\\cup\\{p_{ij}^{-}\\}_{ij}\\setminus\\mathcal{P}_{s_{i}}^{+}$$ should be simplified to $\\{p_{ij}^-\\}_{j=1}^{B^-}$ directly. \n3. The final performance achieved by LeanHammer is not that impressible compared to the performance of today's LLM theorem provers. On miniCTX-v2, the current SOTA Seed-Prover(light mode) can prove 81.8% of the theorems without accessing any external ATP/SMT solvers. In contrast, LeanHammer could only achieve 26.1% even with ground truth premises, let alone the 20.7% using LeanPremise.", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "", "claims_and_evidence": "", "methods_and_evaluation_criteria": "", "theoretical_claims": "", "experimental_designs_or_analyses": "", "relation_to_broader_scientific_literature": "", "essential_references_not_discussed": "", "other_strengths_and_weaknesses": "", "other_comments_or_suggestions": "", "questions_for_authors": "", "summary_of_paper": "", "summary_of_recommendation": "", "technical_quality": "", "clarity_of_presentation": "", "potential_impact": "", "robotics_focus": "", "quality_of_limitations": "", "questions_for_rebuttal": "", "reasons_to_accept": "", "reasons_to_reject": "", "questions_to_authors": "", "extra_scores": {}}, {"review_id": "EyoBFzoubG", "reviewer": "Reviewer_rKRM", "summary": "The paper introduces LEANPREMISE, a learned premise retriever for Lean, and integrates it into LEANHAMMER, an automated “hammer” tactic for Lean. The system retrieves relevant lemmas, translates to higher-order logic, calls ATPs, and reconstructs proofs back in Lean. The authors claim this is the first practical, general-purpose Lean hammer that normal Lean users can call. They train LEANPREMISE on hammer-style data (including implicit premises and both tactic/term proofs), and show strong gains on Mathlib and an out-of-distribution benchmark (miniCTX-v2), with substantially higher recall and proof rates than baselines like MePo or ReProver.", "questions": "How robust is LEANHAMMER to hallucinated lemmas (names that don’t exist)? Do they just get ignored like harmless false positives?\n\nWhat exact hardware produced the reported latencies, and how does latency scale with many user-defined lemmas?\n\nFor hard miniCTX-v2 splits, what is the main blocker: retrieval, ATP search, or Lean reconstruction?", "limitations": "", "rating": 8, "confidence": 3, "soundness": 3, "presentation": 3, "contribution": 3, "strengths": "1. The pipeline design is careful and realistic for Lean’s dependent type theory. The data extraction method (capturing all premises truly used in a proof state, not just the next tactic) is well motivated, and ablations support it. The system also supports dynamically including a user’s local lemmas at inference time via FAISS indexing.\n\n2. LEANPREMISE achieves much higher recall@32 (≈70%+) than MePo and ReProver, and when plugged into LEANHAMMER, proof rates jump from ~20–27% (baselines) toward ~33%+ for Mathlib-test, and near 40% with ensembles. It also transfers to miniCTX-v2, suggesting generalization beyond Mathlib.\n\n3. A turnkey hammer for Lean is genuinely impactful for interactive theorem proving and AI-for-math. The work is clearly written, includes ablations, and promises to release code, data, and models.", "weaknesses": "1. The paper does not compare against a simple LLM as premise suggester baseline: prompt a modern LLM with the Lean goal and ask it to list ~32 relevant lemmas from Mathlib, then feed those to the same hammer. Because the hammer mainly needs high recall and tolerates many irrelevant premises, this is an important baseline. It would clarify how much LEANPREMISE beats “just ask an LLM.”\n\n2. Some miniCTX-v2 domains are still barely solved, and it would help to briefly analyze where the pipeline fails (missing premises vs. reconstruction failures).", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "", "claims_and_evidence": "", "methods_and_evaluation_criteria": "", "theoretical_claims": "", "experimental_designs_or_analyses": "", "relation_to_broader_scientific_literature": "", "essential_references_not_discussed": "", "other_strengths_and_weaknesses": "", "other_comments_or_suggestions": "", "questions_for_authors": "", "summary_of_paper": "", "summary_of_recommendation": "", "technical_quality": "", "clarity_of_presentation": "", "potential_impact": "", "robotics_focus": "", "quality_of_limitations": "", "questions_for_rebuttal": "", "reasons_to_accept": "", "reasons_to_reject": "", "questions_to_authors": "", "extra_scores": {}}, {"review_id": "6i7bYedYdZ", "reviewer": "Reviewer_XPxN", "summary": "I think this is a well-written and impactful paper that makes a meaningful contribution to the growing intersection between neural methods and formal theorem proving. The authors present LeanHammer, an end-to-end system for automated reasoning in the Lean proof assistant that combines a new neural premise selection model (LeanPremise) with existing components for translation and proof reconstruction. The central innovation lies in designing LeanPremise specifically for dependent type theory, and in showing that it can dynamically adapt to user-specific contexts including both large existing libraries and locally defined lemmas. This is a significant advance over prior premise selection systems for Lean, which were often static or trained on limited corpora.\n\nEmpirically, the paper is strong. The authors demonstrate that LeanPremise enables LeanHammer to solve 21% more goals compared to existing premise selectors, and that it generalizes effectively across diverse mathematical domains. I found the experiments to be thorough and convincing, and the evaluation metrics appropriate for the problem setting.", "questions": "1. I really liked that LeanPremise can incorporate locally defined facts at runtime. Could the authors clarify how new lemmas are embedded on-the-fly? For example, are these signatures tokenized and passed through the encoder server dynamically, or is there a cached retriever that updates incrementally?\n\n2. Did the authors explore hybrid ranking (e.g., mixing similarity-based and logic-based retrieval) or reinforcement-based refinement of premise scores?\n\n3. The paper describes four hammer variants (aesop, auto, aesop+auto, full). In practice, how sensitive is LeanHammer’s success rate to the choice of variant and to timeout parameters (e.g., 10 s for Zipperposition)? Would adaptive scheduling of these variants yield further gains?", "limitations": "", "rating": 8, "confidence": 5, "soundness": 4, "presentation": 3, "contribution": 3, "strengths": "Strengths:\n\nClear Motivation and Novelty: The paper is well-motivated in the broader context of neuro-symbolic reasoning. The idea of combining neural retrieval (premise selection) with symbolic reasoning (hammer backends) is well-established in Isabelle and Coq, but its extension to dependent type theory in Lean is non-trivial and timely.\n\nPractical Integration: I appreciate that the authors actually built an integrated hammer for Lean! Something the community has wanted for years. The engineering effort here is nontrivial and valuable.\n\nAdaptive Context Handling: The dynamic adaptation to local user contexts is, in my view, one of the paper’s most important contributions. It shows a genuine understanding of how theorem proving workflows operate in practice.\n\nStrong Empirical Results: The 21% improvement in goal-solving rate is not just statistically significant — it’s practically meaningful. The ablation and generalization studies make a solid case for the effectiveness of LeanPremise.\n\nClarity and Presentation: The writing is clear, structured, and accessible even to readers not deeply familiar with Lean. The paper situates itself well within the literature on neural premise selection and hammer systems.", "weaknesses": "Some minor weaknesses that i thought\n\n1. Model Details and Reproducibility: While the authors provide a solid description of the LEANPREMISE training pipeline, the architecture details of the encoder model (layer sizes, tokenization, embedding pooling, etc.) are somewhat brief. The training section mentions that they fine-tune MiniLM and DistilRoBERTa models, but additional detail on input formatting or tokenizer alignment with Lean syntax would help others reproduce or extend this work.\n\n2. Limited Discussion of Failure Cases: The experiments are comprehensive, but it would strengthen the paper to include more qualitative analysis of where the hammer fails e.g., typical patterns of unsuccessful proofs, sensitivity to theorem complexity, or when external provers (like Zipperposition) fail to reconstruct. Understanding these limits could guide future improvements to both premise selection and proof reconstruction.", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "", "claims_and_evidence": "", "methods_and_evaluation_criteria": "", "theoretical_claims": "", "experimental_designs_or_analyses": "", "relation_to_broader_scientific_literature": "", "essential_references_not_discussed": "", "other_strengths_and_weaknesses": "", "other_comments_or_suggestions": "", "questions_for_authors": "", "summary_of_paper": "", "summary_of_recommendation": "", "technical_quality": "", "clarity_of_presentation": "", "potential_impact": "", "robotics_focus": "", "quality_of_limitations": "", "questions_for_rebuttal": "", "reasons_to_accept": "", "reasons_to_reject": "", "questions_to_authors": "", "extra_scores": {}}]

Author rebuttal:

Decision: Accept (Oral)