# Sharing HOL4 and HOL Light proof knowledge

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

## Key facts

- Cited by 4 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 11 Sep 2015.

## Built on by (most cited first, 4 of 4)

- [Proof Artifact Co-training for Theorem Proving with Language Models](https://mlsanity.com/paper/2102.06203/) (2021)
- [REFACTOR: Learning to Extract Theorems from Proofs](https://mlsanity.com/paper/2402.17032/) (2024)
- [BAIT: Benchmarking (Embedding) Architectures for Interactive Theorem-Proving](https://mlsanity.com/paper/2403.03401/) (2024)
- [JEFL: Joint Embedding of Formal Proof Libraries](https://mlsanity.com/paper/2107.10188/) (2021)

## Abstract (arXiv)

New proof assistant developments often involve concepts similar to already formalized ones. When proving their properties, a human can often take inspiration from the existing formalized proofs available in other provers or libraries. In this paper we propose and evaluate a number of methods, which strengthen proof automation by learning from proof libraries of different provers. Certain conjectures can be proved directly from the dependencies induced by similar proofs in the other library. Even if exact correspondences are not found, learning-reasoning systems can make use of the association between proved theorems and their characteristics to predict the relevant premises. Such external help can be further combined with internal advice. We evaluate the proposed knowledge-sharing methods by reproving the HOL Light and HOL4 standard libraries. The learning-reasoning system HOL(y)Hammer, whose single best strategy could automatically find proofs for 30% of the HOL Light problems, can prove 40% with the knowledge from HOL4.