Loogle — поиск лемм в Mathlib по типовым сигнатурам

engineering

loogle-search is a Claude Code skill that searches Mathlib for lemmas by type signature pattern using the Loogle tool. It is especially useful when you know the shape of the type but not the lemma name: the query syntax supports wildcards (`_`), type variables (`?a`, `?b`), multi-identifier search, and exact name lookup. The skill invokes `loogle-search` either directly or through a background `loogle-server` that keeps the 343 MB index in memory, reducing query time from ~10 s to 100–200 ms. JSON output is available via `--json`, and results integrate seamlessly into Lean 4 proof development — a discovered lemma can be applied immediately in the proof context. Ideal for mathematicians and engineers doing formal verification who need fast, type-directed search across the Mathlib library.