| name | loogle |
| description | 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. |
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"
