LeanSearch v2: Global Premise Retrieval for Lean 4 Theorem Proving

Guoxiong Gao, Zeming Sun, Jiedong Jiang +5

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…