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