Wir präsentieren eine Umgebung, einen Benchmark und einen durch tiefes Lernen gesteuerten automatischen Theorembeweiser für höherstufige Logik. Höherstufige interaktive Theorembeweiser ermöglichen die Formalisierung beliebiger mathematischer Theorien und stellen damit eine interessante, offene Herausforderung für tiefes Lernen dar. Wir stellen ein quelloffenes Framework vor, das auf dem HOL Light-Theorembeweiser basiert und als Verstärkungslernumgebung verwendet werden kann. HOL Light umfasst eine breite Palette grundlegender mathematischer Sätze zur Analysis und den formellen Beweis der Keplerschen Vermutung, aus denen wir eine anspruchsvolle Benchmarksituation für automatisches Schließen ableiten. Darüber hinaus präsentieren wir einen durch tiefes Verstärkungslernen gesteuerten automatischen Theorembeweiser, DeepHOL, mit vielversprechenden ersten Ergebnissen bei diesem Benchmark.