Lean Finder API

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

Endpoint

POST https://bxrituxuhpc70w8w.us-east-1.aws.endpoints.huggingface.cloud

The service runs on a Hugging Face Inference Endpoint. No token is required. Send a POST request with a JSON body and these headers:

Accept: application/json
Content-Type: application/json

Request body

Field	Type	Description
inputs	string	Required. Your query text.
top_k	int	How many results to return. Recommended. Example: 5.
version	string	Mathlib index to search. One of v4.19.0, v4.24.0, v4.28.0. Pick the one that matches your project so the names it returns exist in your build.

What inputs can be

• Informal statement: a natural-language version of a Lean statement.
• Question: a free-form question about Lean or Mathlib.
• Proof state: a pasted goal state, optionally with what you want to do next.
• Lean fragment: a rough snippet or draft of the declaration you want.

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

Response

A JSON object with a results array, ordered from most to least relevant.

{
  "results": [
    {
      "formal_name": "IsCompact.bddAbove_image",
      "informal_name": "A continuous function on a compact set is bounded above",
      "kind": "theorem",
      "type": "...",
      "informal_description": "...",
      "path": "Mathlib/Topology/Order/Compact",
      "score": 0.87
    }
  ]
}

Field	Meaning
formal_name	The Lean declaration name you use in code.
informal_name	Short natural-language name.
kind	Declaration kind: theorem, lemma, def, structure, instance, and so on.
type	The Lean type signature.
informal_description	Natural-language description of the declaration.
path	Module path in slash form. The Lean file is <path>.lean in mathlib4.
score	Relevance score. Higher means a closer match.

Build a link to the mathlib repo from path and version:

https://github.com/leanprover-community/mathlib4/tree/v4.28.0/Mathlib/Topology/Order/Compact.lean

Python example

import requests

ENDPOINT = "https://bxrituxuhpc70w8w.us-east-1.aws.endpoints.huggingface.cloud"

def lean_finder(query, top_k=5, version="v4.28.0"):
    headers = {
        "Accept": "application/json",
        "Content-Type": "application/json",
    }
    payload = {
        "inputs": query,
        "top_k": top_k,
        "version": version,
    }
    resp = requests.post(ENDPOINT, json=payload, headers=headers, 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"])
    print("   ", r["informal_name"])
    print("   ", r["type"])

Handling cold starts

The endpoint can scale to zero when idle. The first call after an idle period may fail or return a 503 while the model loads, which takes about 1 to 2 minutes. Retry until it responds.

import time, requests

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(2)  # endpoint is warming up, try again

curl example

curl https://bxrituxuhpc70w8w.us-east-1.aws.endpoints.huggingface.cloud \
  -X POST \
  -H "Content-Type: application/json" \
  -d '{"inputs": "continuous function on a compact set is bounded above", "top_k": 5, "version": "v4.28.0"}'