HolStep: A Machine Learning Dataset for Higher-order Logic Theorem Proving

Large computer-understandable proofs consist of millions of intermediatelogical steps. The vast majority of such steps originate from manuallyselected and manually guided heuristics applied to intermediate goals.So far, machine learning has generally not been used to filter orgenerate these steps. In this paper, we introduce a new dataset...More