François Chollet

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

Large computer-understandable proofs consist of millions of intermediate logical steps. The vast majority of such steps originate from manually selected and manually guided heuristics applied to intermediate goals. So far, machine learning has generally not been used to filter or generate these step…