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
• CSLib
• FLT (Fermat's Last Theorem)
• FormalConjectures
• Init
• Lean
• Mathlib
• PhysLean
• Std

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

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