# Online Machine Learning Techniques for Coq: A Comparison

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

## Key facts

- Cited by 7 papers in the map (data through 14 Oct 2026).
- Builds on 11 of its 28 references that are in the map.
- First posted on arXiv 12 Apr 2021.

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

- [XGBoost: A Scalable Tree Boosting System](https://mlsanity.com/paper/1603.02754/) (2016)
- [Reinforcement Learning of Theorem Proving](https://mlsanity.com/paper/1805.07563/) (2018)
- [TacticToe: Learning to Prove with Tactics](https://mlsanity.com/paper/1804.00596/) (2018)
- [ENIGMA-NG: Efficient Neural and Gradient-Boosted Inference Guidance for E](https://mlsanity.com/paper/1903.03182/) (2019)
- [The Tactician (extended version): A Seamless, Interactive Tactic Learner and Prover for Coq](https://mlsanity.com/paper/2008.00120/) (2020)
- [Learning to Reason with HOL4 tactics](https://mlsanity.com/paper/1804.00595/) (2018)
- [ATPboost: Learning Premise Selection in Binary Setting with ATP Feedback](https://mlsanity.com/paper/1802.03375/) (2018)
- [Tactic Learning and Proving for the Coq Proof Assistant](https://mlsanity.com/paper/2003.09140/) (2020)
- [Premise Selection and External Provers for HOL4](https://mlsanity.com/paper/1509.03534/) (2015)
- [PaMpeR: Proof Method Recommendation System for Isabelle/HOL](https://mlsanity.com/paper/1806.07239/) (2018)
- [A Proof Strategy Language and Proof Script Generation for Isabelle/HOL](https://mlsanity.com/paper/1606.02941/) (2016)

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

- [PutnamBench: Evaluating Neural Theorem-Provers on the Putnam Mathematical Competition](https://mlsanity.com/paper/2407.11214/) (2024)
- [Proving Olympiad Inequalities by Synergizing LLMs and Symbolic Reasoning](https://mlsanity.com/paper/2502.13834/) (2025)
- [Graph2Tac: Online Representation Learning of Formal Math Concepts](https://mlsanity.com/paper/2401.02949/) (2024)
- [Machine-Learned Premise Selection for Lean](https://mlsanity.com/paper/2304.00994/) (2023)
- [Application of AI to formal methods - an analysis of current trends](https://mlsanity.com/paper/2411.14870/) (2024)
- [The Tactician's Web of Large-Scale Formal Knowledge](https://mlsanity.com/paper/2401.02950/) (2024)
- [Learning Rules Explaining Interactive Theorem Proving Tactic Prediction](https://mlsanity.com/paper/2411.01188/) (2024)

## Abstract (arXiv)

We present a comparison of several online machine learning techniques for tactical learning and proving in the Coq proof assistant. This work builds on top of Tactician, a plugin for Coq that learns from proofs written by the user to synthesize new proofs. Learning happens in an online manner, meaning that Tactician's machine learning model is updated immediately every time the user performs a step in an interactive proof. This has important advantages compared to the more studied offline learning systems: (1) it provides the user with a seamless, interactive experience with Tactician and, (2) it takes advantage of locality of proof similarity, which means that proofs similar to the current proof are likely to be found close by. We implement two online methods, namely approximate k-nearest neighbors based on locality sensitive hashing forests and random decision forests. Additionally, we conduct experiments with gradient boosted trees in an offline setting using XGBoost. We compare the relative performance of Tactician using these three learning methods on Coq's standard library.