Loogle Search - Mathlib Type Signature Search
Search Mathlib for lemmas by type signature pattern.
When to Use
-
Finding a lemma when you know the type shape but not the name
-
Discovering what's available for a type (e.g., all Nontrivial ↔ _ lemmas)
-
Type-directed proof search
Commands
Search by pattern (uses server if running, else direct)
loogle-search "Nontrivial _ ↔ _" loogle-search "(?a → ?b) → List ?a → List ?b" loogle-search "IsCyclic, center"
JSON output
loogle-search "List.map" --json
Start server for fast queries (keeps index in memory)
loogle-server &
Query Syntax
Pattern Meaning
_
Any single type
?a , ?b
Type variables (same variable = same type)
Foo, Bar
Must mention both Foo and Bar
Foo.bar
Exact name match
Examples
Find lemmas relating Nontrivial and cardinality
loogle-search "Nontrivial _ ↔ _ < Fintype.card _"
Find map-like functions
loogle-search "(?a → ?b) → List ?a → List ?b"
→ List.map, List.pmap, ...
Find everything about cyclic groups and center
loogle-search "IsCyclic, center"
→ commutative_of_cyclic_center_quotient, ...
Find Fintype.card lemmas
loogle-search "Fintype.card"
Performance
-
With server running: ~100-200ms per query
-
Cold start (no server): ~10s per query (loads 343MB index)
Setup
Loogle must be built first:
cd ~/tools/loogle && lake build lake build LoogleMathlibCache # or use --write-index
Integration with Proofs
When stuck in a Lean proof:
-
Identify what type shape you need
-
Query Loogle to find the lemma name
-
Apply the lemma in your proof
-- Goal: Nontrivial G from 1 < Fintype.card G -- Query: loogle-search "Nontrivial _ ↔ 1 < Fintype.card _" -- Found: Fintype.one_lt_card_iff_nontrivial exact Fintype.one_lt_card_iff_nontrivial.mpr h