Source-linked AI summary
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
TL;DR
Mathlib search queries from mathematicians and coding agents are often short and ambiguous, while common training inputs preserve more context. Lean Finder V2 uses adversarial training and query rewriting built around synthetic ambiguous query-declaration pairs. It reports improved retrieval, stronger judgments on real-interaction queries, and higher downstream proof success.
Problem
Mathlib search queries from mathematicians and coding agents often leave intended mathematics implicit, while existing systems commonly rely on more context-rich inputs.
Source: §1 · p. 1Method
Lean Finder V2 uses retriever-guided adversarial training to generate synthetic ambiguous query-declaration pairs for retriever fine-tuning and input-level query-rewriting optimization.
Source: §1 · pp. 2–3Results
Lean Finder V2 improves retrieval across MathlibQR and unlabeled real-interaction queries and downstream proof evaluation, including 14% relative improvement in Recall@10 over the previous-best semantic search engine on MathlibQR.
Source: §1 · p. 3Takeaways & Limitations
Lean Finder V2 provides infrastructure for autonomous agents in formal mathematics and scalable human-AI collaboration through access to Mathlib using concise, ambiguous queries.
Source: §5 · p. 10
Abstract
from arXiv · showhide
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/
1 INTRODUCTION
Human and coding-agent searches use short, ambiguous queries, while common training inputs preserve much more context. Lean Finder V2 uses synthetic ambiguous query-declaration pairs for adversarial retriever training and query rewriting, improving MathlibQR retrieval and downstream proof success.
1 INTRODUCTION
- Queries from mathematicians and coding agents often use short properties, notation, aliases, or hypotheses that leave intended mathematics implicit.Source: §1 · p. 1
- Human and coding-agent queries have median lengths of 16 and 15 tokens, respectively, compared with 82 tokens for statement informalizations commonly used to train earlier search engines.Source: §1 · p. 2
- A faithful ambiguous query can move its target theorem from rank one to rank seven when the Mathlib concept of an even function is left implicit.Source: §1 · p. 2
- Retriever-guided adversarial training generates challenging, declaration-faithful queries, and the resulting synthetic pairs train the retriever while its feedback recalibrates query difficulty.Source: §1 · pp. 2–3
- 14% relative improvement in Recall@10 over the previous-best semantic search engine on MathlibQR establishes Lean Finder V2’s new state of the art.Source: §1 · p. 3
- On unlabeled Mathlib queries from real user interactions, frontier-LLM judges rank Lean Finder V2 as most helpful 18+% more often than the previous best system.Source: §1 · p. 3
- The same synthetic query-declaration pairs support GEPA-optimized query rewriting, which further improves MathlibQR retrieval for Lean Finder V2.Source: §1 · p. 3
- Integrated with Claude Code, Lean Finder V2 achieves 39.3% proof success on FATE-H, compared with 36.0% for the next-best system.Source: §1 · p. 3
2 RELATED WORK
Prior Lean retrieval systems improve access to Mathlib and are used in agentic systems. Lean Finder V2 differs from RL approaches that optimize queries against fixed retrievers by using generated queries to adapt the retriever itself.
2 RELATED WORK
- Prior Lean retrieval systems improve access to Mathlib and are often incorporated into agentic systems.Source: §2 · p. 3
- Outside Lean, reinforcement learning has primarily optimized queries against fixed retrievers rather than using generated queries to adapt the retriever.Source: §2 · p. 3
- Lean Finder V2 uses declaration-faithful generated queries to challenge and retrain the retriever, which then supplies difficulty feedback for the next generator-training round.Source: §2 · p. 3
3 METHODS
Lean Finder V2 reuses synthetic ambiguous query–declaration pairs to adapt both the retriever and a query-rewriting prompt. Adversarial training creates queries that challenge the current retriever while remaining aligned with their Mathlib declarations.
3 METHODS
- The framework addresses scarce labeled ambiguous queries by using synthetic query–declaration pairs for both retriever training and query-rewriting prompt optimization.The rewriting prompt makes implicit intent explicit before retrieval.Source: §3 · p. 3
3.1 MODEL-LEVEL DISAMBIGUATION THROUGH ADVERSARIAL TRAINING
- The model-level loop trains a generator to produce faithful, challenging queries, then uses retriever feedback to guide its next training round.The retriever is trained on the generated pairs, while its retrieval difficulty signal guides the generator.Source: §3.1 · pp. 3–4
3.1.1 INITIALIZING AND FINE-TUNING THE RETRIEVER
- The initial retriever is fine-tuned on context-rich query–declaration data using masked InfoNCE, masking highly plausible candidates to reduce false-negative supervision.It is initialized from Qwen3-Embedding-8B and trained on synthetic user queries and informalization datasets.Source: §3.1.1 · p. 4
3.1.2 SCALING UP THE GENERATION OF AMBIGUOUS QUERIES VIA ADVERSARIAL ATTACKS
- The generator combines on-policy retriever-guided rewards with supervised fine-tuning on human and coding-agent queries to produce aligned queries that challenge the current retriever.An alignment gate makes alignment a prerequisite for difficulty reward; rank-based difficulty is zero for targets above kmin or beyond kcut and grows within a useful region, with a capped length penalty discouraging overlong queries.Source: §3.1.2 · p. 5
3.1.3 IMPROVING THE RETRIEVER WITH GENERATED QUERIES
- The retriever is retrained on generated pairs alongside context-rich data, and its updated target ranks guide the next generator-training round.The retriever uses the same masked InfoNCE objective.Source: §3.1.3 · p. 6
3.2 INPUT-LEVEL DISAMBIGUATION THROUGH OPTIMIZED QUERY REWRITING
- At the input level, a single optimized prompt rewrites queries to expose implicit mathematical context, with retriever rankings providing optimization feedback.GEPA revises prompts using rank-based scores and textual feedback, then selects the prompt with the best average Pareto-set score.Source: §3.2 · p. 6
4 EXPERIMENTS
The experiments evaluate Lean Finder V2 across concise and context-rich benchmarks, unlabeled real-world queries, query rewriting, and downstream theorem proving. The final retriever leads on MathlibQR, is preferred on unlabeled queries, and improves retrieval and proof outcomes with optimized rewriting and Claude Code integration.
4 EXPERIMENTS
- The evaluation covers short and context-rich benchmarks, 200 unlabeled interaction queries, rewriting variants, and three-run theorem-proving pass rates under matched budgets.The retrieval model starts from Qwen3-Embedding-8B, and generator-retriever training alternates for two rounds.Source: §4 · pp. 6–7, §4.2 · p. 8, §4.3 · p. 9
4.1 LEAN FINDER V2 IS THE STRONGEST RETRIEVER ACROSS QUERY TYPES
- Lean Finder V2 achieves the best result in every reported MathlibQR metric and performs competitively on context-rich queries, outperforming LeanSearch V2.It is a retriever-only system; adversarial training improves every MathlibQR metric from Round 0 to the final model while context-rich performance remains strong.Source: §4.1 · pp. 7–8, Table 1 · p. 7, Table 2 · p. 8
4.2 LEAN FINDER V2 IS PREFERRED ON UNLABELED REAL-WORLD QUERIES
- Both LLM judges rank Lean Finder V2 first overall on 200 unlabeled deployment queries, with mean ranks of 1.980 and 1.945.The judges select the same rank-1 system on 89.0% of queries.Source: §4.2 · p. 8, Table 3 · p. 8
4.3 OPTIMIZED QUERY REWRITING IMPROVES TOP-RANKED RETRIEVAL
- GEPA-optimized rewriting raises MathlibQR nDCG@1 from 0.558 to 0.588 over the original queries.LeanSearch, LeanDex, and the seed prompt reduce performance at every cutoff; reranking with rewriting reaches 0.610 nDCG@1.Source: §4.3 · p. 9, Table 4 · p. 9
4.4 LEAN FINDER V2 HELPS THE MOST ON THEOREM PROVING TASK
- Claude Code with Lean Finder V2 reaches a 39.3% FATE-H proof pass rate, the highest among evaluated settings.The next-best setting, LeanSearch V2 with reranking, reaches 36.0%; only these two semantic retrieval settings outperform the no-tool baseline.Source: §4.4 · p. 9, Table 5 · p. 9
5 CONCLUSION
Lean Finder V2 targets the mismatch between short, ambiguous real-world queries and context-rich retrieval training. The ablations find that alignment and difficulty rewards work best together.
5 CONCLUSION
- Lean Finder V2 uses adversarial training and query-rewriting prompt optimization, powered by the same synthetic ambiguous query-declaration pairs, to address implicit intent in real searches.The conclusion presents this framework as infrastructure for autonomous agents in formal mathematics and scalable human-AI collaboration.Source: §5 · p. 10
A EXTENDED RELATED WORK
- Prior Mathlib search systems largely rely on context-rich informalizations or declaration-derived synthetic data, while Lean Finder V2 trains on adversarially generated short, ambiguous queries.Related approaches use reinforcement learning to optimize queries against fixed retrievers, whereas Lean Finder V2 uses generated queries to retrain its retriever.Source: A EXTENDED RELATED WORK · p. 13
- Prior theorem-proving agents use retrieval to locate reusable Mathlib results, and Lean Finder V2 focuses on improving that infrastructure for concise, ambiguous agent queries.Its adversarial supervision adapts in difficulty to the retriever’s evolving capability.Source: A EXTENDED RELATED WORK · p. 13
B ABLATION STUDIES
- The ablations compare alignment and difficulty rewards and test whether another round of generator reinforcement learning beats base-model generation, fixed-generator sampling, or simply sampling more queries.The reward comparison matches generator steps, query-sampling budgets, and retriever training budgets across variants.Source: B ABLATION STUDIES · p. 14, §B.1 · p. 14
B.1 CONTRIBUTION OF ALIGNMENT AND DIFFICULTY REWARDS
- Across concise and context-rich queries, the full reward delivers the strongest overall retrieval; difficulty alone harms top-rank metrics, while alignment alone yields modest, uneven gains.Difficulty without alignment can reward queries that are hard for the wrong reason and mismatch their target declarations; alignment keeps queries faithful, while difficulty targets retriever gaps.Source: §B.1 · p. 14, Table 7 · p. 14, Table 8 · p. 14
B.2 RL-TRAINED GENERATION VERSUS ADDITIONAL SAMPLING
The ablation compares RL-trained query generation with base or fixed generators and additional sampling. RL training improves MathlibQR retrieval, and a second RL round improves it further while retaining strong context-rich performance.
B.2 RL-TRAINED GENERATION VERSUS ADDITIONAL SAMPLING
- The comparison matches retriever initialization, context-rich data, and optimization steps; Round 1 adds one generated query per declaration and Round 2 adds two in total.The controls include base-model generation, a fixed RL-trained generator, and an SFT-only generator.Source: §B.2 · p. 15
- MathlibQR nDCG@10 rises from 0.628 to 0.682 and Recall@10 from 0.791 to 0.842 from Round 0 to Round 1 with RL-trained generation.Applying another RL round before generating a second query raises nDCG@10 to 0.732 and Recall@10 to 0.893; sampling a second query from a fixed generator adds no material gain.Source: §B.2 · pp. 15–16, Table 9 · p. 15
- Lean Finder V2 Round 2 achieves the best or close-to-best result in every context-rich metric, preserving strong retrieval beyond concise queries.Context-rich results are reported in Table 10, where configurations receive matched optimization steps.Source: Table 10 · p. 15, §B.2 · p. 16
C.1 RETRIEVAL EVALUATION
The evaluation describes retrieval, rewriting, and downstream theorem-proving protocols. It compares systems under specified query, ranking, and cost conditions.
C.1 RETRIEVAL EVALUATION
- Retrieval evaluation runs systems on original benchmark queries against ground-truth declarations; Claude Code returns exactly ten ranked declarations, while TheoremGraph lacks reported Recall@50 and Recall@100.Claude Code can search Mathlib documentation and source pages but cannot use specialized Lean search engines.Source: §C.1 · p. 16
C.2 QUERY-REWRITING EVALUATION
- Each rewriting method replaces the original MathlibQR query before the fixed Lean Finder V2 retriever ranks its target; rewriting metrics average three independently generated query sets.The no-rewrite condition is evaluated once on the original queries.Source: §C.2 · p. 16
C.3 DOWNSTREAM THEOREM-PROVING EVALUATION
- The downstream evaluation tests five retrieval conditions on 100 formal algebra problems, requiring a sorry-free compiling proof of the original statement within a $1 token-cost cap.Each condition is run three times; reported pass rates use the mean and sample standard deviation.Source: §C.3 · pp. 16–17
D LLM-JUDGE EVALUATION AND VALIDATION
Two LLM judges rank anonymized retrieval lists for unlabeled human and coding-agent queries, and are checked against human-curated MathlibQR labels. Their agreement supports the reliability of the preference evaluation.
D LLM-JUDGE EVALUATION AND VALIDATION
- On unlabeled queries, judges independently rank anonymized systems’ five-result lists; they agree on the rank-1 system for 89.0% of queries.The protocol averages ordinal ranks and reports how often each system is ranked first.Source: D LLM-JUDGE EVALUATION AND VALIDATION · p. 17
- Both judges select the human-curated MathlibQR declaration on more than 91% of queries, despite choosing among the retriever’s strongest confusions.The judges see shuffled choices and do not see benchmark labels, retrieval ranks, scores, or which choice was inserted.Source: D LLM-JUDGE EVALUATION AND VALIDATION · p. 17, Table 11 · p. 17
E RERANKER TRAINING AND RESULTS
The reranker is trained to score query–declaration relevance from both context-rich and synthetic short queries. Adding it improves ranking across MathlibQR and context-rich queries, with further gains from combining it with optimized query rewriting.
E RERANKER TRAINING AND RESULTS
- Qwen3-Reranker-8B jointly scores query–declaration pairs, using ground-truth declarations as positives and randomly sampled remaining declarations as negatives.Training includes context-rich and synthetic short queries; the model predicts relevance from its yes/no token logits and is optimized with binary cross-entropy.Source: E RERANKER TRAINING AND RESULTS · p. 17
- 0.610 nDCG@1 on MathlibQR is achieved by Lean Finder V2 with both reranking and GEPA-optimized rewriting, which improves all metrics except Recall@10.The reported comparison covers the 810-query MathlibQR fair set.Source: Table 12 · p. 18, E RERANKER TRAINING AND RESULTS · p. 18
- The reranker improves ranking quality on both MathlibQR and context-rich queries when added to the Lean Finder V2 retriever.The reported evaluations use an 810-query MathlibQR fair set and a 2,526-query context-rich test set.Source: E RERANKER TRAINING AND RESULTS · p. 18, Table 12 · p. 18, Table 13 · p. 18
F.1 GENERATOR TRAINING DETAILS
The training details describe a generator–retriever loop that creates labeled ambiguous queries, fine-tunes retrieval, and optimizes a rewriting prompt. The same synthetic query–declaration corpus supports model-level training and input-level rewriting.
F.1 GENERATOR TRAINING DETAILS
- The generator first uses deployment-query supervision, then adapts to the updated retriever while retaining alignment and length controls.The fixed expert objective is removed in the second round as on-policy rewards adapt generation to the new retriever.Source: §F.1 · p. 18
- The final adversarial-training corpus contains over 600K synthetic query–declaration pairs, with each round generating over 300K queries.Generated pairs are combined with context-rich data to retrain the retriever.Source: §F.1 · p. 19
- The query-length penalty is zero through 40 tokens, rises linearly from 40 to 50, and reaches its maximum beyond 50 tokens.The settings are Lmax = 40, Lbuf = 10, and λlen = 0.15.Source: §F.1 · p. 19
F.2 RETRIEVAL TRAINING DETAILS
- Retriever training uses masked InfoNCE, masking candidates whose cosine similarity exceeds the labeled positive by more than margin m.Each round combines context-rich data with accumulated generated concise queries, and retriever variants receive matched optimization steps.Source: §F.2 · p. 19
F.3 RERANKER TRAINING DETAILS
- Rerankers are trained for one epoch with LoRA on all linear layers, using rank r = 8 and α = 32.Training uses a per-device batch size of 64 and learning rate 5 × 10−5.Source: §F.3 · p. 19
F.4 PROMPT OPTIMIZATION TRAINING DETAILS
- GEPA revises candidate rewriting prompts using retrieval-grounded feedback, retaining revisions that improve minibatch scores and selecting the final prompt by Pareto-set average score.Its score balances absolute target rank with improvements over the original query and seed-prompt rewrite.Source: §F.4 · pp. 19–20
F.5 PSEUDOCODE FOR TRAINING PROCESS
- The pseudocode alternates generator training, query generation from Mathlib declarations, and retriever retraining on generated and context-rich data.When the SFT mixing weight is zero, the hybrid objective reduces to on-policy GRPO.Source: §F.5 · p. 21
G MODEL SCALE AND BACKBONE CHOICE
Lean Finder V2 uses a single 8B retriever initialized from the same Qwen3-Embedding-8B checkpoint as LeanSearch V2, but fine-tunes it for Mathlib retrieval. The length penalty is calibrated to preserve ordinary deployment query lengths while discouraging unnecessary text.
G MODEL SCALE AND BACKBONE CHOICE
- Lean Finder V2 uses one 8B retriever, while reranked LeanSearch V2 combines an 8B retriever and an 8B reranker.Both systems rely on Qwen3-Embedding-8B; Lean Finder V2 fine-tunes the checkpoint for Mathlib retrieval, whereas LeanSearch V2 does not.Source: G MODEL SCALE AND BACKBONE CHOICE · p. 21, Table 14 · p. 21
- The method is described as architecture- and checkpoint-agnostic, while the authors choose a strong base model for their Mathlib search engine.The stated goal is to deliver a strong search engine for the AI4Math and Lean communities.Source: G MODEL SCALE AND BACKBONE CHOICE · p. 21
H.1 LENGTH-PENALTY THRESHOLDS
- The length penalty leaves queries unpenalized through 40 tokens, grows smoothly to 50, and caps its deduction at 0.15.The thresholds are set above deployment-query percentiles so ordinary query lengths remain unpenalized.Source: §H.1 · pp. 21–22
H.2 RANK REGIONS FOR THE DIFFICULTY REWARD
The difficulty reward targets queries that expose retrieval gaps while retaining target alignment. The authors also report an alignment-gate audit and note that testing alternative rank thresholds would require retraining the full generator–retriever pipeline.
H.2 RANK REGIONS FOR THE DIFFICULTY REWARD
- No difficulty reward is assigned for target ranks ≤5 or >100; ranks 6–30 receive increasing reward before saturation.The top-five cutoff reflects how often deployment requests return at least five results, while the rank-100 cutoff guards against queries that omit target-identifying content.Source: §H.2 · p. 22
- The rank thresholds were not selected by benchmark-driven hyperparameter sweep because testing alternatives requires retraining the complete generator–retriever pipeline.The authors report that the fixed-setting synthetic data already improves complementary model-side training and input-side prompt optimization.Source: §H.2 · p. 22
I ALIGNMENT-GATE AUDIT
- On a 100-pair audit, GPT-OSS-120B agreed with human labels on 98 pairs and incorrectly accepted 1 of 40 human-labeled misaligned pairs.It also agreed with Claude Opus 5 on 97 of 100 pairs.Source: I ALIGNMENT-GATE AUDIT · p. 22
J QUERY REWRITING CASE STUDY
The case study shows that a focused clarification of an implicit mathematical role can improve retrieval, while the prompt section specifies constraints for generating and rewriting queries without changing their intent.
J QUERY REWRITING CASE STUDY
- GEPA clarifies that Φ is Adjunction.homEquiv and the equation expresses its left naturality, preserving the adjunction setting without adding assumptions or adjacent theorems.The original query states the equation but leaves Φ’s role implicit.Source: J QUERY REWRITING CASE STUDY · p. 23
- GEPA’s focused rewrite ranks the target 1, versus ranks 8 for LeanSearch, 16 for LeanDex, and 7 for the seed rewrite.The alternatives rank lower while either mislabeling the equation, broadening its context, or leaving its missing context unresolved.Source: J QUERY REWRITING CASE STUDY · p. 23
K PROMPTS
- The optimized rewriting prompt preserves mathematical intent, setting, assumptions, and ambiguity; it keeps clear queries nearly verbatim and otherwise favors one concise, supported clarification.Its reflection principles compare outcomes and caution against example-specific rules or unsupported changes.Source: OPTIMIZED PROMPT FOR QUERY REWRITING · pp. 23–24, GEPA REFLECTION PROMPT · p. 24
- The seed adversarial-query prompt requires a relevant, plausible, concise query that avoids the formal name and near-verbatim paraphrase.It asks the model to generate a query that is genuinely relevant while challenging the retriever.Source: QUERY GENERATOR PROMPT · p. 25