mlsanityData to 14 Oct 2026

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

arXiv 1904.03241 ↗First posted 5 Apr 2019cs.LO cs.AI cs.LGcited by 19

Not on the map. Why?

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.

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

Builds on

No reference list yet.

Built on by

Cited by year (2026 to 14 Oct)

Citing papers per year: 2021: 5; 2022: 2; 2023: 1; 2024: 3; 2025: 3; 2026: 5.

19 papers.

Sort:

By area:

  1. 2021Measuring Mathematical Problem Solving With the MATH Datasetcited by 5,371
  2. 2024Large Language Models for Mathematical Reasoning: Progresses and Challengescited by 284
  3. 2021Proof Artifact Co-training for Theorem Proving with Language Modelscited by 132
  4. 2021NaturalProofs: Mathematical Theorem Proving in Natural Languagecited by 81
  5. 2021Learning to Guide a Saturation-Based Theorem Provercited by 15
  6. 2022A Survey in Mathematical Language Processingcited by 9
  7. 2021Training a First-Order Theorem Prover from Synthetic Datacited by 8
  8. 2023An Ensemble Approach for Automated Theorem Proving Based on Efficient Name Invariant Graph Neural Representationscited by 4
  9. 2024NeuroSynt: A Neuro-symbolic Portfolio Solver for Reactive Synthesiscited by 3
  10. 2025Performance of LLMs on Stochastic Modeling Operations Research Problems: From Theory to Practicecited by 3
  11. 2025Scaling Natural-Language Graph-Based Test Time Compute for Automated Theorem Provingcited by 2
  12. 2026Duel-Evolve: Reward-Free Test-Time Scaling via LLM Self-Preferencescited by 2
7 more
  1. 2026TheoremBench: Evaluating LLMs on Theorem Proving in Formal Mathematicscited by 1
  2. 2026From Solvers to Research: Large Language Model-Driven Formal Mathematics at the Research Frontiercited by 1
  3. 2022Feynman on Artificial Intelligence and Machine Learning, with Updatescited by 0
  4. 2024EvoGPT-f: An Evolutionary GPT Framework for Benchmarking Formal Math Languagescited by 0
  5. 2025Automated Proof of Polynomial Inequalities via Reinforcement Learningcited by 0
  6. 2026From Pixels to Digital Agents: An Empirical Study on the Taxonomy and Technological Trends of Reinforcement Learning Environmentscited by 0
  7. 2026AdvancedMathBench: A Benchmark Suite for Advanced Mathematical Proof Generation and Verificationcited by 0