---
title: "HOList — paper by Bansal et al. (2019) — summary and ideas"
description: "Learning-based theorem proving has lacked a shared, large-scale benchmark. 20 references, cited by 59 papers here."
authors: ["Kshitij Bansal", "Sarah M. Loos", "Markus N. Rabe", "Christian Szegedy", "Stewart Wilcox"]
year: 2019
venue: "arXiv:1904.03241"
source: "https://arxiv.org/abs/1904.03241"
doi: "10.48550/arxiv.1904.03241"
arxiv: "1904.03241"
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/bansal-2019-holist-environment-machine-learning-higher/"
---
[Elamur Research](https://md.research.elamur.ai/free/en/) · [this page in HTML](https://research.elamur.ai/free/en/papers/bansal-2019-holist-environment-machine-learning-higher/)

[home](https://md.research.elamur.ai/free/en/) / [papers](https://md.research.elamur.ai/free/en/papers/) / [2019](https://md.research.elamur.ai/free/en/papers/2019/page/6/) / HOList: An Environment for Machine Learning of Higher-Order Theorem Proving

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

**Authors:** [Kshitij Bansal](https://md.research.elamur.ai/free/en/authors/kshitij-bansal/), [Sarah M. Loos](https://md.research.elamur.ai/free/en/authors/sarah-m-loos/), [Markus N. Rabe](https://md.research.elamur.ai/free/en/authors/markus-n-rabe/), [Christian Szegedy](https://md.research.elamur.ai/free/en/authors/christian-szegedy/) and Stewart Wilcox · **Year:** 2019 · **Venue:** arXiv:1904.03241 · **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/1904.03241) · [PDF](https://arxiv.org/pdf/1904.03241v3) · [DOI 10.48550/arxiv.1904.03241](https://doi.org/10.48550/arxiv.1904.03241) · [arXiv 1904.03241](https://arxiv.org/abs/1904.03241) · [OpenAlex](https://openalex.org/W2951286161)

**Citations:** 19 citations (OpenAlex, 2026-10-14) · [59](https://md.research.elamur.ai/free/en/papers/bansal-2019-holist-environment-machine-learning-higher/cited-by/) in our library, of the 149,439 papers whose bibliographies we read

## Summary
Learning-based theorem proving has lacked a shared, large-scale benchmark. Existing proof assistants use incompatible logical foundations, and earlier datasets were either small or scored only with proxy metrics. HOList fills this gap. It is an open-source environment built on the HOL Light interactive prover, packaged as a Docker image and controlled through a Python API, so agents can search for proofs as in reinforcement learning. The authors added logging of the human-written proofs, faster startup for distributed search, and an independent proof checker, so a proof found through the API does not have to be trusted blindly. The benchmark comes from HOL Light's core library, its complex-analysis library and the Flyspeck formalization of the Kepler conjecture. To show the setup is usable, they built DeepHOL, a neural prover. It first imitates human proofs, then improves through reinforcement learning, picking a tactic and ranking premises for each goal. On the complex-analysis validation set, its best version proved 38.9% of theorems. The resource gives higher-order automated reasoning a reproducible yardstick based on how many theorems a system actually proves.

## Key points
- The benchmark covers about 2,200 definitions and 29,462 theorems across three corpora (core, complex, flyspeck), with over 1 million proof states. The Coq-based GamePad has only 1,602 theorems.
- DeepHOL uses WaveNet-style encoders to choose among 41 tactics and to rank theorem arguments (premises). The deeper variant has about 47M parameters.
- On the 3,225-theorem complex validation set, the scores were:
  - ASM_MESON_TAC baselines: 6.1% (no arguments) and 9.2% (with argument selection)
  - Supervised WaveNet models: 27.6–32.65%
  - Reinforcement-learning loops: 36.3–38.9%
- In each reinforcement-learning round, the system tries 2,000 training theorems spread over 1,000 cores, with limits of 100 proof states and 300 s per attempt. Together, all loops proved 58.0% of the training set (5,919 of 10,199 theorems).
- Code and tools are released at deephol.org, including proof export/import and a separate checker that replays found proofs inside HOL Light.

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

## Institutions

- [Google](https://md.research.elamur.ai/free/en/companies/google/) — Company, Mountain View, United States · 492 works · 440,463 citations

📚 Shelves (2): [🖥️ Computer Science](https://md.research.elamur.ai/free/en/shelves/computer-science/) · 18,614 works · [🤖 Artificial Intelligence](https://md.research.elamur.ai/free/en/shelves/computer-science/artificial-intelligence/) · 17,965 works

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

## Cite

Cite as: Kshitij Bansal, Sarah M. Loos, Markus N. Rabe, Christian Szegedy and Stewart Wilcox. 2019. HOList: An Environment for Machine Learning of Higher-Order Theorem Proving. arXiv:1904.03241.

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

```bibtex
@misc{bansal2019holist,
  title = {{HOList: An Environment for Machine Learning of Higher-Order Theorem Proving}},
  author = {Kshitij Bansal, Sarah M. Loos, Markus N. Rabe, Christian Szegedy and Stewart Wilcox},
  year = {2019},
  doi = {10.48550/arxiv.1904.03241},
  eprint = {1904.03241},
  archivePrefix = {arXiv},
  url = {https://doi.org/10.48550/arxiv.1904.03241}
}
```

- [← previous QuaRTz: An Open-Domain Dataset of Qualitative Relationship Questions](https://md.research.elamur.ai/free/en/papers/tafjord-2019-quartz-open-domain-dataset-qualitative/)
- [next → Pragmatically Informative Text Generation](https://md.research.elamur.ai/free/en/papers/shen-2019-pragmatically-informative-text-generation/)
- [↑ back to papers of 2019](https://md.research.elamur.ai/free/en/papers/2019/page/6/)

## References

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

1. Vassil Panayotov, Guoguo Chen, Daniel Povey, and Sanjeev Khudanpur. Librispeech: an asr corpus based on public domain audio books. In Acoustics, Speech and Signal Processing (ICASSP), 2015 IEEE International Conference on, pages 5206–5210. IEEE, 2015. [find](https://scholar.google.com/scholar?q=Vassil+Panayotov%2C+Guoguo+Chen%2C+Daniel+Povey%2C+and+Sanjeev+Khudanpur%2E+Librispeech%3A+an+asr+corpus+based+on+public+domain+audio+books%2E+In+Acoustics%2C+Speech+and+Signal+Processing+%28ICASSP%29%2C+2015+IEEE+Intern)
2. James Bennett, Stan Lanning, et al. The netflix prize. In Proceedings of KDD cup and workshop, volume 2007, page 35. New York, NY, USA, 2007. [find](https://scholar.google.com/scholar?q=James+Bennett%2C+Stan+Lanning%2C+et+al%2E+The+netflix+prize%2E+In+Proceedings+of+KDD+cup+and+workshop%2C+volume+2007%2C+page+35%2E+New+York%2C+NY%2C+USA%2C+2007%2E)
3. Jia Deng, Wei Dong, Richard Socher, Li-Jia Li, Kai Li, and Li Fei-Fei. Imagenet: A large-scale hierarchical image database. In Computer Vision and Pattern Recognition, 2009. CVPR 2009. IEEE Conference on, pages 248–255. Ieee, 2009. [find](https://scholar.google.com/scholar?q=Jia+Deng%2C+Wei+Dong%2C+Richard+Socher%2C+Li%2DJia+Li%2C+Kai+Li%2C+and+Li+Fei%2DFei%2E+Imagenet%3A+A+large%2Dscale+hierarchical+image+database%2E+In+Computer+Vision+and+Pattern+Recognition%2C+2009%2E+CVPR+2009%2E+IEEE+Conference)
4. Tsung-Yi Lin, Michael Maire, Serge Belongie, James Hays, Pietro Perona, Deva Ramanan, Piotr Dollár, and C Lawrence Zitnick. [Microsoft coco: Common objects in context](https://md.research.elamur.ai/free/en/papers/lin-2014-microsoft-coco-common-objects-context/). In European conference on computer vision, pages 740–755. Springer, 2014.
5. Ondrej Bojar, Christian Buck, Christian Federmann, Barry Haddow, Philipp Koehn, Johannes Leveling, Christof Monz, Pavel Pecina, Matt Post, Herve Saint-Amand, et al. [Findings of the 2014 workshop on statistical machine translation](https://md.research.elamur.ai/free/en/papers/bojar-2014-findings-2014-workshop-statistical-machine/). In Proceedings of the ninth workshop on statistical machine translati…
6. Pranav Rajpurkar, Jian Zhang, Konstantin Lopyrev, and Percy Liang. [Squad: 100,000+ questions for machine comprehension of text](https://md.research.elamur.ai/free/en/papers/rajpurkar-2016-squad-100-000-questions-machine/). arXiv preprint arXiv:1606.05250, 2016.
7. Thomas Hales, Mark Adams, Gertrud Bauer, Tat Dat Dang, John Harrison, Hoang Le Truong, Cezary Kaliszyk, Victor Magron, Sean McLaughlin, Tat Thang Nguyen, et al. A formal proof of the kepler conjecture. In Forum of Mathematics, Pi, volume 5. Cambridge University Press, 2017. [find](https://scholar.google.com/scholar?q=Thomas+Hales%2C+Mark+Adams%2C+Gertrud+Bauer%2C+Tat+Dat+Dang%2C+John+Harrison%2C+Hoang+Le+Truong%2C+Cezary+Kaliszyk%2C+Victor+Magron%2C+Sean+McLaughlin%2C+Tat+Thang+Nguyen%2C+et+al%2E+A+formal+proof+of+the+kepler+conjecture)
8. Josef Urban, Geoff Sutcliffe, Petr Pudlák, and Jiří Vyskočil. [21] Daniel Whalen. Holophrasm: a neural automated the-Malarea sg1-machine learner for automated reasoning with orem prover for higher-order logic. arXiv preprint semantic guidance. In International Joint Conference on arXiv:1608.02644,… [find](https://scholar.google.com/scholar?q=Josef+Urban%2C+Geoff+Sutcliffe%2C+Petr+Pudl%C3%A1k%2C+and+Jir%CC%8C%C3%AD+Vyskoc%CC%8Cil%2E+%5B21%5D+Daniel+Whalen%2E+Holophrasm%3A+a+neural+automated+the%2DMalarea+sg1%2Dmachine+learner+for+automated+reasoning+with+orem+prover+for+higher%2Do)
9. Thibault Gauthier, Cezary Kaliszyk, and Josef Urban. Tactictoe: Learning to reason with hol4 tactics. In LPAR-21. [23] Sarah Loos, Geoffrey Irving, Christian Szegedy, and 21st International Conference on Logic for Programming, Cezary Kaliszyk. [Deep network guided proof search](https://md.research.elamur.ai/free/en/papers/loos-2017-deep-network-guided-proof-search/). arXiv Artificial Intel…
10. Daniel Huang, Prafulla Dhariwal, Dawn Song, and Ilya Holstep: A machine learning dataset for higher-order logic Sutskever. Gamepad: A learning environment for theorem theorem proving. arXiv preprint arXiv:1703.00426, 2017. proving. arXiv preprint arXiv:1806.00608, 2018. [25] Cezary Kaliszyk, Josef U… [find](https://scholar.google.com/scholar?q=Daniel+Huang%2C+Prafulla+Dhariwal%2C+Dawn+Song%2C+and+Ilya+Holstep%3A+A+machine+learning+dataset+for+higher%2Dorder+logic+Sutskever%2E+Gamepad%3A+A+learning+environment+for+theorem+theorem+proving%2E+arXiv+preprint+a)
11. Konrad Slind and Michael Norrish. A brief overview of arXiv preprint arXiv:1805.07563, 2018. hol4. In International Conference on Theorem Proving in Higher Order Logics, pages 28–32. Springer, 2008. [26] Rong-En Fan, Kai-Wei Chang, Cho-Jui Hsieh, Xiang-Rui Wang, and Chih-Jen Lin. Liblinear: A librar… [find](https://scholar.google.com/scholar?q=Konrad+Slind+and+Michael+Norrish%2E+A+brief+overview+of+arXiv+preprint+arXiv%3A1805%2E07563%2C+2018%2E+hol4%2E+In+International+Conference+on+Theorem+Proving+in+Higher+Order+Logics%2C+pages+28%E2%80%9332%2E+Springer%2C+2008%2E+%5B)
12. Yves Bertot and Pierre Castéran. Interactive theorem prov-linear classification. Journal of machine learning research, ing and program development: Coq’Art: the calculus of 9(Aug):1871–1874, 2008. inductive constructions. Springer Science & Business Media, 2013. [27] Jens Otten and Wolfgang Bibel. l… [find](https://scholar.google.com/scholar?q=Yves+Bertot+and+Pierre+Cast%C3%A9ran%2E+Interactive+theorem+prov%2Dlinear+classification%2E+Journal+of+machine+learning+research%2C+ing+and+program+development%3A+Coq%E2%80%99Art%3A+the+calculus+of+9%28Aug%29%3A1871%E2%80%931874%2C+2008%2E+ind)
13. Mizar. The Mizar Mathematical Library. URL http: 161, 2003. //mizar.org. Accessed: 2018/01/18. [28] Stephan Schulz. Learning search control knowledge [find](https://scholar.google.com/scholar?q=Mizar%2E+The+Mizar+Mathematical+Library%2E+URL+http%3A+161%2C+2003%2E+%2F%2Fmizar%2Eorg%2E+Accessed%3A+2018%2F01%2F18%2E+%5B28%5D+Stephan+Schulz%2E+Learning+search+control+knowledge)
14. Makarius Wenzel, Lawrence C. Paulson, and Tobias Nip-for equational deduction, volume 230 of DISKI. Infix kow. The isabelle framework. In Otmane Aït Mohamed, Akademische Verlagsgesellschaft, 2000. ISBN 978-3-César A. Muñoz, and Sofiène Tahar, editors, Theorem Prov-89838-230-4. ing in Higher Order Lo… [find](https://scholar.google.com/scholar?q=Makarius+Wenzel%2C+Lawrence+C%2E+Paulson%2C+and+Tobias+Nip%2Dfor+equational+deduction%2C+volume+230+of+DISKI%2E+Infix+kow%2E+The+isabelle+framework%2E+In+Otmane+A%C3%AFt+Mohamed%2C+Akademische+Verlagsgesellschaft%2C+2000%2E+ISB)
15. Leonardo de Moura, Soonho Kong, Jeremy Avigad, Floris machine learning connection prover. In International Con-Van Doorn, and Jakob von Raumer. The lean theorem ference on Automated Reasoning with Analytic Tableaux prover (system description). In International Conference and Related Methods, pages 2… [find](https://scholar.google.com/scholar?q=Leonardo+de+Moura%2C+Soonho+Kong%2C+Jeremy+Avigad%2C+Floris+machine+learning+connection+prover%2E+In+International+Con%2DVan+Doorn%2C+and+Jakob+von+Raumer%2E+The+lean+theorem+ference+on+Automated+Reasoning+with+Ana)
16. Gerwin Klein, Kevin Elphinstone, Gernot Heiser, June vadze, Josef Urban, and Tom Heskes. Overview and eval-Andronick, David Cock, Philip Derrin, Dhammika Elka-uation of premise selection techniques for large theory duwe, Kai Engelhardt, Rafal Kolanski, Michael Norrish, mathematics. In International… — [doi:10.1145/1629575.1629596](https://doi.org/10.1145/1629575.1629596) [find](https://scholar.google.com/scholar?q=Gerwin+Klein%2C+Kevin+Elphinstone%2C+Gernot+Heiser%2C+June+vadze%2C+Josef+Urban%2C+and+Tom+Heskes%2E+Overview+and+eval%2DAndronick%2C+David+Cock%2C+Philip+Derrin%2C+Dhammika+Elka%2Duation+of+premise+selection+techniques+fo)
17. Cezary Kaliszyk and Josef Urban. Learning-assisted au-Theorem Proving, pages 35–50. Springer, 2013. tomated reasoning with flyspeck. Journal of Automated [34] Jesse Alama, Tom Heskes, Daniel Kühlwein, Evgeni Tsivt-Reasoning, 53(2):173–213, 2014. sivadze, and Josef Urban. Premise selection for mathe- [find](https://scholar.google.com/scholar?q=Cezary+Kaliszyk+and+Josef+Urban%2E+Learning%2Dassisted+au%2DTheorem+Proving%2C+pages+35%E2%80%9350%2E+Springer%2C+2013%2E+tomated+reasoning+with+flyspeck%2E+Journal+of+Automated+%5B34%5D+Jesse+Alama%2C+Tom+Heskes%2C+Daniel+K%C3%BChlwein%2C)
18. Cezary Kaliszyk and Josef Urban. Initial experiments with matics by corpus analysis and kernel methods. Journal of external provers and premise selection on hol light corpora. Automated Reasoning, 52(2):191–213, 2014. 2012. [35] James P. Bridge, Sean B. Holden, and Lawrence C. Paulson. [find](https://scholar.google.com/scholar?q=Cezary+Kaliszyk+and+Josef+Urban%2E+Initial+experiments+with+matics+by+corpus+analysis+and+kernel+methods%2E+Journal+of+external+provers+and+premise+selection+on+hol+light+corpora%2E+Automated+Reasoning%2C+52%28)
19. Alexander A Alemi, François Chollet, Geoffrey Irv-Machine learning for first-order theorem proving. J. Autom. ing, Niklas Eén, Christian Szegedy, and Josef Urban. Reasoning, pages 1–32, 2014. [ISSN 0168-7433](https://md.research.elamur.ai/free/en/papers/alemi-2016-deepmath-deep-sequence-models-premise/). doi: 10. Deepmath-deep sequence models for premise selection. 1007/s10817-014-9301-5. URL ht…
20. Stephan Schulz. E - A Brainiac Theorem Prover. AI learner for automated reasoning 0.4 and 0.5. arXiv preprint Commun., 15(2-3):111–126, 2002. arXiv:1402.2359, 2014. [37] Cezary Kaliszyk, Lionel Mamane, and Josef Urban. Machine learning of coq proof guidance: First experiments. arXiv preprint arXiv:1… [find](https://scholar.google.com/scholar?q=Stephan+Schulz%2E+E+%2D+A+Brainiac+Theorem+Prover%2E+AI+learner+for+automated+reasoning+0%2E4+and+0%2E5%2E+arXiv+preprint+Commun%2E%2C+15%282%2D3%29%3A111%E2%80%93126%2C+2002%2E+arXiv%3A1402%2E2359%2C+2014%2E+%5B37%5D+Cezary+Kaliszyk%2C+Lionel+Mamane)

*Updated 2 November 2026*