Die Formalisierung bestehender mathematischer Beweise ist ein äußerst schwieriger Prozess. Trotz mehrerer Jahrzehnte Forschung im Bereich der Automatisierung und Beweisassistenten bleibt die Erstellung formaler Beweise mühsam und nur einer kleinen Gruppe von Experten zugänglich. Während frühere Studien zur Automatisierung der Formalisierung sich auf leistungsstarke Suchalgorithmen konzentrierten, wurde bisher kein Ansatz unternommen, um vorhandene informelle Beweise zu nutzen. In dieser Arbeit stellen wir DSP (Draft, Sketch, and Prove) vor – eine Methode, die informelle Beweise in formale Beweisskizzen überführt und diese Skizzen nutzt, um einen automatisierten Beweiser zu leiten, indem dessen Suche auf leichter lösbare Teilprobleme gerichtet wird. Wir untersuchen zwei relevante Szenarien, in denen informelle Beweise entweder von Menschen verfasst oder von einer Sprachmodell generiert werden. Unsere Experimente und Ablationsstudien zeigen, dass große Sprachmodelle in der Lage sind, gut strukturierte formale Skizzen zu erzeugen, die denselben Schlussfolgerungsschritten wie die informellen Beweise folgen. Die Führung eines automatisierten Beweisers durch diese Skizzen verbessert dessen Leistung von 20,9 % auf 39,3 % bei einer Sammlung mathematischer Wettbewerbsaufgaben.