HOL(y) Hammer Machine learning based premise selection for HOL Light

Publications:

• Cezary Kaliszyk and Josef Urban. Learning-assisted Automated Reasoning with Flyspeck. Submitted to JAR. Arxiv.

Abstract:

The considerable mathematical knowledge encoded by the Flyspeck project is combined with external automated theorem provers (ATPs) and machine-learning premise selection methods trained on the proofs, producing an AI system capable of answering a wide range of mathematical queries automatically. The performance of this architecture is evaluated in a bootstrapping scenario emulating the development of Flyspeck from axioms to the last theorem, each time using only the previous theorems and proofs. It is shown that 39% of the 14185 Flyspeck theorems could be proved in a push-button mode (without any high-level advice and user interaction) in 30 seconds of real time on a fourteen-CPU workstation.

Command Line Advice

• Try:

  echo "1+1=2" | nc colo12-c703.uibk.ac.at 8080

Local version

• Download source code: version 0.13.
• Unpack in your HOL Light directory and follow the instructions in the included README file.

Back to top