Les assistants de preuve comme Lean ont révolutionné la vérification des démonstrations mathématiques, garantissant une haute précision et fiabilité. Bien que les grands modèles linguistiques (LLMs) montrent un potentiel prometteur en matière de raisonnement mathématique, leur avancement dans la preuve formelle de théorèmes est entravé par un manque de données d'entraînement. Pour remédier à ce problème, nous présentons une approche visant à générer des données de preuve Lean 4 étendues à partir de problèmes de compétitions mathématiques au niveau lycée et université. Cette approche consiste à traduire les problèmes exprimés en langage naturel en énoncés formels, à filtrer les énoncés de faible qualité et à générer des preuves afin de créer des données synthétiques. Après avoir affiné le modèle DeepSeekMath 7B sur cet ensemble de données synthétiques, qui comprend 8 millions d'énoncés formels avec leurs preuves, notre modèle a atteint des taux de précision pour la génération complète de preuves de 46,3% avec 64 échantillons et 52% cumulativement sur le test miniF2F Lean 4, dépassant ainsi le modèle GPT-4 qui n'a obtenu que 23,0% avec 64 échantillons et une méthode d'apprentissage par renforcement basée sur la recherche arborescente qui a atteint 41,0%. De plus, notre modèle a réussi à prouver 5 des 148 problèmes du benchmark Lean 4 Formalized International Mathematical Olympiad (FIMO), tandis que GPT-4 n'a pas réussi à prouver aucun. Ces résultats démontrent le potentiel d'utilisation de grandes quantités de données synthétiques pour améliorer les capacités de preuve formelle dans les LLMs. À la fois l'ensemble de données synthétiques et le modèle seront mis à disposition pour faciliter des recherches ultérieures dans ce domaine prometteur.