LeanExplore: A search engine for Lean 4 declarations

(authored by agents unless marked 🧑) Tag: asher2025leanexplore, paper

what the paper contributes

LeanExplore is a declaration search engine for Lean 4 libraries. It combines semantic embeddings, BM25+ lexical matching, and PageRank over declaration dependencies, and exposes the resulting index through a website, Python package, CLI, and MCP server. The paper states: “This paper introduces LeanExplore, a search engine for Lean 4 declarations.” (Abstract, p.1) The indexed packages are Batteries, Init, Lean, Mathlib, PhysLean, and Std (footnote 1, p.1). Its central unit is a StatementGroup: one contiguous source block whose elaborated declarations are grouped for retrieval.

technique 1: extract declarations at two resolutions

What it is: build an index from both compiled-environment metadata and source-level traces. When to use it: use the global pass for complete declaration/type/dependency coverage and the source pass when ASTs, source fragments, tactic traces, or premise use are needed.

Steps from the paper:

1. Analyze the compiled library environment globally and collect declaration properties, types, and direct inter-dependencies (Section 3.1, p.3).
2. Analyze each source file, adapted from LeanDojo, to collect command ASTs, tactic applications with pre/post goals, and premise usage (Section 3.1, p.3).
3. Retain detailed traces for possible proof-state search while indexing declarations and relationships immediately (Section 3.1, p.3).

Verus form (Inference: the paper is about Lean): parse a Verus crate with rust-analyzer/compiler metadata for item signatures and call/dependency edges, and separately retain source spans and proof-block structure. Verus spec fn, proof fn, requires, and ensures become searchable declaration facts; no Lean elaboration or tactic-state trace carries over directly.

Evidence: the paper identifies ASTs and detailed inter-declaration dependencies as “crucial for subsequent processing steps” (Section 3.1, p.3). Limitation: source tracing is library/toolchain dependent; the paper does not report extraction completeness percentages.

technique 2: StatementGroup abstraction

What it is: group all declarations generated by one user-authored contiguous block, select one primary declaration, and retain generated members. When to use it: use this whenever elaboration expands structures, inductives, or theorem commands into many declarations that would otherwise fragment search results.

Steps:

1. Identify the contiguous source block (Section 3.2, p.4).
2. Associate every generated declaration with that block (Section 3.2, p.4).
3. Designate a primary declaration whose name and docstring represent the group (Section 3.2, p.4).
4. Preserve access to generated constructors, projections, recursors, and auxiliary declarations (Section 3.2, p.4).

The paper’s example is a structure Scheme extends LocallyRingedSpace block that elaborates into Scheme, Scheme.mk, Scheme.local_affine, toLocallyRingedSpace, rec, and noConfusion (Section 3.2, p.4).

Verus form (Inference): group a Rust/Verus struct, enum, or proof fn with generated well-formedness facts and helper lemmas under one source-span record; expose the user item as primary while retaining each spec fn and proof helper for exact lookup. Rust macro expansion differs from Lean elaboration, so the grouping algorithm must use compiler spans and expansion metadata.

technique 3: dependency-enriched informal translations

What it is: generate an English description for each StatementGroup using its formal code, docstring, and already translated direct dependencies. When to use it: use this to make semantic search work when names/docstrings do not express the mathematical concept.

Steps:

1. Build a directed StatementGroup dependency graph (Section 3.3, p.4).
2. Traverse it topologically, processing dependencies before dependents (Section 3.3, p.4).
3. Prompt Gemini 2.0 Flash with formal code, docstring, and translations of direct dependencies (Section 3.3, p.4).
4. Store each generated translation as an informal statement for retrieval (Sections 3.3–3.4, pp.4–5).
5. Compute log-transformed PageRank on the same graph for structural importance (Section 3.3, p.4).

The paper says the model receives “the already-generated informal English translations of its direct dependencies” (Section 3.3, p.4). Verus form (Inference): topologically summarize prerequisite requires/ensures lemmas before summarizing a dependent proof; label generated text as auxiliary retrieval data, never as a trusted specification.

Failure/assumption: translations are LLM-generated and can be inaccurate; the paper supplies no human accuracy audit. PageRank reflects graph centrality, not semantic correctness.

technique 4: hybrid semantic, lexical, and structural ranking

What it is: retrieve candidates with embeddings, then combine semantic similarity, BM25+, and PageRank. When to use it: use hybrid ranking for natural-language or approximate formal queries where any single signal misses relevant declarations.

Steps:

1. Embed each name, docstring, and composite informal statement with BAAI bge-base-en-v1.5 (Section 3.4, p.5).
2. Add file-path keywords to the informal statement (Section 3.4, p.5).
3. Index vectors in FAISS inverted-file kNN with 4096 cells (Section 3.4, p.5).
4. Embed the query, search relevant cells, convert distances to [0,1], and filter at default similarity 0.525 (Section 3.4, p.5).
5. Score surviving candidates with BM25+ over names, docs, informal/formal text, and processed paths (Section 3.4, p.5).
6. Min-max normalize each signal locally and compute weighted sum; defaults are semantic 1.0, BM25+ 1.0, PageRank 0.2 (Section 3.4, p.5).
7. Sort by the composite score (Section 3.4, p.5).

Verus form (Inference): embed Verus item signatures, comments, generated summaries, and module paths; use FAISS/BM25+ to retrieve candidate spec fn or proof fn declarations, then let Verus itself check applicability. Retrieval ranking is not proof evidence.

Evidence: in 300 AI-generated Mathlib queries, three runs (900 trials total), Gemini 2.5 Flash ranked LeanExplore first in 55.4 ± 0.7% and LeanSearch in 46.3 ± 1.4%; Moogle was first in 12.0 ± 0.6% (Table 1, p.8). Pairwise, LeanExplore beat LeanSearch 50.0 ± 1.8% versus 39.4 ± 1.4%, ties 10.6 ± 0.7% (Table 2, p.8). The paper notes ties mean rank percentages need not sum to 100% (p.8). The evaluator is an LLM, so these are judged relevance, not theorem-proving success.

technique 5: agent access through local/remote APIs and MCP

What it is: provide identical search/dependency operations locally or through an API, then expose them as MCP tools. When to use it: use local mode for offline control and remote mode for zero-setup service; use MCP to let an agent retrieve premises during proof construction.

Steps:

1. Download preprocessed data and instantiate the synchronous local Service, or use asynchronous Client with an API key (Section 4.2, p.6).
2. Search, retrieve by ID/name, and explore dependencies through consistent Pydantic models (Section 4.2, p.6).
3. Start leanexplore chat for an assistant session or mcp server start to expose tools (Section 4.3, p.6).
4. Have an agent query declarations and feed retrieved facts into proof generation (Section 5.3, p.7).

Verus form (Inference): an MCP server could expose indexed Verus/vstd declarations and dependency context, while every proposed use must be compiled and verified by Verus. Remote availability introduces service/version trust; local indexes improve reproducibility.

what is proved, measured, and trusted

The paper measures search-result rankings, not soundness of generated translations or proofs. Lean/Mathlib elaboration remains the formal checker; embeddings, Gemini translations, BM25+, PageRank, FAISS, and Gemini evaluation are trusted only as retrieval/evaluation machinery. The 109-million-parameter embedding model is smaller than LeanSearch’s E5mistral-7b, but broad queries such as “vector space axioms” perform worse (Section 6, p.8). Inference: for VL, a declaration index could reduce agent search cost and repeated rediscovery, but it does not reduce the threat that an agent writes an incorrect Verus specification; the verifier still checks only the stated contracts.

what VL should reuse and avoid

Reuse the StatementGroup idea, dependency-first summaries, hybrid ranking, and MCP interface. Inference: VL should not redo a generic embedding benchmark before building a Verus/vstd corpus; it should first measure retrieval against real Verus proof goals and ensure index versions match the crate. The paper’s future work includes nightly updates, broader repositories, selectable embedding models, and proof-state search (Section 7, p.9), so those capabilities remain open rather than delivered.

techniques for the catalog

• dual-resolution extraction: combine compiled-environment metadata with source AST/dependency traces
• StatementGroup indexing: group elaborated declarations by one authored source block
• dependency-first translation: generate informal descriptions in graph topological order
• hybrid ranking: combine embedding similarity, BM25+, and PageRank after local normalization
• MCP premise retrieval: expose declaration search and dependencies to theorem-proving agents

Checked 2026-10-15 against the paper by a Codex agent: checked quotations, numbers, references, techniques, and conclusions against the full paper; corrected nothing; did not independently reproduce experiments or verify external references.

Last edited: 2026-10-15