REVIEW 11 cited by
LeanExplore: A search engine for Lean 4 declarations
Not yet reviewed by Pith; the record is open.
This paper has not been read by Pith yet. Machine review is queued; the pith claim, tier, and objections will appear here once it completes.
SPECIMEN: schema-true, not a live event
T0 review · schema-true
One-sentence machine reading of the paper's core claim.
pith:XXXXXXXX · record.json · timestamp
LeanExplore: A search engine for Lean 4 declarations
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
Forward citations
Cited by 11 Pith papers
-
MechMath Agent Team: LLM Driven Agents for Mathematical Research
A decoupled multi-agent LLM system (Harness + KB/NL/FL provers) co-piloted solutions to 11 open math problems, some with Lean formalization.
-
LAMP: Lean-based Agentic framework with MCP and Proof Repair
LAMP achieves 96.7% success generating verified Lean proofs for 90 Combinatorics on Words theorems by coordinating Planner, Builder, and Verifier agents with a CoW ontology accessed through Model Context Protocol.
-
Does My Embedding Reflect That $A = B$? Evaluating Mathematical Equivalence in Embedding Models
Current embedding models fail to capture mathematical equivalence across lexical variants, but contrastive alignment of informal and formal statements improves retrieval on both equivalence and formalization tasks.
-
LeanSearch v2: Global Premise Retrieval for Lean 4 Theorem Proving
LeanSearch v2 recovers 46.1% of ground-truth premise groups on research-level Mathlib theorems and raises fixed-loop proof success from 4% to 20% via embedding-reranker plus iterative sketch-retrieve-reflect retrieval.
-
LeanSearch v2: Global Premise Retrieval for Lean 4 Theorem Proving
LeanSearch v2 recovers 46.1% of ground-truth premise groups for research-level Lean 4 theorems within 10 candidates and raises fixed-loop proof success to 20%.
-
Matlas: A Semantic Search Engine for Mathematics
Matlas introduces a semantic retrieval system over 8.07 million mathematical statements from papers and textbooks, using dependency graphs and topological unfolding for self-contained search via natural language queries.
-
Does My Embedding Reflect That $A = B$? Evaluating Mathematical Equivalence in Embedding Models
Embedding models fail to capture mathematical equivalence due to lexical bias, but contrastive training on informal-formal pairs improves performance on MELD and retrieval tasks.
-
OpenProver: Agentic and Interactive Theorem Proving with Lean 4
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.
-
Beyond Benchmarks: MathArena as an Evaluation Platform for Mathematics with LLMs
MathArena is broadened into a maintained platform with new benchmarks for proofs, research questions, and formal verification, where GPT-5.5 scores 98% on 2026 USAMO and 74% on research-level tasks.
-
Beyond Benchmarks: MathArena as an Evaluation Platform for Mathematics with LLMs
MathArena is a maintained platform evaluating LLMs across olympiad problems, proofs, research questions, and formal proofs, with GPT-5.5 reaching 98% on 2026 USAMO and 74% on research-level tasks.
-
AI for Mathematics: Progress, Challenges, and Prospects
AI for math combines task-specific architectures and general foundation models to support research and advance AI reasoning capabilities.
discussion (0)
Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.