# HOList: An Environment for Machine Learning of Higher-Order Theorem Proving Source: [HOList: An Environment for Machine Learning of Higher-Order Theorem Proving]() Collection index: [llms.txt]() Data updated: 2026-01-04T03:06:31.117Z Authors: Kshitij Bansal, Sarah M. Loos, Markus N. Rabe, Christian Szegedy, Stewart Wilcox Published: 2019-04-05T19:04:33.000Z ## Abstract 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. ## Recorded benchmark results A research result applies to its stated dataset, split, metric and evaluation configuration. Compare like-for-like settings, preserve the metric's unit and direction, and distinguish paper-reported results from independent reproduction. The best result recorded here is not a claim of exhaustive, current global coverage. - [Higher-Order Theorem Proving on Complex corpus (val)](): Higher-Order Theorem Proving; Complex corpus (val); Proof Success: 38.9. - [Automated Theorem Proving on HOList complex analysis corpus (val)](): Automated Theorem Proving; HOList complex analysis corpus (val); Proofs Closed Rate: 32.65. ## Original sources and implementation [Original paper]() [PDF]() [Implementation]()