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

Cezary Kaliszyk, François Chollet, Christian Szegedy

Large computer-understandable proofs consist of millions of intermediate logical steps. The vast majority of such steps originate from manually selected and manually guided heurist…