Loogle Search

This is type signature search for Mathlib, the massive Lean mathematics library. You know the shape of what you need (like "something that turns Nontrivial into a cardinality bound") but not the lemma name. Feed it patterns with wildcards and type variables, get back actual lemma names. The syntax is clean: `?a` for type variables, `_` for wildcards, commas for "must mention both". Cold starts take 10 seconds to load a 343MB index, but spin up the server and queries drop to 100ms. It's proof search for when you're reasonably sure the lemma exists but have no idea what it's called, which in a library with thousands of theorems is most of the time.