## Learning-assisted automated reasoning with $$\mathsf{Flyspeck}$$.(English)Zbl 1314.68283

J. Autom. Reasoning 53, No. 2, 173-213 (2014); erratum ibid. 54, No. 1, 99 (2015).
Summary: 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 {\mathsf{Flyspeck}} proofs, producing an AI system capable of proving a wide range of mathematical conjectures automatically. The performance of this architecture is evaluated in a bootstrapping scenario emulating the development of {\mathsf{Flyspeck}} from axioms to the last theorem, each time using only the previous theorems and proofs. It is shown that 39 % of the 14185 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. The necessary work involves: (i) an implementation of sound translations of the {\mathsf {HOL Light}} logic to ATP formalisms: untyped first-order, polymorphic typed first-order, and typed higher-order, (ii) export of the dependency information from {\mathsf {HOL Light}} and ATP proofs for the machine learners, and (iii) choice of suitable representations and methods for learning from previous proofs, and their integration as advisors with {\mathsf {HOL Light}}. This work is described and discussed here, and an initial analysis of the body of proofs that were found fully automatically is provided.

### MSC:

 68T15 Theorem proving (deduction, resolution, etc.) (MSC2010) 68T05 Learning and adaptive systems in artificial intelligence
Full Text: