Lean Finder: Semantic Search for Mathlib That Understands User Intents
Authors: Jialin Lu
Kye Emond
Kaiyu Yang
Swarat Chaudhuri
Weiran Sun
Wuyang Chen
Venue: ICLR 2026 Poster (2026)
Keywords: Lean
mathlib
code search
informalization
Primary area: other topics in machine learning (i.e., none of the above)
TL;DR: We present Lean Finder, a semantic search engine for Lean and mathlib that understands and aligns with the intents of mathematicians.

Abstract: We present Lean Finder, a semantic search engine for Lean and mathlib that understands and aligns with the intents of mathematicians. Progress in formal theorem proving is often hindered by the difficulty of locating relevant theorems and the steep learning curve of the Lean 4 language, making advancement slow and labor-intensive. Existing Lean search engines, though helpful, rely primarily on informalizations (natural language translation of the formal statements), while largely overlooking the mismatch with real-world user queries. In contrast, we propose a user-centered semantic search tailored to the needs of mathematicians. Our approach begins by analyzing and clustering the semantics of public Lean discussions, then fine-tuning text embeddings on synthesized queries that emulate user intents. We further align Lean Finder with mathematicians’ preferences using diverse feedback signals, encoding it with a rich awareness of their goals from multiple perspectives. Evaluations on real-world queries, informalized statements, and proof states demonstrate that our Lean Finder achieves over 30% relative improvement compared to previous search engines and GPT-4o. In addition, Lean Finder is compatible with LLM-based theorem provers, bridging retrieval with formal reasoning. Lean Finder is available at: https://leanfinder.github.io.

Published as a conference paper at ICLR 2026
LEAN FINDER: SEMANTIC SEARCH FOR MATHLIB THAT UNDERSTANDS USER INTENTS
Jialin Lu', Kye Emond?, Kaiyu Yang" Swarat Chaudhuri', Weiran Sun', Wuyang Chen' Simon Fraser University Uniierriity of Waterloo SIndependent Researcher
University of Texas at Austin
ABSTRACT
We present Lean Finder, a semantic search engine for Lean and mathlib that understands and aligns with the intents of mathematicians. Progress in formal theorem proving is often hindered by the difficulty of locating relevant theorems and the steep learning curve of the Lean language, making advancement slow and labor-intensive. Existing Lean search engines, though helpful, rely primarily informalizations (natural language translation of the formal statements), while largely overlooking the mismatch with real-world user queries. In contrast, we propose user-centered semantic search tailored the needs of mathematicians. Our approach begins by analyzing and clustering the semantics of public Lean discussions, then fine-tuning text embeddings on synthesized queries that emulate user intents. We further align Lean Finder with mathematicians' preferences using diverse feedback signals, encoding it with a rich awareness of their goals from multiple perspectives. Evaluations real-world queries, informalized statements, and proof states demonstrate that our Lean Finder achieves over 30% relative improvement compared to previous search engines and GPT-4o. In addition, Lean Finder is compatible with LLM-based theorem provers, bridging retrieval with formal reasoning. Lean Finder is available httpp::/leantf. /tte://eeannnneeeee inder
github. io
INTRODUCTION
Advances in Lean and mathlib (De Moura al. 2015 Moura Ulirich| 2021) are turning mathe- matical discovery into collaborative and verifiable research workflow. On this foundation, provers
powered by large language models (LLMs) have sprinted ahead (AlphaProof & teams 2024 Xin
2024a by Ren et al. 2025 Lin et al. 2025a). Parallel progress in autoformalization has shifted from hrnttwritten grammars to few-shot LLM translation, and large corpora generated through
al.
back tracklarnnl Lean code ("informaiization" have bootstrapped even stronger translators (Wu et al.
2022
Jiang et al. 2024 Lu et al. 2024).
Despite these advances, state-of-the-art LLMs still cannot solve math research problems. This underscores the continued need for substantial human efforts, which unfortunately remain slow and labor-intensive for two bottlenecks. First, locating the right theorem is frustrating: search tools are rudimentary, naming conventions are often inconsistent (Zulip) 202 (020b), and high-quality Lean examples remain scarce. Moreover, as we will demonstrate in our experiments (Table 2 identifying the correct theorem is challenging not only for humans, but also for state-of ofiee--f-hhearrrr art LLMs. Second, Lean's 's syntax, grammar, and tactics incur steep learning curve. Even veteran mathematicians and experienced programmers regularly report difficulties when writing Lean (Zulip, 2021a 2020a). To facilitate mathematicians, semantic search is vital to Lean formalization and theorem proving. Recent search engines take informal statements live proof states and retrieve mathlib4 lemmas or tactic suggestions, thereby aiding human Lean users (Gao et al. 2024a Tao et al. 2025aa] Shen et al.
2025 Ju & Dong 2025 Asher 2025). However, these search engines target machine translation
rather than human use. They "informalize" statements from a supposedly neutral viewpoint, whereas
real users bring inherent bias, typically seeking explanations from their specific perspective.
Consider the two queries below. The first is an informalization of formal statement that current
Lean search engines handle (Gao et al. 2024a Ju & Dong 2025 Asher 2025):

---

Published as a conference paper at ICLR 2026
Lean Finder
81.6% Upvote by mathematician
Figure In evaluation with user queries, users preferred Lean Finder 81.6% of cases, compared with 56.9% for Lean Search Gao et al. (2024a) and 54.1% for GPT-4o.
Query Denote L/K a field extension, 2,y L are algebraic elements over K with the same minimal polynomial. Then the K-algebra isomorphism algEquiv between the simple field extensions K(x) and K(y) maps the generator of ((x) to the generator of K(y), i.e., alg y-
Target Statement 1:
theorem Desiquiv_apllyy (x L) (hx : IsAlgebraic K x) (h_mp minpoly K = minpoly K y) algEquiv hx h_ (AdjoinSimple.co K AdjoinSimple.ge
proof omitted for brevity
However, human query practice may look like:
I'm working with algebraic elements over field extension and have two elements, say æ and y in L. know is algebraic over K, and I've ve shown that y is a root of the minimal polynomial of z. Does this imply that the minimal polynomials of and are actually equal?
Query 2:
Target Statement 2:
theorem of root (x y L) (hx : IsAlgebraic X x) (b_ev yolymorial solynoiial.aeval proof omitted for brevity
mpoly K x) - 0) minpoly K y = minpoly K
Although both queries involve similar mathematical context (algebraic elements x, y in field extension L/K and their minimal polynomials), they have different concerns: the first asserts an isomorphism between field extensions (generated by two algebraic elements with the same minimal polynomial), whereas the second seeks to decide whether the two minimal polynomials are equal from the fact that y root of r's minimal polynomial. This user latent (motivation, perspective, abstraction) cannot be inferred or encoded by a purely syntactic informalization. Addressing this challenge calls for Lean search engines that can understand a mathematician' 's intent, not merely surface-level matches. We defer more rigorous analysis in Section 2.2 and ask our core question:
How to make the Lean search engine user-centered and tailored to understand the intents and needs of working mathematicians?
In this paper, we aim to build search engine for Lean and mathlib4 that captures the diverse intents of mathematicians. Our approach analyzes and clusters public discussions, then synthesizes queries that simulate user intents (Section 3.1). We incorporate Lean code from wide variety of sources, and support multiple input types such as informalizations and proof states (Section (3.2). With the diverse data, we fine-tune LLM embeddings to achieve both strong retrieval performance and alignment with user preferences (Section 3.3). Lean Finder is extensively evaluated on different input types and real user queries (Section Section 4.2). It is released as a web service (Figure X) to support mathematicians coding in Lean. Finally, Lean Finder is compatible with -LM-based theorem provers via prover-agnostic retrievals, serving as a plug-and-play tool to boost prover performance without retraining (Section 4.3).
We summarize our contributions below:
When evaluating on real-world queries by real users, our Lean Finder is upvoted 81.6% compared to 56.9% from Lean Search (Gao et al. 2025) and 54.1% 1.1% from GPT-4o in an LMArena-style test (Chiang et al. 2024).
Lean Finder outperforms GPT-4o and other Lean search engines, achieving 30%+ and 16%+ relative gains (Recall @ 1) when queried with informalized statements and proof states, respectively.
WWe synthesized this "Query 2" (see Section 3.1 concerns (Section N
we do not release any real user queries due to privacy
2

---

Published as a conference paper at ICLR 2026
3. Lean Finder also boost the performance of LLM-based provers via in-context retrieval augmentation, making it prover-agnostic retrieval model.
We release the largest code search dataset for Lean repositories, consisting of over 1.4M query- code pairs (582,102 synthesized user queries, 244,521 informalized statements, 337,647 proof states, and 244,521 formal statements).
2
MOTIVATION
2.1 BACKGROUND; SEARCH ENGINE FOR LEAN AND MATHLIB
Lean (De Moura et al. 2015 Moura & Ullrich 2021) an interactive theorem prover based on dependent type theory, with community-run library (mathlib4) containing over 230k theorems and 10k definitions. This offers far more "entry points" than typical programming platforms (Python exposes 89 built-in functions; C++ standard library has 105 headers). Finding the right lemma in this vast library is difficult: existing tools like #find, library _search, and Loogle depend on exact names or goal states and often fail when namiig conventions drift or examples are sparse. Recent LLM-based search engines (ao et al., 2024a b, Yang et al. 2023 Tao et al. 2025a Shen et al. 2025) Ju Dong 2025 Asher 2025: Zhu et al., 2005) embed informal queries or proof goals, but remain optimized for embedding similarity rather than the nuanced, shifting intents of mathematicians. In short, sheer library scale and rudimentary search together make locating lemmas first-order pain point, even before one tackles Lean's non-trivial syntax and tactic language.
2.2 CURRENT SEARCH ENGINES MISALIGNED WITH MATIIEMATICAANS NEEDS
Informalized Statement
Synthetic User Query (Ours)
Real User Query (Zulip. GitHub)
Figure 2: PCA of Lean/mathlib-relln queries from different sources. Our synthesized user query (orange, Section 3.1) aligns more closely with real queries (green). whereas direct informalization (Gao et al, 2024b) (blue) shows distributional deviations. Real user queries are from Zulip and GitHub.
Despite notable progress, current Lean search engines are optimized for informalized statements, instead of questions mathematicians actually pose. Most systems embed informal descriptions (natural languages) of statements or proof states, together with possible context or dependencies, then retrieve matching lemmas (Yang et al.) 2023] Gao et al. [2024a] b) Tao et al. 2025a Shen et al. (025). Because these informalizations are generated by LLMS rather than user logs, we have no guarantee that their wording, granularity, and purpose align with the queries real Lean practitioners type. This unexamined domain gap between L.LMs' informalizations and authentic human queries has so far been largely ignored, leaving retrieval systems potentially over-tuned to deviated distributions.
To justify this domain gap, we use PCA to visualize distributions of different query embeddings generated by all-MiniLL--L6-22 (Wang et al.) 2020). As shown in Figure 2 the cluster of LLM- generated informalizations (blue) only spans over a subspace of the cluster by queries collected from Zulip and Github (green), highlighting clear domain gap between real user queries and surrogate ones on which current Lean search engines are trained. By contrast, embeddings of our synthesized user queries in orange (Section 3.1 are much more aligned with the human cluster, suggesting that they better capture the practical needs of mathematicians coding in Lean.
htttps://oogllc..anlllag
3

---

Published as a conference paper at ICLR 2026
3 LEAN FINDER: DATA SYNTHESIS, CODE SEARCH, HUMAN ALIGNMENT
3.1
UIEERCENTERRED QUERY SYNTHESIS
Section 2.2 underscores that effective Lean retrieval for mathematicians requires authentic user queries, yet assembling such data scale is obstructed by two bottlenecks:
1. The volume of publicly available Lean questions by real users is tiny (for example, are only able to fetch 693 answerable user queries from Zulip/GitHub), which is orders of magnitude smaller than the billions-token corpora consumed by modern L.Mss;
Even with real user queries, tracing the precise answer (formal statement) that eventually resolves each query is infeasible, due to open math problems and evolving Lean/mathlib4 development.
Therefore, preparing a large fully annotated set of genuine user queries is unrealistic. Instead, we propose novel reverse strategy synthesize a large amount of diverse and realistic queries, as overviewed in Figure [ The core idea is: based on different perspectives that mathematicians ask Lean/mathlib4-relate questions (Section 3.1.Ip, we prompt LLM generation simulate mathemati- cians' intents (Section 3.1.2..
Post Processing
Sources of Formal Statements
Informalize, extract proof states
N iv
Sec. 3.2)
Real User Queries
Formel Stalemants
GitHub
Z Zulpp
Informaliao and
Secc
Statemacto.
Augmerted Prool
Discussions
(Sec 3.1.1)
(Scc 3.1
Synthetic User Quertts
Training Data for Lean Finder
t Real Queries Mithermticiaee
Semantic Clustering Analyze intents
'Reverse Engineering' Synthesize queries from different intents
Synthetic User Queries
Figure 3: We synthesize user queries part of our training data. First, analyze the semantics of public Lean/mathlib queries posted by real mathematicians and cluster them into intents (Section
These intents then prompt the generation synthetic user queries from formal Lean statements collected Trom mathlib, GitHuu, and research papers (Section [3.122) The synthesized user queries form the core part of our training data for our Lean Finder. To generalize Lean Finder across diverse inputs. we further include additional modalities (formal/informal statements and proof states, see Sections 3.2) extracted from formal Lean statements.
3.1.1 SEMANTIC ANALYSIS OF REAL HUMAN QUERY
The first step for user query synthesis is to systematically collect real user discussions, and then analyze the diverse semantics and intents mathematicians coding in Lean.
Collect User Discussions. To achieve this semantic analysis, we utilize Lean Zulip Cha the primary discussion forum for Lean, as well as GitHub, as the main sources of real-world queries. We use the Zulip API to extract high-quality discussions from five active and thematically rich channels (new members, lean4, mathlib4, Is there code for X, metapprogramminn/aatiio up to the first five user messages, which typically capture the core query. We then prompt GPT-4o (Appendix (.2) to filter for questions answerable by Lean statements and paraphrase the main query articulated in the messages. This process yields 693 real user discussions from Zulip and Githut")
retaining
Cluster User Intents. Mathematicians may ask Lean/mathiib4-elltee questions from different perspectives (see examples in Section I aan our analysis in Figure therefore we need to identify the distinct types of queries collected from Zulip/Github. We first prompt OpenAl o3 to bootstrap the initial set of clusters from a subset of collected queries. Then, the same model is fed with more user discussions and is prompted iteratively update existing clusters or introduce new clusters necessary.
hhttss//eenprroeezzllpph...cm
*Due privacy concerns, we do release either Zulip GitHub collections.
4

---

Published as a conference paper at ICLR 2026
Table Five clusters of mathematicians" intents categorized from our collections of real user queries from Zulip GitHub.
Intent Clus-
Semantic Definition
Examples
ter
Scarching
Whether a definition, data-structure implementation, lemma, or theorem already available in Math- lib/Lcan, or if there is an easy way to get the desired statement.
"Is there code for "Do a lemma which Where can find
"Do we have ...". "Is there
for existing code lem-
mas
Meta- tactic- pro- gramming questions
Questions about Lcan mecaprogrammmin:: writing tactics or elaborators, creating macros, manipulating Expr or environments, controlling metavariables, interacting with simp"''acsop ""omega" from meta
"Why docsn't the code give an crror about a cy- cle existing when using Lean. M Varld.ass assign" "Is there way to make my first approach work to get Exp out of Q(Exp) using expr% macro?"
code.
Type-class, instance, axiom
Proofs fail, or definitions cannot he written hecause Lean cannot find (or should not use) certain type- class instances, or users need advice on construct- ing/avoiding such instances and on the correct logi- cal meaning of such instances.
"How to define or derive instances...", "Why certain instance-scarde problems happen...". "Whether particular instances should exist at all..."
Proof engi- neering & everyday
Concrete goals or failing scripts uround practical. day-to-day proof writing in Lean.
How to: finish or shorten proofs, make simp. rw, omega, linarith, etc, succeed, rewrite or unfold expressions, handle coercions and subtypes, ma- nipulate logicul connectives (F, 3, A, V). pattern- match over inductives, or split cases.
Lean usage
Library design
Conversations that concern the construction of large-
"How can I apply the co Yoneda Jemma or den- sity theorem to simplicial sets valued in an arhi- trary universe without restricting the variable?"
scale statements: proposing new mathemattcal struc- tures or tactics, refactoring existing ones, perfor- mance trade-offs, big formalizations theorems.
large-scale formaliza-
See Appendix 0.3 and Appendix O.4 for the prompts. This process results five distinct and semantically meaningful clusters of queries, as shown Table capturing comprehensive range of intents from which mathematicians ask about Lean/mathlib4.
3.1.2 QUERY SYNTHESIS WITH USER INTENTS
Based on semantic clusters of real queries in Table I we synthesize large-scale dataset of queries simulating diverse user intents. Although it typically challenging to resolve a query with precise formal statements in Lean, we can still reversely synthesize the query, instead of the ground truth. Specifically, we assume each formal Lean/mathlib4 statement could be the true answer to some unknown user queries, and now the key is to simulate queries with realistic user intents.
aim to instruct the LLM to generate plausible user queries that align with the specified cluster's perspective while remaining grounded in the given formal content. To avoid forcing every statement into all intent clusters, we adopt a two-step procedure. First, we prompt GPT-4o to analyze the given Lean statement and determine which query clusters from Table arre applicable. This filtering step ensures that only semantically meaningful queries are generated, avoiding unnatural cases where a statement. Second, for each selected cluster, prompt GPT-4o with rich context information (e.g. Yormal/informal Lean statement, cluster information) to synthesize the queries. See Appendix 0.5 our prompt. This procedure yields total of 582102 synthetic queries distributed across five distinct intent clusters, enabling fine-tuning of embedding models to better meet mathematicians' needs on Lean search.
cluster is irrelevant
We visualize the distribution of clusters in synthetic user queries in Figure (a).
3.2 THE LARGEST CODE SEARCH DATASET FOR LEAN REPOSITORIES
Beyond the synthesized user queries discussed above, we additionally incorporate the following data sources and modalities, releasing the largest code search dataset for Lean and mathlib4.
Research-driven Data Collection. While mathlib4 is the main source of formal statements for Lean, it does not capture the full breadth formal mathematics. To address this, we expand beyond mathlib4 and include GitHub repositories linked to recent research papers and domain-specific
5

---

Published as a conference paper at ICLR 2026
Library Metaprogramming Design
Formal Statements
Type-dees/instanne
2
Issues
17%
Synthetic
81%
Proof Engineering
Informalized Statement
17%
User Queries
24%
Augmented Froot States
(a) Distribution of clusters in synthetic user queries.
(b) Distribution of input modalities.
Figure 4: Distribution of our training dataset. (a) At fine granularity. our synthetic user queries distribute across five clusters of user intents (identified in Section 3.I.I). This distribution also aligns with the weekly popularity trends of relevant channels Lean Zulip Chat (Appendix [B.S]. For detailed descriptions and examples of clusters, see Table D (b) Overall, our dataset contains a total of 1.4M pairs queries and formal Lean statements, distributed across four input modalities.
libraries. This ensures our search engine is trained on diverse, up-to-date statements that reflect both everyday Lean practice and cutting-edge math research. See Appendix [.I for the detailed sources of our formal Lean statements.
Informalization. To support retrievals by both informalized statements and the generation of synthetic user queries (Section 3.1.2). we convert formal Lean statements into natural language descriptions. Inspired by Herald (Gao et al. 2024b), for each Lean statement, we provide rich context information for GPT-4o to better understand the Lean statement and provide good quality informal- ization. The context includes information like dependent statements, related statements, neighbor statements, along with their informalization. See Appendix B.3 for details about informalizations.
Other Input Modalities. To better capture intent, introduce augmented Lean proof states, which enrich a Lean proof state (subgoals with context and target) by describing the intended direction of progress. These descriptions are synthetically generated from Lean proofs with GPT-4o, providing natural explanations of proof transitions that mirror how users query the system when searching for applicable lemmas, enabling more fine-gras gra-gre retrieval (see Appendix [B.4 for details). We also include formal statements, which retain only the declaration without the proof body, supporting cases where users recall a statement only partially or seek semantically similar ones. Lean Finder can thus retrieve relevant statements even from imprecise inputs. We visualize the distribution of input modalities in Figure 4 (b). More statistics about our training data are summarized Appendix B.2
3.3 TRAINING LEAN FINDER WITH CODE SEARCH
We train our code search model, Lean Finder, with a two-stage pipeline (Figure In the first stage, employ contrastive learning objective to establish general alignment between queries of diverse input modalities and formal Lean statements (Section (.3.II. In the second stage, we incorporate user votes collected via our web service, along with auxiliary feedback from LLMs, further refine Lean Finder, aligning retrieval more closely with mathematicians" actual preferences (Section 3.3.2
3.3.1 CONTRASTIVE LEARNING FOR LEAN CODE SEARCH
We adopt DeepSeck- SrepSeek-Prover-Viee Prover-V1.5-PP 7B (Xin et al. 2024b) the base model for fine-tuning, for its extensive training on Lean 4 syntax and theorem proving tasks.
As decoder-only architecture, only the final token in each sequence has access the full context due to the causal atfentttnnion. Therefore, we extract the final hidden state of the last token in the last decoder layer to embed the entire sequence. The model is fine-ture tunet with contrastive loss "informal query qi formal code oj pairs, which aims to align the embeddings matching pairs in shared embedding space.

---

Published as a conference paper at ICLR 2026
Preference Data
Model
Model
Model
Model
Base Model
Lean Finder
3.3.1)
Contrastive Learning
+ Formal Statements
A/B lests
Up/Down voles (retrieval-leve)
(Sec 3.3.2)
(model-level)
Informalized
RLHF
Augmented Proof States
Synthalic User
Quaries
Query-Code Pairs
Figure 5: Lean Finder training pipeline. We first fine-tune the base LLM with contrastive learning Wang 2023) on four input modalitics in our training datasct (Figure 4 synthetic queries, informalized statements, augmented proof states, and formal statements) to build a strong retrieval model for Lean (Section 3.3.1 We then deploy Lean Finder web service and collect real users' retrieval preferences, which serve as human feedback. These preferences used further improve Lean Finder via Direct Preference Optimization (DPO (Rafailov al. 2024). Section 3.3.2). resulting a human-aligned boosted Lean Finder.
Training data and in-batch negatives. We construct sample groups of size G. For each query qi we pair one ground-truth Lean statement cf and attach G negatives [ drawn from the statement corpus. With batch size B, a training batch contains such groups, yielding the candidate code
B ULG
C. = I
12 with |c| B.
i=1
For given query ge, we apply token-level augmentation to obtain di enhancing robustness noisy or partial queries (e.g.. misspellings or incomplete recollection), and we treat all codes in C, except its paired positive o, as negatives; thus the number of negatives per query is B G combining intra-group negatives and code from all other groups (in-batch negatives).
Contrastive Loss. Let denote temperature. We optimize the contrastive loss over in-batch candidates, where Sim(.,) is the cosine similarity between two embeddings:
exp(Sim(@,, )/7)
Leontrastive
Σ log
exp(Sim(q: c)/T)
nECs
3.3.2 PREFERENCE ALIGNMENT
After initial training, Lean Finder shows strong retrieval performance across input modalities. To further adapt to real user needs, we deployed it as a web service where users can provide feedback retrieval results. We align the retriever with these preferences using Direct Preference Optimization (DPO) RRfailov et al. 2024).
Preference data. Our preference dataset P {(p,, of , })) consists of triplets where y is user query and ct,c c denote a chosen and rejected Lean statement, respectively. It is built from a unique combination of user and LLM feedback. We collect preferences two hierarchical levels. First, individual retrievals are explicitly upvoted or downvoted by users on our web service. Second, blinded model-wise preferences between Lean Finder and Lean Search (Gao al., 2024a) are obtained both from users' online selections (see Figure 99) and from retrievals of real community queries on Lean Zulip, judged by GPT-4o. This design blends direct human feedback with L.Lee evaluations, and yields high-quality and heterogeneous resource of 1154 triplets for aligning with user preferences. See Appendix for more details.
DPO fine-tuning, We adapt the original DPO objective (Rafailov et al. 2024 to retrieval, by replacing sequence likelihoods with probabilities defined over candidate statements. computed from query-code similarity scores. Let denote the current retriever (policy) and 0.o denote the reference
7

---

The adapted DPO objective for retrieval is Published as a conference paper at ICLR 2026
retriever obtained from initial contrastive training. simplified
LDPO -Big. iaaeceeTiio jop (o
Si (Simo (9, Sima (g.
where a is the sigmoid function and controls the deviation of the model from the reference. To prevent large degradation of general retrieval performance, we jointly train with the contrastive loss Ccontrative defined in Section Let À represent the weight given to contrastive loss, the fine-tuning objective for this stage becomes
C LDPO conttrastvve
EXPERIMENTS
Our data collection pipeline involves the OpenAl API, and our configurations are shown in Ap- pendix C Our training settings are in Appendix D
Our experiments primarily compare Lean Finder with other Lean search engines across different input modalities, with particular emphasis user-centered queries reflecting mathematicians' intents. In Section 4.1 we evaluate retrieval performance across input modalities, followed by a user study on real queries in Section 4.2 Section 4.3 explores explorrs Lean Finder as retrieval backbone for LLM-based
provers, and Appendix K reports ablation studies on the impact of preference alignment and using synthetic queries in training. Appendix preports comparisons with additional baselines such as Lean
Explore (Asher 2025 and Qwen3-Embedding--e (Zhang et al. 2025).
4.1 LEAN FINDER DEMONSTRATES STRONG RETRIEVAL PERFORMANCE
To evaluate the performance of our Lean Finder across different inputs, we compare it against recent search engines that support corresponding modalities. For the input modalities of informalized statement, synthetic user query, and formal statement, we compare with Lean Scarch [Gao et al. 2024a b) and GPT-4o. For proof state input, we compare with Lean State Search Tao al. 2025b Real Prover Search (Shen et al. 2025), and GPT-4o.
Metrics.
We assess retrieval performance using the following metrics, both are higher the better:
Recall@K: K: This measures the proportion of relevant results within the top K retrieved results.
Mean Reciprocal Rank (MRR): Computes the mean of the reciprocals of the first relevant result's rank across N queries: MRR / E 1 MRR omitted for GPT-4o because it often generates fewer than 10 candidates.
rank;"
Settings.
To enable a fair comparison with Lean Search (Gao et al. 2024a b), which relies on a fixed database Lean statements, we require that every testing sample appears in its database.
Since GPT-4o is puts to Lean statement names and evaluate with two criteria: 1) full-name match, which requires the exact full identifier of the Lean statement to match the ground truth: 2) stem match, a looser criterion where only the final component of the identifier must match (e.g.. Di rect.Sum. Iannternal. cow.llalllccllloooooooooo gEquiv counts as correct if the ground truth ends with coeA gE
retrieval model, we enable its web search tool and restrict its out-
Our test set includes 1000 informalized statements, 1000 formal statements, 1000 synthetic user queries, and 2224 proof states. We augment the formal statement inputs by replacing 20% of the query tokens with random tokens from vocabulary to simulate noisy queries. For proof states, we evaluate both the augmented version (with natural language guidance, Section 3.2) and the raw version (without augmentation) against other search engines. See Appendix G for detailed settings.
'https//leanscarch.ne/// "htpss/ppeeisee-saacc.com
8

---

Published as a conference paper at ICLR 2026
report Results. Table 2 and Table 3 report retrieval performance across input modalities. Lean Finder
consistently outperforms all baselines. Notably, GPT-4o with web search performs poorly even under the relaxed stem-match strategy, which inflate scores. This suggests that while the latest LLMs may demonstrate strong generation performance, they struggle to accurately retrieve dependent statements, highlighting the need for specialized systems such as Lean Finder. While Lean Search and Lean State Search target informalized statements and raw proof states, Lean Finder surpasses them as well, including on raw proof states that it was never explicitly trained on. These results highlight Lean Finder's 's ability to generalize across diverse query formats and capture user intents, making it an effective tool for supporting real-world Lean theorem proving workflows.
Table Comparison Lean Finder with Lean Search and GPT-4o on retrieval performance across three input modalities: informalized statement, synthetic user query, and augmented statement. MRR is omitted for GPT-4o because it often generates fewer than 10 candidates. The best results are presented in bold.
Informalized Statement
Synthetic User Query (Sec. 3.1
Augmented Statement
Model
R@1 I R@5
R@ 10
MRR
R@1
R@5
R@ 10
MRR
R@1 I R@5
R@ 10
MRR
Lean Finder
64.2
88.9
93.3
0.75
54.4
84,4
91.4
0.68
82.7
97.0
97.7
0.89
GPT-4o (full name match)
14.8
20.9
22.6
13.6
21.5
23.3
39.7
42.9
44.1
GPT-4o (stem match)
21.1
28.4
30.0
17.8
27.4
30.5
48.2
52.6
54.1
Lean Search
49.2
76.5
82.5
0.61
47.1
77.7
83.7
0.60
59.2
81.9
85.5
0.69
Table 3: Comparison of Lean Finder with Lean State Search, Real Prover Search, and GPT-4o retrieval performance across two input modalities: augmented proof state raw proof state. "Augmented proof state": proof state augmented with natural language description of proofs [Section[3.2] "Raw proof state": proof state without the augmentation. MRR is omitted for GPT-4o because it often generates fewer than 10 candidates. The best results are presented in bold.
Augmented Proof State
Raw Proof State
Model
R@
1
R@5
R@ 10
MRR
R@1
R@s
RΦ 10
MRR
Lean Finder
24.6
56.8
67.9
0.40
8.3
30.1
40.0
0.19
GPT-4o (full name match)
7.4
13.3
15.0
4.5
8.5
9.9
GPT-4o (stem match)
10.1
17.3
19.7
6.4
11.5
13.6
Lean State Search
4.99
27.7
39.6
0.16
3.3
23.1
32.1
0.13
Real Prover Search
8.0
29.0
39.2
0.18
7.1
26.2
34.3
0.16
4.2 LEAN FINDER IS PREFERRED BY REAL LEAN USERS
To evaluate Lean Finder on real-world queries, we conduct a user study with participants on 128 GitHub-sourced queries. For each query, participants examine three retrievals from each model and rank them according to how likely they are to resolve the query (ties allowed). Model identities are hidden and their orders are shuffled. Participants can also choose "All Bad" or "I don't Know" to indicate that all models' responses are bad or they don't know how to answer. We record each model's frequency of being ranked at 1st/2nd/3rd place and its percentage of top-3 appearances among valid ballots (i.c., queries not marked as All Bad/I don't know). We also compute the normalized Borda
score as Borda (m)) 3-m 4-2 (m)) +0m++11-mgg mm(mm) where 7u (m). (22)),, Ma (s(m)) are the counts of 3,V
1st/2nd/3rd place votes for model m and N the number of valid ballots. Further details are provided in Appendix FF]
The user study result in Table shows that Lean Finder is strongly preferred over baselines. receives the most best votes (139), almost twice as many baselines. It also achieves a much higher Top-3 rate of 81.6%, compared to 56.9% for Lean Search and 54. 1 % for GPT-4o. Its normalized Borda score (0.67) is also much higher than baselines, indicating that participants consistently rank Lean Finder's results as more helpful. These results confirm that Lean Finder better aligns with user preferences and provides more helpful retrieval results in ceal-world query settings.
4.3 LEAN FINDER IS COMPATIBLE WITH LLM PROVERS
To examine whether Lean Finder act as a prover-agnostic retrieval tool, integrate Lean Finder with whole- generation models like Goedel Prover (Lin et al., 2025a) and DeepSeek-Prow Provvr V1.5 (Xin et al., 2024b), well step-wise provers like REAL (Shen al. 2025), following

---

Published as a conference paper at ICLR 2026
Table 4: User ranking outcomes retrieval models, where na (m)) (2()), nz(m) refers the counts of 1st/2nd/3rd place votes model m. Best results are bold.
Model (m)
Ri (m)
12 (m2)
(14)
Top-3 3 (%)
Bordasorm
Lean Finder
139
56
36
81.6%
0.67
Lean Search
70
51
40
56.9%
0.41
GPT-4o
46
36
54.1
0.40
retrieval-augmeeted generation (RAG) setup where Lean Finder provides candidate lemmas during proof attempts, Evaluation on MiniF2F (Zheng et al., 2022), ProofNet (Azerbayey et al. 2023). PutnamBench (Tsoukalas al., 2024p. and FATE-M (Shen et al. 2025) shows that integrating Lean Finder yields performance that is mostly consistent with the non-integrated setting, with modest improvements on certain benchmarks. The detailed results and discussion can found in Appendix
RELATED WORKS
Prior efforts in code search Huuaai et al. 2019 Wang et al. 2023 Lean retrieval (Gao al.
2024a by Asher
2025 Lean FRO Morph Labs). and autoformalization (Jang et al.) 2023 Lin
al. 2024: Wang al. 2024 Ying et al. 2024 Soroco al., 2025) have advanced retrieval and translation between natural language and formal mathematics, but remain limited by narrow input types, paraphrase-leve alignment, or brittle translations. Our work complements these directions by introducing user-centered, intent-aware retrieval framework that explicitly models mathematicians' real query styles and integrates them into training, enabling Lean Finder to generalize across diverse modalities and substantially outperform existing systems on real user queries. Extended related work provided in Appendix
CONCLUSION
We present Lean Finder, significant advancement in the development of search tools for formal mathematics. By centering on real user intent and leveraging synthesized queries, semantic clustering, and fine-tuned embeddings, bridges the gap between mathematicians' informal reasoning and formal theorem proving in Lean. Its superior performance over existing search tool demonstrate both practical utility and academic impact. Lean Finder not only enhances accessibility to mathlib4 but also lays the groundwork for future intelligent systems that assist in rigorous, collaborative mathematical discovery.
THE USE OF LARGE LANGUAGE MODELS (LLMS)
LLMs did not play a significant role either the research ideation or the writing of this paper. Their use was limited to correcting minor grammatical issues and typographical errors.
ACKNOWLEDGMENT
This research used resources the National Energy Research Scientific Computing Center, a DOE Office of Science User Facility supported by the Office of Science of the U.S. Department of Energy under Contract No. DE-ACC02-0CCH1223 using NERSC award NERSC DIDR-ERCAP0034662 and ASCR-ERCAP0031445
REFERENCES
Jesse Alama, Tom Heskes, Daniel Kühlwein, Evgeni Tsivtsivadze, and Josef Urban. Premise selection for mathematics by corpus analysis and kernel methods. Journal of Automated Reasoning, 52: 191-213, 2014.
AlphaProof and AlphaGeometry teams. Al achieves silver-medal standard solving interna- tional mathematical olympiad problems. http://tttt/se/eeeeeiiidda htt.://mmnnn..oooooee/////e////e
ai-sol ves- mo- probl ems httt-=ssiveemmmeaa-aaa---- 2024.
10

---

Published as a conference paper at ICLR 2026
Justin Asher. Leanexplore: A search engine for lean 4 declarations. https:/ httl//gitttt wit.tgtthhh.o. com/ http:///ww.oocao///aa//aaaaaaaaa
pdf, 2025.
Zhangir Azerbayev, Bartosz Piotrowski, Hailey Schoelkopf, Edward W. Ayers, Dragomir Radev, and Jeremy Avigad. Proofner: Autoformalizing and formally proving undergraduate- mathematics, 2023.
12433
Wei-Lin Chiang, Lianmin Zheng, Ying Sheng, Anastasios Nikolas Angelopoulos, Tianle Li, Dacheng Li. Banghua Zhu, Hao Zhang, Michael Jordan, Joseph E Gonzalez, et al. Chatbot arena: An open platform for evaluating Ilms by human preference. In Forty-first International Conference on Machine Learning, 2024.
Leonardo De Moura, Soonho Kong, Jeremy Avigad, Floris Van Doorn, and Jakob von Raumer. The lean theorem prover (system description). In Automated Deduction-CADE--2 25th International Conference on Automated Deduction, Berlin, Germany, August 1-7, 2015, Proceedings 25, pp- 378-388. Springer, 2015.
Guoxiong Gao, Haocheng Ju, Jiedong Jiang, Zihan Qin, and Bin Dong. A semantic search engine for mathlib4. arXiv preprint arXiv:2403.133100 2024a.
Guoxiong Gao, Yutong Wang, Jiedong Jiang, Qi Gao, Zihan Qin, Tianyi Xu, and Bin Dong. Herald: natural language annotated lean 4 dataset. arXiv preprint arXiv:2410. 10878, 2024b.
Guoxiong Gao, Haocheng Ju, Jiedong Jiang, Zihan Qin, and Bin Dong, A semantic search engine for mathlib4, 2025. Utttttss:://art /ttp///avvvv/.. wttpaaawwww.gaaaa.a/aaaaaaaaaaaa
abs /tt/://bbb222311333
Timnit Gebru, Jamie Morgenstern, Briana Vecchione, Jennifer Wortman Vaughan, Hanna Wallach, Hal Daumé lii, and Kate Crawford. Datasheets for datasets. Communications of the ACM, 64(12): 86-92, 2021.
Edward J. Hu, Yelong Shen, Phillip Wallis, Zeyuan Allen-Zhu, Yuanzhi Li, Shean Wang. Lu Wang, and Weizhu Chen. Lora: Low-rank adaptation of large language models, 2021. URL https
7/arxiv. orq/ abs 2106.00600000 09685
Hamel Husain, Ho-Hsiang Wu, Tiferet Gazit, Miltiadis Allamanis, and Mare Brockschmidt. Code- searchnet challenge: Evaluating the state of semantic code search. arXiv preprint 4rXiv:1909.09436,
2019.
Geoffrey Irving, Christian Szegedy, Alexander A Alemi, Niklas Eén, François Chollet, and Josef Urban. DeepMath- sequence models for premise selection. In NIPS, 2016.
Albert Q Jiang, Wenda Li, and Mateja Jamnik. Multilingual mathematical autoformalization. arXiv preprint arXiv:2311.03756 2023.
Albert Q. Jiang, Wenda Li, and Mateja Jamnik. Multi-language diversity benefits autoformalization, 2024.
Haocheng Ju and Bin Dong. Mirb: Mathematical information retrieval benchmark. arXiv preprint arXiv:2505.15585 2025.
Vladimir Karpukhin, Barlas Oguz, Sewon Min, Patrick SH Lewis, Ledell Wu, Sergey Edunov, Danqi Chen, and Wen-tau Yih. Dense passage retrieval for open-domain question answering. In EMNLP (I), pp. 6769-6781, 2020.
Lean FRO. Loogle.
Chenyi Li, Zichen Wang, Yifan Bai, Yunxi Duan, Yuqing Gao, Pengfei Hao, and Zaiwen Wen. Formalization of algorithms for optimization with block structures, 2025a. URL https://
Sexiv.orgu abs / 2503.111111111 18806
Chenyi Li. Shengyang Xu, Chumin Sun, Li Zhou, and Zaiwen Wen. Formalization of optimality conditions for smooth constrained optimization problems, 2025b. URL/attps :/tppp:://rrre aar.iv.oggg abs/ /203.250... 18821
11

---

Published as a conference paper at ICLR 2026
Haohan Lin, Zhiqing Sun, Yiming Yang, and Sean Welleck. Ltan-star: Learning to interleave thinking and proving, 2024. URL https: /ttp:v///axvv...o wwwp:xii.vr//ab////eee 10040
Yong Lin, Shange Tang, Bohan Lyu, Jiayun Wu, Hongzhou Lin, Kaiyu Yang. Jia Li, Mengzhou Xia, Danqi Chen, Sanjeev Arora, et al. Goedel-prover: frontier model for open-source automated theorem proving. arXiv preprini arXiv:2502.076.4 2025a.
Yong Lin, Shange Tang, Bohan Lyu, Ziran Yang, Jui-Hui Chung, Haoyu Zhao, Lai Jiang, Yihan Geng, Jiawei Ge. Jingruo Sun, Jiayun Wu, Jiri Gesi, Ximing Lu, David Acuna, Kaiyu Yang, Hongzhou Lin, Yejin Choi, Danqi Chen, Sanjeev Arora, and Chi Jin. Grover--r Scaling formal theorem proving with scaffolded data synthesis and self correctin,, 2025b. URLhttps
//arxiv. wtw.vvoorgggaaoo abs/ 2508 03613
Jianqiao Lu, Yingjia Wan, Zhengying Liu, Yinya Huang, Jing Xiong, Chengwu Liu, Jianhao Shen, Hui Jin, Jipeng Zhang, Haiming Wang, Zhicheng Yang. Jing Tang, and Zhijiang Guo. Process-driven autoformalization in Lean 4. arXiv preprint vxXiv:2406001944 2024.
Sven Manthe. A formalization of borel determinacy in lean, 2025. URL https:://aax....oott abs/2502. 03432
Maciej Mikula, Szymon Antoniak, Szymon Tworkowski, Albert Qiaochu Jiang, Jin Peng Zhou, Christian Szegedy, Eukasz Kuciñiski, Piotr Mitos, and Yuhuai Wu. Magnushammer: A transformer- based approach to premise selection. arXiv preprint UrXiv:2303.04488 2023.
Ludwig Monnerjahn. Formalisation of constructable numbers. 2024.
Pietro Monticone. Formalising fermat's last theorem for exponent 3 in lean. 2024.
Morph Labs. Moogle.
Leonardo de Moura and Sebastian Ullrich. The Lean 4 theorem prover and programming language. In CADE, 2021.
Gabriel Poesia, David Broman, Nick Haber, and Noah D Goodman. Learning formal mathematics from intrinsic motivation. arXiv preprint arXiv:2407.00695, 2024.
Yingqi Qu, Yuchen Ding, Jing Liu, Kai Liu, Ruiyang Ren, Wayne Xin Zhao, Daxiang Dong, Hua Wu, and Haifeng Wang. Rocketqa: An optimized training approach dense passage retrieval for open-domain question answering. arXiv preprint arXiv:2010.0819), 2020..
Rafael Rafailov, Archit Sharma, Eric Mitchell, Stefano Ermon, Christopher D. Manning, and Chelsea Finn. Direct preference optimization: Your language model is secretly a reward model, 2024. URL
https://arxiv/ org/ wwwp//////////o////oeo///eeeeee/ abs/2303.33 18290
ZZ Ren, Zhihong Shao, Junxiao Song, Huajian Xin, Haocheng Wang, Wanjia Zhao, Liyue Zhang, prover-v2: Advancing formal mathematical
Zhe Fu, Qihao Zhu, Dejian Yang, al. Deepseek-prover--2. reasoning via reinforcement learning for subgoal decomposition. arXiv preprint 0rXiv:2504.2180) 2025.
Ziju Shen, Naohao Huang, Fanyi Yang, Yutong Wang, Guoxiong Gao, Tianyi Xu, Jiedong Jiang, Wanyi He, Pu Yang, Mengzhou Sun, et al. Real-provee Retrieval augmented lean prover for mathematical reasoning. arXiv preprint arXiv:2505.20613. 2025.
Peiyang Song, Kaiyu Yang, and Anima Anandkumar. Towards large language models as copilots for theorem proving in lean. In The 3rd Workshop on Mathematical Reasoning and Al at 233, 2023. htRlttttss:/ http::::s////peeevvieiee
net. net//forumt formm? fttp://rmmmmmmmcx0x5..axaaaaa d=c9x55xa2kx
Mauricio Soroco, Jialin Song, Mengzhou Xia, Kye Emond, Weiran Sun, and Wuyang Chen. Pde- controller: Lims for autoformalization and reasoning of pdes. International Conference on Machine Learning, 2025.
Yicheng Tao, Haotian Liu, Shanwen Wang, and Hongteng Xu. Assisting mathematical formalization with learning-based premise retriever. arXiv preprint 2395925501.1395, 2025a.
12

---

Published as a conference paper at ICLR 2026
Yicheng Tao, Haotian Liu, Shanwen Wang, and Hongteng Xu. Learning effective premise retrieval model for efficient mathematical formalization, 2025b. URL http::tts://aat http:://axxxvv.ooo.. abs/
13959
George Tsoukalas, Jasper Lee, John Jennings, Jimmy Xin. Michelle Ding. Michael Jennings, Ami- tayush Thakur, and Swarat Chaudhuri. Putnambench: Evaluating neural thheoremmproeeeee on the putnam mathematical competition, 2024. URL
Josef Urban. MPTP- motivation,, implementation, first experiments. Journal of Automated Reasoning, ReatoonnntedReoonnnnn 33:319-339, 2004.
Mingzhe Wang and Jia Deng, Learning to prove theorems by learning to generate theorems. 2020.
Qingxiang Wang, Cezary Kaliszyk, and Josef Urban. First experiments with neural translation of informal to formal mathematics. In Conferences Intelligent Computer Mathematics (CICM), 2018.
Ruida Wang, Jipeng Zhang, Yizhen Jia, Rui Pan, Shizhe Diao, Renjie and Tong Zhang. Theoreml- lama: Transforming general-purposs. purpose Ilms into lean4 experts. arXiv preprint arXiv:2407.03203 2024.
Wenhui Wang, Furu Wei, Li Dong, Hangbo Bao, Nan Yang, and Ming Zhou. Minilm: Deep self-attention distillation for task agnossti compression of pre-trained transformers, 2020. URL
https://arxiv: org/ abs 2002.1095
Yue Wang, Hung Le, Akhilesh Deepak Gotmare, Nghi DQ Bui, Junnan Li, and Steven CH Hoi. Codet5+: Open code large language models for code understanding and generation. arXiv preprint arXiv:2305.07992, 2023.
Sean Welleck and Rahul Saha. IImstep: LLM proofstep suggestions lean. In The 3rd Workshop Mathematical Reasoning and Al NeurlPS'23 23, 2023. URL
n
Yuhuai Wu, Albert Qiaochu Jiang, Jimmy Ba, and Roger Grosse. Int: An inequality benchmark for evaluating generalization in theorem proving. arXiv preprint arXiv:2007.02924, 2020.
Yuhuai Wu, Albert Qiaochu Jiang, Wenda Li, Markus Rabe, Charles Staats, Mateja Jamnik, and Christian Szegedy. Autoformalization with large language models. 2022.
Zijian Wu, Suozhi Huang, Zhejian Zhou, Huaiyuan Ying. Jiayu Wang, Dahua Lin, and Kai Chen. Me.nLLMM..--StPProvve Advancing automated theorem proving via expert iteration on large-scale lean problems. arXiv preprint 11Xi::2410.15700 2024.
Huajian Xin, Daya Guo, Zhihong Shao, Zhizhou Ren, Qihao Zhu, Bo Liu, Chong Ruan, Wenda Li, and Xiaodan Liang. Deepseek-provee proverr. Advancing theorem proving in Ilms through large-scale synthetic data, arXiv preprint arXiv:2405. /4333, 2024a.
Huajian Xin, ZZ Ren, Junxiao Song, Zhihong Shao, Wanjia Zhao, Haocheng Wang, Bo Liu, Liyue Zhang, Xuan Lu, Qiushi Du, et al. seepseek-prover-v// Harnessing proof assistant feedback for reinforcement learning and monte-carlo tree search. arXiv preprint arXiv:2408.08/ 08/52, 2024b.
Kaiyu Yang, Aidan Swope, Alex Gu, Rahul Chalamala, Peiyang Song, Shixing Yu, Saad Godil, Ryan J Prenger, and Animashree Anandkumar. Leandojo: Theorem proving with estrieval-augmeene language models. Advances in Neural Information Processing Systems, 36:21573-21611 2023.
Eric Yeh, Briland Hitaj, Sam Owre, Maena Quemener, and Natarajan Shankar. CoProver: A recommender system for proof construction. arXiv preprint urXiv:2304. 10486, 2023.
Huaiyuan Ying. Zijian Wu, Yihan Geng, Jiayu Wang, Dahua Lin, and Kai Chen. Lean workbook: A large-scale lean problem set formalized from natural language math problems, 2024. URL https://arxx org/ abs /206. 03847
13

---

Published as a conference paper at ICLR 2026
Yanzhao Zhang, Mingxin Li, Dingkun Long, Xin Zhang, Huan Lin, Baosong Yang, Pengjun Xie, An Yang, Dayiheng Liu, Junyang Lin, Fei Huang, and Jingren Zhou. Qwen3 embed- ding: Advancing text embedding and reranking through foundation models, 2025. URL
http://bs//2000 051766
Kunhao Zheng, Jesse Michael Han, and Stanislas Polu. Minif2f: a cross-system benchmark for formal olympiad-level mathematics, 2022. /LL/E/oss//aax....r///////.0.
Thomas Zhu, Joshua Clune, Jeremy Avigad, Albert Qiaochu Jiang, and Sean Welleck. Premise
selection for a lean hammer. arXiv preprint arXin:2500000777,.222.
Zulip. How does noob learn write tactics. 20 201.eea....ccco0vvvveeee...e..ed
Naming htgpr/a........i...ia....oo.onnn
1o [ttp:///tteaan/lgggaee/////////0
222paa/g.eeoooool........0...222 2020b.
Zulip.
Improving documentation. http:///aapporr.oooottttttttttoo
html 2021a.
Zulip.
Library search failures. https://lenppeerr.cmuuutt....g.
io/
archi ve/ http://aaea.aaaaa/ee///////////a lures.
html 2021b.
14

---

Published as a conference paper at ICLR 2026
A EXTENDED RELATED WORKS
Code Search and Lean Retrieval. Code search, aimed at retrieving the most semantically relevant code snippets from a codebase according to a specified natural language query, is a common activity
that plays important role in software development (Husain et al. 2019: Wang et al. 2023 and aligns closely with premise selection: both problems require retrieving a small set of code blocks
that are helpful for downstream tasks. Early methods relied on lexical heuristics (Alama et al. 2014
Urban 2004), while recent work leverages neural encoders (Irving et al. [0166] Wang & Deng 2020
Mikula et al. 2023 Yeh et al. 2023) and dense retrieval models (Karpukhin et al. 2020: Qu et al.
2020> by learning semantic embeddings. In formal domains like Lean, retrieval systems like Lean Search (Gao al., 2024a b) assist users by allowing them search for relevant mathlib statements using natural language queries. These systems primarily function by matching the natural language translation of a formal statement to other formal statements in mathlib, While effective in some settings, this approach supports only narrow input types and treats informal queries as approximate paraphrases of formal code and focuses on surface-level alignment, without capturing the diverse intents behind real-world user questions or the broader context in which they arise. Lean Finder addresses this gap by introducing a user-centered, intent-aware retrieval framework for Lean that supports broad range of imput modalities and explicitly bridges the gap between the natural queries posed by mathematicians and the formal statements stored in Lean projects. By modeling real user intent and query diversity, Lean Finder achieves consistently strong retrieval performance across all modalities and demonstrates substantial gains over existing systems in a user study based on real Lean queries.
Auto AutoFormalliztion Autoformalization, the automated translation of informal mathematics into formal proof-assistant code, has become a key strategy for addressing the scarcity of high-quality formal data. Early neural encoders for statement formalization (Wang et al.) 2018) have been eclipsed by
pipelines that translate at scale with few-shot prompting or fine-tuning (Wu et al. Xin et al. 2024a ()) [oroco et al.) 2025). Systems such as DeepSeek-Proves InternI.M2.5. StepProver, and Goedel Prover series formalize vast. Lean corpora for expert iteration (Xin et al. 2024a| [u et al., 2024) Lin et 2025a (b). while others generate synthetic formal proofs without informal seeds (Wu et al. 2020 Wang & Deng 2020 Poesia et al. (024).. Projects such MMA,
2022, 2024
(NL-FL) pairs to mitigate data scareity (Jiang et al., 2023 Lin et al. 2024 Wang al., 2024 Ying et al. 2024): yet LLM brittleness still introduces subtle logical errors. Recent LLM tools embedded in user workflows (e.g., LeanDojo, LeanCopilot, LLM-Step) further streamline manual formalization by suggesting premises and proof tactics (Yang et al., 22023] [Song et al.] [023] Welleck & Saha 2023 Shen et al. 2025). Our work tackles the complementary challenge of autoformalization: synthesizing intent-rich, user-style queries from formal Lean statements to better serve practitioners. Unlike previous informalization approaches that simply translate formal statements into natural language, our pipeline explicitly models user intent and query phrasing. Injecting this intent-awan signal during fine-tuning yields significant retrieval improvements on real user queries, and bridges the gap between informal user needs and the formal knowledge encoded in Lean libraries.
Lean-STaR, TheoremLlama, and Lean Workbook create natural- -
B DETAILS FOR DATASET CONSTRUCTION
B. DATA SOURCE DETAILS
To build a more comprehensive and representative corpus of Lean 4 statements, we consider the following sources in addition to mathlib4:
Research-linked repository: GitHub projects that are part of math papers, which often contain formalizations of novel theorems and lemmas.
Domain-speeific library: Projects such as SciLean that cover applied mathematical domains.
Transitive dependency: Any Lean 4 project dependencies required by the above repositories.
We use LeanDojo (Yang et al. 2023 to extract formal statements from collected projects. The
complete list of repositories in data is shown in Table
15

---

Published as a conference paper at ICLR 2026
Table 5: Lean sources included in dataset beyond mathlib4.
Project name
Category
URL
Mathlib4
comaan--peciffe
https//github.com//eappnpo
library
community/Mathlitt
SciLean
Domain-speciife
http://giiub.ccm//ccpppioosssssu
lihrary
A Iormalization of Borel deter-
Research-linkee repus- itory
hupp://gilabb.oom///eeeemnnntcc
minacy in Lean Manthe 2025
Optlib Li et al. 2025a b
Research-linked repos-
http://giiab..comm/ppsssiicppppb
itory
Formalising Fermat's Last The- orem for Exponent Monti
Research- repos-
http://giitaabaommrrccctttasssss
itory
cone
2024
Formalisation of constructable numbers/ Monnerjahn [2024)
Research linked repos- itory Transitive dependency
https:/ggituub.comLLouiis-.LL
Plausible
http://gittub.comm/eaappvvrr
community/plausihlc
ProolWidgets4
Transitive dependency
hutps//giilobccom//aaprveerr
communityPProotWideeess
Aesop
Transitive dependency
Batteries
Transitive dependency
https//gittub.com//caaprroo
community/batteris
B.2 SUMMARY OF OUR DATASET
We summarize our dataset by input modalities in Table and by data sources Table
Table 6: Overview of our dataset by input modalitics.
Input Modality
Samples
Percent
Synthesized User Query
582102
42%
Augmented Proof State
337647
24%
Informalized Statements
244521
17%
Formal Statement
244521
17%
Table 7: Overview of our data sources. Note that the numbers below are original samples collected, and the numbers in Table indicate augmented samples.
Source
Samples
Percent
Mathlib
238021
97%
Research- repository
Lean related libraries
4302
B.3 INFORMALIZATION DETAILS
The context we provide to GPT-4o consists of the following six components:
Formal name: The full name of the statement to be informalized.
Formal statement code: The complete Lean 4 code, including the statement and body.
Doestring: Any human-written docstring associated with the statement in the codebase.
Neighbor statement: The closest statement in the same file, based positional proximity. We include its full code, as nearby statements often share related concepts. This helps the model understand the local context and inter-connectiness of the statement.
Dependent statements: All the dependent statements used in the body of the statement to be informalized, along with their informalizations. This provides the necessary prerequisite knowledge and semantic dependencies for achieving high-quality informalization.
16

---

Published as a conference paper at ICLR 2026
Related statement in Herald (Gao al. 2024b): A formal statement and its corresponding informalization from the Herald dataset that closely aligns with the target statement. This example serves an in-context demonstration for GPT-4o, helping generate more accurate and stylisti- cally consistent informalization. We use DeepSeek-Prone Prover to retrieve the most relevant statements from Herald, and use the top-matching informal statement along with its corresponding formal statement as the related statement in the prompt for informalization.
B.4 AUGMENTED PROOF STATE DETAILS
We introduce augmented proof-state input modality, where a proof state in Lean denotes the current list of pending subgoals, each with its local context of hypotheses and target proposition. Some previous search engines support queries of type proof state (Tao et al. 2025a Shhnn et al. [025] Yang et al. 2023) to retrieve relevant theorems that could be applied in the next step, but they neglect that from given proof state, can expect multiple plausible directions to advance the proof. A mathematician might therefore want to search not only from the proof state itself, but also conditioned on their intended path forward.
Formally, a theorem's 's proof trajectory æ with m steps can be represented as sequence of states and tacties
= ((S
(s(), (1() S(()),
(s(m (m(), s(m)))
where 5(()) is the initial proof state, each ( is tactic, and ((m) denotes no remaining goals (proof completed). Each triplet (S(i-1), , (() corresponds to transition step. From these trajectories, we collect unique state- trantt-ranntiion pairs (S(i-1), g(t) where the tactic T() makes use of at least one premise (i.e., a previously established Lean statement).
To support this finer-grained retrieval, we synthetically generate augmented proof states: given state- before and state-after pair (S(i-2), s()) collected from proofs of Lean statements, we prompt GPT-4o to produce natural description of the intended transition, without revealing the exact theorems used in 7(1. This augmentation better supports
querying with proof states, enabling them to specify how they intend to proceed and to receive theorem suggestions that are more precisely aligned with their reasoning process. Lean Finder also implicitly supports raw proof-state inputs, ensuring compatibility with conventional retrieval settings while offering more fine-grained capabilities.
B.5 DISCUSSION ON IMBALANCED CLUSTERS IN SYNTHETIC USER QUERIES
We note clear cluster imbalance within the synthetic user queries modality, shown in Figure 4 For instance, the Metaprogramming cluster accounts for only 1% of the data, whereas Lemma Search and Proof Engineering dominate with 41% % each. This imbalance arises from the filtering step applied prior to query generation (Section 3.1.2). where we ensure that each Lean statement is genuinely answerable under the chosen cluster. As result, synthetic queries reflect natural usage patterns rather than being artificially uniform across categories. This skew is not an artifact of our pipeline alone and similar distribution emerges in real user behavior. On Lean Zulip Chat, the peetaroogramiing/uae channel sees roughly 13 messages per week, whereas the estimated count of messages per week in the channel is there code for X exceeds 300. Thus, the scarcity of metaprogrammingg queries relative to lemma search mirrors genuine community practices, reinforcing that our synthetic data distribution aligns with the way mathematicians actually interact with Lean.
C OPENAI API CONFIGURATIONS
We prompt OpenAl models during data collection and generation, and we describe the detailed configurations below.
Informalization.
We leverage the GPT-4o API convert formal Lean statements into informal
statements (Section
3.2 The temperature is set to 0.2 and the maximum output token limit is 1000.
Inspired by Herald Gao al. 2024b), the prompt for informalization shown in Section 0.1
17

---

Published as a conference paper at ICLR 2026
User Query Filtering. We employ 4PT-4o filter out user queries that cannot be addressed by any Lean 4 formal statement (Section 3.1.1. The temperature is set to 0.0 with maximum of 500 output tokens. The prompt for query filtering is shown in Section 0.2
User Intent Clustering. To cluster user intents (Section 3.1.1. we use the o3 API. The process involves two stages:
Bootstrap Categorization. An initial set representative user queries is clustered using a temperature of 1.0 and token limit of 20000. The prompt used for initial cluster generation is shown in Section O.3
Progressive Clustering. Remaining queries are progressively categorized with the same tem- perature and token settings. The prompt used for this part is shown in Section O..
User Query Generation. To synthesize diverse user queries (Section 3.1.2) , we use the GPT-4o API with temperature of 0.7 and maximum output of 1000 tokens. The prompt used is shown in Section
0.5
D TRAINING DETAILS
We fine-tune our Lean Finder based on the DeepSeek-Prover--V 1.5--R 7B Xin et al. (2024b). using a query-code code contrastive learning objective. We apply LoRA Hu al. (2021) with rank 64 and = 128. We train Lean Finder for epoch with a per-GPU batch size of 8, gradient accumulation steps of 4, and 4 NVIDIA 6000Ada GPUs. We use the AdamW optimizer with learning rate of 1 x 10 The learning rate is linearly warmed up over the first 1550 steps, then decayed to 0 using a cosine schedule. The group size G is and the temperature is set to 0.01.
2 x 10-5 and
For DPO, we start with the checkpoint trained with contrastive loss described above. The two losses CDro. Ccontrastive are computed on independent batches, where the DPO loss LDro is trained on preference data from user and LLM feedback and the contrastive loss Leomtrasivve is trained on mixture of the original training set (which is more abundant and less noisy) and new user queries. This design mitigates the limitations of real feedback data, which are relatively scarce, noisy, and potentially shifted distribution compared to the original input modalities. We train with NVIDIA 6000Ada GPUs using per-GPU batch size of 2 and 4 gradient accumulation steps for a total of epochs. We set to 0.1 and À to 0.01.
E PREFERENCE DATA CONSTRUCTION DETAILS
Our preference dataset consists of triplets (g,ct.c") where is a user query and ct and c are, respectively, chosen and rejected Lean statement. We construct these triplets from three complementary sources:
Direct refrieval-level feedback. Users may upvote or downvote individual retrieved state- ments. For query g, we form triplets by pairing each upvoted statement with each downvoted one. This provides explicit statement-level supervision from user feedback. See Figure an example.
Model-level feedback. We also design blinded comparison interface on our web service where users are shown the top-k results for a given query from two retrievers Lean Finder (Rvr(g)) and Lean Search (R)s(q)) without knowing which system produced which results as the order of the retrievers is randomized across interactions, ensuring unbiased comparisons (See Figure g for an example). Users then select one of four outcomes: Retriever A better, Retriever B better, Tie, or Both bad. Since this feedback is coarse, we refine it into triplets using GPT-4o with rules to best preserve user feedback. For example, Lean Finder is preferred, then at least one statement in the set difference RIF(g) Ris(g) is labeled helpful and at least one in (g)(g) labeled unhelpful; ties require at least one helpful statement in the intersection RLr(q) n Ris both-bad cases discarded. For each query, every selected ct is paired with c to form (q, c "t,c" triplets. As we use GPT-4o in the process of constructing preference data, evaluate how well GPT-4o aligns
18

---

Published as a conference paper at ICLR 2026
with human preference (Appendix H). The results show that GPT-4o aligns well with human preference.
Lean Zulip discussions. To diversify queries beyond our web service, we extract real user questions from Lean Zulip. Since these lack explicit statement-leve feedback, GPT-4o is prompted to identify helpful and unhelpful retrieved statements from Lean Finder. This source captures community-drin driven problem formulations.
The resulting dataset p (q: , aggregates these sources. By combining explicit statement-level votes, blinded system-level comparisons with refinement, and original community queries, we construct heterogeneous preference resource for aligning with user preference in Lean retrieval.
F USER STUDY DETAILS
To evaluate the effectiveness Lean Finder in handling real-world user queries, We conduct user study with 5 participants using 128 high-quality real user queries for Lean statements, collected from GitHub. The participants all have rich experiences in Lean 4, with two PhD holders in Mathematics and Computer Science, a Master's student in Physics, and two Undergraduate students majoring in Mathematics.
For each query in the user study, we retrieve the top-3 results from each of the models. The identity of the models hidden from participants, and the order of models is randomized for every query to ensure fairness. Because GPT-4o hallucinate incorrect Lean statements that do not exist in mathlib or other Lean libraries, we apply a special treatment: instead of prompting it to generate full Lean statements directly, GPT-4o is asked produce only the full name of the statement believes answers the query. We then match this name against our database of mathlib statements and retrieve the corresponding ground-truth statement. This guarantees that GPT-44oss results are valid Lean statements and prevents hallucinated outputs from affecting the evaluation.
Participants are asked to evaluate the retrievals by selecting and ranking the top three models that provide the most helpful results for answering the given query. To account for ties, participants may assign the same rank (Best, Second Best, or Third Best) to multiple models. If none of the retrieved results are useful, or if the participants don't know how to answer the query, they may indicate this through a dedicated option.
Examples of the user study format is in Figure 6
G DETAILS FOR EVALUATION SETTINGS AND DATA
We describe below the details of evaluation settings and data we used for each input modality.
Evaluation on Informalized Statements. Since GPT-4o is included baseline but not retrieval model and lacks direct access to mathlib and other Lean libraries during inference, we enable web-search tool and restrict its output to ensure fair comparison. Specifically, GPT-4o is prompted to generate only the full name of Lean statement (the fully qualified identifier with namespace hierarchy). which avoids the generation of hallucinated Lean code. We evaluate GPT-4o under two matching strategies:
1. Full-name match; the prediction is correct only if the full name exactly matches the ground truth. Stem match: looser criterion where the prediction correct if the name stem (e.g.. coeAlgEquiv in DirectSum. w.reetttum..IInneeeee www.nnsennnnnn.cc.....e.......at cow.lgguuooeeeeeuuuuu..uu matches.
For all other models, a retrieved statement considered correct only the full Lean code matches.
To ensure fair comparison with Lean Search, which has fixed database, we impose two constraints: 1) The ground- -tuth formal statement must exist in the Lean Search database (otherwise Lean Search would always fail retrieve it). 2) The corresponding informal query must appear in either the Lean Search database or our training data (otherwise Lean Search would retrieve perfectly, and our model would already have seen near-duplicate). Following these nules, construct fair test set
19

---

Published as a conference paper at ICLR 2026
Rate the models
Mora than one model can be sa selected for each rank (Best/Swcord Beat/ Bear) fied
You ranks you these
Model
Best
O
Cherr
Third Best
models are helpful you don't understand the quary, ski Rata the models and choose:
Bed
Figure Google Form for user study. compare models: Lean Finder, Lean Search (Gao 2025 GPT-4o, Lean Finder w/o DPO, and Lean Finder w/o DPO and synthetic user query. Each model retrieves Lean statements, with the model order randomized across questions to avoid bias.
by randomly sampling 1000 Lean statements from Lean Search's 's database that are not in our training set and informalize them with simplified prompt.
Formal Statement. For the statement input modality, we use 1000 Lean statements from the Lean Search database, ensuring none appear in Lean Finder's training set. To simulate noisy queries and test model robustness, we randomly replace 20% of the tokens in each statement with tokens sampled from the vocabulary. To prevent invalid characters that may arise from the retrieval model's tokenizer during augmentation, we instead use a custom tokenizer. The same matching strategies for GPT-4o is applied.
Synthetic User Query. For the synthetic user query modality, we use 1000 queries from our test set whose ground truth statement is in Lean Search database. Same matching strategies for GPT-4o are used to compare with Lean Finder in this input modality.
Proof State. Finally, for the proof state modality, we randomly sample 2224 proof states from the test set. We evaluate both the augmented proof state queries (the modality that Lean Finder is explicitly trained on) and the raw proof state queries. Same matching strategies for GPT-4o are used to compare with Lean Finder in this input modality.
H EVALUATING GPT-40 ALIGNMENT WITH HUMAN PREFERENCES
Since GPT-4o is used to extract preference pairs for constructing DPO fine-tuning data, evaluate how well it aligns with human preferences on Lean statements through two complementary tests.
Retriever-level preference. We use 100 queries collected from our web service, where users compared retrieval results from Lean Finder and Lean Search and could choose one retriever the better one, a tie, or both bad. Since the ground -orun preferences are known from users, we directly prompt GPT-4o to make choice from the same four options. For the 63 cases where preferred one retriever over the other, GPT-4o match the human choice 58 times (92%). However, in the 37 cases where users selected tie or both bad, GPT--4o is correct only 15 times (43%). Manual inspection
20

---

Published as a conference paper at ICLR 2026
of GPT-4o's explanations suggests that the model tends to force choice between retrievers, often providing far-fetched reasoning instead of recognizing the tie or both bad scenarios.
Statement-level preference. We also evaluate 35 unique queries paired with user feedback on individual statements (upvotes downvotes). Since users may not comprehensively rate every statement they see, we use coverage metrie: GPT-4o is asked to classify statements as useful or not useful for answering the query, and we check whether all statements that received human feedback receive the same label as predicted by GPT-4o. We find that in 31 out of 35 queries, GPT-4o achieve full coverage, i.e., every user-rated statement matches GPT-4o'ss judgment.
These results indicate that GPT-4o closely mimics human preferences at both the retriever and statement levels, which indicates it's strong understanding in Lean semanties. While the model struggles to recognize lie or both bad cases, these scenarios are not relevant to our preference data collection process. Overall, this confirms that GPT-4o is reliable tool for extracting preference pairs aligned with human judgment.
Despite its strength preference alignment, GPT-4o performs poorly on the retrieval task from Section 4. In the retrieval setting, the model is required to take a natural user query and, with access search tool, output the full name of the relevant Lean statement. While GPT-4o demonstrates strong understanding of Lean semantics and can interpret the formal statements, it struggles to locate the exact corresponding result within the vast space of mathlib and the broader internet. The challenge is in precise identification: natural queries often map to highly specific statements which can be hard to locate through open-ended search. This makes retrieval particularly demanding for GPT-4o, in contrast to specialized systems like Lean Finder that designed index and surface the correct statement reliably.
I RAG FOR LLM PROVERS DETAILS
To examine whether Lean Finder can act as prover-agnostic retrieval backbone, integrate it with two representative types of LLM-based theorem provers: whole-proof generation model (Section L.I and step-wise theorem proving model (Section (.2) The whole-proof generation models take theorem statement and produces an entire proof in one shot, while step-wise provers interact with the proof assistant iteratively, generating one step time based the current proof state. Each integration follows retrieval-augmented generation (RAG) setup, where Lean Finder provides relevant supporting lemmas that the prover can condition on during proof generation.
1.1 WHOLE PROOF GENERATION MODEL
For whole-proof generation provers, evaluate Goedel Prover (Lin et al. 2025a) and DeepSeek- Prover V1.5 (Xin et al.) 2024b). Experiments are conducted on three benchmarks: MiniF2F (Zheng
et al. 2022), ProofNet (Azerbayev et al., 2023), and the PutnamBench (Tsoukalas et al. 2024). For each theorem to be proved, we first pass the initial proof state of the theorem to Lean Finder, which retrieves between six and ten relevant statements from our Lean statement corpus that are likely to be helpful in completing the proof. These retrieved statements are added to the prover's 's input as supporting context.
The proof performance with and without Lean Finder is summarized in Table Integrating Lean Finder retrieval into whole-proof generation provers yields modest but consistent improvements on MiniF2F and ProofNet. Although the gains are relatively small, the positive shift indicates that Lean Finder is compatible with existing provers and can provide helpful supporting context without disrupting performance. This result is encouraging given our primary goal of building a user-centered search engine that effectively captures user intent. On the more challenging PutnamBench dataset, however, there is inconsistent performance difference between using Lean Finder and not using it, suggesting that current provers are not yet able to fully leverage retrieved statements for highly complex and creative problems. Overall, these results demonstrate that Lean Finder integrates seamlessly with provers while preserving stability and delivering measurable benefits on standard benchmarks.
21

---

Published as a conference paper at ICLR 2026
Table 8: Performance of whole-proof generation models MiniF2F, ProofNet, and PutnamBench, comparing with and without Lean Finder retrieval (LF: integration with Lean Finder retrieval). The best results are presented in bold.
Prover System
Budget
MiniF2F Test
ProofNet
Test
PutnamBench
w/o LF
w/ LF
w/o LF
w/ LF
w/ LF
w/ LF
Goedel-Prover-Se.
38.1%
38.5%
6.6%
7.2%
3
32
57.7%
58.2%
13.2%
14.4%
6
6
128
59.4%
59.8%
17.6%
17.6%
DeepSeek-Prover-V1...5
34.4%
35.7%
4.3%
6.5%
32
50.0%
50.0%
14.5%
18.3%
7
128
51.6%
51.6%
17.7%
19.4%
7
1.2 STEP-WISE THEOREM PROVING MODEL.
For step-wise provers, we focus on REALProver (Shen et al. 2025). which consists of retrieval mod- ule and tactic generator. The tactic generator is trained to produce the next proof step conditioned on the retrieved statements provided by the retrieval module. In our setup, we replace REALProver's original retrieval module with Lean Finder. At each proof step, Lean Finder receives the current proof state and retrieves candidate statements, which are then fed into the tactic generator to generate the next tactic.
We evaluate this setup on three benchmarks: MiniF2F (Zheng et al. 2022), ProofNet (Azerbayev al., 2023), and FATE-M (Shen al. 2025) which is the dataset introduced in the REAL.rrover. The proof performance with Lean Finder integration is summarized in Table
Table 9;
Performance of REALProver on MiniF2F, ProofNet, and FATE-M M test sets, comparing with and without Lean Finder retrieval (LF integration with Lean Finder retrieval). The best results are in bold.
Prover System
Budget
MiniF2F
ProofNet
FATE-M
w/o LF
w/ LF
w/o LF
w/ w/LF L.
w/o LF
w/ LF
REALProver 8x8
52.0%
52.0%
23.7%
23.1%
51.1%
49.6%
The results Table show that integrating Lean Finder into REALProver maintains largely similar performance, with negligible changes across datasets. This suggests that REALProver's performance may be more constrained by its tactic generator than by retrieval. Moreover, its tactic generator may be tuned the specific retrieval signals of its native module, so replacing with Lean Finder does not yield immediate gains.
The limited gains suggest that while Lean Finder can be integrated into additional provers, the immediate benefits are marginal, which is why we restrict our experiments to a few representative systems.
ADDITIONAL EXPERIMENTS
We further compare Lean Finder with Lean Search that has augmentation mode enabled, Qwen3- Embedding-SB (Zhang et al, 2025), and Lean Explore (Asher 2025) their supported input types. For Lean Search with augmentation mode enabled, we first use built-in query augmentation functionality to augment the query, then submit it to Lean Search for retrieval. Since Lean Search and Lean Explore doesn't support proof state as input, we do not compare their retrieval performance when the input is of type proof state. We require the ground truth formal statement to be present in the respective static databases for both Lean Search and Lean Explore for fair comparison. Because this filtering process yields different test sets for each, report their results separately.
Lean Finder consistently surpasses all baselines, including specialized Lean search engines (such Lean Explore) and the state-of-the-ee ofrt Owen3-EEmeeddin 8B model, which is larger than Lean Finder by IB parameters. This indicates Lean Finder's strong performance and robustness across input types.
22

---

Published as a conference paper at ICLR 2026
Table 10: Retrieval performance comparison between Lean Finder, Lean Search with augmentation mode enabled, and Sreen--Emeddingg53 across three input modalities: informalized statement, synthetic user query, and augmented statement, The best results are presented in bold.
Informalized Statement
Synthetic User Query (Sec.
3.1
Augmenied Statement
Model
R@
R@
R@:
MRR
R@1
R@5
RØ 10
MRR
R@
R@55
R@ 10
MRR
Lean Finder
64.2
88.9
93.3
0.75
54.4
84,4
91.4
0.68
82.7
97.0
97.7
0.89
Lean Search (augmentation mode)
31.9
77.4
84,8
0.44
30.0
72.7
83.3
0,43
45.4
86.0
93.0
0.58
Qwen3- -aaae-dinbeddd--
57.7
82.5
89.2
0.69
41.2
73.8
82.8
0.55
76.2
93.4
95.1
0.83
Table 11:
Comparison Lean Finder with Qwen3 Eenenddiiidddd--88 on retrieval performance across two input modalities: augmented proof state and raw proof state. "Augmented proof state": proof state augmented with "Raw proof state": proof state without the augmentation.
natural language description of proofs (Section 3.2)
The best results are presented in bold.
Augmented Proof State
Raw Proof State
Model
R@D 1 R@5 R@ 10
MRR R@1 1
R@5
R@ 10
MRR
Lean Finder
24.6
56.8
67.9
0.40
8.3
30.1
40.0
0.19
Twenn--Emeeding
8.0
26.1
34.7
0.17
5.4
21.1
27.4
0.13
Table 12: Retrieval performance comparison between Lean Finder and Lean Explore the input types that Lean Explore support: informalized statement, synthetic user query. and augmented statement. The test set used is a cleaned version of the original test set to ensure the ground truth Lean statement is present in Lean Explore's s static database.The The best results are presented in bold.
Informalized Statement
Synthetic User Query (Sec. 3.1
Augmented Statement
Model
R@1
R@5
R@ 10
MRR R@1 R@S
R@ 10
MRR
@@1 1 R@5 R@ 10
MRR
Lean Finder
65.7
89.0
93.2
0.76
57.3
85.4
91.2
0.69
86.8
96.7
98.0
0.91
Lean Explore
35.0
61.8
68.0
0.46
26.3
51.3
60.1
0.37
85.8
93.6
95.2
0.89
K ABLATION STUDIES
DPO improves alignment with human preference. Table 13 shows that adding DPO improves retrieval quality on real user queries. Compared to the variant trained without DPO, Lean Finder is more frequently chosen by participants the preferred model in the user study. This supports our design goal: DPO fine-tuning on preference pairs mined from user and LLM feedback yields a retriever that better aligns with human judgments, even though the underlying retrieval metrics on synthetic data degrade only slightly as shown in Table 14
Synthetic queries are essential for intent understanding. To isolate the effect of synthetic user queries, we train variant without both DPO and synthetic queries while keeping training steps consistent. In the user study (Table 13). this model receives lower Best and Second Best votes compared to both the full Lean Finder and the variant trained without DPO. Since the only difference compared to the latter is the absence of synthetic queries during training, this decline provides strong evidence that synthetic queries are critical for teaching the model how to interpret natural, free-form user inputs. The user study thus offers the clearest demonstration that synthetic queries critical for helping the retriever to understand real user intent. In retrieval metrics on synthetic data (Table [4] and Table 11),, we also observe moderate decrease in performance for input modalities closer natural queries Tike informalized statement and synthetic user queries, while more structured modalities like proof states remain largely unaffected, reflecting the fact that synthetic queries rarely involve proof states.
Alignment-retrieval trade-off. In Table 14 we compare Lean Finder with the variant trained without DPO on retrieval when the inputs are synthetic data. We observe a small but consistent reduction in retrieval metrics across most modalities after DPO fine-tuning, We interpret this as modest aligument tax: even with a regularized objective that combines contrastive and DPO losses, shifting the embedding space to match human preferences necessarily incurs slight cost in retrieval metrics. However, this trade-off is offset by the clear gains in the user study (Table [3]. where the DPO-aligned model demonstrates improved usability and better alignment with real user preferences.
23

---

Published as a conference paper at ICLR 2026
Due to the time and financial costs of semantic analysis of real-world queries (Section 3.1.1 do not explore different number of intent clusters by re-clustering real user queries.
Table 13:
Comparison of Lean Finder and it's variants on the user study. w/o DPO is the model fine-tuned without DPO, w/o SynQ+DPO is the model fine-tuned without synthetic user query and without DPO. na (m)) (e2()). (m(m) refers to the counts of 1st/2nd/3rd place votes for model m. "SynQ": synthetic query.
Model (m)
(m)
(2(m)
n3(m)
Top 3 (%)
Bordanorm
Lean Finder
139
56
36
81.6%
0.67
w/o DPO
132
51
34
76.7%
0.63
w/o SynQ+DPO
90
51
37
62.9%
0.48
Table 14: Comparison Lean Finder and it's variants on retrieval performance where input modalities are informalized statement, synthetic user query, and augmented statement. w/o DPO the model fine-tuned without DPO. w/o SynQ+DPO is the model fine-tuned without synthetic user query and without DPO. The hest results presented in bold. "SynQ": our synthetic user query.
Informalized Statement
Synthetic User Query
Augmented Statement
Model
@@1 R@5
R@
MRR
R@1
R@5
R@ 10
MRR R@1 1 R@5 R@
MRR
Lean Finder
64.2
88.9
93.3
0.75
54.4
84.4
91.4
0.68
82.7
97.0
97.7
0.89
w/o DPO
66.9
91.2
95.1
0.77
58.1
86.8
93.1
0.71
84.9
97.4
98.4
0.91
w/o SynQ+DPO
61.1
87.5
91.6
0.73
38.4
66.4
73.7
0.51
86,4
96.8
98.0
0.91
Table Comparison of Lean Finder and it's variants on retrieval performance where the input modalities are augmented proof state and raw proof state. w/o DPO is the model fine- fine-tuned without DPO. w/o SymQ+DPO is the model fine-tuned without DPO and without synthetic user query. The best results are presented in bold. "SynQ": our synthetic user query.
Augmented Proof State
Raw Proof State
Model
R@I I R@S R@
MRR
R@!
R@5
R@ MRR
Lean Finder
24.6
56.8
67.9
0.40
8.3
30.1
40.0
0.19
w/o DPO
27.7
62.3
74.1
0.44
8.8
29.5
39.9
0.19
w/o SynQ+DPO
28.5
62.5
73.7
0.44
8.7
28.4
41.0
0.18
L MODULE-WIST ANALYSIS
Figure 7 shows Lean Finder's recall@ across mathematical modules, comparing synthetic user queries (bluc) with informalized statements (orange). Performance consistently higher with informalized statements, reflecting the stronger alignment between formal statements and their informalized counterparts than with free-form queries. Modules such as Combinatorics, Ring Theory, and Probability achieve particularly high recall with informalization. exceeding 80-90%. By contrast, synthetic user queries yield lower recall overall, especially in Set Theory, Ring Theory, and Data, where recall dips near 40%. The gap highlights the challenge of bridging natural queries with formal statements.
M LEAN FINDER'S S USER INTERFACE
To facilitate Lean users, we also develop and deploy our user interface, shown in Figure X and Figure [ We retrieve formal statements and also show their informalizations to help users better understand the Lean statements. Our Lean Finder also includes an Arena mode Fig where users can compare retrieval results from Lean Finder and Lean Search. The two retrieval systems presented in randomized order Retriever A or Retriever B, and users may vote for the better one, choose a tie, or mark both as bad. These pairwise preferences, together with votes on individual retrieved statements, form the core of our DPO fine-tuning data.
24

---

Published as a conference paper at ICLR 2026
Input: synthetic user query
Input: informalized statements
Algebra
Topology
CategoryTheory
Tactle
Combinatorics
SetTheory
Data
RingTheory
Theory
Probability
Geometry
Order
GroupTheory
NumberTheeory- 100 Linrrrrrleeerrrr
MeasureTheory
Figure 7: Lean Finder recall performance on different mathematical modules for synthetic user query and informalized statements as inputs.
DM
Understands
Duiyy
Figure 8: Web service interface of our Lean Finder in the Normal mode.
N PRIVACY AND DATA RELEASE
To protect user privacy, we do not release any real user discussion data collected from Lean Zulip. will only release these synthetic queries, along with queries from other input modalities. No identifiable information or original messages from Zulip users are included in our datasets.
O PROMPTS
0.1 PROMPT USED FOR LEAN STATEMENT INFORMALIZATION
You are an export mathematician and an expert in Lean and Mathlib.
Instructioon+: Your task is to translate the formal theorem belcw
25

---

Published as a conference paper at ICLR 2026
PaNi S
Lean Finder: Semaniic Search for Matthl That Understands User indertss
Model-level Arena A/B Tests
Retrieval-level Up/Down Vote
Figure 9; Web service interface of our Lean Finder the mode. We collect both the retrieval- and model-level feedback, which supports the fine-tuning of Lean Finder.
into informal statement (in LaTeX) that is accessible mathematiicinss.
Inputs include:
Formal name:
2. Formal statement:
3. Docstrings:
4. Neighbor statement:
5. Dependent theorems:
6. Related statement:
Then create informal and informal statement.
v*Principles of Informal Statements**
Use human mathematical notations and LaTeX formulas as much as possible
*PPrinippess of Informal Names**:
Emphasize logical relationships, not just listing concepts.
Input:
*Formal name+:
Formal statement*;
-Dosstrig*:
Neighhor statement
*Dependent theorems*:
Relaatdd theoremx:
O.2 PROMPT USED FOR USER QUERY FILTERING
You are expert Lean and experienced of Lean Zulip Chat
26

---

Published as a conference paper at ICLR 2026
ewInstruction<= :Yur task is first read the excerpt provided below that contains the first 5 messages from discussion thread Lean Zulip Chat and then decide to accept or reject the excerpt based on the following criteria:
1. You should accept the excerpt if the main user question in the excerpt can be answered at least partially by providing statement.
2. You should accept the excerpt if showing a pre-existing Lean statement will move the discussion forward in meaningful way. excerpt.
3. You should reject the excerpt if none of the above is true for this
4. When uncertain, use your best judgment.
Then identify the main question in this discussion thread...
Examples (not exhaustive): ACCEPT: Is there a Lemma/ haama//thorren/teiiitttt. that ..."?
REJECT: Library infrastructure, version bumps, build tools, CI, style.
ImputAA:
O.3 PROMPT FOR GENERATING INITIAL CLUSTERS OF USER QUERIES
You are an expert at Lean and experienced user of Lean Zulip Chat
+ Instruction==:
You will be provided below with 50 excerpts that contain the first few messages from discussion threads in Lean Zulip Chat and the main user question that is being asked in that discussion thread. Each excerpt has been filtered so that the main user question can be answered at least partially by a statement written in Lean 4 or showing a pre- existing Lean statement will move the discussion forward in a meaningful way.
You need to group the following 50 excerpts into clusters by their quezy purpose/type, and follow the instructions below:
:. Each cluster should represent distinct type of query based on the underlying intent or perspective of the main question in the excerpt.
2. Give each cluster descriptive name (a few words) that query type.
summarizes
3. For each cluster, give detailed description of what the cluster represents. This should include the common properties shared by the queries that belong in these clusters, and the description of the underlying intent or perspective of the queries made by the user. This must be detailed enough, such that a person reading this description can create new queries for Lean statement that belong in this cluster.
4. For each cluster, include most representative example queries that best define this cluster in the description. The chosen example queries must be the main_question provided in the input for the excerpt.
The input will be list excerpts, where each excerpt will have the following contents:
1. channel:
2. topic:
3. main question: ...
27

---

Published as a conference paper at ICLR 2026
4. messages:
Iaput**:
O.4 PROMPT FOR PROGRESSIVE CLUSTERING OF USER QUERIES
You are an expert at Lean and an experienced user Lean Zulip Chat
*IIstruction==::
You will be provided below with 25 excerpts that contain the first few measages from discussion threads in Lean Zulip Chat and the main user question that is being asked in that discussion thread. Each excerpt has been filtered that the main user question can be answered at least partially by statement written in Lean existing Lean statement will move the discussion forward in a meaningful way. You will also be provided with the current clusters of queries based on previous excerpts. Each cluster represents a distinct type of query based the underlying intent or perspective of the main question the excerpt. You need to do the following:
showing pre-
*aaas A: Pitting new excerpt***:
1. For each input excerpt, try to fit the excerpt into existing cluster based on the 'clusters description and representative examples provided for queries that cluster.
2. If new excerpts fit into an existing cluster of queries and the new excerpts reveal nuances that the current description of the cluster does not capture, you should append most one sentence to existing cluster description.
3. If new excerpts fit into an existing cluster of queries and the main_question in the new excerpts reveal nuances that the current examples for that cluster does not capture, you should add at most one example
existing cluster examples.
4. DO NOT remove any description and examples in the existing cluster. You are only allowed to add new ones when needed.
5. If the excerpt DOES Nor sit into an existing cluster, do Task B, otherwise skip Task B.
v*lask B: New cluster proposal (if needed) **:
1. If the input excerpt 'doesnt fit into any existing cluster, then you should propose one new cluster.
2. The new cluster must have descriptive description of what the cluster represents. The description should include the property of the query in this new cluster, and the description of underlying intent perspective of the query made by the user...
and detailed
10 representative example queries that best define this cluster. Each included example must illustrate different situations within the cluster...hen
3. The new cluster must include
4. DO NOT remove existing clusters, even it they are not used by the excerpts.
Each input excerpt will have the following contents:
1. channel:
2. topic:
3. main question:
4. messages:
Each input cluster will have the following contents:
1. cluster_name:
2. cluster_descripptie
28

---

Published as a conference paper at ICLR 2026
3. examples:
** Iaputs**:
O.5 PROMPT FOR GENERATING USER QUERIES
You are an expert Lean 4 user and an experienced participant in the Lean Zulip chat. You know how people usually phrase questions when they are soarching for existing Lean statements.
winnsrructions:::
You will be given:
1. The name, description, and 10 canonical examples specific cluster of queries from Lean Zulip or GitHub. The queries in this cluster share the same underlying intent or perspective, precisely captured by the description.
2. single Lean 4 formal statement, formal name, informal name, and the natural language description Write one realistic user query that:
statement.
1. Clearly belorgs in this cluster. The intent and perspective of the query should mirror the description and examples.
least partially by showing the Lean statement you were given, or would be moved forward a meaningful way by that statement.
2. Could be answered
3. Does not explicitly reveal the statement.
4. Peels like genuine measage mathemati commatician ician Lean user would
post (natural tore, sensible level of detail).
** **Inpu***:
29

---

Published as a conference paper at ICLR 2026
P DATASHEETS FOR DATASETS
This document based on Datasheets for Datasets by (Gebru et al. 2021
P.I MOTIVATION
For what purpose was the dataset created? Was there specific task mind? Was there specific gap that needed to be filled? Please provide a description.
The dataset was created to support user-centered semantic search Lean by capturing the diverse intents of mathematicians. It includes synthesized user queries grounded in formal statements, informalized statements from various libraries and research-linkes repositories, and augmented proof states. The purpose is to create retrieval models that better reflect real user needs and integrate seamlessly with LLM-based theorem provers. The dataset bridges real user queries and raw informalizations for search engines, fostering research in retrieval-augmented theorem proving and intent-aware formal reasoning.
Who created this dataset (e.g,, which team, research group) and on behalf of which entity (e.g., company, institution, organization)? The dataset was created by the anonymous authors of this Lean Finder project, affiliated with research group focused on Al-for-math applications.
What support was needed make this dataset? (e.g.who funded the creation of the dataset? If there is an associated grant, provide the name of the grantor and the grant name and number, or if it was supported by a company or government agency, give those details.) The creation of the dataset was supported by research funding for developing novel applications of LLMs in formal mathematics. Additional support included access to computational resources for fine-tuning and coverage of API costs for data synthesis and processing.
Any other comments?
N/A
P.2 COMPOSITION
What do the instances that comprise the dataset represent (e.g,, documents, photos, people, countries)? Are there multiple types of instances (e.g., movies, users, and ratings; people and interactions between them; nodes and edges)? Please provide a description.
Each instance represents Lean-related query, which includes statement pair or proof context designed to capture mathematicians' intents. The dataset includes multiple types of instances: (i) synthesized user queries grounded in formal Lean statements, (ii) informalized statements providing natural language descriptions of Lean theorems, (iii) augmented proof states representing transitions between proof steps, and (iv) formal statement extracted from Lean libraries and research- linked repositories. Together, these instance types reflect different ways mathematicians interact with Lean and enable comprehensive training for semantic retrieval models.
How many instances are there in total (of each type, if appropriate)?
The dataset comprises over 1.4 million query codyy-coeeppe pairs. Specifically, it includes 582k synthesized user queries, 244k informalized statements, 338k augmented proof states, and 244k formal statement.
Does the dataset contain all possible instances or is it a sample (not necessarily random) of instances from a larger set? If the dataset is a sample, then what is the larger set? Is the sample representative of the larger set (e.g., geographic coverage)? If so, please describe how this representativeness was validated/verified. If it is not representative the larger set, please describe why not (e.g., to cover more diverse range of instances, because instances were withheld or unavailable).
The dataset is curated sample rather than the complete set of possible Lean queries. The larger set consists of all formal statements and proofs in mathlib4 and research- linked Lean repositories, along with the open-ended space of user queries posed by mathematicians, Since real user queries
30

---

Published as a conference paper at ICLR 2026
limited in number and often lack ground-trune truth resolutions, synthesize queries grounded in formal statements to approximate this space. While not exhaustive, the dataset designed to be broadly representative by covering multiple imput modalities (symthetic user queries, informalizations, proof states, and formal statements) and by drawing from both mathlib and research-linked repositories to capture diverse mathematical content.
What data does each instance consist of? "Raw" data (e.g., unprocessed text or images) or features? In either case, please provide a description. Each instance consists of raw text in the form of Lean 4 formal statements, their associated natural language variants, or proof contexts. Depending on modality, this may include: (i) synthesized user queries phrased in natural language, (ii) informalized statements produced from formal Lean code, (iii) augmented proof states describing proof progressions, and (iv) formal statement. All data are stored as text pairs.
Is there label or target associated with each instance? If so, please provide description. Yes. Each query paired with one or more target Lean formal statements that serve as the ground-truth retrieval target. In the case of augmented proof states, the target can be one more Lean statements used in the corresponding proof transition. For informalizations, synthetic user queries, formal statement, the target is the complete Lean statement from which they were derived.
Is any information missing from individual instances? If so, please provide description, explaining why this information is missing (e.g., because it was unavailable). This does not include intentionally removed information, but might include, e.g., redacted text.
N/A
Are relationships between individual instances made explicit (e.g., users' movie ratings, social network links)? If so, please describe how these relationships are made explicit. No. Each instance is an independent query-code pair.
Are there recommended data splits (e.g., training, developmenzvaliiattonn,, testing)? If so, please provide description of these splits, explaining the rationale behind them.
Yes, the dataset is split into training and testing sets.
Are there any errors, sources of noise, or redundancies in the dataset? If so, please provide description.
Yes. The synthesized queries from formal statements are generated using LLMs, some may contain minor phrasing inconsistencies or unnatural wording compared to real user queries. Informalizations may also result in inaccuracies.
Is the dataset self-contained, does it link to otherwise rely external resources (e.g., websites, tweets, other datasets)? If links to or relies on external resources, a) are there guarantees that they will exist, and remain constant, over time; b) are there official archival versions of the complete dataset (i.e., including the external resources as they existed at the time the dataset was created); c) are there any restrictions (e.g., licenses, fees) associated with any of the external resources that might apply to a future user? Please provide descriptions of all external resources and any restrictions associated with them, as well as links or other access points, as appropriate. The dataset is self-contained, with no reliance on external or dynamic resources.
Does the dataset contain data that might be considered confidential (e.g., data that is protected by legal privilege or by doctor-patient confidentiality, data that includes the content of individuals' non-public communications?? If so, please provide a description. No. We do not release any real user queries that we collected for fine-tuning and data synthesis.
Does the dataset contain data that, if viewed directly, might be offensive, insulting, threatening, or might otherwise cause anxiety? If so, please describe why.
31

---

Published as a conference paper at ICLR 2026
No.
Does the dataset relate to people? If not, you may skip the remaining questions in this section. No.
Does the dataset identify any subpopulations (e.g., by age, gender)? If so, please describe how these subpopulations are identified and provide description of their respective distributions within the dataset. No.
Is it possible to identify individuals (i.e., one or more natural persons), either directly or indirectly (i.e., in combination with other data) from the dataset? If so, please describe how. No.
Does the dafaset contain data that might be considered sensitive in any way (e-g., data that reveals racial or ethnic origins, sexual orientations, religious beliefs, political opinions or union memberships, or locations; financial or health data; biometric or genetic data; forms of government identification, such as social security numbers; criminal history)? If so, please provide a description. No.
Any other comments?
The dataset's richness in diversity makes a significant resource for advancing formal mathematics via AI.
P.3 COLLECTION
How was the data associated with each instance acquired? Was the data directly observable (e.g.. raw text, movie ratings), reported by subjects (e.g., survey responses), indirectly inferred/derived from other data (e.g., part-of-speech tags, model-based guesses for age or language)? If data was reported by subjects indirectly inferred/derived from other data, was the data validated/verified? If so, please describe how.
The data primarily derived from existing Lean 4 formal statements and proofs in mathlib and repositories. From these Lean statements, additional modalities were generated: informalizations, synthetic user queries and augmented proof states were produced by prompting LLMs.
Over what timeframe the data collected? Does this timeframe match the creation timeframe of the data associated with the instances (c.g., recent crawl of old news articles)? If not, please describe the timeframe in which the data associated with the instances was created. Finally, list when the dataset was first published. All the data is collected in 2025.
What mechanisms or procedures were used to collect the data (e.g., hardware apparatus or sensor, manual human curation, software program, software API)? How were these mechanisms or procedures validated?
We extract Lean statements from mathlib and other Lean repositories, and GPT-4o API to generate the queries.
What was the resource cost of collecting the data? (e.g. what were the required computational resources, and the associated financial costs, and energy consumption estimate the carbon footprint.) The total cost for GPT-4o API is around $2000.
32

---

Published as a conference paper at ICLR 2026
If the dataset is sample from larger set, what the sampling strategy (e.g., deterministic, probabilistic with specific sampling probabilities)?
N/A
Who was involved in the data collection process (e.g., students, crowdworkers, contractors) and how were they compensated (e.g,, how much were crowdworkers paid)? Graduate students and researchers with expertise in formal mathematics and Al.
Were any ethical review processes conducted (e.g., by institutional review board)? If so, please provide a description of these review processes, including the outcomes, as well as link or other access point any supporting documentation. No.
Does the dataset relate to people? If not, you may skip the remainder of the questions in this section. No.
Did you collect the data from the individuals in question directly, or obtain it via third parties or other sources (e.g., websites)? The Lean statements from our data was collected through mathlib and other Lean related github repositories.
Were the individuals in question notified about the data collection? so, please describe (or show with screenshots other information) how notice was provided, and provide link other access point to, or otherwise reproduce, the exact language of the notification itself. N/A
Did the individuals in question consent to the collection and of their data? If so, please describe (or show with screenshots or other information) how consent was requested and provided, and provide link or other access point to, otherwise reproduce, the exact language which the individuals consented. N/A
If consent was obtained, were the consenting individuals provided with a mechanism revoke their consent in the future or for certain uses? If so, please provide a description, well as a link or other access point to the mechanism (if appropriate) N/A
Has analysis of the potential impact of the dataset and its use on data subjects (e.g., data protection impact anel conducted? If so, please provide description of this analysis, including the outcomes, well a link or other access point to any supporting documentation. No.
Any other comments? N/A
P.4 PREPROCESSING/ / CLEANING LABELING
Was any proprccesingddeenngghbeeiene of the data diiere.g. bucketing, tokenization, part-of-speech tagging, SIFT feature extraction, removal of instances, processing of missing values)? If please provide description. If not, you may skip the remainder of the questions in this section.
Yes. Formal Lean statements extracted from mathlib and related repositories and filtering was
33

---

Published as a conference paper at ICLR 2026
applied keep only the relevant Lean statements. Filtering also applied clusters before generating synthetic user queries to avoid invalid synthetic user queries.
Was the "raw" data saved addition to the preprocssed/cteencd/bbbeed data (e.g., to support unanticipated future uses)? If so, please provide link other access point the "raw" data. Yes, raw data and intermediate representations are retained for reproducibility and future use.
Is the software used to preprocess/clan//lbel the instances available? If so, please provide link other access point. The tools and scripts for preprocessing will be released upon acceptance.
Any other comments? No.
P.5 USES
Has the dataset been used for any tasks already? If so, please provide a description. Yes, it was used to train and evaluate the Lean Finder and benchmark its performance against other retrieval models.
Is there a repository that links to any or all papers or systems that use the dataset? so, please provide link other access point. N/A
What (other) tasks could the dataset be used for?
Beyond semantic search and retrieval, the dataset could support tasks such as query generation, informal-to-formal translation, retrieval-augmented theorem proving, and exploring human-AI interaction in formal reasoning systems.
Is there anything about the composition of the dataset or the way was collected and rrggrocssealcleeneedabeeeee that might impact future uses? For example, is there anything that a future user might need to know to avoid uses that could result in unfair treatment of individuals or groups (e.g., stereotyping, quality of service issues) or other undesirable harms (e.g., financial harms, legal risks) If so, please provide a description. Is there anything future user could do to mitigate these undesirable harms? N/A
Are there tasks for which the dataset should not be used? If so, please provide a description. The dataset is not suitable for tasks unrelated Lean 4.
Any other comments?
No.
P.6 DISTRIBUTION
Will the dataset be distributed to third parties outside of the entity (e.g., company, institution, organization) on behalf which the dataset was created? If so, please provide a description. Yes, the dataset will be made publicly available for research purposes.
How will the dataset will be distributed (e.g., tarball website, API, GitHub)? Does the dataset have a digital object identifier (DOI)? The dataset will be distributed via GitHub and academic repositories, with accompanying
34

---

Published as a conference paper at ICLR 2026
documentation.
When will the dataset be distributed?
The dataset is expected to be released following the ICLR 2026 conference.
Will the dataset be distributed under a copyright or other intellectual property (IP) license, and/or under applicable terms of use (ToU)? If so, please describe this license and/or ToU, and provide a link or other access point to, or otherwise reproduce, any relevant licensing terms or ToU, well any fees associated with these restrictions.
Yes, it will be distributed under permissive license (c.g., CC BY-SA 4.0) to encourage research use.
Have any third parties imposed IP-based or other restrictions on the data associated with the instances? If so, please describe these restrictions, and provide link or other access point to, or otherwise reproduce, any relevant licensing terms, as well as any fees associated with these restrictions.
All charts are subjected to their respective copyrights by the authors of this paper.
Do any export controls or other regulatory restrictions apply to the dataset or to individual instances? If so, please describe these restrictions, and provide a link or other access point to, or otherwise reproduce, any supporting documentation. N/A
Any other comments?
Distribution will include detailed usage guidelines ensure proper application of the dataset.
P.7 MAINTENANCE
Who is uupporting/hostiggmmannnt the dataset? The authors of Lean Finder.
How can the owner//uraatormmangge of the dataset be contacted (e.g., email address)?
Contact information will be provided with the dataset release.
Is there an erratum? If so, please provide link or other access point. N/A
Will the dataset be updated (e.g., to correct labeling errors, add new instances, delete instances)? If so, please describe how often, by whom, and how updates will be communicated to users (c.g.. mailing list, GitHub)? Yes, we will frequently update the dataset to include new Lean statements in mathlib and other Lean related repositories we used.
If the dataset relates people, are there applicable limits on the retention of the data associated with the instances (e.g,, were individuals in question told that their data would be retained for fixed period of time and then deleted)? so, please describe these limits and explain how they will be enforced. N/A
Will older versions of the dataset continue to be suporte/hosteemminttieedd If so, please describe how. If not, please describe how its obsolescence will be communicated to users. Yes, previous versions will remain accessible for reproducibility.
35

---

Published as a conference paper at ICLR 2026
If others want to extend/auggment/huld on/contribute to the dataset, is there mechanism for them to do so? If so, please provide description. Will these contributions validated/verified? so, please describe how. If not, why not? Is there process for communicainngddssritttnngg these contributions to other users? If so, please provide description.
Yes, contributions will be encouraged through collaborative platform (e.g., GitHub).
Any other comments?
The dataset's 's maintainers are committed to ensuring its long-term usability and relevance for scientific research.
Q MISC.
URL to our web service, model, and benchmark. We will continually update our system to support more Lean projects and growing database of Lean statements.
Author statement & license information. We the authors bear all responsibility in case of violation of rights.
Dataset Structure. All files are stored the ISONI. format. Each input modality will be stored in separate JSONI. file. Each sample will contain the query and the ground truth I Lean statements. We will also release our corpus of Lean statements.
36


Reviews:
[{"review_id": "8HPScdOIfM", "reviewer": "Reviewer_xHpC", "summary": "This paper proposes **Lean Finder**, a user-centered semantic search engine for Lean and mathlib, aiming to address the bottlenecks of theorem localization difficulty and steep Lean 4 learning curve in formal theorem proving. The core approach involves: collecting 693 real user queries from Lean Zulip and GitHub, filtering and paraphrasing them with GPT-4o, clustering them into 5 user intent categories via OpenAI o3, generating synthetic user queries based on formal Lean statements and the 5 intents to build a 1.4M+ query-code pair dataset, and training a two-stage model (contrastive learning + DPO preference alignment). Evaluations show Lean Finder achieves over 30% relative improvement in retrieval performance compared to baselines like Lean Search and GPT-4o, with 81.6% user preference (from 5 participants) and compatibility with LLM-based provers. The authors promise to release code, models, and datasets upon acceptance, contributing to the Lean community.", "questions": "1. During the filtering and paraphrasing of real user discussions with GPT-4o (Section 3.1.1), what validation measures were taken to ensure that the processed queries do not deviate from the original user intent? For example, was there a manual check of a subset of queries or a comparison with user feedback?\n2. Why were newer retrievers like LEAN-EXPLORE not included in the baseline comparison? If there were practical constraints (e.g., unavailable code), could you analyze the potential differences in design principles between Lean Finder and these tools, and explain how Lean Finder might excel or fall short?\n3. Regarding the 5 user intent categories, did you test whether they can cover the intents of newly collected user queries (beyond the initial 693)? If not, do you have plans to expand or dynamically adjust the intent categories to reduce the \"difference set\" with the complete intent set?\n4. Given the small sample size (5 participants) in the user preference study, do you plan to conduct a larger-scale user study (e.g., involving more Lean practitioners from different backgrounds) to verify the generalizability of the 81.6% preference rate?\n5. For differences in theorem paths or syntax across Lean versions, what technical routes do you consider to make Lean Finder compatible with multiple versions? For example, will you build a version-aware index or a mapping between theorem names across versions?", "limitations": "", "rating": 4, "confidence": 4, "soundness": 3, "presentation": 3, "contribution": 3, "strengths": "1. **Targeted Problem-Solving**: Directly addresses core pain points in Lean usage (theorem localization and language learning curve) that hinder formal theorem proving progress, with strong practical relevance for mathematicians and Lean users.\n2. **User-Centered Data Construction**: Innovatively clusters real user intents (5 categories) to guide synthetic query generation, solving the scarcity of high-quality real user query data. The 1.4M+ multimodal query-code dataset (synthetic queries, informalized statements, etc.) is the largest Lean code search dataset to date, laying a solid foundation for model training.\n3. **Rigorous Model Design**: The two-stage training pipeline (contrastive learning for embedding alignment + DPO for human preference alignment) balances retrieval performance and user adaptability, and evaluations across multiple input modalities (informalized statements, proof states) demonstrate robust generalization.\n4. **Community Value**: The commitment to release code, models, and datasets will provide valuable resources for the Lean and formal theorem proving communities, promoting follow-up research and practical applications.", "weaknesses": "1. **Potential Bias in Query Filtering/Paraphrasing**: The use of GPT-4o to filter and paraphrase real user discussions may introduce inconsistencies—GPT-4o’s interpretation of \"questions answerable by Lean statements\" and its paraphrasing style could deviate from the original user intent, affecting the authenticity of subsequent intent clustering and synthetic query generation.\n2. **Incomplete Baseline Comparison**: Fails to compare with newer Lean retrievers (e.g., LEAN-EXPLORE), nor does it analyze the advantages/disadvantages of such state-of-the-art tools. This limits the paper’s ability to fully demonstrate Lean Finder’s competitiveness in the current research landscape.\n3. **Limited Coverage of User Intents**: The 5 clustered user intent categories may not fully cover all real-world user intents (there is likely a \"difference set\" from the complete set of intents). This could lead to synthetic queries that miss niche or underrepresented user needs, restricting Lean Finder’s applicability to diverse scenarios.\n4. **Small-Scale User Preference Study**: The 81.6% user preference rate is based on only 5 participants, which is a small sample size. This may result in biased or ungeneralizable conclusions about user acceptance, weakening the credibility of the user-centric design claim.\n5. **Lack of Solutions for Lean Version Differences**: Lean’s different versions may lead to changes in theorem paths or syntax, but the paper does not propose solutions to handle such version-related inconsistencies. This could reduce Lean Finder’s practicality when applied to different Lean versions.", "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": "IPPDJzSiy2", "reviewer": "Reviewer_jNAc", "summary": "This paper proposes an intelligent search tool for the Lean 4 formal mathematical proof system—Lean Finder. This system aims to help mathematical researchers and automated theorem proving models more efficiently retrieve lemmas and theorems relevant to their current proof tasks.\n\nIt analyzes queries posted by real mathematicians on public platforms and clusters them into different user intentions. Based on these user intentions, it generates synthetic user queries for Lean formal statements to build a training dataset.\n\nThen, through contrastive learning and the DPO algorithm, the large model is fine-tuned to obtain a model that better matches human query intentions. The model achieves good performance.", "questions": "In line 201, the paper mentions “high-quality discussion.” Could the authors clarify how “high-quality” is defined in this context? Specifically, what criteria or metrics are used to determine whether a discussion qualifies as high-quality data?", "limitations": "", "rating": 4, "confidence": 3, "soundness": 3, "presentation": 2, "contribution": 3, "strengths": "1. Lean Finder addresses the scarcity of query and answer data in Lean when constructing datasets. It first clusters queries from real mathematicians to identify different user intents, then generates prompts based on these intents. Secondly, to construct data pairs, it utilizes a large model to synthesize inverse queries based on Lean formal statements, resulting in a large dataset.\n\n2. During model training, it fine-tunes the model using contrastive learning and DPO methods, achieving better results compared to current methods.", "weaknesses": "1. While the paper describes how synthetic user queries are generated from formal Lean statements, it does not provide a quantitative or qualitative analysis of the semantic quality, correctness, or diversity of these synthesized queries. Such an evaluation would be crucial to demonstrate the reliability of the training data.\n\n2. The fine-tuning experiments are conducted solely on the DeepSeek-Prover-V1.5-RL 7B model. It remains unclear whether the proposed approach generalizes to other base models or architectures. Moreover, the paper lacks a comparison with existing large retrieval models that could serve as relevant baselines.\n\n3. In the experiment that examines whether Lean Finder can serve as a prover-agnostic retrieval tool, the paper does not include results combining other Lean search or Lean state search methods with the referenced provers.", "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": "rVgztc32bZ", "reviewer": "Reviewer_2WYg", "summary": "This paper proposes a semantic search engine for Lean and its mathematical library mathlib, named Lean Finder. The core objective of this work is to better understand the true intent of mathematicians to address the inefficiency of existing search tools when handling ambiguous, non-canonical queries. The authors mine user intent by analyzing public Lean community discussions and, based on this, \"reverse-engineer\" a large-scale training dataset of simulated real-world user queries. The model is fine-tuned using contrastive learning and Direct Preference Optimization (DPO) to align with user preferences. Experimental results show that Lean Finder achieves significant improvements over the existing Lean Search and the general-purpose GPT-4o model across multiple evaluation metrics, and it received a higher preference rate in a user study.", "questions": "1.  Regarding the choice of baselines, why did you not include newer Lean search systems like LeanExplore in your comparison? Given the existence of these systems, how do you support Lean Finder's leading position?\n2.  When comparing with Lean Search, did you consider its \"query augmentation\" feature?", "limitations": "", "rating": 4, "confidence": 4, "soundness": 2, "presentation": 3, "contribution": 2, "strengths": "1.  **High Importance of the Problem:** How to efficiently find required theorems in the vast mathlib library is a recognized pain point for the Lean community and the entire field of formal mathematics. This paper is dedicated to solving a very practical and impactful problem.\n\n2.  **Potential Community Value:** If the performance improvements reported in the paper hold up under fairer comparisons, Lean Finder could become a very useful tool for Lean developers and mathematicians, potentially increasing the efficiency of formalization work significantly.", "weaknesses": "Although the motivation and basic idea of this paper are commendable, there are several major flaws in demonstrating its effectiveness, which severely impact the credibility of its conclusions.\n\n1.  **Baselines for Comparison are Severely Insufficient and Outdated:**\n    *   The paper's primary comparison is with Lean Search (Gao et al., 2024a/b). Some time has passed since that work was published. In the interim, other new search tools have emerged in the Lean community, such as **LeanExplore (Asher, 2025)**. These tools may use different technical approaches or index a broader range of data. A paper claiming to achieve state-of-the-art (SOTA) performance should be comprehensively compared with all relevant systems, especially the latest ones. Merely outperforming a system from over a year ago is not sufficient to prove its superiority.\n\n2.  **Obvious Fairness Issues in Experimental Setup and Comparison Methods:**\n    *   **The comparison with Lean Search is likely unfair:** The paper repeatedly emphasizes its advantage in handling \"ambiguous user queries.\" However, the original Lean Search paper and system include a key technique specifically designed for such queries: **query augmentation**. This paper does not seem to have enabled or discussed this feature in its comparative experiments, instead directly testing the system with raw, ambiguous queries, which it may not be optimized for. This constitutes a comparison under an \"unintended use case,\" and the results naturally favor the proposed model. A fair comparison should be conducted with both systems running in their optimal configurations.\n    *   **Using GPT-4o as a primary baseline is not convincing:** GPT-4o is a powerful general-purpose large language model, but it is not a specialized model specifically optimized for the highly vertical task of Lean theorem retrieval. It may not be familiar with Lean 4 syntax, the internal structure of mathlib, or its naming conventions. Therefore, it is not surprising that Lean Finder surpasses GPT-4o. More importantly, this does not prove that it is superior to other **purpose-built** theorem search systems.\n    *   **The numerical results are consequently less persuasive:** The paper's claimed \"over 30% relative improvement\" was obtained on the aforementioned unfair baselines. If compared against Lean Search with query augmentation enabled or other more advanced systems, this advantage might significantly shrink or even disappear.\n\n3.  **Limited Methodological Innovation:**\n    *   The core techniques of this paper—**Contrastive Learning** for training retrieval models, synthesizing data oriented towards user intent, and **Direct Preference Optimization (DPO)** for aligning with human feedback—are all mature and standard techniques in the current fields of retrieval and alignment. While successfully applying these techniques to the Lean domain is a valuable engineering practice, from the perspective of algorithmic innovation, this paper does not propose a new model architecture or training paradigm.", "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": "8ngr2R4V1O", "reviewer": "Reviewer_XmGe", "summary": "The paper introduces Lean Finder, a semantic search engine for Lean and mathlib designed to better reflect the intents of mathematicians. It aims to improve retrieval of relevant theorems by moving beyond naive string or informalized statement matching. The system clusters semantic patterns from public Lean discussions, fine-tunes text embeddings on synthesized user-style queries, and incorporates human preference feedback to align results with mathematicians’ goals. Evaluations show roughly 30% relative improvement over existing Lean search engines and GPT-4o on several retrieval benchmarks. The method integrates cleanly with LLM-based theorem provers, offering a bridge between retrieval and formal reasoning.", "questions": "1. Can the pipeline be extended to include more types of interactions with human feedback involved?\n2. Is it possible to provide ablation studies on each component to evaluate more on their contributions?\n3. I have some concern on the use of OpenAI API since they are constantly updated and their code/weight is not released to the public, and I would personally doubt if relying on it will harm the reproducibility of your results. How would you justify this part?", "limitations": "", "rating": 6, "confidence": 3, "soundness": 3, "presentation": 3, "contribution": 3, "strengths": "1. Timely and useful application: it addresses a real pain point in the Lean community (retrieving theorems efficiently), motivation is clear, relevant, and meaningful.\n2. Reasonable methodology grounding and convincing empirical validation: The pipeline is technically consistent and design decisions are reasonably justified, even if not groundbreaking. The quantitative results (e.g., relative gain) demonstrate significant improvement over SOTA baselines.\n3. Writing is coherent, the structure clear, and the contribution easy to follow despite imperfect figures. And also, they released their code already. This is very helpful in understanding more details of their work.", "weaknesses": "1. Significant improvement can be made to the figures, especially Fig 1 and Fig 5, they are not even close to informative. It would be better off without them if your figure content can be replaced by a sentence or two.\n2. Not so much discussion on the results. Would like to see more investigation into what makes your method so different from everyone else's and what makes the improvement so significant, if possible (maybe through some solid ablation study, if pages permit).\n3. Real user feedback is integrated in the simplest form possible, basically just upvoting and downvoting. This is a good starting point though, but still kind of limited.", "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 (Poster)