Pith. sign in

REVIEW 4 major objections 5 minor 4 cited by

LeanExplore: A search engine for Lean 4 declarations

T0 review · 4 major / 5 minor · reviewed 2026-08-07 · deepseek-v4-flash

Challenge this review Re-run · record.json Download PDF Read on arXiv ↗ Review JSON

Pith's one-line read LeanExplore claims a hybrid ranking of semantic, lexical, and structural signals retrieves Lean 4 declarations more effectively than earlier search tools, and reports winning an LLM-judged comparison 55.4% to 46.3%.

desk verdict A real, well-engineered search tool for Lean 4 whose central performance claim is undermined by an LLM-judged evaluation that bundles AI-generated summaries into the result cards. read the letter →

arxiv 2506.11085 v1 pith:FPBJJVLB submitted 2025-06-04 cs.SE cs.AIcs.CLcs.IRcs.LGcs.LO

Justin Asher (Independent Researcher) This is my paper · ORCID
classification cs.SEcs.AIcs.CLcs.IRcs.LGcs.LO
keywords Lean4theoremprovingsemanticsearchhybridrankingStatementGroupBM25+PageRankmodelcontextprotocol
verification ladder T0 review T1 audit T2 compute T3 formal

The pith

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The reading

LeanExplore is a search engine for Lean 4, the interactive theorem-proving language, and it lets users find formal declarations by typing natural language, keywords, or known names. The paper's central claim is that a hybrid ranking, combining semantic embeddings of code and informal text, BM25+ lexical matching, and a PageRank-style importance score, retrieves relevant declarations better than existing tools. In an automated comparison over 300 natural-language queries, an LLM judge ranked LeanExplore's top five results first in 55.4% of instances, versus 46.3% for the strongest existing engine and 12.0% for a third. If the result holds, LeanExplore would be the most effective publicly described semantic search tool for Lean 4, lowering the barrier to finding and reusing formalized mathematics.

What carries the argument

The central organizational object is the StatementGroup, which groups all compiled declarations generated from one user-authored block of Lean source code and is identified by a primary declaration name and docstring. The load-bearing mechanism is the hybrid scoring pipeline: multi-source semantic embeddings drive approximate k-nearest-neighbor recall; BM25+ adds lexical precision; and log-transformed PageRank over the dependency graph encodes structural importance. The three scores are min-max normalized for the candidate set and combined as a weighted sum, with default weights 1.0 for semantic similarity, 1.0 for BM25+, and 0.2 for PageRank. The informal English translations are generated by an LLM that traverses the dependency graph in topological order, so each statement is described using concepts already translated, which the paper argues is what makes semantic search work on formal libraries.

What would settle it

Run the same 300 queries with human experts, blind to engine identity, rating top-five declarations for relevance, or re-run the LLM judge on result cards with informal descriptions removed so all engines show only formal code and docstrings. If LeanExplore's first-place rate drops to parity with LeanSearch under either condition, the reported advantage is an artifact of the descriptions rather than of retrieval.

Watch

Extended reading notes

Core claim

The paper claims that declaration retrieval in Lean 4 is best served by combining three complementary signals rather than relying on any one. Each user-written declaration block, called a StatementGroup, is embedded from multiple textual facets: formal Lean code, the docstring, an LLM-generated informal English translation produced inductively from already-translated dependencies, and file-path keywords. Queries are filtered by semantic similarity, then re-ranked by a weighted sum of normalized semantic similarity, BM25+ lexical score, and log-scaled PageRank computed over the StatementGroup dependency graph. The paper reports that in a blind, order-permuted evaluation repeated three times on 300 queries over Mathlib, the evaluator language model placed LeanExplore first in 55.4% of instances, beat LeanSearch in 50.0% of head-to-head comparisons, and beat Moogle in 79.2%, while using the lightest embedding model of the three systems.

Load-bearing premise

The evaluation treats an AI language model, given AI-generated queries and result cards that include AI-written informal descriptions, as an impartial judge of which engine retrieved the best declarations; if that judge is swayed by the wording of the descriptions rather than by which engine actually found the most relevant formal statements, the reported win rates do not measure retrieval quality.

Editorial extensions

If this is right

  • Users can search for Lean 4 declarations by describing a mathematical idea in everyday words, even when the declaration's name or docstring is unknown.
  • LLM-based theorem-proving agents can query the declaration database programmatically through an MCP server, giving them a retrieval step for premise selection.
  • Because the whole processed database can be downloaded, individuals and teams can run the search engine offline or behind their own infrastructure.
  • The StatementGroup abstraction aligns search results with the code users actually wrote, so retrieval is not fragmented across dozens of compiler-generated auxiliary declarations.
  • The inductive translation pipeline offers a general recipe for producing informal descriptions of large formal libraries with modest LLM cost.

Reading between the lines

Editorial extensions of the paper, not claims the author makes directly.

  • The reported margin may partly reflect that the judge's preferences could be driven by the AI-written informal descriptions shown on LeanExplore's result cards rather than by which engine retrieved the most relevant formal declarations; a human relevance judgment or a test with descriptions stripped would separate these explanations.
  • Because PageRank rewards being depended upon, foundational statements are structurally favored, which may explain the paper's observation that very general queries such as 'vector space axioms' fare worse.
  • The same three-signal recipe should transfer to any theorem-proving ecosystem whose libraries record dependency information, so the approach is testable beyond Lean 4.
  • Making the semantic similarity threshold adaptive per query, rather than fixed at 0.525, is a natural next experiment and could recover relevant declarations that the current filter discards.
Share X Bluesky LinkedIn Reddit HN

Signed reviews

No signed human review yet.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, and a circularity audit.

Referee Report

4 major / 5 minor

Summary. The paper presents LeanExplore, a search engine for Lean 4 declarations that combines semantic embeddings over multiple textual facets (formal code, docstrings, AI-generated informal translations, names, file-path keywords), BM25+ lexical scoring, and a PageRank-style centrality score over a StatementGroup-level dependency graph. The system is deployed as a website, Python package/CLI, and MCP server, and the paper describes its data extraction pipeline and the StatementGroup abstraction in detail. To evaluate retrieval effectiveness, the author compares LeanExplore against LeanSearch and Moogle on 300 AI-generated queries using Gemini 2.5 Flash as an automated judge, reporting that LeanExplore's result sets are ranked first in 55.4% of instances versus 46.3% for LeanSearch. The paper's central claim is that this hybrid ranking strategy significantly improves declaration retrieval.

Significance. If the comparative claim were supported, LeanExplore would be a valuable contribution to the Lean 4 ecosystem: it is a fully functional, publicly accessible system with a lightweight embedding model, a downloadable database, a local/remote API, and an MCP interface for AI agents. The StatementGroup abstraction is a sensible response to the mismatch between user-authored Lean code and elaborated declarations, and the inductive use of dependency structure to generate informal descriptions is a useful engineering idea. The paper also ships substantial artifacts (website, GitHub repository, data) and gives a detailed architecture description. However, the evaluation currently does not isolate retrieval quality from the content of AI-generated informal descriptions, so the headline performance numbers should not be taken at face value.

major comments (4)
  1. [Section 6 and Appendix B] The evaluation bundles AI-generated informal descriptions into the result cards shown to the judge. LeanExplore results always include an 'Informal description' field produced by Gemini 2.0 Flash (Section 3.3), while Moogle's entries are often 'N/A', a disparity the paper itself acknowledges in Section 6. The judge could therefore be rewarding the fluency or apparent helpfulness of the summaries rather than the relevance of the retrieved declarations. Since the central claim is that the hybrid ranking improves retrieval, the headline numbers in Tables 1 and 2 do not yet establish that claim. I ask for an ablation or re-evaluation that removes or standardizes informal descriptions across engines, together with the raw top-5 result sets and human relevance judgments for at least a sample of the 300 queries.
  2. [Section 6, Appendix C] All three components of the evaluation are tied to the same model family: the queries are AI-generated, the informal descriptions are generated by Gemini 2.0 Flash, and the judge is Gemini 2.5 Flash. This creates a risk that the judge systematically prefers results whose descriptions match the style and content of AI-generated text, rather than results that a human Lean user would judge as most relevant. Please specify how the queries were generated (including the prompt), and provide an additional evaluation with human annotators or with a judge from a different model family, as well as a comparison against a baseline where the informal description field is removed from all result cards.
  3. [Section 3.4] The hybrid ranking depends on several configurable parameters: the semantic similarity threshold (default 0.525), the combination weights (semantic 1.0, BM25+ 1.0, PageRank 0.2), and the evaluation top-k. The paper does not describe how these defaults were chosen, whether they were tuned on the 300 evaluation queries, or how sensitive the reported win rates are to these values. If the parameters were selected after seeing the evaluation queries, the comparison is overfit; please report a sensitivity analysis or a separate validation set.
  4. [Tables 1 and 2] The reported uncertainties are standard errors across three runs of the same LLM judge on the same 300 queries, so they capture judge stochasticity, not variability across query samples or judge instances. The claim that LeanExplore outperforms LeanSearch would be stronger with confidence intervals across independent query samples or across multiple judge models; the current presentation may overstate the precision of the 55.4% versus 46.3% difference.
minor comments (5)
  1. [Section 5.2] The phrase 'Such an setup' should be 'Such a setup'.
  2. [References] The reference for Wu et al. contains a typo: 'Meteja Jammik' should be 'Mateja Jamnik'.
  3. [Figure 1] Figure 1 is difficult to read at the current resolution; please provide a higher-resolution diagram with larger text for the pipeline stages and score names.
  4. [Appendix A] The sentence describing 'the raw (unnormalized) score range for the underlying normalized semantic similarity' is confusing; clarify whether the ranges are before or after min-max normalization and label the columns in the example lists accordingly.
  5. [Section 6] The main text should state explicitly in the limitations discussion that Moogle's frequent 'N/A' informal descriptions make the comparison unequal, rather than only noting this in passing as an observation during evaluation.

Circularity Check

1 steps flagged · score 4.0 of 10

LLM-judged evaluation bundles AI-generated informal descriptions into result cards, so the reported win rates may reflect summary fluency rather than retrieval ranking.

  1. other [Section 6 (Experimental results) and Appendix B (LLM evaluation prompt), in conjunction with Sections 3.3 and 3.4]
    "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."

    LeanExplore populates the 'Informal description' field on result cards with Gemini 2.0 Flash translations (Section 3.3), and those same informal statements are a retrieval input embedded by the BAAI model (Section 3.4). The Section 6 judge (Gemini 2.5 Flash) is shown that field for every result and asked to rank accuracy; Appendix B always includes it, while Moogle entries are sometimes 'N/A'. The paper concedes Moogle's rank 'may have been impacted by its occasional lack of natural language statements.' So the reported 1st-place margin may measure which engine supplied fluent same-family LLM summaries, not which hybrid ranking retrieved the most relevant declarations.

full rationale

The central architecture and hybrid ranking method are genuinely self-contained: semantic embeddings, BM25+, and PageRank are combined with stated weights, and the system is implemented and publicly available. I found no self-citation chain, no imported uniqueness theorem, and no fitted parameter renamed as a prediction. The only substantive circularity concern is in the evaluation: the judged result cards include AI-generated informal descriptions that are themselves part of LeanExplore's indexed representation and that were produced by a sibling Gemini model. Since the evaluator is also a Gemini model and Moogle often lacks such descriptions, the reported win rates do not cleanly measure retrieval quality; they may partly measure the quality of generated informal text. This weaknesses the central empirical claim but does not make the derivation itself circular, so a moderate score is appropriate.

Assumptions & free parameters 3 free parameters · 4 assumptions · 1 invented entities

The core search architecture introduces no free parameters in the physics sense, but several hand-chosen thresholds and weights shape the ranking. The main assumptions are about the embedding model, the faithfulness of LLM translations, the meaning of PageRank in a dependency graph, and the validity of an LLM judge. These assumptions are reasonable for a systems paper, but the evaluation claim depends on the last one.

free parameters (3)
  • semantic similarity threshold = 0.525 (default)
    Configurable cutoff for candidate admission after FAISS retrieval; chosen by hand and affects precision and recall.
  • hybrid ranking weights = semantic 1.0, BM25+ 1.0, PageRank 0.2
    Weights in the final linear combination; chosen by hand and not tuned against a held-out set.
  • evaluation top-k = 5
    The evaluator sees only the top five results from each engine, which may favor engines with one highly relevant top hit and ignores recall.
assumptions (4)
  • domain assumption BAAI bge-base-en-v1.5 embeddings capture semantic similarity between natural language queries and Lean code, docstrings, and informal text.
    The semantic search stage depends on this pretrained model generalizing to formal mathematics text; no domain-adapted fine-tuning is reported (Section 3.4).
  • domain assumption LLM-generated informal translations are faithful enough to serve as searchable text and context.
    Informal statements are generated by Gemini 2.0 Flash and used both for embedding and as display text; errors would propagate into search quality and evaluation (Section 3.3).
  • domain assumption PageRank on the StatementGroup dependency graph measures declaration importance relevant to search ranking.
    PageRank is applied to a graph where edges mean one declaration depends on another; no evidence connects this centrality to user-perceived relevance (Section 3.3).
  • ad hoc to paper An LLM judge's ranking of top-5 result sets is a valid proxy for search quality.
    The evaluation treats Gemini 2.5 Flash rankings as ground truth without validating against human preferences; the judge may be influenced by presentation and informal text (Section 6 and Appendix B).
invented entities (1)
  • StatementGroup abstraction independent evidence
    purpose: Groups all elaborated declarations originating from one user-authored source block into a single searchable and rankable unit.
    Not a physical entity; it is a data-model abstraction. Its validity is checkable from the shipped code and the website, and it does not require falsification outside the system.

how reviews work

0 comments
Cite this review

Pith. "Pith review of LeanExplore: A search engine for Lean 4 declarations." pith.science (2026). https://pith.science/paper/FPBJJVLB

@misc{pith2026250611085,
  author       = {Pith},
  title        = {Pith review of: LeanExplore: A search engine for Lean 4 declarations},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/FPBJJVLB}},
  note         = {Machine review of arXiv:2506.11085}
}
read the original abstract

The expanding Lean 4 ecosystem poses challenges for navigating its vast libraries. This paper introduces LeanExplore, a search engine for Lean 4 declarations. LeanExplore enables users to semantically search for statements, both formally and informally, across select Lean 4 packages (including Batteries, Init, Lean, Mathlib, PhysLean, and Std). This search capability is powered by a hybrid ranking strategy, integrating scores from a multi-source semantic embedding model (capturing conceptual meaning from formal Lean code, docstrings, AI-generated informal translations, and declaration titles), BM25+ for keyword-based lexical relevance, and a PageRank-based score reflecting declaration importance and interconnectedness. The search engine is accessible via a dedicated website (https://www.leanexplore.com/) and a Python API (https://github.com/justincasher/lean-explore). Furthermore, the database can be downloaded, allowing users to self-host the service. LeanExplore integrates easily with LLMs via the model context protocol (MCP), enabling users to chat with an AI assistant about Lean declarations or utilize the search engine for building theorem-proving agents. This work details LeanExplore's architecture, data processing, functionalities, and its potential to enhance Lean 4 workflows and AI-driven mathematical research

Figures

Figures reproduced from arXiv: 2506.11085 by the authors.

Figure 1
Figure 1. LeanExplore hybrid search pipeline. 5 [PITH_FULL_IMAGE:figures/full_fig_p005_1.png] view at source ↗

Discussion (0). Continue with ORCID to comment.

Forward citations

Cited by 4 Pith papers

Reviewed papers in the Pith corpus that reference this work. Sorted by Pith novelty score. Full citation record

  1. MechMath Agent Team: LLM Driven Agents for Mathematical Research

    cs.AI 2026-07 conditional novelty 7.0 of 10 partial

    A decoupled multi-agent LLM system (Harness + KB/NL/FL provers) co-piloted solutions to 11 open math problems, some with Lean formalization.

  2. OpenProver: Agentic and Interactive Theorem Proving with Lean 4

    cs.AI 2026-07 conditional novelty 5.0 of 10

    OpenProver is an open-source Planner-Worker-Verifier ATP system with Lean 4 that raises ProofNet success rates over linear LLM rollouts and adds interactive human guidance.

  3. LeanFlow: A Case Study in Workflow-Driven Lean Autoformalization

    cs.AI 2026-06 conditional novelty 5.0 of 10

    Workflow control and a cached Lean verifier improve completion and token efficiency in document-to-project autoformalization.

  4. Integrating Rules and Semantics for LLM-Based C-to-Rust Translation

    cs.SE 2025-08 unverdicted novelty 5.0 of 10

    IRENE combines rule-based retrieval, structured summarization, and compiler feedback to improve LLM-based C-to-Rust translation accuracy and safety.

Reference graph

Works this paper leans on

12 extracted references · 10 canonical work pages · cited by 4 Pith papers

  1. [1]

    • Weighted semantic score: 1.0000 • Weighted BM25+ score: 0.9622 • Weighted PageRank score: 0.0050 • Total weighted score: 1.9672

    Name: AlgebraicGeometry.IsFinite.instLocallyOfFiniteType • Informal description: A finite morphism of schemes is locally of finite type. • Weighted semantic score: 1.0000 • Weighted BM25+ score: 0.9622 • Weighted PageRank score: 0.0050 • Total weighted score: 1.9672

    work page

  2. [2]

    • Weighted semantic score: 0.8840 • Weighted BM25+ score: 0.9415 • Weighted PageRank score: 0.0035 • Total weighted score: 1.8290

    Name: AlgebraicGeometry.IsFinite.instIsIntegralHom • Informal description: A finite morphism of schemes is an integral morphism. • Weighted semantic score: 0.8840 • Weighted BM25+ score: 0.9415 • Weighted PageRank score: 0.0035 • Total weighted score: 1.8290

    work page

  3. [3]

    • Weighted semantic score: 0.8202 • Weighted BM25+ score: 0.9007 • Weighted PageRank score: 0.0000 • Total weighted score: 1.7209

    Name: AlgebraicGeometry.instIsProperOfIsFinite • Informal description: A finite morphism of schemes is proper. • Weighted semantic score: 0.8202 • Weighted BM25+ score: 0.9007 • Weighted PageRank score: 0.0000 • Total weighted score: 1.7209

    work page

  4. [4]

    • Weighted semantic score: 0.8202 • Weighted BM25+ score: 0.8683 • Weighted PageRank score: 0.0028 • Total weighted score: 1.6913

    Name: AlgebraicGeometry.IsProper.instOfIsFinite • Informal description: A finite morphism of schemes is proper. • Weighted semantic score: 0.8202 • Weighted BM25+ score: 0.8683 • Weighted PageRank score: 0.0028 • Total weighted score: 1.6913

    work page

  5. [5]

    Name: AlgebraicGeometry.IsFinite.iff_isIntegralHom_and_locallyOfFiniteType • Informal description: A morphism of schemes is finite if and only if it is an integral morphism and locally of finite type. • Weighted semantic score: 0.7204 12 • Weighted BM25+ score: 0.9275 • Weighted PageRank score: 0.0083 • Total weighted score: 1.6562 Results with scoring wi...

    work page

  6. [8]

    • Weighted semantic score: 1.0000 • Weighted PageRank score: 0.0050 • Total weighted score: 1.0050

    Name: AlgebraicGeometry.IsFinite.instLocallyOfFiniteType • Informal description: A finite morphism of schemes is locally of finite type. • Weighted semantic score: 1.0000 • Weighted PageRank score: 0.0050 • Total weighted score: 1.0050

    work page

  7. [9]

    • Weighted semantic score: 0.9188 • Weighted PageRank score: 0.0026 • Total weighted score: 0.9214

    Name: AlgebraicGeometry.Scheme.Hom.toRationalMap • Informal description: A morphism of schemes from X to Y can be viewed as a rational map from X to Y by first considering the morphism as a partial map defined on all of X, and then viewing this partial map as a rational map. • Weighted semantic score: 0.9188 • Weighted PageRank score: 0.0026 • Total weigh...

    work page

  8. [10]

    Name: AlgebraicGeometry.Scheme.Hom.toPartialMap • Informal description: Given a morphism f of schemes, we can view it as a partial map from X to Y whose domain is the entire scheme X. This partial map is represented by the entire scheme X (as the domain), the fact that X is a dense subset of itself, and the morphism itself, precomposed with the canonical ...

    work page

Show all 12 references
  1. [11]

    • Weighted semantic score: 0.8840 • Weighted PageRank score: 0.0035 • Total weighted score: 0.8875

    Name: AlgebraicGeometry.IsFinite.instIsIntegralHom • Informal description: A finite morphism of schemes is an integral morphism. • Weighted semantic score: 0.8840 • Weighted PageRank score: 0.0035 • Total weighted score: 0.8875

  2. [12]

    { Query }

    Name: AlgebraicGeometry.Scheme.Cover.Hom.comp • Informal description: Given two composable morphisms f and g between covers of a scheme with respect to a morphism property P that is stable under composition, their composition is the morphism defined by mapping an index j in U ...

  3. [1547]

    doi: 10.18653/v1/2020.findings-emnlp.139

    Association for Computational Linguistics, 2020. doi: 10.18653/v1/2020.findings-emnlp.139. URL https://aclanthology.org/2020.findings-emnlp.139. Guoxiong Gao, Haocheng Ju, Jiedong Jiang, Zihan Qin, and Bin Dong. A semantic search engine for Mathlib4. In Yaser Al-Onaizan, Mohit...

    2020 arXiv

  4. [2017]

    finite morphism schemes

    Accessed on June 2, 2025. Morph Labs. Moogle: Semantic search over mathlib4. https://www.moogle.ai/. Accessed on June 2, 2025. Chase Norman and Jeremy Avigad. Canonical for automated theorem proving in lean, April 2025. URL https://arxiv.org/abs/2504.06239. Lawrence Page, Serg...

    2025

Pith tools

Reviewed August 7, 2026 · model on record in the stance chip above.