Simple Dataset for Proof Method Recommendation in Isabelle/HOL (Dataset Description)

Recently, a growing number of researchers have applied machine learning to assist users of interactive theorem provers. However, the expressive nature of underlying logics and esoteric structures of proof documents impede machine learning practitioners from achieving a large scale success in this field. In this data description, we present a simple dataset that represents the essence of choosing appropriate proof methods in Isabelle/HOL. 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.