justincasher/lean-explore
A search engine for Lean 4 declarations
Supports both remote API and local search backends with on-device embedding/reranking models, enabling offline declaration discovery across major Lean 4 projects (Mathlib, Batteries, FLT, etc.). Exposes search functionality via an MCP server architecture, allowing integration with compatible tools and editors. The local backend eliminates heavy ML dependency requirements from the base package while maintaining full indexing across nine core Lean ecosystem libraries.
Available on PyPI.
Stars
55
Forks
14
Language
Python
License
Apache-2.0
Category
Last pushed
Mar 09, 2026
Commits (30d)
0
Dependencies
19
Get this data via API
curl "https://pt-edge.onrender.com/api/v1/quality/embeddings/justincasher/lean-explore"
Open to everyone — 100 requests/day, no key needed. Get a free key for 1,000/day.
Related tools
cocoindex-io/cocoindex
Data transformation framework for AI. Ultra performant, with incremental processing. 🌟 Star if...
dtsola/xiaoyaosearch
小遥搜索，听懂你的话、看懂你的图，用AI找到本地任何文件。让搜索像聊天一样简单。XiaoyaoSearch: Understands your words, reads your...
Ryandonofrio3/osgrep
Open Source Semantic Search for your AI Agent
yoanbernabeu/grepai
Semantic Search & Call Graphs for AI Agents (100% Local)
starthackHQ/Contextinator
Turning messy repos into weapons of mass structured context.