Examples

Collection of example code demonstrating Lean Explore usage.

Basic Search

import asyncio
from lean_explore.api.client import Client

async def main():
    client = Client(api_key="your-api-key")
    results = await client.search("natural numbers")

    for item in results.results[:5]:
        print(f"{item.primary_declaration.lean_name}")
        if item.informal_description:
            print(f"  {item.informal_description}")
        print()

asyncio.run(main())

Search with Filters

import asyncio
from lean_explore.api.client import Client

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

    results = await client.search(
        "monoid",
        package_filters=["Mathlib", "Batteries"]
    )

    print(f"Found {len(results.results)} results in Mathlib and Batteries")
    for item in results.results:
        print(f"- {item.primary_declaration.lean_name}")

asyncio.run(main())

Multiple Queries

import asyncio
from lean_explore.api.client import Client

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

    queries = [
        "natural numbers",
        "group theory",
        "topology"
    ]

    results = await client.search(queries)

    for result in results:
        print(f"\nQuery: {result.query}")
        print(f"Results: {len(result.results)}")
        for item in result.results[:3]:
            print(f"  - {item.primary_declaration.lean_name}")

asyncio.run(main())

Get Citations

import asyncio
from lean_explore.api.client import Client

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

    # Search first
    search_results = await client.search("Nat")
    if search_results.results:
        first_result = search_results.results[0]

        # Get dependencies (citations)
        dependencies = await client.get_dependencies(first_result.id)

        if dependencies:
            print(f"Dependencies for {first_result.primary_declaration.lean_name}:")
            for citation in dependencies.citations:
                print(f"  - {citation.primary_declaration.lean_name}")

asyncio.run(main())

Local Backend

import asyncio
from lean_explore.local.service import Service

async def main():
    # Initialize local service
    service = Service()

    # Search
    results = await service.search("natural numbers")

    print(f"Found {len(results.results)} results")
    for item in results.results[:5]:
        print(f"- {item.primary_declaration.lean_name}")

asyncio.run(main())

HTTP Server Client

import asyncio
from lean_explore.api.client import Client

async def main():
    # Connect to local server
    client = Client(base_url="http://localhost:8001")

    # Use as normal
    results = await client.search("natural numbers")

    for item in results.results:
        print(item.primary_declaration.lean_name)

asyncio.run(main())

Error Handling

import asyncio
import httpx
from lean_explore.api.client import Client

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

    try:
        results = await client.search("natural numbers")
        print(f"Found {len(results.results)} results")
    except httpx.HTTPStatusError as e:
        print(f"HTTP error: {e.response.status_code}")
        print(f"Response: {e.response.text}")
    except httpx.RequestError as e:
        print(f"Request error: {e}")
    except Exception as e:
        print(f"Unexpected error: {e}")

asyncio.run(main())

Custom Configuration

import asyncio
from lean_explore.api.client import Client

async def main():
    client = Client(
        api_key="your-api-key",
        base_url="https://custom-api.example.com/api/v1",
        timeout=30.0
    )

    results = await client.search("natural numbers")
    print(f"Found {len(results.results)} results")

asyncio.run(main())