Wir stellen ein Online-Trainingsverfahren für einen auf Transformers basierenden automatischen Beweisführer vor. Unser Ansatz nutzt einen neuen Suchalgorithmus, den HyperTree Proof Search (HTPS), der sich an dem jüngsten Erfolg von AlphaZero orientiert. Unser Modell lernt durch Online-Training aus vorherigen Beweissuchen und kann somit auf Domänen generalisieren, die weit von der Trainingsverteilung entfernt liegen. Wir präsentieren detaillierte Ablationsstudien der zentralen Komponenten unseres Pipelines durch die Analyse der Leistung in drei Umgebungen mit zunehmender Komplexität. Insbesondere zeigen wir, dass ein Modell, das allein mit HTPS trainiert wurde und auf annotierten Beweisen basiert, 65,4 % einer ausgelassenen Testmenge von Metamath-Sätzen beweisen kann – deutlich besser als der bisherige Stand der Technik von 56,5 % durch GPT-f. Durch Online-Training auf diesen bisher unbewiesenen Sätzen steigt die Genauigkeit auf 82,6 %. Bei vergleichbarem Rechenaufwand verbessern wir den Stand der Technik auf dem Lean-basierten miniF2F-Curriculum-Datensatz von 31 % auf 42 % Beweisgenauigkeit.