A Semantic Search Engine for Mathlib4

TL;DR

This work addresses the challenge of searching mathlib4 with informal queries by building a semantic search engine that converts formal Lean 4 theorems into informal counterparts and indexes them alongside formal statements. The approach uses offline embeddings of informal-formal theorem pairs in a vector store (Chroma DB) with HNSW search, and enhances user queries through LLM-based augmentation to improve semantic matching. A benchmark of 50 queries organized into 18 intent groups evaluates retrieval performance using metrics such as precision and ranking quality, showing that embedding-based retrieval with query augmentation, particularly using the E5_mistral-7b model, yields the strongest overall results. The study also includes ablation analyses on document preparations and query augmentation, demonstrating the value of a combined formal+informal corpus and targeted prompting. Overall, the work offers a practical, scalable framework for Lean 4 theorem search that can accelerate formalization workflows and informs future improvements in informalization guidelines and embedding-based MIR for mathematics.

Abstract

The interactive theorem prover Lean enables the verification of formal mathematical proofs and is backed by an expanding community. Central to this ecosystem is its mathematical library, mathlib4, which lays the groundwork for the formalization of an expanding range of mathematical theories. However, searching for theorems in mathlib4 can be challenging. To successfully search in mathlib4, users often need to be familiar with its naming conventions or documentation strings. Therefore, creating a semantic search engine that can be used easily by individuals with varying familiarity with mathlib4 is very important. In this paper, we present a semantic search engine (https://leansearch.net/) for mathlib4 that accepts informal queries and finds the relevant theorems. We also establish a benchmark for assessing the performance of various search engines for mathlib4.

Figures (6)

• Figure 1: Overview of our method for creating a semantic search engine for mathlib4. We employ an informalizer to convert formal statements from mathlib4 into their informal counterparts. These informal-formal pairs are then stored in a vector database. When users input a query, the system augments the query and searches across the database, yielding a list of relevant theorems.
• Figure 2: Our approach to informalizing mathlib4 theorems. We extract the theorem name, statement, and documentation string from the mathlib4 documentation. Moreover, we collect related definitions via the hyperlinks in the theorem statements. The gathered information is then inputted into GPT-3.5 to generate informal names and statements. These are then organized in the format "theorem name: informal statement" and added to an informal corpus.
• Figure 3: Prompt for informalizing mathlib4 statements with documentation strings.
• Figure 4: nDCG@20 performance of $\text{E5}_{\text{mistral-7b}}$ across formal, informal and formal + informal corpus on our benchmark, averaged by query groups. These evaluations are conducted using non-augmented queries.
• Figure 5: Prompt for query augmentations.