Wir untersuchen die Anwendung transformerbasierter Sprachmodelle auf das automatisierte Beweisen von Sätzen. Diese Arbeit wird motiviert durch die Möglichkeit, dass eine wesentliche Einschränkung automatisierter Beweissysteme im Vergleich zu Menschen – die Erzeugung origineller mathematischer Begriffe – möglicherweise durch die Generierung mittels Sprachmodelle überwunden werden könnte. Wir präsentieren einen automatisierten Beweiser und Beweishilfssystem, GPT-f, für die formale Sprache Metamath, und analysieren dessen Leistung. GPT-f fand neue, kurze Beweise, die in die Hauptbibliothek von Metamath aufgenommen wurden – soweit uns bekannt, das erste Mal, dass ein auf tiefen Lernverfahren basierendes System Beweise beigetragen hat, die von einer formalen Mathematikgemeinschaft übernommen wurden.