LeanSearch v2: Global Premise Retrieval for Lean 4 Theorem Proving

arXiv:2605.13137v1 Announce Type: cross 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...