# JEFL: Joint Embedding of Formal Proof Libraries

arXiv: https://arxiv.org/abs/2107.10188 · HTML: https://mlsanity.com/paper/2107.10188/

## Key facts

- No citing papers in the map yet (data through 14 Oct 2026).
- Builds on 12 of its 37 references that are in the map.
- First posted on arXiv 21 Jul 2021.

## Builds on (most cited first, 12 of 12)

- [Efficient Estimation of Word Representations in Vector Space](https://mlsanity.com/paper/1301.3781/) (2013)
- [Distributed Representations of Words and Phrases and their Compositionality](https://mlsanity.com/paper/1310.4546/) (2013)
- [node2vec: Scalable Feature Learning for Networks](https://mlsanity.com/paper/1607.00653/) (2016)
- [Enriching Word Vectors with Subword Information](https://mlsanity.com/paper/1607.04606/) (2016)
- [DeepWalk: Online Learning of Social Representations](https://mlsanity.com/paper/1403.6652/) (2014)
- [Bag of Tricks for Efficient Text Classification](https://mlsanity.com/paper/1607.01759/) (2016)
- [HOL(y)Hammer: Online ATP Service for HOL Light](https://mlsanity.com/paper/1309.4962/) (2013)
- [Sharing HOL4 and HOL Light proof knowledge](https://mlsanity.com/paper/1509.03527/) (2015)
- [Lemma Mining over HOL Light](https://mlsanity.com/paper/1310.2797/) (2013)
- [The MMT API: A Generic MKM System](https://mlsanity.com/paper/1306.3199/) (2013)
- [Proof Pattern Search in Coq/SSReflect](https://mlsanity.com/paper/1402.0081/) (2014)
- [Matching concepts across HOL libraries](https://mlsanity.com/paper/1405.3906/) (2014)

## Abstract (arXiv)

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.