HOList instrumented HOL Light so learning systems could interact with proof states and tactics through a machine-learning environment. The benchmark packaged theorem statements from core, complex and Flyspeck corpora with train, validation and test labels, while DeepHOL supplied a neural prover and…
Google Research and collaborators released HOList, an open-source reinforcement-learning environment and benchmark built on HOL Light, together with DeepHOL, a deep-learning-driven tactic-based prover trained on human and synthesized proofs and evaluated on theorem corpora including Flyspeck-derived material.
HOList instrumented HOL Light so learning systems could interact with proof states and tactics through a machine-learning environment. The benchmark packaged theorem statements from core, complex and Flyspeck corpora with train, validation and test labels, while DeepHOL supplied a neural prover and reinforcement-learning loop for generating additional successful proof traces.
The release showed how a mature proof assistant and a substantial mathematical library could be exposed as a learning environment rather than only as a static corpus. That environment-plus-benchmark pattern became central to later neural theorem-proving infrastructure and made proof-assistant-native reinforcement learning a concrete experimental program.
Significance rationale: HOList combined an open HOL Light interaction environment, a benchmark drawn from a substantial formal mathematics library, and the DeepHOL neural prover in one reproducible research stack. It became an important early reference point for reinforcement-learning and neural proof guidance inside interactive theorem provers, preceding later systems that learned more of search and tactic selection end to end.
The arXiv and ICML research records establish HOList, its benchmark and the reported DeepHOL experiments. Machine checking refers to proof traces accepted through HOL Light and does not imply independent reproduction of the reported benchmark performance.
The public Deepmath codebase and HOList benchmark site expose the prover code, benchmark definition, model resources and proof-checking workflow. E3 denotes inspectable artifacts rather than independent confirmation of all experimental claims.
No corrections recorded.
