LeanSearch v2: Global Premise Retrieval for Lean 4 Theorem Proving

• URL: http://arxiv.org/abs/2605.13137v2
• Date: Thu, 14 May 2026 05:15:13 GMT
• Title: LeanSearch v2: Global Premise Retrieval for Lean 4 Theorem Proving
• Abstract summary: Proving theorems in Lean 4 often requires identifying a scattered set of library lemmas whose joint use enables a concise proof.<n>We present LeanSearch v2, a two-mode retrieval system for this task.
• Score: 7.326381497366569
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: 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/ .

Related papers

• ExecRetrieval: Measuring the Functional-Correctness Gap in Code-Embedding Retrieval [0.0]
  Embedding-based code retrieval is a core component of coding agents and retrieval-augmented code generation.<n>Existing benchmarks do not plant controlled, execution-verified single-edit variants of each query's canonical implementation.<n>We introduce ExecRetrieval, 939 Python tasks each paired with one execution-verified canonical implementation and up to four execution-verified buggy distractors.
  arXiv  Detail & Related papers  (2026-09-01T20:55:17Z)
• VisDocAgentBench: Benchmarking Agents for Visually Rich Document Retrieval [65.89247522243959]
  VisDocAgentBench is a closed-corpus benchmark comparing static and agentic retrieval under a ranked-output contract.<n>It contains 2,375 pages from 100 documents and 120 unique-target queries balanced across direct, one-bridge, and two-bridge evidence structures.<n>A strong late-interaction visual retriever reaches 97.50% Recall@1 on direct items but 2.50% on two-bridge items, exposing the limits of query--target matching when relevance depends on corpus context.
  arXiv  Detail & Related papers  (2026-08-18T15:23:06Z)
• Keep the Proof State Live: Snapshotting for Efficient Tactic Search in Lean 4 [1.2816802110958607]
  We introduce proof-state snapshotting, which captures the elaborated proof state once and reuses it across branches via a small extension to the Lean 4 language server.<n>Across 48 miniF2F-v2 problems, our approach achieves a 5.6-50x wall-time speedup over the standard fallback.
  arXiv  Detail & Related papers  (2026-05-25T08:12:26Z)
• Reproducing Complex Set-Compositional Information Retrieval [11.891887979573925]
  Complex information needs may involve set-compositional queries using conjunction, disjunction, and exclusion.<n>We benchmark major retrieval families and reasoning-targeted methods on QUEST and QUEST+Variants.
  arXiv  Detail & Related papers  (2026-05-05T14:51:40Z)
• Agentic Forecasting using Sequential Bayesian Updating of Linguistic Beliefs [1.7470133607730627]
  BLF (Bayesian Linguistic Forecaster) is an agentic system for binary forecasting.<n>On 400 backtesting questions from the ForecastBench leaderboard, BLF outperforms all the top public methods.
  arXiv  Detail & Related papers  (2026-04-20T17:57:51Z)
• From BM25 to Corrective RAG: Benchmarking Retrieval Strategies for Text-and-Table Documents [0.0]
  We benchmark ten retrieval strategies spanning sparse, dense, hybrid fusion, cross-encoder reranking, query expansion, index augmentation, and adaptive retrieval.<n>We evaluate retrieval quality via Recall@k, MRR, and nDCG, and end-to-end generation quality via Number Match.
  arXiv  Detail & Related papers  (2026-04-02T07:53:40Z)
• PeopleSearchBench: A Multi-Dimensional Benchmark for Evaluating AI-Powered People Search Platforms [14.675528528017653]
  We introduce PeopleSearchBench, an open-source benchmark that compares four people search platforms on 119 real-world queries.<n>A key contribution is Criteria-Grounded Verification, a factual relevance pipeline that extracts explicit, verifiable criteria from each query.<n>Lessie, a specialized AI people search agent, performs best overall, scoring 65.2, 18.5% higher than the second-ranked system.
  arXiv  Detail & Related papers  (2026-03-29T02:21:09Z)
• Towards Global Retrieval Augmented Generation: A Benchmark for Corpus-Level Reasoning [50.27838512822097]
  We introduce GlobalQA, the first benchmark specifically designed to evaluate global RAG capabilities.<n>We propose GlobalRAG, a multi-tool collaborative framework that preserves structural coherence through chunk-level retrieval.<n>On the Qwen2.5-14B model, GlobalRAG achieves 6.63 F1 compared to the strongest baseline's 1.51 F1.
  arXiv  Detail & Related papers  (2025-10-30T07:29:14Z)
• LLM-guided Hierarchical Retrieval [54.73080745446999]
  LATTICE is a hierarchical retrieval framework that enables an LLM to reason over and navigate large corpora with logarithmic search complexity.<n>A central challenge in such LLM-guided search is that the model's relevance judgments are noisy, context-dependent, and unaware of the hierarchy.<n>Our framework achieves state-of-the-art zero-shot performance on the reasoning-intensive BRIGHT benchmark.
  arXiv  Detail & Related papers  (2025-10-15T07:05:17Z)
• Eigen-1: Adaptive Multi-Agent Refinement with Monitor-Based RAG for Scientific Reasoning [53.45095336430027]
  We develop a unified framework that combines implicit retrieval and structured collaboration.<n>On Humanity's Last Exam (HLE) Bio/Chem Gold, our framework achieves 48.3% accuracy.<n>Results on SuperGPQA and TRQA confirm robustness across domains.
  arXiv  Detail & Related papers  (2025-09-25T14:05:55Z)
• BRIGHT: A Realistic and Challenging Benchmark for Reasoning-Intensive Retrieval [54.54576644403115]
  We introduce BRIGHT, the first text retrieval benchmark that requires intensive reasoning to retrieve relevant documents.<n>Our dataset consists of 1,384 real-world queries spanning diverse domains, such as economics, psychology, mathematics, and coding.<n>We show that incorporating explicit reasoning about the query improves retrieval performance by up to 12.2 points.
  arXiv  Detail & Related papers  (2024-07-16T17:58:27Z)
• ExcluIR: Exclusionary Neural Information Retrieval [74.08276741093317]
  We present ExcluIR, a set of resources for exclusionary retrieval. evaluation benchmark includes 3,452 high-quality exclusionary queries. training set contains 70,293 exclusionary queries, each paired with a positive document and a negative document.
  arXiv  Detail & Related papers  (2024-04-26T09:43:40Z)
• An In-Context Learning Agent for Formal Theorem-Proving [10.657173216834668]
  We present an in-context learning agent for formal theorem-context in environments like Lean and Coq. COPRA repeatedly asks a large language model to propose tactic applications from within a stateful backtracking search. We evaluate our implementation of COPRA on the miniF2F benchmark for Lean and a set of Coq tasks from the CompCert project.
  arXiv  Detail & Related papers  (2023-10-06T16:21:22Z)

This list is automatically generated from the titles and abstracts of the papers in this site.

This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.