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

Mathlib is the mathematics library of the Lean proof assistant and contains a large number of theorems and definitions; people writing proofs and coding agents alike must first find suitable theorems in it. Real search queries are short: the median length of human-written queries is 16 tokens and of agent-written queries 15, while the natural-language paraphrases of theorems used to train earlier retrievers have a median length of 82 tokens. Short queries leave out much of the intent, and the same phrase may correspond to several similar theorems. Lean Finder V2 tackles the problem from both ends. On the model side, the authors use reinforcement learning to train a query generator that writes, for each theorem, short queries the current retriever ranks poorly but whose meaning still matches; these queries train the retriever, the new retriever then scores the generator, and the two alternate for two rounds, producing more than 600,000 query–theorem pairs. On the input side, the authors use GEPA to automatically optimize a rewriting prompt that makes the user's short query more explicit before retrieval. On MathlibQR, made up of 810 human-written short queries, Lean Finder V2 reaches Recall@10 of 0.893, against 0.780 for the previous best retriever-plus-reranker system. In the ablation, rewarding only "hard" without checking whether the query and theorem agree makes the top-rank metrics worse than using no synthetic data at all, because the generator learns to write off-target queries to manufacture difficulty.

1. Why short queries are hard to search

The paper gives an example: the target is Mathlib's theorem that "a constant function is even". Searching with a complete description (stating the types, the form of the function and f(−x)=f(x)) puts the target at rank 1; switching to the synonymous short query "constant function invariant under input negation" drops the target to rank 7, because the short query does not name the Mathlib concept of an "even function". Such queries are common in practice: the authors gathered 20,000 human-written queries and 100,000 agent queries, and both length distributions center around 15 tokens. Earlier retrievers were trained on long paraphrases of theorems and learned to match detailed descriptions item by item, so with short queries they cannot tell several similar candidates apart.

2. Method

2.1 Initial retriever

The retriever starts from Qwen3-Embedding-8B and is fine-tuned with contrastive learning: each query and its theorem form a positive pair, and the other theorems in the same batch are negatives. Many theorems in Mathlib are close to one another, so the authors remove from the negatives any candidate whose cosine similarity exceeds that of the positive by more than a threshold $m$, to avoid penalizing theorems that are in fact also correct. The initial training data are existing long paraphrases and synthetic queries; this step yields the round-0 retriever.

2.2 Generating hard queries with reinforcement learning

The query generator is Qwen3-4B, trained with GRPO (a reinforcement learning method that updates the policy by the relative quality of results sampled within the same group). It generates one short query per theorem, with the reward:
$$r=\max \{0,j(q,d)\cdot f_{\mathrm{rank}}(k)-{\lambda }_{\mathrm{len}}{p}_{\mathrm{len}}(L)\}$$
Here $q$ is the generated query, $d$ the theorem, $k$ the rank the current retriever gives the target theorem, and $L$ the query length. The three terms do the following:

• Consistency $j(q,d)$: GPT-OSS-120B judges whether the query and theorem state the same thing; if not, it is 0 and the whole reward goes to zero.
• Difficulty $f_{\mathrm{rank}}(k)$: if the target theorem ranks in the top 5, the query is too easy and scores 0; between ranks 5 and 30 the reward grows logarithmically with rank; between ranks 30 and 100 it scores the full 1; outside the top 100 it scores 0, because that most likely means the query is wrong rather than revealing a weakness of the retriever.
• Length penalty: queries longer than 40 tokens start losing points, reaching the full penalty at 50 tokens, with penalty coefficient ${\lambda }_{\mathrm{len}}=0.15$. The threshold is based on the length distribution of real queries: the 90th percentiles of human and agent queries are 37 and 28 tokens.

Training also mixes in some supervised fine-tuning whose targets are queries in the real style of how humans and agents search, with the mixing ratio decreasing over training: early on, the supervised signal pins the generator's writing near real queries, and later updates follow mainly the reinforcement learning reward. After each round of generator training, the authors use it to generate more than 300,000 queries for Mathlib theorems and retrain the retriever on them together with the existing long-paraphrase data; the new retriever then provides the ranking reward for the next round. The two alternate for two rounds in total.

2.3 Rewriting queries before retrieval

On the input side, GEPA optimizes the rewriting prompt. GEPA is a method for automatically revising prompts: a candidate prompt rewrites a small batch of queries, the fixed Lean Finder V2 retriever ranks the target theorems, the prompt is revised based on the ranks and textual feedback, and only versions that improve are kept. Both rewriting and prompt optimization use DeepSeek-V4.1-Flash, and the queries used for optimization come from the synthetic data of Section 2.2, not the test set.

3. Experiments

3.1 Main results: a large lead on short queries, no regression on long ones

This experiment checks whether Lean Finder V2 beats existing systems on short queries without getting worse on long ones. The short-query test set is MathlibQR, with 810 human-written short queries; the long-query test set has 2,526 complete descriptions. The authors ensure that the target theorems in the test sets and their queries never entered training at any stage. The compared systems are: LeanExplore (a 109M-parameter retriever); LeanSearch V2, also based on Qwen3-Embedding-8B, optionally with an 8B reranker; TheoremGraph; the predecessor Lean Finder (7B); and Claude Code (Sonnet 5) searching the documentation itself. The table below is taken from the paper's Table 1 (MathlibQR):

Lean Finder V2 uses a single retriever and beats LeanSearch V2 with its 8B reranker on every metric. Both retrievers start from the same Qwen3-Embedding-8B, so the gap comes mainly from the training data. From round 0 to the final version, nDCG@1 rises from 0.463 to 0.558, and this gain comes entirely from the adversarially generated short queries, because round 0 used only existing long-paraphrase data. Claude Code also reaches nDCG@1 of 0.527; the authors attribute this to Sonnet 5 knowing Mathlib's naming conventions and being able to search the documentation repeatedly.

On the long-query test set, Lean Finder V2 reaches nDCG@10 of 0.749 and Recall@10 of 0.919, against 0.742 and 0.914 for the predecessor Lean Finder (paper Table 2): adding a large amount of short-query training does not hurt long-query retrieval.

3.2 Real unlabeled queries

This experiment checks whether Lean Finder V2 is still better on real queries with no reference answers. The authors take 200 real human and agent queries, shuffle the five systems' results and hide the system names, and have GPT-5.6 Sol and Claude Opus 5 each rank the five systems by usefulness. Both judges place Lean Finder V2 first: mean rank 1.980 and 1.945, ranking first on 35% and 38% of queries respectively; the corresponding figures for LeanSearch V2 are 26% and 32%. The two judges agree 89% of the time.

3.3 Query rewriting

This experiment checks whether rewriting before retrieval adds further gains. The retriever is fixed to Lean Finder V2, and each rewriting method generates three times. The GEPA-optimized prompt raises nDCG@1 from 0.558 without rewriting to 0.588 (standard deviation over three runs 0.004); the initial version of the same prompt before optimization reaches only 0.532, worse than not rewriting; the two existing rewriting methods LeanSearch and LeanDex reach 0.475 and 0.520. Recall@100 is already 0.973, so rewriting mainly moves the correct theorem from among the candidates into the top few ranks. Adding the authors' own 8B reranker brings nDCG@1 to 0.610.

3.4 Downstream proving

This experiment checks whether better retrieval actually helps write proofs. FATE-H is a set of 100 fairly hard formal algebra problems; Claude Code is given different search tools under the same prompt and budget, and the pass rate is averaged over three runs (counting only proofs that compile and contain no sorry placeholder): no search tool 34.0%, LeanExplore 27.3%, Lean Finder 30.7%, LeanSearch V2 36.0%, Lean Finder V2 39.3%. Weaker search tools do worse than no tool at all, which shows that inaccurate retrieval results lead the agent toward the wrong theorems.

3.5 Ablation: both difficulty and consistency are needed

This experiment checks whether both parts of the reward are necessary. The authors change only the reward of the round-1 generator and keep all other settings fixed (paper Table 7, MathlibQR):

• Difficulty reward only: nDCG@1 0.453, below round 0's 0.463.
• Consistency reward only: nDCG@1 0.463, level with round 0, with Recall@10 rising from 0.760 to 0.780.
• Both: nDCG@1 0.520, Recall@10 0.842.

With only the difficulty reward, the generator can worsen the ranking by writing off-target queries, and a retriever trained on such queries learns wrong correspondences. With only the consistency reward, the queries are too easy for the retriever and provide little new information.

The round-2 ablation answers whether more sampling is enough: with the same two queries sampled per theorem and the same number of optimization steps, generating round-2 queries with the frozen base model gives nDCG@1 of 0.469; a generator supervised-fine-tuned on real queries gives 0.473; reusing the round-1 reinforcement-learning generator without further updates gives 0.515; training the generator for another round against the new retriever gives 0.558 (paper Table 9). The generator must be updated along with the retriever's weaknesses for the second round to bring a clear gain.

4. Limitations

The paper has no separate limitations section. Two points can be added. First, MathlibQR has only 810 queries, and the real-query evaluation relies on LLM judges; the two judges agree 89% of the time, but there are no human-verified rankings. Second, the consistency judgment in the reward is made by GPT-OSS-120B, and its criterion directly decides which kind of "hard" is kept; the paper does not report the error rate of this judgment, and if it is too lenient, off-target queries still slip into the training data.

5. Practical implications

First, when training a retriever for a specialized domain, first measure the length and phrasing of real queries, then build training data to match that distribution. This paper's data show that the same 8B retriever beats a system with a reranker simply by switching its training data from long paraphrases to short queries close to real lengths.

Second, when synthesizing hard examples with reinforcement learning, a difficulty reward must be paired with a consistency check and a rank cap that gives no reward outside the top 100. The ablation in this paper shows directly that chasing difficulty alone turns synthetic data into noise.