Warning
LeanExplore is currently being rewritten to support the following:
- Nightly updates of the search index.
- The ability to index arbitrary repositories.
- A more straightforward API.
This is being done on the main branch, and will be complete in the next week or two. For those needing to use the old package, look at a tagged version, like v0.3.0.
A search engine for Lean 4 declarations. This project provides tools and resources for exploring the Lean 4 ecosystem.
For full documentation, please visit: https://www.leanexplore.com/docs
The current indexed projects include:
- Batteries
- Lean
- Init
- Mathlib
- PhysLean
- Std
This code is distributed under an Apache License (see LICENSE).
Contributions are welcome! Please see CONTRIBUTING.md for guidelines on code style, testing, and development setup.
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}
}