Lean Finder V2: Semantic Search for Mathlib That Disambiguates User Queries

Jialin Lu; Xiaoyu Liu; Hengrui Luo; Rodrigo Stehling; Linxi Liu; Weiran Sun; Yuepeng Wang; Wuyang Chen

cs.LGOct 22, 2026

Lean Finder V2: Semantic Search for Mathlib That Disambiguates User Queries

Authors: Jialin Lu, Xiaoyu Liu, Hengrui Luo, Rodrigo Stehling, Linxi Liu, Weiran Sun, Yuepeng Wang, Wuyang Chen

Organizations: Simon Fraser University · Rice University · University of Pittsburgh

Abstract

We introduce Lean Finder V2, a semantic search framework for Mathlib that disambiguates user queries through complementary model-level adversarial training and input-level query rewriting. Human mathematicians and coding agents rarely search Mathlib by providing detailed context. In practice, they query short properties, notation, aliases, or hypotheses, leaving much of the intended mathematics implicit. In contrast, existing Mathlib search engines unrealistically assume context-rich queries. The scarcity of real-world short queries paired with ground-truth Mathlib statements makes this ambiguity even more intractable. We argue that this is essentially a data problem. Through adversarial training, we scale up the generation of labeled short and ambiguous queries, and learn to disambiguate user queries at both model-level fine-tuning and input-level query rewriting. On the human-curated MathlibQR benchmark, our Lean Finder V2 sets a new state of the art, with at least 11% relative improvement over the previous best Mathlib semantic search engines. On top of our state-of-the-art retriever, optimized query rewriting further improves MathlibQR retrieval. On unlabeled queries from human and coding-agent interactions, Lean Finder V2 is ranked as the strongest system. Integrated with Claude Code, Lean Finder V2 improves proof success on downstream theorem-proving task. Lean Finder V2 is available at: https://leanfinder.github.io/

Figures & tables

Panel of Figure 1 — Figure 1: Real-world queries expose the ambiguity gap. (a) Human and coding-agent queries contain far less explicit context than statement informalizations which are commonly used to train Lean search engines, as shown by the length gap. Our generated queries used to train retrievers better match the length of real-world queries. Table 6 shows more details. (b) Every existing Lean search engine performs worse on ambiguous queries compared to context-rich ones, with Lean Finder V2 closing the gap to the smallest 2.6 percentage points and having the best performance on both query types. This further demonstrates previous Lean search engines leave the ambiguity gap unaddressed.

Figure 2: Lean Finder V2 disambiguates Mathlib queries at two complementary levels. Model-level adversarial training (Section 3.1 ) uses a hybrid objective that combines reinforcement learning and supervised fine-tuning with retriever-guided difficulty rewards to incentivize the query generator LLM to generate faithful, challenging, and ambiguous queries for Mathlib declarations. Contrastive learning on these query-declaration pairs improves the retriever, which supplies the query-difficulty feedback for the next training round of the generator. Input-level query rewriting (Section 3.2 ) uses the same generator-produced query-declaration pairs as the training data for optimizing the query-rewriting prompt, guided by the rank-improvement feedback based on the retriever. The optimized query rewriting prompt makes implicit mathematical context explicit before retrieval.

		nDCG@ $k$			Recall@ $k$
System	Model size	1	5	10	10	50	100
LeanExplore	109M	0.246	0.358	0.393	0.569	0.743	0.789
LeanSearch V2 (retriever-only)	8B	0.340	0.472	0.494	0.657	0.790	0.830
LeanSearch V2 (retriever+reranker)	8B + 8B	0.470	0.601	0.623	0.780	0.847	0.858
Claude Code (Sonnet 5)	–	0.527	0.629	0.641	0.747	–	–
TheoremGraph	8B	0.391	0.534	0.558	0.733	–	–

Table 1: Retrieval performance on the 810-query MathlibQR fair set of short, human-written queries. Systems in comparison include LeanExplore, LeanSearch V2, Claude Code (Sonnet 5), TheoremGraph, Lean Finder, and three Lean Finder V2 variants (Round 0, Round 1, and the final model). Lean Finder V2 denotes the final model. As TheoremGraph uses cutoff of 10 in Kurgan et al. (2026) , its Recall@50 and Recall@100 are not reported. Claude Code returns only ten candidates, so its Recall@50 and Recall@100 are also not reported. We also report the model size of each system in comparison. Best results in each metric column are bold .

	nDCG@ $k$			Recall@ $k$
System	1	5	10	10	50	100
LeanExplore	0.180	0.376	0.406	0.661	0.837	0.872
LeanSearch V2 (retriever-only)	0.414	0.569	0.596	0.783	0.907	0.942
LeanSearch V2 (retriever+reranker)	0.506	0.669	0.691	0.873	0.954	0.964
Claude Code (Sonnet 5)	0.245	0.345	0.363	0.485	–	–
Lean Finder	0.544	0.720	0.742	0.914	0.980	0.989

Table 2: Retrieval performance on the 2,526-query context-rich test set. Systems in comparison include LeanExplore, LeanSearch V2, Claude Code (Sonnet 5), Lean Finder, and three Lean Finder V2 variants (Round 0, Round 1, and the final model). Lean Finder V2 denotes the final model. Claude Code returns only ten candidates, so its Recall@50 and Recall@100 are not reported. Best results in each column are bold .

	GPT-5.6 Sol		Claude Opus 5
System	Mean rank $\downarrow$	Rank 1	Mean rank $\downarrow$	Rank 1
LeanExplore	3.740	14 (7.0%)	3.735	8 (4.0%)
LeanSearch V2 (retriever+reranker)	2.380	52 (26.0%)	2.305	64 (32.0%)
Claude Code (Sonnet 5)	3.775	32 (16.0%)	3.920	22 (11.0%)
Lean Finder	3.125	32 (16.0%)	3.095	30 (15.0%)
Lean Finder V2	1.980	70 (35.0%)	1.945	76 (38.0%)

Table 3: LLM-judged retrieval preference on 200 unlabeled deployment queries. GPT-5.6 Sol and Claude Opus 5 independently rank LeanExplore, LeanSearch V2, Claude Code (Sonnet 5), Lean Finder, and Lean Finder V2. Rank 1 is reported as count (percentage); lower mean rank is better. Best results are bold .

	nDCG@ $k$			Recall@ $k$
Input Rewrite Config.	1	5	10	10	50	100
Original query (no rewrite)	$0.558$	$0.707$	$0.732$	$0.893$	$0.956$	$0.973$
LeanSearch augmentation	$0.475{\scriptstyle\,\pm\,0.006}$	$0.612{\scriptstyle\,\pm\,0.004}$	$0.637{\scriptstyle\,\pm\,0.004}$	$0.808{\scriptstyle\,\pm\,0.004}$	$0.908{\scriptstyle\,\pm\,0.005}$	$0.936{\scriptstyle\,\pm\,0.005}$
LeanDex augmentation	$0.520{\scriptstyle\,\pm\,0.013}$	$0.665{\scriptstyle\,\pm\,0.009}$	$0.688{\scriptstyle\,\pm\,0.009}$	$0.852{\scriptstyle\,\pm\,0.008}$	$0.944{\scriptstyle\,\pm\,0.005}$	$0.962{\scriptstyle\,\pm\,0.005}$
GEPA seed rewriting	$0.532{\scriptstyle\,\pm\,0.002}$	$0.674{\scriptstyle\,\pm\,0.004}$	$0.695{\scriptstyle\,\pm\,0.005}$	$0.854{\scriptstyle\,\pm\,0.010}$	$0.942{\scriptstyle\,\pm\,0.004}$	$0.963{\scriptstyle\,\pm\,0.004}$
GEPA-optimized rewriting	$\mathbf{0.588}{\scriptstyle\,\pm\,0.004}$	$\mathbf{0.722}{\scriptstyle\,\pm\,0.003}$	$\mathbf{0.741}{\scriptstyle\,\pm\,0.002}$	$\mathbf{0.895}{\scriptstyle\,\pm\,0.002}$	$\mathbf{0.964}{\scriptstyle\,\pm\,0.007}$	$\mathbf{0.975}{\scriptstyle\,\pm\,0.003}$

Table 4: Query-rewriting performance on the 810-query MathlibQR fair set . We compare GEPA-optimized rewriting with no rewriting, LeanSearch and LeanDex augmentation, and the GEPA seed prompt rewriting. Each rewriting method produces three query sets, with the Lean Finder V2 retriever fixed; results report their mean and standard deviation, while the no-rewriting condition is evaluated once. Best results in each column are bold .

Retrieval tool	Pass rate (%)
No semantic retrieval tool	$34.0{\scriptstyle\,\pm\,1.0}$
LeanExplore	$27.3{\scriptstyle\,\pm\,0.6}$
Lean Finder	$30.7{\scriptstyle\,\pm\,1.2}$
LeanSearch V2 (retriever+reranker)	$36.0{\scriptstyle\,\pm\,1.0}$
Lean Finder V2	$\mathbf{39.3}{\scriptstyle\,\pm\,1.2}$

Table 5: Theorem-proving performance on FATE-H benchmark. Mean pass rates and standard deviations of Claude Code (Sonnet 5) over three runs under matched agent settings and budgets; best result is bold .

Appendix figures & tables9 assets

Supplementary material from the paper’s appendix.

Appendix

	Source	Median length	Count
Training data	Informalizations ( Lu et al., 2026 ; Gao et al., 2026 )	82	309579
	Synthetic user queries ( Lu et al., 2026 )	34	503378
	Our synthetic queries (Round 1)	15	307085
	Our synthetic queries (Round 2)	14	306948
Real-world & Test queries	MathlibQR ( Gao et al., 2026 )	14	810
	Human queries	16	20000

Appendix

Table 6: Median query length in tokens (Qwen3 tokenizer). Human and coding-agent queries are collected from 1 month period of Lean Finder usage.

	nDCG@ $k$			Recall@ $k$
Configuration	1	5	10	10	50	100
Round 0	0.463	0.590	0.611	0.760	0.864	0.901
Round 1 (difficulty only)	0.453	0.575	0.602	0.762	0.870	0.919
Round 1 (alignment only)	0.463	0.598	0.623	0.780	0.884	0.910
Round 1 (full reward)	0.520	0.657	0.682	0.842	0.925	0.951

Appendix

Table 7: Ablation of the query-generator reward after one generator-retriever training round on the 810-query MathlibQR fair set. Round 0 uses only context-rich data; the Round 1 variants differ only in the reward used to train the query generator. Generator steps, sampling budgets, and retriever steps are matched. Best result in each column is bold.

	nDCG@ $k$			Recall@ $k$
Configuration	1	5	10	10	50	100
Round 0	0.563	0.720	0.743	0.910	0.967	0.981
Round 1 (difficulty only)	0.530	0.689	0.711	0.879	0.956	0.975
Round 1 (alignment only)	0.552	0.718	0.738	0.903	0.968	0.980
Round 1 (full reward)	0.569	0.728	0.743	0.916	0.985	0.993

Appendix

Table 8: Ablation of the query-generator reward after one generator-retriever training round on the context-rich test set. The configurations and matched training budgets are identical to Table 7 . Best result in each column is bold.

	nDCG@ $k$			Recall@ $k$
Round	1	5	10	10	50	100
Round 0	0.463	0.590	0.611	0.760	0.864	0.901
Frozen base-generator control
Round 1	0.472	0.603	0.628	0.791	0.895	0.921
Round 2	0.469	0.597	0.620	0.789	0.898	0.919
Expert-query SFT-generator control

Appendix

Table 9: Ablation of generator RL training on the 810-query MathlibQR fair set. Round 1 uses one generated query per declaration, and Round 2 uses two in total. All retrievers receive a matched number of optimization steps. Best result in each column is bold .

	nDCG@ $k$			Recall@ $k$
Round	1	5	10	10	50	100
Round 0	0.563	0.720	0.743	0.910	0.967	0.981
Frozen base-generator control
Round 1	0.559	0.710	0.729	0.894	0.967	0.981
Round 2	0.552	0.705	0.725	0.890	0.965	0.981
Expert-query SFT-generator control

Appendix

Table 10: Ablation of generator RL training on the context-rich test set. The configurations are identical to Table 9 , and all retrievers receive a matched number of optimization steps. Best result in each column is bold .

Judge	Agreements	Agreement (%)
GPT-5.6 Sol	738/810	91.11
Claude Opus 5	745/810	91.98

Appendix

Table 11: Agreement of GPT-5.6 Sol and Claude Opus 5 with human-curated labels on the 810-query MathlibQR fair set. Each judge selects one of five candidate declarations; we report agreement counts and rates.

	nDCG@ $k$			Recall@ $k$
System	1	5	10	10	50	100
LeanExplore	0.246	0.358	0.393	0.569	0.743	0.789
LeanSearch V2 (retriever-only)	0.340	0.472	0.494	0.657	0.790	0.830
LeanSearch V2 (retriever+reranker)	0.470	0.601	0.623	0.780	0.847	0.858
Claude Code (Sonnet 5)	0.527	0.629	0.641	0.747	–	–
Lean Finder	0.370	0.514	0.533	0.698	0.824	0.875

Appendix

Table 12: Retrieval performance on the 810-query MathlibQR fair set of short, human-written queries. Systems include LeanExplore, LeanSearch V2, Claude Code (Sonnet 5), Lean Finder, Lean Finder V2 with and without our reranker, and Lean Finder V2 with both our reranker and GEPA-optimized query rewriting. Lean Finder V2 denotes the retriever-only model. Claude Code returns only ten candidates, so its Recall@50 and Recall@100 are not reported. Best results in each column are bold.

	nDCG@ $k$			Recall@ $k$
System	1	5	10	10	50	100
LeanExplore	0.180	0.376	0.406	0.661	0.837	0.872
LeanSearch V2 (retriever-only)	0.414	0.569	0.596	0.783	0.907	0.942
LeanSearch V2 (retriever+reranker)	0.506	0.669	0.691	0.873	0.954	0.964
Claude Code (Sonnet 5)	0.245	0.345	0.363	0.485	–	–
Lean Finder	0.544	0.720	0.742	0.914	0.980	0.989

Appendix

Table 13: Retrieval performance on the 2,526-query context-rich test set. Systems in comparison include LeanExplore, LeanSearch V2, Claude Code (Sonnet 5), Lean Finder, and Lean Finder V2 with and without our reranker. Lean Finder V2 denotes the retriever-only model. Claude Code returns only ten candidates, so its Recall@50 and Recall@100 are not reported. Best results in each column are bold.

System	Retrieval configuration	Parameters
LeanExplore	Retriever	109M
LeanSearch V2	Retriever only	8B
LeanSearch V2	Retriever + reranker	8B + 8B
TheoremGraph	Retriever	8B
Lean Finder	Retriever	7B
Lean Finder V2	Retriever	8B

Appendix

Table 14: Retrieval-model scale for the systems in Table 1 . For a two-stage system, the values before and after

+

give the retriever and reranker sizes, respectively.

Semantic Search

Semantic search retrieves information by meaning, matching queries and documents even when they use different words.

See all 42 papers

LeanSearch v2: Global Premise Retrieval for Lean 4 Theorem Proving
May 13, 2026Guoxiong Gao, Zeming Sun, Jiedong Jiang +5Lean Theorem Proving Evidence Retrieval
School of Mathematical Sciences, Peking University · 2IQuest Research · 3Research Institute for Mathematical Sciences, Kyoto University +5
TheoremGraph: Bridging Formal and Informal Mathematics
Jun 24, 2026Simon Kurgan, Evan Wang, Eric Leonen +6KG Construction Graph-Based Retrieval
University of Washington Math AI Lab
EquivPruner: Boosting Efficiency and Quality in LLM-Based Search via Action Pruning
May 22, 2025Jiawei Liu, Qisi Chen, Jianshu Zhang +2LLM Inference Efficiency Semantic Textual Similarity
School of Computer Science and Technology, University of Science and Technology of China · Department of Data Science, City University of Hong Kong · iFLYTEK Research

May 13, 2026J/K move · Enter open · S save

LeanSearch v2: Global Premise Retrieval for Lean 4 Theorem Proving

Guoxiong Gao, Zeming Sun, Jiedong Jiang, Yutong Wang+4

School of Mathematical Sciences, Peking University · 2IQuest Research · 3Research Institute for Mathematical Sciences, Kyoto University+5

Lean Theorem Proving Evidence Retrieval

Open paper AskPDF arXiv

Proving theorems in Lean 4 often requires identifying a scattered set of library lemmas whose joint use enables a concise proof -- a task we call global premise retrieval. Existing tools address adjacent problems: semantic search engines find individual declarations matching a query, while premise-selection systems predict useful lemmas one tactic step at a time. Neither recovers the full premise set an entire theorem requires. We present LeanSearch v2, a two-mode retrieval system for this task. Its standard mode applies a hierarchy-informalized Mathlib corpus with an embedding-reranker pipeline, achieving state-of-the-art single-query retrieval without domain-specific fine-tuning (nDCG@10 of 0.62 vs. 0.53 for the next-best system). Its reasoning mode builds on standard mode as its retrieval substrate, targeting global premise retrieval through iterative sketch-retrieve-reflect cycles. On a 69-query benchmark of research-level Mathlib theorems, reasoning mode recovers 46.1% of ground-truth premise groups within 10 retrieved candidates, outperforming strong reasoning retrieval systems (38.0%) and premise-selection baselines (9.3%) on the same benchmark. In a controlled downstream evaluation with a fixed prover loop, replacing alternative retrievers with LeanSearch v2 yields the highest proof success (20% vs. 16% for the next-best system and 4% without retrieval), confirming that retrieval quality propagates to proof generation. We have open-sourced all code, data, and benchmarks. Code and data: https://github.com/frenzymath/LeanSearch-v2 . The standard mode is publicly available with API access at https://leansearch.net/ .

Abstract

Semantic Search

Explore similar work

LeanSearch v2: Global Premise Retrieval for Lean 4 Theorem Proving

TheoremGraph: Bridging Formal and Informal Mathematics

EquivPruner: Boosting Efficiency and Quality in LLM-Based Search via Action Pruning