LeanExplore: A search engine for Lean 4 declarations

• URL: http://arxiv.org/abs/2506.11085v1
• Date: Wed, 04 Jun 2025 16:09:54 GMT
• Title: LeanExplore: A search engine for Lean 4 declarations
• Abstract summary: This paper introduces LeanExplore, a search engine for Lean 4 declarations.<n>LeanExplore enables users to semantically search for statements across select Lean 4 packages.
• Score: 0.0
• License: http://creativecommons.org/licenses/by/4.0/
• 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

Related papers

• ORBIT: Scalable and Verifiable Data Generation for Search Agents on a Tight Budget [56.6320292944541]
  ORBIT is a training dataset with 20K reasoning-intensive queries with short verifiable answers.<n>Our framework, code and datasets are open-sourced and available publicly.
  arXiv  Detail & Related papers  (2026-04-01T17:42:41Z)
• LEAPS: An LLM-Empowered Adaptive Plugin for Taobao AI Search [17.074638179635613]
  We propose LEAPS (LLM-Empowered Adaptive for Taobao AI Search), which seamlessly upgrades traditional search systems via a "Broaden-and-Empower" paradigm.<n>It employs a novel three-stage training strategy--inverse data augmentation, posterior-knowledge supervised fine-tuning, and diversity-aware reinforcement learning--to generate adaptive and complementary query combinations.<n>Fully deployed on Taobao AI Search since August 2025, LEAPS currently serves hundreds of millions of users monthly.
  arXiv  Detail & Related papers  (2026-01-09T03:41:27Z)
• Lean Finder: Semantic Search for Mathlib That Understands User Intents [19.454158593716578]
  Lean Finder is a semantic search engine for Lean and mathlib.<n>It understands and aligns with the intents of mathematicians.<n>It is compatible with LLM-based theorem provers, bridging retrieval with formal reasoning.
  arXiv  Detail & Related papers  (2025-10-08T19:51:49Z)
• Reasoning-enhanced Query Understanding through Decomposition and Interpretation [87.56450566014625]
  ReDI is a Reasoning-enhanced approach for query understanding through Decomposition and Interpretation.<n>We compiled a large-scale dataset of real-world complex queries from a major search engine.<n> Experiments on BRIGHT and BEIR demonstrate that ReDI consistently surpasses strong baselines in both sparse and dense retrieval paradigms.
  arXiv  Detail & Related papers  (2025-09-08T10:58:42Z)
• LESER: Learning to Expand via Search Engine-feedback Reinforcement in e-Commerce [6.294743632371883]
  User queries in e-commerce search are often vague, short, and underspecified.<n>Existing methods, including neural query expansion and prompting-based LLM approaches, fall short in real-world settings.<n>We propose Learning to Expand via Search Engine Reinforcement (LESER), a novel framework that fine-tunes a context-aware LLM using real-time search engine feedback.
  arXiv  Detail & Related papers  (2025-09-06T02:54:13Z)
• Context-Aware Scientific Knowledge Extraction on Linked Open Data using Large Language Models [0.0]
  This paper introduces WISE (Workflow for Intelligent Scientific Knowledge Extraction), a system to extract, refine, and rank query-specific knowledge.<n>WISE delivers detailed, organized answers by systematically exploring and synthesizing knowledge from diverse sources.
  arXiv  Detail & Related papers  (2025-06-21T04:22:34Z)
• Iterative Self-Incentivization Empowers Large Language Models as Agentic Searchers [74.17516978246152]
  Large language models (LLMs) have been widely integrated into information retrieval to advance traditional techniques.<n>We propose EXSEARCH, an agentic search framework, where the LLM learns to retrieve useful information as the reasoning unfolds.<n>Experiments on four knowledge-intensive benchmarks show that EXSEARCH substantially outperforms baselines.
  arXiv  Detail & Related papers  (2025-05-26T15:27:55Z)
• ManuSearch: Democratizing Deep Search in Large Language Models with a Transparent and Open Multi-Agent Framework [73.91207117772291]
  ManuSearch is a transparent and modular multi-agent framework designed to democratize deep search for large language models (LLMs)<n>ManuSearch decomposes the search and reasoning process into three collaborative agents: (1) a solution planning agent that iteratively formulates sub-queries, (2) an Internet search agent that retrieves relevant documents via real-time web search, and (3) a structured webpage reading agent that extracts key evidence from raw web content.
  arXiv  Detail & Related papers  (2025-05-23T17:02:02Z)
• Focus, Merge, Rank: Improved Question Answering Based on Semi-structured Knowledge Bases [2.6524539020042663]
  We present FocusedRetriever, a modular SKB-based framework for multi-hop question answering.<n>It integrates components (VSS-based entity search, LLM-based generation of Cypher queries and pairwise re-ranking) in a way that enables it to outperform state-of-the-art methods.<n>The average first-hit rate exceeds that of the second-best method by 25.7%.
  arXiv  Detail & Related papers  (2025-05-14T09:35:56Z)
• LLM4PR: Improving Post-Ranking in Search Engine with Large Language Models [9.566432486156335]
  Large Language Models for Post-Ranking in search engine (LLM4PR) We introduce a novel paradigm named Large Language Models for Post-Ranking in search engine (LLM4PR)
  arXiv  Detail & Related papers  (2024-11-02T08:36:16Z)
• Harnessing the Power of Semi-Structured Knowledge and LLMs with Triplet-Based Prefiltering for Question Answering [2.6524539020042663]
  Large Language Models (LLMs) frequently lack domain-specific knowledge and even fine-tuned models tend to hallucinate. We present a pipeline, 4StepFocus, and specifically a preprocessing step, that can substantially improve the answers of LLMs. The method narrows down potentially correct answers by triplets-based searches in a semi-structured knowledge base in a direct, traceable fashion.
  arXiv  Detail & Related papers  (2024-09-01T22:43:27Z)
• When Search Engine Services meet Large Language Models: Visions and Challenges [53.32948540004658]
  This paper conducts an in-depth examination of how integrating Large Language Models with search engines can mutually benefit both technologies. We focus on two main areas: using search engines to improve LLMs (Search4LLM) and enhancing search engine functions using LLMs (LLM4Search)
  arXiv  Detail & Related papers  (2024-06-28T03:52:13Z)
• TaxoLLaMA: WordNet-based Model for Solving Multiple Lexical Semantic Tasks [54.01153045234468]
  In this paper, we explore the capabilities of LLMs in capturing lexical-semantic knowledge from WordNet. We present TaxoLLaMA, the everything-in-one model, lightweight due to 4-bit quantization and LoRA.
  arXiv  Detail & Related papers  (2024-03-14T09:21:25Z)
• Crafting Knowledge: Exploring the Creative Mechanisms of Chat-Based Search Engines [3.5845457075304368]
  This research aims to dissect the mechanisms through which an LLM-powered search engine, specifically Bing Chat, selects information sources for its responses. Bing Chat exhibits a preference for content that is not only readable and formally structured, but also demonstrates lower perplexity levels. Our investigation documents a greater similarity among websites cited by RAG technologies compared to those ranked highest by conventional search engines.
  arXiv  Detail & Related papers  (2024-02-29T18:20:37Z)
• UFO: a Unified and Flexible Framework for Evaluating Factuality of Large Language Models [73.73303148524398]
  Large language models (LLMs) may generate text that lacks consistency with human knowledge, leading to factual inaccuracies or textithallucination. We propose textttUFO, an LLM-based unified and flexible evaluation framework to verify facts against plug-and-play fact sources.
  arXiv  Detail & Related papers  (2024-02-22T16:45:32Z)
• DIVKNOWQA: Assessing the Reasoning Ability of LLMs via Open-Domain Question Answering over Knowledge Base and Text [73.68051228972024]
  Large Language Models (LLMs) have exhibited impressive generation capabilities, but they suffer from hallucinations when relying on their internal knowledge. Retrieval-augmented LLMs have emerged as a potential solution to ground LLMs in external knowledge.
  arXiv  Detail & Related papers  (2023-10-31T04:37:57Z)
• Using an LLM to Help With Code Understanding [13.53616539787915]
  Large language models (LLMs) are revolutionizing the process of writing code. Our plugin queries OpenAI's GPT-3.5-turbo model with four high-level requests without the user having to write explicit prompts. We evaluate this system in a user study with 32 participants, which confirms that using our plugin can aid task completion more than web search.
  arXiv  Detail & Related papers  (2023-07-17T00:49:06Z)
• Synergistic Interplay between Search and Large Language Models for Information Retrieval [141.18083677333848]
  InteR allows RMs to expand knowledge in queries using LLM-generated knowledge collections. InteR achieves overall superior zero-shot retrieval performance compared to state-of-the-art methods.
  arXiv  Detail & Related papers  (2023-05-12T11:58:15Z)

This list is automatically generated from the titles and abstracts of the papers in this site.

This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.