# Proof Recommendation System for the HOL4 Theorem Prover

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

## Key facts

- No citing papers in the map yet (data through 14 Oct 2026).
- Builds on 6 of its 13 references that are in the map.
- First posted on arXiv 31 Dec 2024.

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

- [Attention Is All You Need](https://mlsanity.com/paper/1706.03762/) (2017)
- [BERT: Pre-training of Deep Bidirectional Transformers for Language Understanding](https://mlsanity.com/paper/1810.04805/) (2018)
- [Exploring the Limits of Transfer Learning with a Unified Text-to-Text Transformer](https://mlsanity.com/paper/1910.10683/) (2019)
- [RoBERTa: A Robustly Optimized BERT Pretraining Approach](https://mlsanity.com/paper/1907.11692/) (2019)
- [Tactic Learning and Proving for the Coq Proof Assistant](https://mlsanity.com/paper/2003.09140/) (2020)
- [CoProver: A Recommender System for Proof Construction](https://mlsanity.com/paper/2304.10486/) (2023)

## Abstract (arXiv)

We introduce a proof recommender system for the HOL4 theorem prover. Our tool is built upon a transformer-based model [2] designed specifically to provide proof assistance in HOL4. The model is trained to discern theorem proving patterns from extensive libraries of HOL4 containing proofs of theorems. Consequently, it can accurately predict the next tactic(s) (proof step(s)) based on the history of previously employed tactics. The tool operates by reading a given sequence of tactics already used in a proof process (in our case, it contains at least three tactics), referred to as the current proof state, and provides recommendations for the next optimal proof step(s).