A Semantic Search Engine for Mathlib4

1 Introduction

• Lean verifies formal mathematical proofs, while mathlib4 provides a collaboratively maintained library for formalizing new theories.Reusing established mathlib4 theorems can avoid repeatedly formalizing known results.Source: §1 · p. 1
• Existing mathlib4 search relies on formal names, documentation, or keyword matches, which can miss semantically similar informal queries.Beginners may not know naming conventions, documentation strings are incomplete, and exact lexical matching can fail.Source: §1 · p. 1
• Neither current search method adequately supports informal theorem discovery, motivating a semantic engine to improve retrieval efficiency.The need for such a system has also been highlighted in Zulip discussions.Source: §1 · p. 1
• The paper introduces a search engine that translates formal theorems into informal-formal pairs, augments queries, and searches the resulting database semantically.It also establishes a benchmark for comparing mathlib4 search engines.Source: §1 · pp. 1–2

Text Retrieval

• Classical text retrieval methods measure lexical similarity, while dense neural retrievers encode queries and documents to assess semantic similarity.Cross-encoders jointly process query-document pairs, whereas bi-encoders encode them separately.Source: §2 · p. 2
• Retrieval research has developed pre-training and fine-tuning paradigms for dense retrievers, including contrastive learning and direct decoder-only model fine-tuning.Wang et al. (2024) report competitive results without a necessary two-stage training process.Source: §2 · p. 2

Mathematical Information Retrieval

• Mathematical information retrieval represents formulas structurally or with dense retrievers, often combining formula matching with contextual semantic search.Approach0 hybrid search combines structural search with a ColBERT bi-encoder.Source: §2 · pp. 2–3
• Unlike prior MIR work on natural-language corpora containing formulas, this paper searches formal mathlib4 and compares against Moogle, whose technical details are unreleased.The comparison is presented in Section 5.Source: §2 · p. 3

3 Methodology

• The system stores vectorized informal-formal theorem pairs and retrieves relevant theorems by embedding-space similarity after query augmentation.Corpus embedding is performed offline, while query vectorization and retrieval occur at search time.Source: §3 · p. 3, §3.2 · p. 4

3.1 Informalizing Mathlib4

• Informalization supplies an LLM with theorem names, statements, documentation strings, and linked definitions to generate informal names and statements.The resulting records use the format "theorem name: informal statement"; missing documentation strings are handled by using the theorem name and statement.Source: §3.1 · p. 3, Figure 2 · p. 4
• Providing related definitions and documentation strings is presented as an improvement over informalization based only on formal statements, as in Jiang et al. (2023).The paper argues that the added context helps the LLM interpret and convert formal theorems more accurately.Source: §3.1 · p. 3

3.2 Semantic Search Engine for Mathlib4

• Dense embedding models encode the corpus with task-specific instructions, and Chroma DB uses cosine distance with HNSW approximate nearest-neighbor search for retrieval.The paper investigates instruction effects on retrieval performance in Appendix D.Source: §3.2 · pp. 3–4

3.3 Query Augmentation

• Query augmentation transforms brief or vague inputs into detailed, mathematically equivalent formal and informal statements before embedding them in the database format.The process emphasizes precision, mathematical notation, and clarification of ambiguous inputs, while acknowledging occasional Lean-code inaccuracies.Source: §3.3 · pp. 4–5

4 Mathlib4 Semantic Search Benchmark

• The benchmark combines curated queries, theorem relevance labels, and performance metrics to rigorously compare mathlib4 retrieval methods.Source: §4 · p. 5

4.1 Composition of the Query Set

• The 50-query set spans calculus, algebra, number theory, set theory, and mathematical logic, with queries organized into 18 groups sharing search intent.Groups include multiple representations where possible, including natural-language descriptions, LaTeX formulas, theorem names, and Lean 4 term descriptions.Source: §4.1 · p. 5

4.2 Relevance Judgments

• Relevance judgments prioritize whether retrieved theorems support Lean 4 formalization workflows rather than merely sharing topics, formats, or formula structures.Source: §4.2 · p. 5
• Assessors label the top 50 results for each query group and add omitted relevant theorems by inspecting files containing exact matches.The benchmark assumes related theorems are often colocated in files, that omitted items are irrelevant, and that every query has at least one exact match.Source: §4.2 · p. 5

4.3 Performance Measures

• The benchmark reports P@10 and R@10 for retrieval effectiveness and nDCG@k for retrieval plus ranking quality across the full query set and each category.Precision counts relevant results among the top k, recall measures retrieved exact matches, and nDCG applies position-dependent decaying weights.Source: §4.3 · p. 6

5.1 Experiment Setup

• The benchmark compares BM25, Moogle, and four embedding models on formal, informal, and augmented retrieval configurations.The embedding models are evaluated with original formal corpora and with formal–informal corpus and query augmentation.Source: §5.1 · p. 6, Table 3 · p. 7

5.2 Main Results

• E5mistral-7b with the retrieval pipeline achieves the best performance across three overall metrics, outperforming other methods and its formal-corpus unaugmented variant.All retrieval methods benefit from augmented corpora and queries.Source: §5.2 · p. 6, Table 3 · p. 7
• E5mistral-7b performs best in nearly every query category except nDCG@20 for Lean 4 Terms, where informal information can hurt lexical retrieval.Query augmentation substantially improves Theorem Name retrieval by expanding theorem statements and providing richer context.Source: §5.2 · pp. 6–7, Table 4 · p. 7

5.3.1 Ablation of Document Preparations

• Incomplete formal or informal corpora lower overall scores, while a combined formal + informal corpus improves Lean 4 Terms and Natural Description retrieval.For Theorem Name queries, E5mistral-7b benefits from unfolded mathematical descriptions in the informalized statements, whereas lexical Lean 4 Term retrieval can favor the formal corpus.Source: §5.3.1 · p. 7, Table 5 · p. 8
• Across query groups, the formal + informal corpus usually avoids the abrupt performance declines seen with solely formal or informal corpora.Informalized statements reduce lexical mismatch between queries and formal theorem statements.Source: §5.3.1 · p. 7, Figure 4 · p. 7

5.3.2 Ablation of Query Augmentations

• Query augmentation improves all compared methods and especially helps identify Theorem Names by expanding terms and adding context.E5mistral-7b performs comparably without augmentation on the formal + informal corpus, making that configuration a cost-effective deployment option.Source: §5.3.2 · p. 8, Table 6 · p. 8

6 Conclusion

• The system translates formal mathlib4 statements into informal versions, searches paired informal–formal theorem data, and is evaluated with a purpose-built dataset.It is designed to help users locate theorems through informal queries.Source: §6 · p. 8
• The best retrieval performance comes from augmenting user queries and embedding the corpus, so the system augments queries before semantic search.This sequence is intended to align retrieval with users’ search intentions.Source: §6 · p. 8
• Future work will improve informalization guidelines, expand the benchmark query set, and fine-tune an embedding model for theorem retrieval.These directions address informal-corpus quality, benchmark coverage, and search-engine performance.Source: §6 · p. 8

• Hyperlink-based dependency extraction can be inaccurate and may omit certain theorem dependencies.The paper notes that interacting with Lean’s language server would provide a more precise extraction method.Source: §7 · p. 8
• E5mistral-7b may challenge deployment on resource-constrained devices such as laptops.Future work targets improving smaller embedding models for theorem retrieval to broaden accessibility.Source: §7 · p. 8

A Example of Informalized Mathlib4 Statements

• The contextualized informal statement preserves the theorem’s equivalence while explicitly explaining its decidability and conditional branches.It states that the expression equals c exactly when either branch has a proof yielding c.Source: A Example of Informalized Mathlib4… · p. 11
• Additional context translates the mathlib4 notation “dite” into the more accessible phrase “dependent if-then-else.”The approach extracts the definition and documentation string of “dite” for inclusion in the prompt.Source: A Example of Informalized Mathlib4… · p. 11

B Prompt for Query Augmentation

• Query augmentation emphasizes precise information, LaTeX for mathematical expressions, and clarification of ambiguous inputs.The section also provides examples to explain the augmentation task.Source: B Prompt for Query Augmentation · p. 11

C Implementation Details

• E5mistral-7b uses different document and query instructions without augmentation, but the same instructions for both with query augmentation.The implementation modifies the original document-side omission to use two-sided prompts for theorem retrieval.Source: C Implementation Details · p. 11
• Inputs exceeding 4096 characters were truncated because of GPU memory limitations.Corpus embedding for all tested models finished within three hours on one Nvidia V100 GPU with 16GB memory.Source: C Implementation Details · p. 11
• Figure 5 presents the prompt used for query augmentations.Source: Figure 5 · p. 12
• Table 7 defines “None & Formal” as the baseline and “F+IF & F+IF” as the method setting for E5mistral-7b.Here, “aug.” denotes augmentation, while F and IF denote formal and informal inputs.Source: Table 7 · p. 12

D Ablation Study on Task Instructions

• The four embedding engines are evaluated by visualizing embeddings for 50 benchmark queries with t-SNE.E5mistral-7b is tested with empty, mathematics-retrieval, and Lean 4 retrieval instructions.Source: D Ablation Study on Task Instructions · p. 12
• Mathematics-aware task instructions remove theorem-name clusters for E5mistral-7b, indicating better grouping by query intent.The study assumes queries sharing a color represent the same search intent and should therefore be proximal.Source: D Ablation Study on Task Instructions · p. 12
• text-embedding-3-large and E5mistral-7b show superior performance in discerning mathematical search intentions relative to the other compared subfigures.This visual comparison is reported as aligning with the paper’s main results in Table 3.Source: D Ablation Study on Task Instructions · p. 12
• The absence of theorem clusters suggests that embeddings associate theorem names with corresponding statements despite differences in appearance and structure.The paper concludes that appropriate task instructions improve sensitivity to mathematical search intents and retrieval effectiveness.Source: D Ablation Study on Task Instructions · p. 12

E Models for Query Augmentation

• The evaluation compares DeepSeek-V2-Chat and GPT-4 using the informal+formal corpus setting.Table 8 reports performance averaged over 10 runs.Source: E Models for Query Augmentation · p. 12, Table 8 · p. 13
• DeepSeek-V2-Chat outperforms GPT-4 in effectiveness while offering significantly lower cost for query augmentation.The comparison uses the informal+formal corpus setting and results averaged over 10 runs.Source: E Models for Query Augmentation · p. 12
• The results identify DeepSeek-V2-Chat as a more efficient and cost-effective choice for query augmentation tasks.Source: E Models for Query Augmentation · pp. 12–13