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.

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

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}
}