LeanExplore

A search engine for Lean 4 declarations

A search engine for Lean 4 declarations. This project provides tools and resources for exploring the Lean 4 ecosystem.

The current indexed projects include:

• Batteries
• CSLib
• FLT (Fermat's Last Theorem)
• FormalConjectures
• Init
• Lean
• Mathlib
• PhysLean
• Std

Installation

The base package connects to the remote API and does not require heavy ML dependencies:

pip install lean-explore

To run the local search backend (which uses on-device embedding and reranking models), install the extra ML dependencies:

pip install lean-explore[local]

Then fetch the data files and start the local MCP server:

lean-explore data fetch
lean-explore mcp serve --backend local

Documentation

Full docs live in the docs/ folder, or at https://www.leanexplore.com/docs.

Page	Description
Getting Started	Install and run your first search.
CLI Reference	Every lean-explore command and flag.
MCP Server	Wire LeanExplore into Claude, Cursor, or any MCP client.
API Client	Use ApiClient from Python.
Local Search Backend	How hybrid BM25 + FAISS + reranking works.
Configuration	Environment variables and data layout.
Data Models	SearchResult, SearchResponse, and related types.
Extraction Pipeline	Rebuild the dataset from Lean source (contributors).

Contributing

Contributions are welcome! Please see CONTRIBUTING.md for guidelines on code style, testing, and development setup.

Cite

If you use LeanExplore in your research or work, please cite it as follows:

General Citation:

Justin Asher. (2025). LeanExplore: A search engine for Lean 4 declarations. https://arxiv.org/abs/2506.11085

BibTeX Entry:

@software{Asher_LeanExplore_2025,
  author = {Asher, Justin},
  title = {{LeanExplore: A search engine for Lean 4 declarations}},
  year = {2025},
  url = {https://arxiv.org/abs/2506.11085}
}

License

This code is distributed under an Apache License (see LICENSE).