Lean Finder V2 improves semantic search for math library queries
Lean Finder V2: Semantic Search for Mathlib That Disambiguates User Queries
Machine LearningInformation Retrieval
Summary
Searching for math statements in large libraries can be tricky because people usually give short, unclear queries. The authors show that this ambiguity is mostly a data problem and address it by creating more training examples with ambiguous queries and teaching the search system to better understand them. Their improved search system, Lean Finder V2, works better than previous ones, helping both humans and coding tools find the right math statements faster. It also supports proving math facts with greater success when paired with an automated tool.
What this means in practice
- •For software developers: Use Lean Finder V2 to quickly find relevant math library statements when writing formal proofs in Lean.
- •For automated theorem proving teams: Integrate Lean Finder V2 to improve search-based guidance in automated proof generation tasks.
Authors
Jialin Lu, Xiaoyu Liu, Hengrui Luo, Rodrigo Stehling, Linxi Liu, Weiran Sun, Yuepeng Wang, Wuyang Chen
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/