Loogle - Lean/Mathlib Search
loogle
Search for Lean 4 and Mathlib theorems, lemmas, and definitions by type signature, name, or subexpression pattern. Use when the user asks to find a theorem, look up a Lean definition, search for lemmas, or needs help discovering Mathlib functions.
SKILL.md
Full skill instructions
Loogle - Lean/Mathlib Search
Search for Lean 4 and Mathlib declarations using the Loogle API.
How to Search
Use WebFetch to query the Loogle JSON API:
https://loogle.lean-lang.org/json?q=<URL-encoded-query>
Query Syntax
| Type | Syntax | Example |
|---|---|---|
| By constant | ConstantName | List.map |
| By name substring | "text" | "differ" |
| By subexpression | _ * (_ ^ _) | Pattern matching |
| By type signature | (?a -> ?b) -> List ?a -> List ?b | Type search |
| By conclusion | ` | - goal` |
| Combined | filter1, filter2 | AND logic |
Response Handling
Success response:
count: Total matches foundhits: Array of results (max 200)name: Declaration nametype: Type signaturemodule: Source moduledoc: Documentation (may be null)
Error response:
error: Error messagesuggestions: Array of suggested corrections
When presenting results, show the declaration name, type signature, and module. Include documentation if available.
Example Queries
- Find list functions:
List, ?a -> ?b - Search by name:
"append" - Type signature:
Nat -> Nat -> Bool - Parsec functions:
Std.Internal.Parsec - Option operations:
Option, "map"