Lean Finder: Semantic Search for Mathlib That Understands User Intents

TL;DR

Lean Finder addresses the core problem of finding relevant Lean/mathlib lemmas in large libraries by aligning retrieval with working mathematicians’ intents rather than relying on informalized translations alone. It combines a data synthesis pipeline (including five real-intent clusters and 1.4M query–statement pairs across multiple modalities), contrastive embedding learning, and Direct Preference Optimization to create an intent-aware code-search model that integrates with LLM provers. The approach yields substantial improvements over prior Lean search engines and GPT-4o in real-user and benchmark evaluations, and it provides a public web service and a developer-friendly retrieval backbone for prover systems. By bridging informal user queries with formal content and supporting diverse inputs (informalizations, proof states, and formal statements), Lean Finder advances rigorous, AI-assisted mathematical discovery and formal verification workflows.

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 statements, and proof states demonstrate that our Lean Finder achieves over $30\%$ relative improvement compared to previous search engines and GPT-4o. In addition, Lean Finder is compatible with LLM-based theorem provers, bridging retrieval with formal reasoning. Lean Finder is available at: https://leanfinder.github.io

Figures (9)

• Figure 1: In the evaluation with user queries, real users preferred Lean Finder in 81.6% of cases, compared with 56.9% for Lean Search gao2024semantic and 54.1% for GPT-4o.
• Figure 2: PCA of Lean/mathlib-related queries from different sources. Our synthesized user query (orange, Section \ref{['sec:user_query_synthesis']}) aligns more closely with real queries (green), whereas direct informalization gao2024herald (blue) shows distributional deviations. Real user queries are from Zulip and GitHub.
• Figure 3: We synthesize user queries as part of our training data. First, we analyze the semantics of public Lean/mathlib queries posted by real mathematicians and cluster them into user intents (Section \ref{['sec:semantic_analysis_user_query']}). These intents then prompt the generation of synthetic user queries from formal Lean statements collected from mathlib, GitHub, and research papers (Section \ref{['sec:query_synthesis_perspectives']}). The synthesized user queries form the core part of our training data for our Lean Finder. To generalize Lean Finder across diverse inputs, we further include additional modalities (formal/informal statements and proof states, see Sections \ref{['sec:largest_code_search_dataset']}) extracted from formal Lean statements.
• Figure 4: Distribution of our training dataset. (a) At a fine granularity, our synthetic user queries distribute across five clusters of user intents (identified in Section \ref{['sec:semantic_analysis_user_query']}). This distribution also aligns with the weekly popularity trends of relevant channels on Lean Zulip Chat (Appendix \ref{['imbalance_discussion']}). For detailed descriptions and examples of these clusters, see Table \ref{['table:user_intents_clusters']}. (b) Overall, our dataset contains a total of 1.4M pairs of queries and formal Lean statements, distributed across four input modalities.
• Figure 5: Lean Finder training pipeline. We first fine-tune the base LLM with contrastive learning wang2023codet5+ on four input modalities in our training dataset (Figure \ref{['fig:dataset_statistics']}, synthetic queries, informalized statements, augmented proof states, and formal statements) to build a strong retrieval model for Lean (Section \ref{['sec:constrastive_learning']}). We then deploy our Lean Finder as a web service and collect real users' retrieval preferences, which serve as human feedback. These preferences are used to further improve Lean Finder via Direct Preference Optimization (DPO rafailov2024directpreferenceoptimizationlanguage, Section \ref{['sec:rlhf']}), resulting in a human-aligned boosted Lean Finder.