![[2510.15940] Lean Finder: Semantic Search for Mathlib That Understands User Intents](https://arxiv.org/static/browse/0.3.4/images/arxiv-logo-fb.png){kind=logo}
[2510.15940] Lean Finder: Semantic Search for Mathlib That Understands User Intents
Summary
Lean Finder is a semantic search engine designed for the Lean programming language and mathlib, improving theorem retrieval by understanding user intents and enhancing search accuracy.
Why It Matters
The development of Lean Finder addresses a significant challenge in formal theorem proving, where existing search engines fall short in aligning with user queries. By improving search capabilities, it enhances mathematicians' productivity and facilitates advancements in formal methods, making this tool highly relevant in the fields of machine learning and artificial intelligence.
Key Takeaways
- Lean Finder improves theorem search accuracy by over 30% compared to existing tools.
- The search engine is tailored to understand the intents of mathematicians, enhancing user experience.
- It integrates feedback from users to continuously refine its performance.
- Lean Finder is compatible with LLM-based theorem provers, bridging search and formal reasoning.
- The tool addresses the steep learning curve of Lean 4, making it more accessible for users.
Computer Science > Machine Learning arXiv:2510.15940 (cs) [Submitted on 8 Oct 2025 (v1), last revised 20 Feb 2026 (this version, v2)] Title:Lean Finder: Semantic Search for Mathlib That Understands User Intents Authors:Jialin Lu, Kye Emond, Kaiyu Yang, Swarat Chaudhuri, Weiran Sun, Wuyang Chen View a PDF of the paper titled Lean Finder: Semantic Search for Mathlib That Understands User Intents, by Jialin Lu and 5 other authors View PDF HTML (experimental) Abstract:We present Lean Finder, a semantic search engine for Lean and mathlib that understands and aligns with the intents of mathematicians. Progress in formal theorem proving is often hindered by the difficulty of locating relevant theorems and the steep learning curve of the Lean 4 language, making advancement slow and labor-intensive. Existing Lean search engines, though helpful, rely primarily on informalizations (natural language translation of the formal statements), while largely overlooking the mismatch with real-world user queries. In contrast, we propose a user-centered semantic search tailored to the needs of mathematicians. Our approach begins by analyzing and clustering the semantics of public Lean discussions, then fine-tuning text embeddings on synthesized queries that emulate user intents. We further align Lean Finder with mathematicians' preferences using diverse feedback signals, encoding it with a rich awareness of their goals from multiple perspectives. Evaluations on real-world queries, informalized...
