{"repo":"justincasher/lean-explore","free":true,"listed":false,"github":"https://github.com/justincasher/lean-explore","clone":"git clone https://github.com/justincasher/lean-explore.git","description":"A search engine for Lean 4 declarations","language":"Python","stars":76,"topics":["api","lean4","machine-learning","search","semantic-search"],"license":"Apache-2.0","category":"machine-learning","readme_excerpt":"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: To run the local search backend (which uses on-device embedding and reranking models), install the extra ML dependencies: Then fetch the data files and start the local MCP server: 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: In Codex: Start a new Codex session after installation so the MCP tools a","default_branch":null,"files":null,"tree":[],"storefront":"/r/justincasher","claimed":false,"request_supported":{"post":"https://gitbuyer.com/r/justincasher/lean-explore/request-supported","requests":0},"note":"indexed from public GitHub; nothing is for sale on this page. Clone it from GitHub. Paid listings live at /search."}