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

Claude Code and Codex plugin

The repository includes a plugin for both Claude Code and Codex. It connects to
the hosted MCP server, so it does not need a Python install, a local search
index, account, API key, or browser authorization. The tools are available as
soon as the plugin is installed.

The hosted endpoint allows 30 POST requests per client IP in any 60-second
window. Protocol initialization and tool-discovery requests count toward the
limit, and clients sharing a public IP share the same budget.

Agents should begin with the token-efficient search_summary tool, then use
the per-field retrieval tools for the declarations they need. The older
full-result search MCP tool is deprecated and remains only for compatibility.
All LeanExplore MCP tools are read-only and cannot modify Lean packages or
external systems.

In Claude Code:

/plugin marketplace add justincasher/lean-explore
/plugin install lean-explore@lean-explore
/reload-plugins

In Codex:

codex plugin marketplace add https://github.com/justincasher/lean-explore
codex plugin add lean-explore@lean-explore

Start a new Codex session after installation so the MCP tools are loaded.

Documentation

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

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).

{
  "name": "lean-explore",
  "owner": {
    "name": "Justin Asher",
    "email": "justinchadwickasher@gmail.com"
  },
  "description": "Plugins for searching Lean 4 declarations with LeanExplore.",
  "plugins": [
    {
      "name": "lean-explore",
      "source": "./plugins/lean-explore",
      "description": "Search Lean 4 declarations through the hosted LeanExplore MCP server.",
      "version": "0.1.0"
    }
  ]
}