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
bash
# 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
bash
# 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:
bash
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
lean
-- 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