Dans cet article, nous proposons StepProof, une nouvelle méthode de formalisation automatique qui convertit les preuves en langage naturel en preuves formelles à l'aide de modèles de langage à grande échelle (MLH). Contrairement aux méthodes existantes qui ne vérifient que les preuves complètes, StepProof décompose les preuves en plusieurs sous-preuves vérifiables, permettant ainsi une vérification au niveau de la phrase. Les résultats expérimentaux montrent que StepProof améliore significativement le taux de réussite et l'efficacité des preuves par rapport aux méthodes existantes, et que les performances peuvent être encore améliorées en ajoutant quelques ajustements manuels aux preuves en langage naturel.
