  The heterogeneous nature of the logical foundations used in different
interactive proof assistant libraries has rendered discovery of similar
mathematical concepts among them difficult. In this paper, we compare a
previously proposed algorithm for matching concepts across libraries with our
unsupervised embedding approach that can help us retrieve similar concepts. Our
approach is based on the fasttext implementation of Word2Vec, on top of which a
tree traversal module is added to adapt its algorithm to the representation
format of our data export pipeline. We compare the explainability,
customizability, and online-servability of the approaches and argue that the
neural embedding approach has more potential to be integrated into an
interactive proof assistant.
