Bei der Beweisführung stellt die Auswahl nützlicher Prämissen aus einer großen Bibliothek zur Lösung einer gegebenen Vermutung eine entscheidend wichtige Aufgabe dar. Dies stellt eine Herausforderung für alle Beweisverfahren dar, insbesondere für solche, die auf Sprachmodellen basieren, da diese aufgrund ihrer begrenzten Fähigkeit, große Mengen an prämissenhaltigen Texten zu verarbeiten und zu schließen, Schwierigkeiten haben. In dieser Arbeit stellen wir Thor vor, einen Rahmen, der Sprachmodelle und automatisierte Beweissysteme integriert, um diese Schwierigkeit zu überwinden. In Thor werden Methoden der Klasse der sogenannten „Hammers“ eingesetzt, die die Stärken automatisierter Beweissysteme nutzen, um Prämissen auszuwählen, während alle übrigen Aufgaben den Sprachmodellen übertragen werden. Thor steigert die Erfolgsrate eines Sprachmodells auf dem PISA-Datensatz von 39 % auf 57 % und löst zudem 8,2 % der Probleme, die weder Sprachmodelle noch automatisierte Beweissysteme allein bewältigen können. Zudem erreicht Thor mit einem deutlich geringeren Rechenaufwand eine Erfolgsquote auf dem MiniF2F-Datensatz, die mit den besten bestehenden Methoden vergleichbar ist. Thor kann über einen einfachen, von uns bereitgestellten Protokollmechanismus für die Mehrheit der gängigen interaktiven Beweissysteme implementiert werden.