{"id":"34224e1b-76d6-496b-bc6d-78ba81656261","arxiv_id":"2506.11085","paper_version":1,"verdict":"CONDITIONAL","confidence":"MODERATE","novelty_score":6.0,"correctness_risk":"medium","formal_verification":"none","parameter_count":3,"one_line_summary":"LeanExplore combines semantic embeddings, BM25+ lexical matching, and PageRank to retrieve Lean 4 declarations from natural language queries, and reports an LLM-judged win rate over existing tools.","lead":"LeanExplore is a new search engine that lets people find Lean 4 math declarations using natural language, keywords, or formal names. It combines three ranking signals and offers a website, Python API, and AI-agent interface for formalization and theorem-proving workflows.","discovery_kind":"new_application","skeptic_critique":{"model":"deepseek-v4-flash","headline":"The LLM-judged evaluation bundles AI-generated informal descriptions into result cards, so the reported win rates may reflect summary quality rather than retrieval quality.","rationale":"LeanExplore is a real, usable system: the StatementGroup abstraction, dependency-graph enrichment, PageRank, BM25+ blending, MCP server, and downloadable database are concrete contributions, and the Appendix A worked example shows the hybrid scoring behaves as described. The central performance claim, however, rests entirely on the LLM-judged comparison in Section 6. The Reader's weakest assumption correctly identifies the core problem, and the paper itself confirms part of it when it says Moogle's scores may have been hurt by missing natural-language statements. That admission shows the evaluator is sensitive to the presence of informal descriptions, which means LeanExplore's always-present Gemini-generated summaries are a direct confound. A stripped-description ablation is the minimal experiment that would separate 'better retrieval' from 'better card text.' Without it, the headline win rate is ambiguous, so the conditional verdict remains appropriate: accept the systems contribution, but do not treat the retrieval improvement as established until the evaluation isolates it from display artifacts.","tokens_in":14988,"tokens_out":3830,"duration_ms":35869,"concrete_test":"Re-run the Section 6 experiment on the same 300 queries with the Informal description field removed (or set to 'N/A') for every engine's result cards, keeping the code and docstring fields unchanged, and average over the same three ranking runs. If LeanExplore's 1st-place rate in Table 1 falls from 55.4% toward LeanSearch's 46.3%, the original gap is attributable to the AI-generated informal descriptions rather than to hybrid retrieval ranking; if the margin persists, the concern is resolved.","verdict_should_be":"UNCHANGED","load_bearing_attack":"Section 6's evaluation presents each engine's top-5 results 'including the formal Lean code, docstring, and any provided informal statement' to Gemini 2.5 Flash, and the prompt in Appendix B explicitly includes an 'Informal description' field for every result. For LeanExplore, that field is always populated by translations generated by Gemini 2.0 Flash (Section 3.3); for Moogle it is often absent, and the paper itself notes this 'may have impacted' Moogle's performance. The evaluator is therefore not forced to judge which declarations are most relevant; it can (and likely does) prefer whichever result card reads most fluently. Since LeanExplore's cards are enriched with same-family LLM summaries, the 55.4% vs 46.3% 1st-place margin may measure the summaries, not the hybrid ranking. That is exactly the paper's central claim, so the evaluation does not currently isolate retrieval quality from display artifacts. The AI-generated query set (Appendix C) and same-model-family judge compound the risk, but the decisive confound is the bundled informal descriptions.","agreement_with_reader":"agree"},"referee_report":{"model":"deepseek-v4-flash","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.","tokens_in":15181,"tokens_out":2817,"duration_ms":29046,"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":[{"comment":"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.","section":"Section 6 and Appendix B"},{"comment":"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.","section":"Section 6, Appendix C"},{"comment":"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.","section":"Section 3.4"},{"comment":"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.","section":"Tables 1 and 2"}],"minor_comments":[{"comment":"The phrase 'Such an setup' should be 'Such a setup'.","section":"Section 5.2"},{"comment":"The reference for Wu et al. contains a typo: 'Meteja Jammik' should be 'Mateja Jamnik'.","section":"References"},{"comment":"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.","section":"Figure 1"},{"comment":"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.","section":"Appendix A"},{"comment":"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.","section":"Section 6"}],"recommendation":"major_revision","confidential_remarks":"The paper is a useful systems contribution and the artifacts are genuinely valuable, but the evaluation confound is central to the main claim. I would support publication after the authors provide a retrieval-only comparison that removes or controls for the AI-generated informal descriptions, plus sensitivity and robustness checks. The scope is appropriate for a venue that accepts tool/system papers, though the current evidence is not yet sufficient for the claimed 'significant improvement'."},"author_rebuttal":null,"desk_editor":{"model":"deepseek-v4-flash","letter":"LeanExplore is a genuine, working system and the paper is worth reading for the architecture, but the comparative evaluation doesn't prove the hybrid ranking beats the alternatives. The StatementGroup abstraction, the dependency-aware LLM translation pipeline, the multi-source embedding approach, and the MCP server are all genuinely new in this combination. The artifact itself ships: website, Python API, downloadable database, and the paper documents the pipeline well enough to reproduce. That is real, citable work.\n\nThe soft spot is Section 6. The evaluator sees result cards that include informal descriptions. For LeanExplore those descriptions are always present, generated by Gemini 2.0 Flash; for Moogle they are often missing, and the paper admits this may have hurt Moogle. The judge is Gemini 2.5 Flash, from the same model family. So the reported 55.4% vs 46.3% first-place rate could measure the quality of the AI-written summaries rather than the retrieval ranking. The queries are also AI-generated, and there are no human labels or raw result sets. The central claim – that the hybrid ranking improves declaration retrieval – is not isolated from these confounds. That is a real gap, not a nitpick.\n\nThat said, the paper is honest about its limitations (the Moogle issue, the weak performance on very general queries), and the system is coherent. The evaluation should be seen as indicative, not conclusive. A serious referee would ask for either a human evaluation or an ablation that strips informal descriptions from all result cards before judging. The paper deserves that round of review; it is not a desk reject.\n\nWho gets value: anyone building semantic search for Lean, and people working on retrieval for formal mathematics. I would cite it for the architecture, not for the evaluation numbers.","headline":"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.","tokens_in":15693,"tokens_out":2614,"would_cite":true,"duration_ms":24379,"reading_group":"maybe","serious_thinker":"yes","would_accept_peer_review":true},"rs_alignment":null,"lean_confirmation":null,"pith_extraction":{"msc":[],"pacs":[],"model":"deepseek-v4-flash","headline":"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%.","keywords":["Lean 4","theorem proving","semantic search","hybrid ranking","StatementGroup","BM25+","PageRank","model context protocol"],"falsifier":"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.","tokens_in":14762,"feed_emoji":"🔍","tokens_out":8076,"duration_ms":71596,"temperature":0.7,"pith_summary":"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.","feed_headline":"Hybrid search engine finds Lean 4 theorems from plain English","feed_subtitle":"Meaning, keywords, and code importance beat existing Lean search tools in an AI-judged contest.","key_machinery":"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.","core_discovery":"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.","pith_inferences":["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."],"forward_implications":["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."],"supporting_citations":[{"why":"Defines LeanSearch, the primary baseline whose win rate and large embedding model the evaluation must beat.","marker":"Gao et al., 2024"},{"why":"Supplies Moogle, the second comparison engine in the 300-query evaluation.","marker":"Morph Labs"},{"why":"Provides the bge-base-en-v1.5 model used to embed all declaration facets and user queries.","marker":"Beijing Academy of Artificial Intelligence (BAAI), 2023"},{"why":"Defines BM25+, the lexical relevance signal in the hybrid ranking.","marker":"Lv and Zhai, 2011"},{"why":"Defines PageRank, the structural importance signal computed over the declaration dependency graph.","marker":"Page et al., 1998"},{"why":"Supplies FAISS, the approximate nearest-neighbor index used for embedding retrieval.","marker":"Johnson et al., 2017"},{"why":"Provides the file-level data-extraction approach adapted for fine-grained AST and dependency analysis.","marker":"Yang et al., 2023"},{"why":"Defines Lean 4, the language and ecosystem the search engine targets.","marker":"de Moura and Ullrich, 2021"}],"fun_headline_variants":["LeanExplore blends meaning, keywords, and PageRank for Lean 4 search","Hybrid ranking: semantic, lexical, and importance scores for Lean 4","Search Lean 4 code by meaning, keywords, and importance","LeanExplore tops AI-judged comparison of Lean 4 search engines"],"cache_read_input_tokens":3200,"weakest_assumption_plain":"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.","fun_headline_variants_meta":{"raw":{"variants":["LeanExplore blends meaning, keywords, and PageRank for Lean 4 search","Hybrid ranking: semantic, lexical, and importance scores for Lean 4","Search Lean 4 code by meaning, keywords, and importance","LeanExplore tops AI-judged comparison of Lean 4 search engines"]},"model":"deepseek-v4-flash","effort":"low","cost_usd":0.001449,"raw_usage":{"total_tokens":5838,"prompt_tokens":951,"completion_tokens":4887,"prompt_tokens_details":{"cached_tokens":384},"prompt_cache_hit_tokens":384,"prompt_cache_miss_tokens":567,"completion_tokens_details":{"reasoning_tokens":4818}},"tokens_in":567,"tokens_out":4887,"duration_ms":34387,"temperature":1.0,"reasoning_tokens":4818,"cache_read_input_tokens":384,"cache_creation_input_tokens":0},"cache_creation_input_tokens":0},"created_at":"2026-08-07T10:46:39.457104+00:00","model_set":{"reader":"deepseek-v4-flash"},"falsifier":"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.","supporting_citations":[],"review_version":1}