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

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

## Key facts

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

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

- [MiniF2F: a cross-system benchmark for formal Olympiad-level mathematics](https://mlsanity.com/paper/2109.00110/) (2021)
- [HyperTree Proof Search for Neural Theorem Proving](https://mlsanity.com/paper/2205.11491/) (2022)
- [Formal Mathematics Statement Curriculum Learning](https://mlsanity.com/paper/2202.01344/) (2022)
- [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)
- [LEGO-Prover: Neural Theorem Proving with Growing Libraries](https://mlsanity.com/paper/2310.00656/) (2023)
- [NaturalProofs: Mathematical Theorem Proving in Natural Language](https://mlsanity.com/paper/2104.01112/) (2021)
- [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)
- [Learning Formal Mathematics From Intrinsic Motivation](https://mlsanity.com/paper/2407.00695/) (2024)
- [Solving Formal Math Problems by Decomposition and Iterative Reflection](https://mlsanity.com/paper/2507.15225/) (2025)
- [Peano: Learning Formal Mathematical Reasoning](https://mlsanity.com/paper/2211.15864/) (2022)
- [Grammars of Formal Uncertainty: When to Trust LLMs in Automated Reasoning Tasks](https://mlsanity.com/paper/2505.20047/) (2025)
- [REFACTOR: Learning to Extract Theorems from Proofs](https://mlsanity.com/paper/2402.17032/) (2024)
- [ATG: Benchmarking Automated Theorem Generation for Generative Language Models](https://mlsanity.com/paper/2405.06677/) (2024)
- [3D-Prover: Diversity Driven Theorem Proving With Determinantal Point Processes](https://mlsanity.com/paper/2410.11133/) (2024)
- [CoProver: A Recommender System for Proof Construction](https://mlsanity.com/paper/2304.10486/) (2023)
- [ProofCompass: Enhancing Specialized Provers with LLM Guidance](https://mlsanity.com/paper/2507.14335/) (2025)
- [LeanTree: Accelerating White-Box Proof Search with Factorized States in Lean 4](https://mlsanity.com/paper/2507.14722/) (2025)
- [Enhancing Neural Theorem Proving through Data Augmentation and Dynamic Sampling Method](https://mlsanity.com/paper/2312.14188/) (2023)
- [BAIT: Benchmarking (Embedding) Architectures for Interactive Theorem-Proving](https://mlsanity.com/paper/2403.03401/) (2024)
- [Towards Data-Centric Automatic R&D](https://mlsanity.com/paper/2404.11276/) (2024)
- [Learning to Prove Trigonometric Identities](https://mlsanity.com/paper/2207.06679/) (2022)
- [The Mathematical Game](https://mlsanity.com/paper/2309.12711/) (2023)
- [Neuro-Symbolic Proof Generation for Scaling Systems Software Verification](https://mlsanity.com/paper/2603.19715/) (2026)
- [From Solvers to Research: Large Language Model-Driven Formal Mathematics at the Research Frontier](https://mlsanity.com/paper/2607.07779/) (2026)
- [EvoGPT-f: An Evolutionary GPT Framework for Benchmarking Formal Math Languages](https://mlsanity.com/paper/2402.16878/) (2024)
- [NanoProof: Open and Efficient Automated Theorem Proving in Lean 4](https://mlsanity.com/paper/2610.11605/) (2026)

## 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.