# LeanSearch v2: Global Premise Retrieval for Lean 4 Theorem Proving

arXiv: https://arxiv.org/abs/2605.13137 · HTML: https://mlsanity.com/paper/2605.13137/

## Key facts

- Cited by 10 papers in the map (data through 14 Oct 2026).
- Builds on 30 of its 35 references that are in the map.
- First posted on arXiv 13 May 2026.

## Builds on (most cited first, 30 of 30)

- [Qwen3 Technical Report](https://mlsanity.com/paper/2505.09388/) (2025)
- [Gemini 2.5: Pushing the Frontier with Advanced Reasoning, Multimodality, Long Context, and Next Generation Agentic Capabilities](https://mlsanity.com/paper/2507.06261/) (2025)
- [Qwen3 Embedding: Advancing Text Embedding and Reranking Through Foundation Models](https://mlsanity.com/paper/2506.05176/) (2025)
- [MTEB: Massive Text Embedding Benchmark](https://mlsanity.com/paper/2210.07316/) (2022)
- [Kimi K2: Open Agentic Intelligence](https://mlsanity.com/paper/2507.20534/) (2025)
- [LeanDojo: Theorem Proving with Retrieval-Augmented Language Models](https://mlsanity.com/paper/2306.15626/) (2023)
- [DeepSeek-Prover-V2: Advancing Formal Mathematical Reasoning via Reinforcement Learning for Subgoal Decomposition](https://mlsanity.com/paper/2504.21801/) (2025)
- [BRIGHT: A Realistic and Challenging Benchmark for Reasoning-Intensive Retrieval](https://mlsanity.com/paper/2407.12883/) (2024)
- [NaturalProofs: Mathematical Theorem Proving in Natural Language](https://mlsanity.com/paper/2104.01112/) (2021)
- [ReasonIR: Training Retrievers for Reasoning Tasks](https://mlsanity.com/paper/2504.20595/) (2025)
- [Rank1: Test-Time Compute for Reranking in Information Retrieval](https://mlsanity.com/paper/2502.18418/) (2025)
- [Herald: A Natural Language Annotated Lean 4 Dataset](https://mlsanity.com/paper/2410.10878/) (2024)
- [Aristotle: IMO-level Automated Theorem Proving](https://mlsanity.com/paper/2510.01346/) (2025)
- [Numina-Lean-Agent: An Open and General Agentic Reasoning System for Formal Mathematics](https://mlsanity.com/paper/2601.14027/) (2026)
- [Seed-Prover 1.5: Mastering Undergraduate-Level Theorem Proving via Learning from Experience](https://mlsanity.com/paper/2512.17260/) (2025)
- [DIVER: A Multi-Stage Approach for Reasoning-intensive Information Retrieval](https://mlsanity.com/paper/2508.07995/) (2025)
- [A Semantic Search Engine for Mathlib4](https://mlsanity.com/paper/2403.13310/) (2024)
- [Automated Conjecture Resolution with Formal Verification](https://mlsanity.com/paper/2604.03789/) (2026)
- [RaDeR: Reasoning-aware Dense Retrieval Models](https://mlsanity.com/paper/2505.18405/) (2025)
- [FATE: A Formal Benchmark Series for Frontier Algebra of Multiple Difficulty Levels](https://mlsanity.com/paper/2511.02872/) (2025)
- [REAL-Prover: Retrieval Augmented Lean Prover for Mathematical Reasoning](https://mlsanity.com/paper/2505.20613/) (2025)
- [LeanExplore: A search engine for Lean 4 declarations](https://mlsanity.com/paper/2506.11085/) (2025)
- [MM-BRIGHT: A Multi-Task Multimodal Benchmark for Reasoning-Intensive Retrieval](https://mlsanity.com/paper/2601.09562/) (2026)
- [Lean Finder: Semantic Search for Mathlib That Understands User Intents](https://mlsanity.com/paper/2510.15940/) (2025)
- [MIRB: Mathematical Information Retrieval Benchmark](https://mlsanity.com/paper/2505.15585/) (2025)
- [Premise Selection for a Lean Hammer](https://mlsanity.com/paper/2506.07477/) (2025)
- [Benchmarking Information Retrieval Models on Complex Retrieval Tasks](https://mlsanity.com/paper/2509.07253/) (2025)
- [Learning an Effective Premise Retrieval Model for Efficient Mathematical Formalization](https://mlsanity.com/paper/2501.13959/) (2025)
- [GroupRank: A Groupwise Paradigm for Effective and Efficient Passage Reranking with LLMs](https://mlsanity.com/paper/2511.11653/) (2025)
- [Combining Textual and Structural Information for Premise Selection in Lean](https://mlsanity.com/paper/2510.23637/) (2025)

## Built on by (most cited first, 10 of 10)

- [Formalizing Numerical Analysis: An Agent Pipeline and Quality Audit Beyond Kernel Acceptance](https://mlsanity.com/paper/2606.14000/) (2026)
- [TheoremGraph: Bridging Formal and Informal Mathematics](https://mlsanity.com/paper/2606.25363/) (2026)
- [MechMath Agent Team: LLM Driven Agents for Mathematical Research](https://mlsanity.com/paper/2607.04394/) (2026)
- [TreeThink: A Modular Tree Search Library for Mathematical Reasoning with LLMs](https://mlsanity.com/paper/2607.11258/) (2026)
- [When Does Structured Knowledge Help Neural Theorem Proving?](https://mlsanity.com/paper/2609.34460/) (2026)
- [ProofLoom: Proof-Obligation-Driven Theory Construction for Autoformalizing Research-Level Stochastic Optimization](https://mlsanity.com/paper/2609.34960/) (2026)
- [GenLimitLib: A Formal Library for Language Generation in the Limit and AI-Assisted Mathematical Research](https://mlsanity.com/paper/2609.36663/) (2026)
- [Second-Order Problem Solving for Recursive Self-Improvement in Formal Verification](https://mlsanity.com/paper/2610.05701/) (2026)
- [Let the Library Speak: Self-Advertised Method Selection for Formal Proving](https://mlsanity.com/paper/2610.09401/) (2026)
- [The Future of AI-assisted Physics: Discovering, Verifying and Organizing Results via Formalization](https://mlsanity.com/paper/2610.14059/) (2026)

## Abstract (arXiv)

Proving theorems in Lean 4 often requires identifying a scattered set of library lemmas whose joint use enables a concise proof -- a task we call global premise retrieval. Existing tools address adjacent problems: semantic search engines find individual declarations matching a query, while premise-selection systems predict useful lemmas one tactic step at a time. Neither recovers the full premise set an entire theorem requires. We present LeanSearch v2, a two-mode retrieval system for this task. Its standard mode applies a hierarchy-informalized Mathlib corpus with an embedding-reranker pipeline, achieving state-of-the-art single-query retrieval without domain-specific fine-tuning (nDCG@10 of 0.62 vs. 0.53 for the next-best system). Its reasoning mode builds on standard mode as its retrieval substrate, targeting global premise retrieval through iterative sketch-retrieve-reflect cycles. On a 69-query benchmark of research-level Mathlib theorems, reasoning mode recovers 46.1% of ground-truth premise groups within 10 retrieved candidates, outperforming strong reasoning retrieval systems (38.0%) and premise-selection baselines (9.3%) on the same benchmark. In a controlled downstream evaluation with a fixed prover loop, replacing alternative retrievers with LeanSearch v2 yields the highest proof success (20% vs. 16% for the next-best system and 4% without retrieval), confirming that retrieval quality propagates to proof generation. We have open-sourced all code, data, and benchmarks. Code and data: https://github.com/frenzymath/LeanSearch-v2 . The standard mode is publicly available with API access at https://leansearch.net/ .