Abstract
The heterogeneous nature of the logical foundations used in differentinteractive proof assistant libraries has rendered discovery of similarmathematical concepts among them difficult. In this paper, we compare apreviously proposed algorithm for matching concepts across libraries with ourunsupervised embedding approach that can help us retrieve similar concepts. Ourapproach is based on the fasttext implementation of Word2Vec, on top of which atree traversal module is added to adapt its algorithm to the representationformat of our data export pipeline. We compare the explainability,customizability, and online-servability of the approaches and argue that theneural embedding approach has more potential to be integrated into aninteractive proof assistant.