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.

翻译：交互式定理证明器Lean支持正式数学证明的验证，并拥有不断发展的社区支持。该生态系统的核心是其数学库mathlib4，它为更广泛的数学理论形式化奠定了基础。然而，在mathlib4中搜索定理具有挑战性。为了在mathlib4中成功搜索，用户通常需要熟悉其命名约定或文档字符串。因此，创建一个能被不同熟悉程度的用户轻松使用的语义搜索引擎非常重要。本文提出了一个面向mathlib4的语义搜索引擎，它接受非正式的查询并找到相关定理。我们还建立了一个基准测试，用于评估mathlib4多种搜索引擎的性能。