Builds a semantic search engine over Mathlib declarations, trained with adversarially generated ambiguous queries, and tests it on Lean theorem proving with Claude Code.
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/
Problem
Mathematicians and coding agents usually search Mathlib with short, ambiguous queries: properties, notation, aliases or hypotheses. Existing Mathlib search engines assume context-rich queries, and labeled short queries paired with Mathlib statements are scarce.
Approach
A Qwen3-4B query generator is trained with RL plus SFT. Its reward combines retriever-guided difficulty with an LLM judge's check that each query stays faithful to its source declaration, so it produces challenging but correct short queries for Mathlib declarations. These query-declaration pairs fine-tune a Qwen3-Embedding-8B retriever by contrastive learning, over two alternating generator-retriever rounds. The same synthetic pairs are reused to optimize a query-rewriting prompt with GEPA.
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 learn
Results
On the 810-query MathlibQR benchmark, Lean Finder V2 reaches nDCG@1 of 0.558 and Recall@10 of 0.893, at least an 11% relative improvement over the previous best Mathlib search engines. LLM judges rank it best on unlabeled real-world human and coding-agent queries. Used as a tool for Claude Code, it gives the highest theorem-proving pass rate, 39.3%.
System
nDCG@1
nDCG@10
Recall@10
LeanSearch V2 (retriever+reranker)
0.470
0.623
0.780
Claude Code (Sonnet 5)
0.527
0.641
0.747
Lean Finder
0.370
0.533
0.698
Lean Finder V2
0.558
0.732
0.893
MathlibQR retrieval (selected systems)
Retrieval tool
Pass rate (%)
No semantic retrieval tool
34.0 ± 1.0
LeanExplore
27.3 ± 0.6
Lean Finder
30.7 ± 1.2
LeanSearch V2 (retriever+reranker)
36.0 ± 1.0
Lean Finder V2
39.3 ± 1.2
Claude Code theorem-proving pass rate by retrieval tool
