Simple Dataset for Proof Method Recommendation in Isabelle/HOL

<p>Recently, a growing number of researchers have applied machine learning to assist users of interactive theorem provers.</p> <p>However, the expressive nature of underlying logics and esoteric structures of proof documents impede machine learning practitioners, who often do not have much expertise in formal logic, let alone Isabelle/HOL, from applying their tools and expertise to theorem proving.</p> <p>In this data description, we present a simple dataset that contains data on over 400k proof method applications in the Archive of Formal Proofs along with over 100 extracted features for each in a format that can be processed easily without any knowledge about formal logic.</p> <p>Our simple data format allows machine learning practitioners to try machine learning tools to predict proof methods in Isabelle/HOL, even if they are unfamiliar with theorem proving.</p>