Technical Summary: LeanSearch v2

Problem Definition: Global Premise Retrieval

The paper identifies a critical gap in automated theorem proving within the Lean 4 ecosystem. While existing tools excel at semantic search (finding individual declarations matching a query) or premise selection (predicting useful lemmas for a single tactic step), they fail at global premise retrieval.

Global premise retrieval is defined as the task of identifying the complete, logically coherent set of library lemmas required to prove an entire theorem. This is distinct from finding a single relevant document because:

1. Non-locality: The necessary lemmas often reside in distant modules of the library (Mathlib) and share no lexical overlap with the problem statement.
2. Strategic Dependency: The connection between the problem and the lemmas is not semantic but structural, relying on the "logical architecture" of a proof strategy (e.g., reshaping a goal to match a theorem's interface).
3. Completeness: Missing a single essential lemma from a set of three or four renders the proof incomplete, a failure mode not captured by standard document-relevance metrics.

The authors argue that without effective global premise retrieval, AI provers waste computation re-proving existing local lemmas and struggle to generate efficient, idiomatic proofs.

Methodology: LeanSearch v2

LeanSearch v2 is a two-mode retrieval system designed to address this challenge.

1. Standard Mode (The Retrieval Substrate)

Standard mode serves as a high-performance search engine for individual Mathlib declarations and acts as the foundation for the reasoning mode.

• Corpus Construction: The system utilizes Jixia, a static analysis tool, to extract all declarations from Mathlib. It constructs a dependency graph and performs bottom-up hierarchy informalization. This process generates natural-language descriptions for each declaration by incorporating the already-informalized descriptions of its dependencies, ensuring descriptions are grounded in mathematical concepts rather than opaque identifiers.
• Pipeline: It employs a two-stage embedding–reranker pipeline using off-the-shelf models (Qwen3-Embedding-8B and Qwen3-Reranker-8B) without domain-specific fine-tuning.
  • Embedding: Queries and corpus items are encoded using a structured passage template that includes declaration kind, type signature, and informalized description.
  • Reranking: A kind-aware reranker scores query-candidate pairs, specifically handling definitions and instances to overcome retrieval difficulties observed in prior systems.

2. Reasoning Mode (Global Premise Retrieval)

Reasoning mode builds upon Standard Mode to retrieve sets of premises through an iterative sketch-retrieve-reflect loop.

• Sketch Generation: Given a theorem statement, a generator (Claude Sonnet 4.5) proposes a step-by-step proof outline, decomposing the theorem into sub-queries. It does not write code but defines the mathematical moves and retrieval intents.
• Retrieval & Filtering: Each sub-query is sent to Standard Mode. A filter model (Kimi K2 Instruct) vets the top candidates, explicitly allowing for empty sets if no retrieved lemma is genuinely useful for a specific step.
• Feasibility Judgment & Reflection: A judge model inspects the filtered results.
  • If the set of lemmas supports the proof strategy, the loop terminates.
  • If the set is insufficient (e.g., missing a premise or suggesting an invalid route), the judge provides structured feedback to a sketch reviser, which modifies the proof outline and re-enters the loop.
• Aggregation: Final outputs are aggregated using a rank-discount rule across sub-queries to form a unified list of supporting lemmas.

Key Contributions

1. Task Formulation: The paper formally defines global premise retrieval as a distinct challenge requiring the recovery of logically coherent premise sets rather than single documents.
2. Benchmarks: Two expert-curated benchmarks are introduced:
   • MathlibQR: 200 declarations and 946 queries for evaluating single-query search (Standard Mode).
   • MathlibMPR: 69 theorems from merged pull requests with expert-annotated premise groups (1–8 per theorem) for evaluating global premise retrieval (Reasoning Mode).
3. System Performance: LeanSearch v2 achieves state-of-the-art results without domain-specific fine-tuning.
   • Standard Mode: Achieves an nDCG@10 of 0.62 on MathlibQR, outperforming the next-best system (0.53).
   • Reasoning Mode: On MathlibMPR, it recovers 46.1% of ground-truth premise groups within the top 10 candidates, significantly outperforming reasoning retrieval baselines (38.0%) and premise-selection systems (9.3%).
4. Downstream Validation: In a controlled experiment with a fixed prover loop, replacing other retrievers with LeanSearch v2 reasoning mode increased proof success rates to 20% (vs. 16% for the next-best and 4% without retrieval), demonstrating that retrieval quality directly propagates to proof generation.

Significance and Claims

The paper positions this work as the first to apply reasoning-retrieval techniques specifically to the Lean premise retrieval problem. The authors claim that while strong agent systems can sometimes compensate for weak retrieval through repeated query reformulation or local proving, the gap between a merely compiling proof and an efficient, idiomatic one depends fundamentally on identifying and reusing existing library results.

The significance lies in establishing retrieval as a distinct axis of progress for formal mathematics. By decoupling the retrieval substrate from the proof generation loop, the system allows for independent improvement of retrieval strategies. The authors note that while the methodology is language-agnostic in design, the current evaluation is exclusive to Lean 4/Mathlib, and the behavior of such systems within highly capable agent architectures on complex, repository-level tasks remains an open area for future exploration.

The paper concludes that the combination of a hierarchy-informalized corpus, a kind-aware retrieval pipeline, and an iterative sketch-retrieve-reflect loop provides a robust solution to the challenge of finding the scattered, non-local lemmas necessary for modern formal proofs.