A Semantic Search Engine for Mathlib4
Guoxiong Gao Haocheng Ju Jiedong Jiang Zihan Qin Bin Dong
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.