Beweisassistenten wie Lean haben die mathematische Beweisverifikation revolutioniert und eine hohe Genauigkeit und Zuverlässigkeit gewährleistet. Obwohl große Sprachmodelle (LLMs) in der mathematischen Argumentation vielversprechend sind, wird ihr Fortschritt im formalen Theorembeweis durch einen Mangel an Trainingsdaten behindert. Um dieses Problem zu lösen, stellen wir einen Ansatz vor, um umfangreiche Lean 4-Beweisdaten aus mathematischen Wettbewerbsaufgaben auf Gymnasial- und Studienanfängerniveau zu generieren. Dieser Ansatz umfasst die Übersetzung natürlichsprachlicher Aufgaben in formale Aussagen, das Filtern von Aussagen geringer Qualität und die Generierung von Beweisen zur Erstellung synthetischer Daten. Nach dem Feinjustieren des DeepSeekMath 7B-Modells auf diesem synthetischen Datensatz, der 8 Millionen formale Aussagen mit Beweisen enthält, erreichte unser Modell Genauigkeiten von 46,3 % bei 64 Proben und kumulativ 52 % beim Lean 4 miniF2F-Test, was den Baseline-GPT-4 bei 23,0 % bei 64 Proben sowie eine Baum-Such-Reinforcement-Learning-Methode bei 41,0 % übertrifft. Zudem bewies unser Modell erfolgreich 5 von 148 Problemen im Lean 4 Formalized International Mathematical Olympiad (FIMO)-Benchmark, während GPT-4 keines beweisen konnte. Diese Ergebnisse zeigen das Potenzial der Nutzung groß angelegter synthetischer Daten zur Verbesserung der Theorembeweiskapazitäten in LLMs. Sowohl der synthetische Datensatz als auch das Modell werden verfügbar gemacht, um weitere Forschung in diesem vielversprechenden Bereich zu fördern.