---
title: "Holophrasm — paper by Whalen (2016) — summary and ideas"
description: "Still, the author presents Holophrasm as the first effective complete prover without… 77.6% accuracy. 18 references, cited by 26 papers here."
authors: ["Daniel Whalen"]
year: 2016
venue: "arXiv:1608.02644"
source: "https://arxiv.org/abs/1608.02644"
doi: "10.48550/arxiv.1608.02644"
arxiv: "1608.02644"
licence: "arXiv — non-exclusive licence to distribute"
licence_url: "https://arxiv.org/licenses/nonexclusive-distrib/1.0/license.html"
summary_licence: "Elamur Cosmic License"
canonical: "https://research.elamur.ai/free/en/papers/whalen-2016-holophrasm-neural-automated-theorem-prover/"
---
[Elamur Research](https://md.research.elamur.ai/free/en/) · [this page in HTML](https://research.elamur.ai/free/en/papers/whalen-2016-holophrasm-neural-automated-theorem-prover/)

[home](https://md.research.elamur.ai/free/en/) / [papers](https://md.research.elamur.ai/free/en/papers/) / [2016](https://md.research.elamur.ai/free/en/papers/2016/page/4/) / Holophrasm: a neural Automated Theorem Prover for higher-order logic

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

**Authors:** Daniel Whalen · **Year:** 2016 · **Venue:** arXiv:1608.02644 · **Licence:** [arXiv — non-exclusive licence to distribute](https://arxiv.org/licenses/nonexclusive-distrib/1.0/license.html)

**Links:** [Publisher's page](https://arxiv.org/abs/1608.02644) · [PDF](https://arxiv.org/pdf/1608.02644v2) · [DOI 10.48550/arxiv.1608.02644](https://doi.org/10.48550/arxiv.1608.02644) · [arXiv 1608.02644](https://arxiv.org/abs/1608.02644) · [OpenAlex](https://openalex.org/W2509751917)

**Citations:** 22 citations (OpenAlex, 2026-10-14) · [26](https://md.research.elamur.ai/free/en/papers/whalen-2016-holophrasm-neural-automated-theorem-prover/cited-by/) in our library, of the 149,439 papers whose bibliographies we read

## Summary

Holophrasm is a fully automatic prover for higher-order logic that avoids hand-engineered features. It works in the Metamath language, where each proof step applies a known theorem through substitution and turns that theorem's hypotheses into new subgoals, so proofs naturally form trees. The system grows partial proof trees with a variant of the UCT bandit algorithm, guided by three neural networks:

- a relevance network that ranks candidate theorems,
- a generative sequence-to-sequence model (GRU with attention and beam search) that proposes expressions for unconstrained variables, an otherwise infinite action space,
- a payoff network that estimates how provable a subgoal is.

Training data come from expanding the proofs in Metamath's set.mm module into individual steps. On held-out theorems, the prover proves 14.3% overall and 45.1% of those from the early part of the database. The results are below state of the art and not directly comparable to Mizar benchmarks. Still, the author presents Holophrasm as the first effective complete prover without hand-crafted features, which suggests that deep learning combined with tree search is a viable path for theorem proving.

## Key points

- Data: set.mm propositions split into 21,786 train, 2711 validation and 2720 test. These expand to about 1.2M training proof steps, and 426k of those steps involve unconstrained variables and are used for the generative network.
- The relevance network reaches 55.3% top-1, 72.8% top-5 and 87.4% top-20 accuracy when choosing among viable theorems.
- The generative network has a test perplexity of 2.08 over 1083 tokens. It produces fully correct substitutions in 39.1%, 51.3% and 57.5% of cases at beam widths 1, 5 and 20.
- The payoff network classifies subgoals with 77.6% accuracy, compared with a 62.1% all-negative baseline.
- Each test theorem gets at most 10,000 search passes or 5 minutes. The system proves 388 of 2720 test theorems, and successful proofs need a median of only 17 passes.

*Our summary of the paper, in our own words — not its text. The work belongs to its authors; read it at the links above.*

📚 Shelves (3): [🖥️ Computer Science](https://md.research.elamur.ai/free/en/shelves/computer-science/) · 19,503 works · [🤖 Artificial Intelligence](https://md.research.elamur.ai/free/en/shelves/computer-science/artificial-intelligence/) · 18,805 works · [🧮 Computational Theory and Mathematics](https://md.research.elamur.ai/free/en/shelves/computer-science/computational-theory-and-mathematics/) · 496 works

🧭 Topics (1): [🧮 Reasoning](https://md.research.elamur.ai/free/en/topics/reasoning/) · 1,948 works

## Cite

Cite as: Daniel Whalen. 2016. Holophrasm: a neural Automated Theorem Prover for higher-order logic. arXiv:1608.02644.

The paper itself, not this page. BibTeX from the library's record of the work.

```bibtex
@misc{whalen2016holophrasm,
  title = {{Holophrasm: a neural Automated Theorem Prover for higher-order logic}},
  author = {Daniel Whalen},
  year = {2016},
  doi = {10.48550/arxiv.1608.02644},
  eprint = {1608.02644},
  archivePrefix = {arXiv},
  url = {https://doi.org/10.48550/arxiv.1608.02644}
}
```

- [← previous Exploring the Realization of Irony in Twitter Data](https://md.research.elamur.ai/free/en/papers/hee-2016-exploring-realization-irony-twitter-data/)
- [next → How Do Cultural Differences Impact the Quality of Sarcasm Annotation?: A Case Study of Indian Annotators and American Text](https://md.research.elamur.ai/free/en/papers/joshi-2016-how-do-cultural-differences-impact/)
- [↑ back to papers of 2016](https://md.research.elamur.ai/free/en/papers/2016/page/4/)

## References

18 references, 6 of them with a card of ours. ↗ leads to the work, «find» searches for one we have no id for yet.

1. Norman Megill. Metamath: A computer language for pure mathematics. 1997. [find](https://scholar.google.com/scholar?q=Norman+Megill%2E+Metamath%3A+A+computer+language+for+pure+mathematics%2E+1997%2E)
2. Roman Matuszewski and Piotr Rudnicki. Mizar: the first 30 years. Mechanized mathematics and its applications, 4(1):3–24, 2005. [find](https://scholar.google.com/scholar?q=Roman+Matuszewski+and+Piotr+Rudnicki%2E+Mizar%3A+the+first+30+years%2E+Mechanized+mathematics+and+its+applications%2C+4%281%29%3A3%E2%80%9324%2C+2005%2E)
3. Thomas C Hales. Introduction to the Flyspeck project. In Dagstuhl Seminar Proceedings. Schloss Dagstuhl-Leibniz-Zentrum für Informatik, 2006. [find](https://scholar.google.com/scholar?q=Thomas+C+Hales%2E+Introduction+to+the+Flyspeck+project%2E+In+Dagstuhl+Seminar+Proceedings%2E+Schloss+Dagstuhl%2DLeibniz%2DZentrum+fu%CC%88r+Informatik%2C+2006%2E)
4. Mauro Jaskelioff and Stephan Merz. Proving the correctness of Disk Paxos. Archive of Formal Proofs, June 2005. ISSN 2150-914x. [http://isa-afp.org/entries/DiskPaxos.shtml](http://isa-afp.org/entries/DiskPaxos.shtml), Formal proof development. [↗](http://isa-afp.org/entries/DiskPaxos.shtml)
5. The Coq development team. The Coq proof assistant reference manual. INRIA, 2012. URL [http://coq.inria.fr](http://coq.inria.fr). Version 8.4. [↗](http://coq.inria.fr)
6. John Harrison. HOL Light: a tutorial introduction. In International Conference on Formal Methods in Computer-Aided Design, pages 265–269. Springer, 1996. [find](https://scholar.google.com/scholar?q=John+Harrison%2E+HOL+Light%3A+a+tutorial+introduction%2E+In+International+Conference+on+Formal+Methods+in+Computer%2DAided+Design%2C+pages+265%E2%80%93269%2E+Springer%2C+1996%2E)
7. Cezary Kaliszyk and Josef Urban. [MizAR 40 for Mizar 40](https://md.research.elamur.ai/free/en/papers/kaliszyk-2013-mizar-40-mizar-40/). Journal of Automated Reasoning, 55(3): 245–256, 2015.
8. Jesse Alama, Tom Heskes, Daniel Kühlwein, Evgeni Tsivtsivadze, and Josef Urban. [Premise selection for mathematics by corpus analysis and kernel methods](https://md.research.elamur.ai/free/en/papers/alama-2011-premise-selection-mathematics-corpus-analysis/). Journal of Automated Reasoning, 52(2):191–213, 2014.
9. Daniel Kühlwein, Twan van Laarhoven, Evgeni Tsivtsivadze, Josef Urban, and Tom Heskes. Overview and evaluation of premise selection techniques for large theory mathematics. In International Joint Conference on Automated Reasoning, pages 378–392. Springer, 2012. [find](https://scholar.google.com/scholar?q=Daniel+Ku%CC%88hlwein%2C+Twan+van+Laarhoven%2C+Evgeni+Tsivtsivadze%2C+Josef+Urban%2C+and+Tom+Heskes%2E+Overview+and+evaluation+of+premise+selection+techniques+for+large+theory+mathematics%2E+In+International+Joint+Con)
10. Daniel Kühlwein, Jasmin Christian Blanchette, Cezary Kaliszyk, and Josef Urban. Mash: machine learning for Sledgehammer. In Interactive Theorem Proving, pages 35–50. Springer, 2013. [find](https://scholar.google.com/scholar?q=Daniel+Ku%CC%88hlwein%2C+Jasmin+Christian+Blanchette%2C+Cezary+Kaliszyk%2C+and+Josef+Urban%2E+Mash%3A+machine+learning+for+Sledgehammer%2E+In+Interactive+Theorem+Proving%2C+pages+35%E2%80%9350%2E+Springer%2C+2013%2E)
11. Alex A Alemi, Francois Chollet, Geoffrey Irving, Christian Szegedy, and Josef Urban. DeepMath-Deep sequence models for premise selection. arXiv preprint arXiv:1606.[04442, 2016](https://md.research.elamur.ai/free/en/papers/alemi-2016-deepmath-deep-sequence-models-premise/).
12. Levente Kocsis and Csaba Szepesvári. Bandit based Monte-Carlo planning. In Machine Learning: ECML 2006, pages 282–293. Springer, 2006. [find](https://scholar.google.com/scholar?q=Levente+Kocsis+and+Csaba+Szepesva%CC%81ri%2E+Bandit+based+Monte%2DCarlo+planning%2E+In+Machine+Learning%3A+ECML+2006%2C+pages+282%E2%80%93293%2E+Springer%2C+2006%2E)
13. Ilya Sutskever, Oriol Vinyals, and Quoc V Le. [Sequence to sequence learning with neural networks](https://md.research.elamur.ai/free/en/papers/sutskever-2014-sequence-sequence-learning-neural-networks/). In Advances in neural information processing systems, pages 3104–3112, 2014.
14. Chris J Maddison, Aja Huang, Ilya Sutskever, and David Silver. Move evaluation in Go using deep convolutional neural networks. arXiv preprint arXiv:1412.6564, 2014. — [arXiv:1412.6564](https://arxiv.org/abs/1412.6564) [find](https://scholar.google.com/scholar?q=Chris+J+Maddison%2C+Aja+Huang%2C+Ilya+Sutskever%2C+and+David+Silver%2E+Move+evaluation+in+Go+using+deep+convolutional+neural+networks%2E+arXiv+preprint+arXiv%3A1412%2E6564%2C+2014%2E+%E2%80%94+%5BarXiv%3A1412%2E6564%5D%28https%3A%2F%2Farxiv%2Eo)
15. David Silver, Aja Huang, Chris J Maddison, Arthur Guez, Laurent Sifre, George Van Den Driessche, Julian Schrittwieser, Ioannis Antonoglou, Veda Panneershelvam, Marc Lanctot, et al. Mastering the game of Go with deep neural networks and tree search. Nature, 529(7587):484–489, 2016. [find](https://scholar.google.com/scholar?q=David+Silver%2C+Aja+Huang%2C+Chris+J+Maddison%2C+Arthur+Guez%2C+Laurent+Sifre%2C+George+Van+Den+Driessche%2C+Julian+Schrittwieser%2C+Ioannis+Antonoglou%2C+Veda+Panneershelvam%2C+Marc+Lanctot%2C+et+al%2E+Mastering+the+game+)
16. Minh-Thang Luong, Hieu Pham, and Christopher D Manning. [Effective approaches to attention-based neural machine translation](https://md.research.elamur.ai/free/en/papers/luong-2015-effective-approaches-attention-based-neural/). arXiv preprint arXiv:1508.04025, 2015.
17. Xavier Glorot and Yoshua Bengio. Understanding the difficulty of training deep feedforward neural networks. In Aistats, volume 9, pages 249–256, 2010. [find](https://scholar.google.com/scholar?q=Xavier+Glorot+and+Yoshua+Bengio%2E+Understanding+the+difficulty+of+training+deep+feedforward+neural+networks%2E+In+Aistats%2C+volume+9%2C+pages+249%E2%80%93256%2C+2010%2E)
18. Diederik Kingma and Jimmy Ba. arXiv:1412.6980, 2014. [Adam: A method for stochastic optimization](https://md.research.elamur.ai/free/en/papers/kingma-2014-adam-method-stochastic-optimization/). arXiv preprint

*Updated 3 November 2026*