Ich schlage ein System für das automatische Beweisen von Sätzen in höherer Ordnungslogik vor, das tiefes Lernen nutzt und auf manuell konstruierte Merkmale verzichtet. Holophrasm nutzt die Formalisierung der Metamath-Sprache und untersucht partielle Beweisbäume mit einem banditenalgorithmus, der durch neuronale Netze erweitert wurde, sowie einem Sequenz-zu-Sequenz-Modell zur Aktionserzeugung. Das System beweist 14 % seiner Testsätze aus dem Modul set.mm von Metamath.