mcpField
L
loogle-search

loogle-search

github.com/parcadeiDevelopment3.9k487 installsUpdated 39w ago
Repository

About loogle-search

A command-line tool for searching Mathlib lemmas by type-signature patterns. It helps Lean users find relevant results when they know the shape of a type but not the lemma name.

Key features

  1. 01Search lemmas by type pattern
  2. 02Support type variables and wildcards
  3. 03Match multiple required terms
  4. 04Return JSON output
  5. 05Search with a running server or directly

Use cases

  1. 01Find a lemma by its expected type
  2. 02Explore results involving selected identifiers
  3. 03Locate a result to apply in a Lean proof

Install

Copy the command and run it in a terminal.

$npx skills add https://github.com/parcadei/continuous-claude-v3 --skill loogle-search

After installing, type/loogle-searchin Claude Code to confirm it loaded.

Details

From the project README

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

PatternMeaning
_Any single type
?a, ?bType variables (same variable = same type)
Foo, BarMust mention both Foo and Bar
Foo.barExact 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:

  1. Identify what type shape you need
  2. Query Loogle to find the lemma name
  3. 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

Comments

Markdown supported