Showing cs.IRShow all
2 papers · 1 filter
cs.IR2026
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…
cs.IR2024
A Semantic Search Engine for Mathlib4
Guoxiong Gao, Haocheng Ju, Jiedong Jiang +2
The interactive theorem prover Lean enables the verification of formal mathematical proofs and is backed by an expanding community. Central to this ecosystem is its mathematical li…