# HolStep: A Machine Learning Dataset for Higher-order Logic Theorem Proving

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

## Key facts

- Cited by 26 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 1 Mar 2017.

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

- [LeanDojo: Theorem Proving with Retrieval-Augmented Language Models](https://mlsanity.com/paper/2306.15626/) (2023)
- [Proof Artifact Co-training for Theorem Proving with Language Models](https://mlsanity.com/paper/2102.06203/) (2021)
- [A Survey of Deep Learning for Mathematical Reasoning](https://mlsanity.com/paper/2212.10535/) (2022)
- [Thor: Wielding Hammers to Integrate Language Models and Automated Theorem Provers](https://mlsanity.com/paper/2205.10893/) (2022)
- [Formal Mathematical Reasoning: A New Frontier in AI](https://mlsanity.com/paper/2412.16075/) (2024)
- [Lean Copilot: Large Language Models as Copilots for Theorem Proving in Lean](https://mlsanity.com/paper/2404.12534/) (2024)
- [A Survey on Deep Learning for Theorem Proving](https://mlsanity.com/paper/2404.09939/) (2024)
- [Magnushammer: A Transformer-Based Approach to Premise Selection](https://mlsanity.com/paper/2303.04488/) (2023)
- [Mathematical Language Models: A Survey](https://mlsanity.com/paper/2312.07622/) (2023)
- [A Survey on Mathematical Reasoning and Optimization with Large Language Models](https://mlsanity.com/paper/2503.17726/) (2025)
- [RealCQA: Scientific Chart Question Answering as a Test-bed for First-Order Logic](https://mlsanity.com/paper/2308.01979/) (2023)
- [MIRB: Mathematical Information Retrieval Benchmark](https://mlsanity.com/paper/2505.15585/) (2025)
- [Generating Symbolic Reasoning Problems with Transformer GANs](https://mlsanity.com/paper/2110.10054/) (2021)
- [Neural Theorem Proving for Verification Conditions: A Real-World Benchmark](https://mlsanity.com/paper/2601.18944/) (2026)
- [Graph Contrastive Pre-training for Effective Theorem Reasoning](https://mlsanity.com/paper/2108.10821/) (2021)
- [PhysNLU: A Language Resource for Evaluating Natural Language Understanding and Explanation Coherence in Physics](https://mlsanity.com/paper/2201.04275/) (2022)
- [QEDCartographer: Automating Formal Verification Using Reward-Free Reinforcement Learning](https://mlsanity.com/paper/2408.09237/) (2024)
- [Performance of LLMs on Stochastic Modeling Operations Research Problems: From Theory to Practice](https://mlsanity.com/paper/2506.23924/) (2025)
- [Learning Structure-Aware Representations of Dependent Types](https://mlsanity.com/paper/2402.02104/) (2024)
- [BAIT: Benchmarking (Embedding) Architectures for Interactive Theorem-Proving](https://mlsanity.com/paper/2403.03401/) (2024)
- [The Tactician's Web of Large-Scale Formal Knowledge](https://mlsanity.com/paper/2401.02950/) (2024)
- [Learning Heuristics for Template-based CEGIS of Loop Invariants with Reinforcement Learning](https://mlsanity.com/paper/2107.09766/) (2021)
- [Genetic Algorithm for Program Synthesis](https://mlsanity.com/paper/2211.11937/) (2022)
- [On a Functional Definition of Intelligence](https://mlsanity.com/paper/2312.09546/) (2023)
- [ProofSketcher: Hybrid LLM + Lightweight Proof Checker for Reliable Math/Logic Reasoning](https://mlsanity.com/paper/2604.06401/) (2026)
- [Re2Math: Benchmarking Theorem Retrieval in Research-Level Mathematics](https://mlsanity.com/paper/2605.09012/) (2026)

## Abstract (arXiv)

Large computer-understandable proofs consist of millions of intermediate logical steps. The vast majority of such steps originate from manually selected and manually guided heuristics applied to intermediate goals. So far, machine learning has generally not been used to filter or generate these steps. In this paper, we introduce a new dataset based on Higher-Order Logic (HOL) proofs, for the purpose of developing new machine learning-based theorem-proving strategies. We make this dataset publicly available under the BSD license. We propose various machine learning tasks that can be performed on this dataset, and discuss their significance for theorem proving. We also benchmark a set of simple baseline machine learning models suited for the tasks (including logistic regression, convolutional neural networks and recurrent neural networks). The results of our baseline models show the promise of applying machine learning to HOL theorem proving.