Große Computer-verstandene Beweise bestehen aus Millionen von Zwischenschritten der Logik. Der überwiegende Teil dieser Schritte entstammt manuell ausgewählten und manuell gesteuerten Heuristiken, die auf Zwischenziele angewendet werden. Bislang wurde maschinelles Lernen im Allgemeinen nicht dazu eingesetzt, diese Schritte zu filtern oder zu generieren. In dieser Arbeit stellen wir einen neuen Datensatz vor, der auf Beweisen der höheren Ordnung Logik (Higher-Order Logic, HOL) basiert und der zur Entwicklung neuer maschinellen Lernverfahren für Beweisstrategien dient. Dieser Datensatz ist unter der BSD-Lizenz öffentlich zugänglich. Wir schlagen verschiedene maschinelle Lernaufgaben vor, die mit diesem Datensatz durchgeführt werden können, und diskutieren ihre Bedeutung für das Beweisen von Sätzen. Zudem evaluieren wir eine Reihe einfacher Baseline-Modelle des maschinellen Lernens, die für diese Aufgaben geeignet sind (darunter logistische Regression, Faltungsneuronale Netze und rekurrente Neuronale Netze). Die Ergebnisse unserer Baseline-Modelle zeigen das Potenzial des Einsatzes von maschinellem Lernen bei Beweisen in der höheren Ordnung Logik (HOL).