Skip to content

Lean Explore

A search engine for Lean 4 declarations

Lean Explore is a powerful search engine designed to help you discover and explore declarations in the Lean 4 ecosystem. It provides semantic search capabilities across multiple Lean projects including Mathlib, Batteries, Std, and more.

Features

  • 🔍 Semantic Search: Find Lean declarations using natural language queries
  • 📚 Multi-Project Support: Search across Mathlib, Batteries, Std, PhysLean, Init, and Lean
  • 🚀 Multiple Interfaces: Use via CLI, Python API, HTTP server, or MCP server
  • 🏠 Local Backend: Run searches locally with your own data
  • 🔗 Dependency Tracking: Explore relationships between declarations
  • 📊 Ranked Results: Results are ranked using semantic similarity, PageRank, and lexical matching

Current Indexed Projects

The following Lean projects are currently indexed:

  • Batteries - Extended standard library for Lean 4
  • Lean - Core Lean 4 library
  • Init - Initialization and basic types
  • Mathlib - Mathematics library for Lean 4
  • PhysLean - Physics library for Lean 4
  • Std - Standard library for Lean 4

Installation

pip install lean-xplore

For more details, see the Installation Guide.

Basic Usage

CLI

# Search for declarations
leanexplore search "natural numbers"

# Configure API key
leanexplore configure api-key YOUR_API_KEY

# Start local HTTP server
leanexplore http serve --backend local

Python API

from lean_explore.api.client import Client

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

HTTP Server

# Start server
leanexplore http serve --backend local

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

Documentation Structure

Citation

If you use Lean Explore in your research or work, please cite it:

@software{Asher_LeanExplore_2025,
  author = {Asher, Justin},
  title = {{LeanExplore: A search engine for Lean 4 declarations}},
  year = {2025},
  url = {http://www.leanexplore.com},
  note = {GitHub repository: https://github.com/justincasher/lean-explore}
}

License

This project is distributed under the Apache License 2.0. See LICENSE for details.