Run any Skill in Manus
with one click
with one click
Run any Skill in Manus with one click
Get Startedloogle-search
Search Mathlib for lemmas by type signature pattern
Stars3,818
Forks294
UpdatedJanuary 22, 2026 at 10:54
SKILL.md
readonlyMenu
Search Mathlib for lemmas by type signature pattern
Create git commits with user approval and no Claude attribution
Create or update continuity ledger for state preservation across clears
Create handoff document for transferring work to another session
Generate comprehensive PR descriptions following repository templates
Deep interview process to transform vague ideas into detailed specs. Works for technical and non-technical users.
Planning agent that creates implementation plans and handoffs from conversation context
| name | loogle-search |
| description | Search Mathlib for lemmas by type signature pattern |
Search Mathlib for lemmas by type signature pattern.
Nontrivial ↔ _ lemmas)# 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 &
| 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 |
# 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"
Loogle must be built first:
cd ~/tools/loogle && lake build
lake build LoogleMathlibCache # or use --write-index
When stuck in a Lean 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