mlsanityData to 7 Oct 2026

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

arXiv 1703.00426 ↗First posted 1 Mar 2017cs.AIcited by 26

Not on the map. Why?

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.

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

Builds on

No reference list yet.

Built on by

Cited by year (2026 to 7 Oct)

Citing papers per year: 2021: 4; 2022: 4; 2023: 5; 2024: 7; 2025: 3; 2026: 3.

26 papers.

Sort:

By area:

  1. 2023LeanDojo: Theorem Proving with Retrieval-Augmented Language Modelscited by 414
  2. 2021Proof Artifact Co-training for Theorem Proving with Language Modelscited by 130
  3. 2022A Survey of Deep Learning for Mathematical Reasoningcited by 124
  4. 2022Thor: Wielding Hammers to Integrate Language Models and Automated Theorem Proverscited by 97
  5. 2024Formal Mathematical Reasoning: A New Frontier in AIcited by 80
  6. 2024A Survey on Deep Learning for Theorem Provingcited by 55
  7. 2024Lean Copilot: Large Language Models as Copilots for Theorem Proving in Leancited by 52
  8. 2023Magnushammer: A Transformer-Based Approach to Premise Selectioncited by 50
  9. 2023Mathematical Language Models: A Surveycited by 24
  10. 2025A Survey on Mathematical Reasoning and Optimization with Large Language Modelscited by 12
  11. 2023RealCQA: Scientific Chart Question Answering as a Test-bed for First-Order Logiccited by 7
  12. 2021Generating Symbolic Reasoning Problems with Transformer GANscited by 5
14 more
  1. 2025MIRB: Mathematical Information Retrieval Benchmarkcited by 5
  2. 2026Neural Theorem Proving for Verification Conditions: A Real-World Benchmarkcited by 4
  3. 2021Graph Contrastive Pre-training for Effective Theorem Reasoningcited by 3
  4. 2022PhysNLU: A Language Resource for Evaluating Natural Language Understanding and Explanation Coherence in Physicscited by 3
  5. 2024QEDCartographer: Automating Formal Verification Using Reward-Free Reinforcement Learningcited by 3
  6. 2025Performance of LLMs on Stochastic Modeling Operations Research Problems: From Theory to Practicecited by 3
  7. 2024Learning Structure-Aware Representations of Dependent Typescited by 2
  8. 2024BAIT: Benchmarking (Embedding) Architectures for Interactive Theorem-Provingcited by 2
  9. 2024The Tactician's Web of Large-Scale Formal Knowledgecited by 1
  10. 2021Learning Heuristics for Template-based CEGIS of Loop Invariants with Reinforcement Learningcited by 0
  11. 2022Genetic Algorithm for Program Synthesiscited by 0
  12. 2023On a Functional Definition of Intelligencecited by 0
  13. 2026ProofSketcher: Hybrid LLM + Lightweight Proof Checker for Reliable Math/Logic Reasoningcited by 0
  14. 2026Re2Math: Benchmarking Theorem Retrieval in Research-Level Mathematicscited by 0