Summary of "Lean Finder V2: Semantic Search for Mathlib that Disambiguates User Queries"

Summary (Overview)

• Core contribution: Lean Finder V2 is a semantic search framework for Mathlib (Lean's mathematical library) that addresses the "ambiguity gap" in theorem retrieval—the mismatch between short, context-poor real-world queries and the context-rich queries assumed by existing search engines.
• Dual-level disambiguation: The framework combines (1) model-level adversarial training—an RL-trained query generator produces challenging ambiguous queries to fine-tune the retriever—and (2) input-level query rewriting—a GEPA-optimized prompt makes implicit mathematical intent explicit before retrieval.
• State-of-the-art results: Achieves 14% relative improvement over the previous best semantic search engine on the MathlibQR benchmark (Recall@10: 0.893 vs. 0.780), while maintaining strong performance on context-rich queries.
• Scalable data generation: Produces over 600K labeled ambiguous query-declaration pairs through retriever-guided adversarial training, addressing the scarcity of real-world labeled ambiguous queries.
• Downstream impact: When integrated with Claude Code, improves theorem-proving pass rate on the FATE-H benchmark to 39.3% (vs. 36.0% for the next-best system).

Introduction and Theoretical Foundation

Background and Motivation

The paper addresses a fundamental bottleneck in formal mathematics: theorem retrieval. Mathlib now contains over 400,000 theorems, making effective search essential for both human mathematicians and automated coding agents. However, real-world search queries are fundamentally different from what existing systems assume:

• Human and coding-agent queries are short (median 15–16 tokens), using properties, notation, aliases, or hypotheses with much of the intended mathematics implicit.
• Existing search engines are trained on context-rich informalizations (median 82 tokens) that preserve detailed mathematical descriptions.

The Ambiguity Gap

The paper demonstrates this gap with a concrete example. For the theorem Function.Even.const (constant functions are even):

• Context-rich query: "for a type α with a negation and any type β, every constant function f : α → β, f(x) = b for some b ∈ β, satisfies f(−x) = f(x) for all x ∈ α, i.e., constant functions are even"
• Ambiguous query: "constant function invariant under input negation"

Both queries express the same mathematical intent, but the ambiguous query moves the target theorem from rank 1 to rank 7 in retrieval results. This illustrates the core research question:

How to disambiguate Mathlib queries, at both model level and input level?

Theoretical Foundation

The authors frame this as fundamentally a data problem: labeled ambiguous queries paired with ground-truth declarations are scarce. They propose generating such data through adversarial training, where a query generator learns to produce queries that challenge the current retriever's weaknesses while remaining faithful to their source declarations.

Methodology

Model-Level Disambiguation via Adversarial Training

The framework couples a retrieval model with a query generator in an iterative adversarial loop:

1. Initialization (Round 0)

• Initialize retriever from Qwen3-Embedding-8B
• Fine-tune on context-rich data: synthetic user queries from Lu et al. (2026) and informalization datasets
• Use masked InfoNCE loss with in-batch negatives, masking candidates whose similarity exceeds the positive by a margin $m$:

$$L_{ret} = -\frac{1}{B}\sum_{i=1}^{B} \log \frac{\exp(\text{Sim}(q_i, c_i^+)/\tau)}{\sum_{c \in C_B} \mathbb{I}(q_i, c) \exp(\text{Sim}(q_i, c)/\tau)}$$

2. Adversarial Query Generation (RL Training)

The query generator (Qwen3-4B) is trained with Group Relative Policy Optimization (GRPO). For each declaration $d$, the generator samples $G$ candidate queries $\{q_i\}_{i=1}^{G}$. The normalized advantage is:

$$\hat{A}_i = \frac{r_i - \text{mean}(r_1, \ldots, r_G)}{\text{std}(r_1, \ldots, r_G) + \epsilon_A}$$

The GRPO loss is:

$$L_{GRPO}(\theta) = -\mathbb{E}\left[\frac{1}{G}\sum_{i=1}^{G}\frac{1}{|q_i|}\sum_{s=1}^{|q_i|}\left[\min\left(\rho_{i,s}(\theta)\hat{A}_i, \text{clip}(\rho_{i,s}(\theta), 1-\epsilon, 1+\epsilon)\hat{A}_i\right) - \beta D^{KL}_{i,s}\right]\right]$$

3. Retriever-Guided Reward

The reward combines alignment, difficulty, and length:

$$r(q, d) = \begin{cases} 0, & \text{if output format is invalid} \\ \max\{0, j(q,d) f_{rank}(k) - \lambda_{len} p_{len}(L)\}, & \text{otherwise} \end{cases}$$

where:

• $j(q,d) \in \{0,1\}$ is an alignment gate (LLM-judge ensures query fidelity to declaration)
• $f_{rank}(k)$ measures difficulty relative to current retriever rank $k$:

$$f_{rank}(k) = \begin{cases} 0, & k \leq k_{min} \text{ or } k > k_{cut} \\ \frac{\log(k/k_{min})}{\log(k_{sat}/k_{min})}, & k_{min} < k \leq k_{sat} \\ 1, & k_{sat} < k \leq k_{cut} \end{cases}$$

with $k_{min}=5$, $k_{sat}=30$, $k_{cut}=100$

• $p_{len}(L)$ is a soft length penalty (zero below 40 tokens, linear to 50, max beyond)

4. Hybrid Objective

Combines on-policy RL with off-policy SFT on expert deployment queries:

$$L_{hybrid}(\theta) = (1-\mu)L_{GRPO}(\theta) + \mu L_{SFT}(\theta)$$

where $\mu$ decreases over training, shifting from supervised anchoring to on-policy learning.

5. Retriever Update

After generator training, generate queries from Mathlib declarations, combine with context-rich data, and retrain the retriever. The updated retriever provides difficulty feedback for the next round.

Input-Level Disambiguation via GEPA-Optimized Query Rewriting

Using the same synthetic query-declaration pairs, the framework optimizes a query-rewriting prompt with GEPA (Reflective Prompt Evolution). The score for each rewrite is:

$$s_i(p) = \frac{\lambda_{abs}}{\log_2(\text{rank}_i(p) + 1)} + \lambda_{orig}\frac{\text{rank}^{orig}_i}{\text{rank}^{orig}_i + \text{rank}_i(p)} + \lambda_{seed}\frac{\text{rank}^{seed}_i}{\text{rank}^{seed}_i + \text{rank}_i(p)}$$

with $\lambda_{abs} = 0.5$, $\lambda_{orig} = \lambda_{seed} = 0.25$.

Empirical Validation / Results

Main Retrieval Results (MathlibQR)

Table 1: Retrieval performance on 810-query MathlibQR fair set

Context-Rich Query Results

Lean Finder V2 also achieves best results on the 2,526-query context-rich test set (nDCG@1: 0.573, Recall@10: 0.919), demonstrating that adversarial training does not sacrifice performance on detailed queries.

Query Rewriting Results

Table 4: Query-rewriting performance on MathlibQR

LLM-Judge Preference on Unlabeled Queries

On 200 real-world deployment queries, both GPT-5.6 Sol and Claude Opus 5 rank Lean Finder V2 first (mean rank 1.980 and 1.945, respectively), with 35% and 38% rank-1 selections.

Downstream Theorem Proving

Table 5: FATE-H benchmark results

Ablation Studies

• Full reward (alignment + difficulty) is the only configuration improving every metric over Round 0; difficulty-only degrades performance (misaligned queries), alignment-only gives modest gains.
• RL training is more effective than generic query generation: a second RL round improves nDCG@10 from 0.682 to 0.732, while sampling more queries from fixed generators adds no material gain.

Theoretical and Practical Implications

Theoretical Contributions

1. Ambiguity as a data problem: The paper reframes query ambiguity as fundamentally a data scarcity issue, demonstrating that synthetic adversarial data generation can effectively bridge the gap between training and deployment distributions.

2. Complementary disambiguation levels: Model-level training and input-level rewriting address ambiguity through different mechanisms—adapting the retriever's internal representations vs. transforming the input space—and each provides independent improvements.

3. Adversarial training for retrieval: Unlike prior work that optimizes queries against fixed retrievers, Lean Finder V2 uses generated queries as supervision to adapt the retriever itself, with the retriever's feedback recalibrating query difficulty in a closed loop.

Practical Implications

1. Infrastructure for AI4Math: Provides critical search infrastructure for autonomous agents in formal mathematics, where retrieval quality directly impacts end-to-end proof success.

2. Scalable data generation: The 600K+ synthetic query-declaration corpus will be released, supporting future research on ambiguous query handling.

3. Deployment-ready performance: Strong results on unlabeled real-world queries suggest the system generalizes beyond benchmark settings to actual usage patterns of mathematicians and coding agents.

Conclusion

Lean Finder V2 addresses the ambiguity gap in Mathlib semantic search through a dual approach: retriever-guided adversarial training generates large-scale labeled ambiguous queries that adapt the retriever to real-world search patterns, while GEPA-optimized query rewriting makes implicit mathematical intent explicit before retrieval. The system achieves state-of-the-art results on MathlibQR (Recall@10: 0.893), strong performance on context-rich queries, and is preferred by LLM judges on unlabeled deployment queries. When integrated with Claude Code, it improves theorem-proving pass rates to 39.3% on FATE-H.

Future directions include exploring additional rounds of adversarial training, extending the approach to other formal mathematics libraries, and further integrating retrieval with agentic reasoning systems. The released corpus of synthetic ambiguous queries will support continued research in this direction.