La formalisation des preuves mathématiques existantes est un processus notoirement difficile. Malgré des décennies de recherches sur l’automatisation et les assistants de preuve, la rédaction de preuves formelles reste fastidieuse et réservée à une poignée d’experts. Alors que les études antérieures visant à automatiser cette formalisation se sont concentrées sur des algorithmes de recherche puissants, aucune tentative n’avait été faite jusqu’ici pour exploiter les preuves informelles disponibles. Dans ce travail, nous introduisons une méthode appelée Draft, Sketch, and Prove (DSP), qui consiste à transformer des preuves informelles en esquisses de preuves formelles, puis à utiliser ces esquisses pour guider un prouveur automatisé en orientant sa recherche vers des sous-problèmes plus accessibles. Nous examinons deux configurations pertinentes, dans lesquelles les preuves informelles sont soit rédigées par des humains, soit générées par un modèle linguistique. Nos expériences et études d’ablation montrent que les grands modèles linguistiques sont capables de produire des esquisses formelles bien structurées, suivant les mêmes étapes de raisonnement que les preuves informelles. Guider un prouveur automatisé à l’aide de ces esquisses améliore sa performance de 20,9 % à 39,3 % sur une collection de problèmes de concours mathématiques.