A Semantic Search Engine for Mathlib4 (2024)

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 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.

## methodology in this section, we will describe the implementation of our semantic search engine for mathlib4 7 . this engine is designed to accept a user query in natural language and return a list of relevant theorems in mathlib4. our approach involves converting formal theorems from mathlib4 into their informal counterparts, as illustrated in figure 1 . these informalformal theorem pairs are then vectorized and stored in a vector database, a step that can be executed offline. when a user query is submitted, we augment the query to better grasp its context, vectorize the enriched query, and locate the corresponding theorems in the embedding space. in the following subsections, we will elaborate on the informalization of mathlib4, the design of the search engine, and the method of query augmentation. ## mathlibsemantic search benchmark to rigorously assess and compare the efficacy of various retrieval methods, we have established the mathlib4 semantic search benchmark. this benchmark encompasses a curated set of queries, relevance labels of each mathlib4 theorem for these queries, and a collection of performance metrics. in this section, we provide a detailed explanation of the benchmark. section 4.1 describes the composition of the query set. in section 4.2, we explain the relevance criteria for our benchmark and the labeling procedure. section 4.3 lists the performance metrics used in our benchmark. ## experiments in this section, we evaluate the performance of various theorem retrieval methods using our benchmark. the experimental setup is detailed in section 5.1. we compare the performances of different retrieval methods in section 5.2. additionally, the ablation study on document preparations and query augmentations is presented in section 5.3. ## conclusion in this paper, we introduce a semantic search engine designed to enable users to locate theorems in mathlib4 using informal queries. specifically, we translate the formal statements of mathlib4 theorems into informal versions and develop our search engine to work with a corpus of informal-formal theorem pairs. additionally, we construct a dataset to facilitate evaluation. our comprehensive experiments on this dataset reveal that the best theorem retrieval performance is attained by augmenting the user's query appropriately and embedding the content of the corpus simultaneously. consequently, our system employs a strategy that first augments the query, followed by a semantic search, thereby precisely aligning with the users' search intentions. our future research will focus on three primary directions. first, in terms of informalizing math-lib4, we aim to design guidelines for translation and provide examples of converting mathlib4 statements to informal language for llms, enhancing the informal corpus's quality. second, regarding the mathlib4 semantic search benchmark, we plan to continually enlarge the query set, aiming for a more comprehensive benchmark. lastly, for the semantic search engine itself, we intend to fine-tune a text embedding model on the task of theorem retrieval, aiming to improve the search engine's performance.