# HOList: An Environment for Machine Learning of Higher-Order Theorem Proving

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

## Key facts

- Cited by 19 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 5 Apr 2019.

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

- [Measuring Mathematical Problem Solving With the MATH Dataset](https://mlsanity.com/paper/2103.03874/) (2021)
- [Large Language Models for Mathematical Reasoning: Progresses and Challenges](https://mlsanity.com/paper/2402.00157/) (2024)
- [Proof Artifact Co-training for Theorem Proving with Language Models](https://mlsanity.com/paper/2102.06203/) (2021)
- [NaturalProofs: Mathematical Theorem Proving in Natural Language](https://mlsanity.com/paper/2104.01112/) (2021)
- [Learning to Guide a Saturation-Based Theorem Prover](https://mlsanity.com/paper/2106.03906/) (2021)
- [A Survey in Mathematical Language Processing](https://mlsanity.com/paper/2205.15231/) (2022)
- [Training a First-Order Theorem Prover from Synthetic Data](https://mlsanity.com/paper/2103.03798/) (2021)
- [An Ensemble Approach for Automated Theorem Proving Based on Efficient Name Invariant Graph Neural Representations](https://mlsanity.com/paper/2305.08676/) (2023)
- [NeuroSynt: A Neuro-symbolic Portfolio Solver for Reactive Synthesis](https://mlsanity.com/paper/2401.12131/) (2024)
- [Performance of LLMs on Stochastic Modeling Operations Research Problems: From Theory to Practice](https://mlsanity.com/paper/2506.23924/) (2025)
- [Scaling Natural-Language Graph-Based Test Time Compute for Automated Theorem Proving](https://mlsanity.com/paper/2503.11657/) (2025)
- [Duel-Evolve: Reward-Free Test-Time Scaling via LLM Self-Preferences](https://mlsanity.com/paper/2602.21585/) (2026)
- [TheoremBench: Evaluating LLMs on Theorem Proving in Formal Mathematics](https://mlsanity.com/paper/2606.09450/) (2026)
- [From Solvers to Research: Large Language Model-Driven Formal Mathematics at the Research Frontier](https://mlsanity.com/paper/2607.07779/) (2026)
- [Feynman on Artificial Intelligence and Machine Learning, with Updates](https://mlsanity.com/paper/2209.00083/) (2022)
- [EvoGPT-f: An Evolutionary GPT Framework for Benchmarking Formal Math Languages](https://mlsanity.com/paper/2402.16878/) (2024)
- [Automated Proof of Polynomial Inequalities via Reinforcement Learning](https://mlsanity.com/paper/2503.06592/) (2025)
- [From Pixels to Digital Agents: An Empirical Study on the Taxonomy and Technological Trends of Reinforcement Learning Environments](https://mlsanity.com/paper/2603.23964/) (2026)
- [AdvancedMathBench: A Benchmark Suite for Advanced Mathematical Proof Generation and Verification](https://mlsanity.com/paper/2607.11849/) (2026)

## Abstract (arXiv)

We present an environment, benchmark, and deep learning driven automated theorem prover for higher-order logic. Higher-order interactive theorem provers enable the formalization of arbitrary mathematical theories and thereby present an interesting, open-ended challenge for deep learning. We provide an open-source framework based on the HOL Light theorem prover that can be used as a reinforcement learning environment. HOL Light comes with a broad coverage of basic mathematical theorems on calculus and the formal proof of the Kepler conjecture, from which we derive a challenging benchmark for automated reasoning. We also present a deep reinforcement learning driven automated theorem prover, DeepHOL, with strong initial results on this benchmark.