HOL(y)Hammer: Online ATP Service for HOL Light
Cezary Kaliszyk, Josef Urban

TL;DR
HOL(y)Hammer is an online AI-powered theorem proving service for HOL Light that automates reasoning on formal mathematics, supporting large projects and providing customizable local and remote access.
Contribution
The paper introduces HOL(y)Hammer, a novel online AI/ATP system for HOL Light that integrates multiple automated reasoning tools and premise selection trained on large formal libraries.
Findings
Supports large formal projects like Flyspeck, Multivariate Analysis, Complex Analysis
Employs parallel AI/ATP combinations and decision procedures for high performance
Provides local installation and user-friendly interface options
Abstract
HOL(y)Hammer is an online AI/ATP service for formal (computer-understandable) mathematics encoded in the HOL Light system. The service allows its users to upload and automatically process an arbitrary formal development (project) based on HOL Light, and to attack arbitrary conjectures that use the concepts defined in some of the uploaded projects. For that, the service uses several automated reasoning systems combined with several premise selection methods trained on all the project proofs. The projects that are readily available on the server for such query answering include the recent versions of the Flyspeck, Multivariate Analysis and Complex Analysis libraries. The service runs on a 48-CPU server, currently employing in parallel for each task 7 AI/ATP combinations and 4 decision procedures that contribute to its overall performance. The system is also available for local…
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Code & Models
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsLogic, programming, and type systems · Advanced Database Systems and Queries · Logic, Reasoning, and Knowledge
