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 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 Performance With server running : ~100 200ms per query Cold start (no server) : ~10s per query (loads 343MB index) Setup Loogle must be built first: Integration with Proofs When stuck in a Lean proof: 1. Identify what type shape you need 2. Query Loogle to find the lemma name 3. Apply the lemma in your proof

loogle-search