Lean Finder V2: Semantic Search for Mathlib That Disambiguates User Queries
As Mathlib grows past 400,000 theorems, effective semantic search is critical for both human formalization and automated proving, yet real-world queries are short and ambiguous while existing engines train on lengthy, context-rich informalizations. Lean Finder V2 closes this gap with an adversarial generator-retriever loop that synthesizes over 600,000 faithful, challenging short queries, then uses them for both retriever fine-tuning and GEPA-optimized input rewriting. The result is a new state of the art on human-curated and real-world benchmarks, plus measurable gains in downstream theorem-proving tasks.
The paper identifies a genuine and quantified data mismatch in Mathlib retrieval and proposes a clean adversarial fix. A reinforcement-learned generator produces challenging yet declaration-faithful short queries, retriever feedback drives progressively harder synthetic data, and the same corpus powers input-level rewriting that further improves top-rank metrics. The gains on labeled benchmarks, LLM-judged unlabeled queries, and downstream theorem proving are substantial and well-ablated, though the work relies on future models and benchmarks that currently block independent reproduction.
Two empirical and methodological strengths stand out. First, the ambiguity gap is carefully measured and convincingly closed: adversarial training with both difficulty and alignment rewards is the only setting that improves every top-rank metric over the context-rich-only baseline, while ablations show that static or misaligned generators fail. Second, the same synthetic data is repurposed for input-level disambiguation, where GEPA-optimized query rewriting raises nDCG@1 from 0.558 to 0.588 on MathlibQR by selectively surfacing implicit context rather than adding verbose paraphrase.
Several issues temper the results. The paper is dated 2026 and relies on multiple models and benchmarks that are not publicly available for verification. Training labels for real-world queries and the alignment gate depend on frontier LLM judges, creating a circularity risk when those same judges later evaluate retrieval quality; although Appendix I reports a 98% agreement rate for the alignment gate, the audit covers only 100 samples. Finally, downstream theorem-proving improvements are modest ($39.3\%$ versus $36.0\%$ pass rate) and observed on just 100 problems, while the no-retrieval baseline at $34.0\%$ suggests that retrieval helps only marginally unless precision is exceptionally high.
The experimental comparisons are mostly fair and well-documented. On MathlibQR, Lean Finder V2 as a single 8B retriever beats the prior best two-stage 8B+8B system in every reported metric, and the consistent gains across Round 0 to Round 2 directly attribute the lift to adversarial synthetic data rather than backbone scale. Context-rich performance is preserved, and unlabeled deployment queries are evaluated with two independent frontier judges that agree $89\%$ of the time. One caveat is that Claude Code is capped at ten candidates, which handicaps Recall@50/100, though the authors disclose this restriction.
Although the authors commit to releasing the 600K synthetic query-declaration corpus and provide training hyperparameters in the appendices, the experimental pipeline is difficult to reproduce. It requires two rounds of GRPO generator training on thousands of declarations, masked InfoNCE retriever fine-tuning with specific margin rules, and a 120B-parameter closed alignment judge for the reward gate. The prompt optimization further needs GEPA with DeepSeek-V4.1-Flash reflection. The compute environment and reliance on several not-yet-public frontier APIs mean that even with code, independent verification would be expensive and partially impossible today.
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/
Pick a starting point or write your own. Challenges run in the background, so you can keep reading while the AI investigates.
No challenges yet. Disagree with the review? Ask the AI to revisit a specific claim.