Große Sprachmodelle haben in letzter Zeit erhebliche Fortschritte bei der Generierung rigoroser mathematischer Beweise erzielt. Im Gegensatz dazu bleibt die Nutzung von LLMs für das Beweisen von Sätzen in formalen Sprachen (wie Lean) weiterhin herausfordernd und rechenintensiv, insbesondere bei Problemen auf Bachelor- und höherem Niveau. In dieser Arbeit stellen wir Seed-Prover 1.5 vor, ein Modell für formales Beweisen, das mittels großskaliger agenter Verstärkungslernverfahren trainiert wurde, sowie einen effizienten Testzeit-Skalierungs-(TTS)-Workflow. Durch umfangreiche Interaktionen mit Lean und weiteren Werkzeugen sammelt das Modell während des Lernprozesses kontinuierlich Erfahrung, was die Fähigkeit und Effizienz des formalen Beweisens erheblich verbessert. Darüber hinaus nutzt unser TTS-Workflow jüngste Fortschritte im Bereich natürlichsprachlicher Beweise, um effizient die Lücke zwischen natürlicher und formalen Sprache zu schließen. Im Vergleich zu aktuellen Spitzenmethoden erreicht Seed-Prover 1.5 eine überlegene Leistung bei geringerem Rechenaufwand. Es löst 88 % der PutnamBench-Probleme (Bachelor-Niveau), 80 % der Fate-H-Probleme (Graduierten-Niveau) und 33 % der Fate-X-Probleme (Doktoranden-Niveau). Besonders bemerkenswert ist, dass wir mit unserem System innerhalb von neun Stunden elf von zwölf Aufgaben aus dem Putnam-Wettbewerb 2025 lösten. Unsere Ergebnisse deuten darauf hin, dass das Skalieren des Lernens aus Erfahrung, angetrieben durch hochwertige formale Rückmeldungen, ein immenses Potenzial für die Zukunft des formalen mathematischen Schließens besitzt.