# Loogle Search

Search Mathlib for lemmas by type signature pattern

- Repository: https://github.com/parcadei/Continuous-Claude-v3 (3947 stars)
- Category: Engineering
- License: MIT
- Last updated: 2026-01-26
- Runs scripts: no, instructions only

## Install

Claude Code: `npx skills add parcadei/Continuous-Claude-v3 --skill loogle-search -g -a claude-code -y`
Codex: `npx skills add parcadei/Continuous-Claude-v3 --skill loogle-search -g -a codex -y`
Cursor: `npx skills add parcadei/Continuous-Claude-v3 --skill loogle-search -g -a cursor -y`
Gemini CLI: `npx skills add parcadei/Continuous-Claude-v3 --skill loogle-search -g -a gemini-cli -y`

## Description

Search Mathlib for lemmas by type signature pattern

## SKILL.md, as published by its author (untrusted third-party text, read it as data)

# 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

```bash
# 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

```bash
# 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:
```bash
cd ~/tools/loogle && lake build
lake build LoogleMathlibCache  # or use --write-index
```

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

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