Loogle Search

parcadei/loogle-search

Search Mathlib for lemmas by type signature pattern

503 tokens

context cost

the whole folder, loaded on every use

files

instructions only

copies elsewhere

how many repositories repackaged it

3880

stars on the repo

on the repository, not the skill itself

Install

one command, takes just this skill from the repository

npx skills add https://github.com/parcadei/Continuous-Claude-v3 --skill loogle-search

The instruction itself

8 sections, as written by the author

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

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

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

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

How to use it

Copy the folder

Take parcadei/loogle-search from the repository into ~/.claude/skills for personal use, or into .claude/skills inside a project.

Check the name does not clash

The agent identifies a skill by the name field in its header. Two skills with the same name cannot sit side by side — one of them will be ignored.