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 glob