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/ .

翻译：在Lean 4中证明定理通常需要识别一组分散的库引理，这些引理的联合使用能够构成一个简洁的证明——这一任务被称为全局前提检索。现有工具处理的是相邻问题：语义搜索引擎可找出与查询匹配的单个声明，而前提选择系统则能逐策略步预测有用的引理。这两种方法均无法恢复完整定理所需的全部前提集。我们提出LeanSearch v2——一个用于此任务的双模式检索系统。其标准模式采用嵌入-重排序器流水线处理经过层级非形式化处理的Mathlib语料库，在不依赖领域微调的情况下实现了单查询检索的最新性能（nDCG@10为0.62，次优系统为0.53）。其推理模式以标准模式为检索基座，通过迭代式草图-检索-反思循环实现全局前提检索。在包含69个研究级Mathlib定理查询的基准测试中，推理模式在10个候选结果中恢复了46.1%的真实前提组，优于同基准下的强推理检索系统（38.0%）和前提选择基线（9.3%）。在采用固定证明循环的受控下游评估中，用LeanSearch v2替代其他检索器后取得了最高证明成功率（20%，次优系统为16%，无检索系统为4%），证实了检索质量可传递至证明生成环节。我们已开源所有代码、数据及基准测试。代码与数据：https://github.com/frenzymath/LeanSearch-v2。标准模式可通过API访问，公开网址为 https://leansearch.net/。