Lean Finder API

Semantic search over Mathlib. Send a query, get back ranked Lean declarations.

Endpoint

POST https://lean-lsp-proxy.leanfinder.workers.dev

No API key needed. Send a JSON body with Content-Type: application/json.

Rate limit: 100 requests per 60 seconds per IP. Over the limit you get HTTP 429 with Retry-After: 60; wait and retry.

Request body

Field	Type	Description
`inputs`	string	Required. Your query text.
`top_k`	int	Number of results. Default 10.
`version`	string	Mathlib index to search: `v4.19.0`, `v4.24.0` or `v4.28.0`. Match your project so returned names exist in your build.

inputs can be an informal statement, a question about Lean or Mathlib, a pasted proof state, or a rough Lean snippet.

{
  "inputs": "continuous function on a compact set is bounded above",
  "top_k": 5,
  "version": "v4.28.0"
}

Response

A results array, most relevant first.

{
  "results": [
    {
      "formal_name": "IsCompact.bddAbove_image",
      "informal_name": "Continuous Image of Compact Set is Bounded Above ...",
      "kind": "theorem",
      "type": "...",
      "informal_description": "...",
      "path": "Mathlib/Topology/Order/Compact",
      "url": "https://leanprover-community.github.io/mathlib4_docs/find/?pattern=IsCompact.bddAbove_image#doc",
      "score": 0.876
    }
  ]
}

Field	Meaning
`formal_name`	Lean declaration name.
`informal_name`	Short natural-language name.
`kind`	theorem, def, structure, instance, ...
`type`	Lean type signature.
`informal_description`	Natural-language description.
`path`	Module path; the file is `<path>.lean` in mathlib4.
`url`	Link to the declaration in the Mathlib docs.
`score`	Relevance score. Higher is better.

Errors come back as {"error": "..."}. A missing inputs returns HTTP 400; an unknown version returns HTTP 200 with an error key, so check for it.

curl

curl https://lean-lsp-proxy.leanfinder.workers.dev \
  -H "Content-Type: application/json" \
  -d '{"inputs": "continuous function on a compact set is bounded above", "top_k": 5, "version": "v4.28.0"}'

Python

import requests

ENDPOINT = "https://lean-lsp-proxy.leanfinder.workers.dev"

def lean_finder(query, top_k=5, version="v4.28.0"):
    payload = {"inputs": query, "top_k": top_k, "version": version}
    resp = requests.post(ENDPOINT, json=payload, timeout=60)
    resp.raise_for_status()
    return resp.json().get("results", [])

for r in lean_finder("continuous function on a compact set is bounded above"):
    print(round(r["score"], 3), r["formal_name"])

Cold starts

The backend scales to zero when idle. The first request after a quiet period may fail or return 503 for 1 to 2 minutes while the model loads. Retry until it responds.

import time

def lean_finder_retry(query, max_wait=300, **kwargs):
    start = time.time()
    while True:
        try:
            return lean_finder(query, **kwargs)
        except requests.exceptions.RequestException:
            if time.time() - start > max_wait:
                raise
            time.sleep(5)

Lean Finder | Semantic Search for Mathlib | Paper | Code | Model