Skip to content

Quick Start

Get up and running with Lean Explore in minutes.

Using the CLI

Search for Lean declarations using natural language:

leanexplore search "natural numbers"

Configure API Key

To use the remote API, you'll need an API key:

leanexplore configure api-key YOUR_API_KEY

Search with Package Filters

Filter results to specific packages:

leanexplore search "monoid" --package Mathlib --package Batteries

Using Python API

Basic Example

import asyncio
from lean_explore.api.client import Client

async def main():
    # Initialize client with API key
    client = Client(api_key="your-api-key")

    # Perform a search
    results = await client.search("natural numbers")

    # Print results
    for item in results.results[:5]:  # Top 5 results
        lean_name = item.primary_declaration.lean_name
        informal = item.informal_description or "No description"
        print(f"{lean_name}: {informal}")

asyncio.run(main())

Search Multiple Queries

async def main():
    client = Client(api_key="your-api-key")

    # Search multiple queries at once
    results = await client.search([
        "natural numbers",
        "group theory",
        "topology"
    ])

    for result in results:
        print(f"Query: {result.query}")
        print(f"Found {len(result.results)} results\n")

asyncio.run(main())

Using Local Backend

Start Local HTTP Server

# First, fetch local data
leanexplore data fetch

# Start the server
leanexplore http serve --backend local

The server will be available at http://localhost:8001.

Query the Local Server

curl "http://localhost:8001/api/v1/search?q=natural+numbers"

Or use the Python client with a custom base URL:

client = Client(base_url="http://localhost:8001")
results = await client.search("natural numbers")

Using MCP Server

The MCP (Model Context Protocol) server allows AI agents to interact with Lean Explore:

leanexplore mcp serve --backend api --api-key YOUR_API_KEY

Next Steps