LLMs haben durch die Nutzung von Verstärkungslernen mit langen Gedankengängen starke mathematische Schlussfolgerungsfähigkeiten demonstriert. Dennoch bleiben sie bei der Beweisführung von Sätzen weiterhin herausgefordert, da reine natürliche Sprache keine klaren Überwachungssignale liefert. Spezialisierte, domain-spezifische Sprachen wie Lean bieten hingegen klare Überwachungssignale durch die formale Verifikation von Beweisen, was eine effektive Ausbildung mittels Verstärkungslernen ermöglicht. In dieser Arbeit präsentieren wir Seed-Prover, ein modulares Beweis-Modell im Stil von Lemmata, das seine Beweisführung iterativ anhand von Lean-Rückmeldungen, bereits bewiesenen Lemmata sowie selbstgenerierter Zusammenfassungen verfeinert. Um Aufgaben der Schwierigkeitsstufe der Internationalen Mathematikolympiade (IMO) zu lösen, entwickeln wir drei Strategien für die Inferenz zur Testzeit, die sowohl tiefe als auch breite Schlussfolgerung ermöglichen. Seed-Prover beweist 78,1 % der formalisierten vergangenen IMO-Aufgaben, erreicht die Sättigung von MiniF2F und erzielt über 50 % auf PutnamBench – dies deutlich besser als der bisherige Stand der Technik. Um die begrenzte Unterstützung geometrischer Beweisführung in Lean zu überwinden, führen wir einen geometrischen Schlussfolgerungs-Engine namens Seed-Geometry ein, der die Leistung bisheriger formaler geometrischer Engines übertrifft. Mit diesen beiden Systemen nehmen wir an der IMO 2025 teil und beweisen fünf von sechs Aufgaben vollständig. Diese Arbeit stellt einen bedeutenden Fortschritt im Bereich der automatisierten mathematischen Schlussfolgerung dar und belegt die Wirksamkeit der formalen Verifikation in Kombination mit langen Gedankengängen.