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.

skills.sh installs: 487
GitHub stars: 3.9K
last updated: Aug 21, 2026

View on GitHub

Install

$ npx -y skills add parcadei/continuous-claude-v3 --skill loogle-search --agent claude-code

Installs into .claude/skills of the current project.

Files

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, ...

SKILL.md on GitHub