mlsanityData to 7 Oct 2026

Holophrasm: a neural Automated Theorem Prover for higher-order logic

arXiv 1608.02644 ↗First posted 8 Aug 2016cs.AI cs.LOcited by 29

Not on the map. Why?

Abstract (arXiv)

I propose a system for Automated Theorem Proving in higher order logic using deep learning and eschewing hand-constructed features. Holophrasm exploits the formalism of the Metamath language and explores partial proof trees using a neural-network-augmented bandit algorithm and a sequence-to-sequence model for action enumeration. The system proves 14% of its test theorems from Metamath's set.mm module.

Key facts. Cited by 29 papers in the map (data through 7 Oct 2026). First posted on arXiv 8 Aug 2016.

Builds on

No reference list yet.

Built on by

Cited by year (2026 to 7 Oct)

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

29 papers.

Sort:

By area:

  1. 2021MiniF2F: a cross-system benchmark for formal Olympiad-level mathematicscited by 380
  2. 2022HyperTree Proof Search for Neural Theorem Provingcited by 192
  3. 2022Formal Mathematics Statement Curriculum Learningcited by 141
  4. 2021Proof Artifact Co-training for Theorem Proving with Language Modelscited by 130
  5. 2022A Survey of Deep Learning for Mathematical Reasoningcited by 124
  6. 2023LEGO-Prover: Neural Theorem Proving with Growing Librariescited by 108
  7. 2021NaturalProofs: Mathematical Theorem Proving in Natural Languagecited by 80
  8. 2024Formal Mathematical Reasoning: A New Frontier in AIcited by 80
  9. 2024A Survey on Deep Learning for Theorem Provingcited by 55
  10. 2024Lean Copilot: Large Language Models as Copilots for Theorem Proving in Leancited by 52
  11. 2024Learning Formal Mathematics From Intrinsic Motivationcited by 45
  12. 2025Solving Formal Math Problems by Decomposition and Iterative Reflectioncited by 35
17 more
  1. 2022Peano: Learning Formal Mathematical Reasoningcited by 15
  2. 2024REFACTOR: Learning to Extract Theorems from Proofscited by 9
  3. 2025Grammars of Formal Uncertainty: When to Trust LLMs in Automated Reasoning Taskscited by 9
  4. 2024ATG: Benchmarking Automated Theorem Generation for Generative Language Modelscited by 6
  5. 20243D-Prover: Diversity Driven Theorem Proving With Determinantal Point Processescited by 6
  6. 2023CoProver: A Recommender System for Proof Constructioncited by 5
  7. 2025ProofCompass: Enhancing Specialized Provers with LLM Guidancecited by 3
  8. 2025LeanTree: Accelerating White-Box Proof Search with Factorized States in Lean 4cited by 3
  9. 2023Enhancing Neural Theorem Proving through Data Augmentation and Dynamic Sampling Methodcited by 2
  10. 2024BAIT: Benchmarking (Embedding) Architectures for Interactive Theorem-Provingcited by 2
  11. 2024Towards Data-Centric Automatic R&Dcited by 2
  12. 2022Learning to Prove Trigonometric Identitiescited by 1
  13. 2023The Mathematical Gamecited by 1
  14. 2026Neuro-Symbolic Proof Generation for Scaling Systems Software Verificationcited by 1
  15. 2026From Solvers to Research: Large Language Model-Driven Formal Mathematics at the Research Frontiercited by 1
  16. 2024EvoGPT-f: An Evolutionary GPT Framework for Benchmarking Formal Math Languagescited by 0
  17. 2026NanoProof: Open and Efficient Automated Theorem Proving in Lean 4cited by 0