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 StatementGroup 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. Inference: 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). Inference: source tracing depends on the library and toolchain. 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. Inference: 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 states: “Each StatementGroup thus represents a unique, contiguous block of source code as authored by the user.” Its example is a structure Scheme extends LocallyRingedSpace block that elaborates into declarations including AlgebraicGeometry.Scheme, AlgebraicGeometry.Scheme.mk, AlgebraicGeometry.Scheme.local_affine, AlgebraicGeometry.Scheme.toLocallyRingedSpace, AlgebraicGeometry.Scheme.rec, and AlgebraicGeometry.Scheme.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. Inference: 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, with an edge from A to B when a declaration in A depends on one in B (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.5).

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.

The paper reports no human accuracy audit of translations. Inference: LLM-generated descriptions can be inaccurate, and graph centrality does not establish semantic correctness.

technique 4: hybrid semantic, lexical, and structural ranking

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

Steps:

1. Concatenate the generated translation with file-path keywords to construct the informal statement (Section 3.4, p.5).
2. Embed the name, available docstring, and composite informal statement separately with BAAI bge-base-en-v1.5 (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 with the same model, search relevant cells using exact distances within those cells, convert distances to [0,1] similarity, and filter at default threshold 0.525 (Section 3.4, p.5).
5. Score surviving candidates with BM25+ over the primary declaration name, docstring, informal descriptions, formal display statement, and processed path; lowercase and tokenize query and candidate text (Section 3.4, p.5).
6. Min-max normalize each signal over the filtered candidates and compute a weighted sum; defaults are semantic 1.0, BM25+ 1.0, PageRank 0.2 (Section 3.4, pp.5–6).
7. Sort by the composite score in descending order (Section 3.4, p.6).

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: Section 6 states: “For each query, the top five search results (including the formal Lean code, docstring, and any provided informal statement) from each engine were presented blindly to Google’s Gemini 2.5 Flash model, which acted as an automated evaluator.” Presentation order was permuted per query (p.7). In 300 AI-generated natural-language queries designed for Mathlib, 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). These uncertainties are ± one standard error across the three runs. The paper notes that, with ties, percentages across engines for a given rank need not sum to 100% (p.8). Inference: these rankings measure LLM-judged search relevance, not theorem-proving success.

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

What it is: provide search, ID retrieval, and dependency exploration locally or through an API, and expose search and retrieval through MCP tools. Inference: 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, and explore dependencies through consistent Pydantic models (Section 4.2, p.6). The web interface additionally supports fully qualified name lookup (Section 4.1, p.6).
3. Start leanexplore chat for an assistant session, or use the CLI’s mcp server start subcommand to expose tools (Section 4.3, pp.6–7).
4. Have an agent query declarations and feed retrieved facts into proof generation (Section 5.3, p.7).

Evidence: “Both interfaces are designed to return data in consistent Pydantic model structures, simplifying client-side development.” (Section 4.2, p.6)

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 and reports no soundness evaluation of generated translations or proofs.

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

Last edited: 2026-10-19