HOL(y)Hammer: Online ATP Service for HOL Light

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 installation by interested users, who can customize it for their own proof development. An Emacs interface allowing parallel asynchronous queries to the service is also provided. The overall structure of the service is outlined, problems that arise and their solutions are discussed, and an initial account of using the system is given.