A Semantic Search Engine for Mathlib4

这篇文章介绍了一个针对数学库mathlib4的语义搜索引擎，它能够接受非正式的查询并找到相关的定理。数学库mathlib4是交互式定理证明器Lean生态系统的核心，它为各种数学理论的形式化奠定了基础，被一个不断扩大的社区所支持。然而，在mathlib4中查找定理可能具有挑战性。为了成功地在mathlib4中搜索，用户通常需要熟悉其命名约定或文档字符串。因此，创建一个语义搜索引擎，可以轻松地被具有不同熟悉程度的mathlib4用户使用，非常重要。此外，本文还建立了一个基准，用于评估各种mathlib4搜索引擎的性能。

创建一个语义搜索引擎，帮助用户更轻松地在mathlib4中搜索定理。

使用自然语言查询，通过语义匹配算法在mathlib4中寻找相关定理。

该论文提出了一种基于语义匹配算法的语义搜索引擎，可以接受自然语言查询，并在mathlib4中找到相关定理。实验结果表明，该搜索引擎的性能优于其他搜索引擎。该论文还建立了一个用于评估搜索引擎性能的基准。论文作者还提供了开源代码和数据集。

在相关研究方面，最近的一些研究包括《A Comparison of Semantic Search Approaches for Mathematical Libraries》和《DeepMath - Deep Sequence Models for Premise Selection》等。