arxiv.org/abs/2403.13310 提出了语义搜索引擎 leansearch.net，可以接受自然语言查询，并在mathlib4中找到相关定理。该论文还建立了一个用于评估搜索引擎性能的基准。论文作者还提供了开源代码和数据集。
相关研究包括《A Comparison of Semantic Search Approaches for Mathematical Libraries》和《DeepMath - Deep Sequence Models for Premise Selection》
