Les grands modèles linguistiques (LLMs) ouvrent une voie prometteuse d'exploration dans le domaine de la démonstration formelle de théorèmes. Néanmoins, l'exploitation complète de ces modèles, en particulier en ce qui concerne la formulation et l'organisation des démonstrations, reste un domaine largement sous-exploité. Dans une perspective d'amélioration de l'efficacité des LLMs, nous proposons un cadre d'apprentissage par démonstration basé sur les sous-objectifs, composé de deux éléments principaux : premièrement, inspirés des avancées en apprentissage par renforcement et en robotique, nous proposons de définir des sous-objectifs distincts pour chaque exemple de démonstration, puis de les affiner selon les théories pertinentes relatives aux sous-objectifs. Deuxièmement, nous nous appuyons sur les progrès récents des modèles de diffusion afin de prédire l'organisation optimale, tout en traitant simultanément deux problèmes complexes persistants dans le domaine de l'organisation des démonstrations : la sélection de sous-ensembles et la détermination de l'ordre. En intégrant des méthodologies d'apprentissage basées sur les sous-objectifs, nous avons réussi à faire passer le taux de précision des preuves courant de 38,9 % à 44,3 % sur le benchmark miniF2F. En outre, l'utilisation des modèles de diffusion pour l'organisation des démonstrations permet une amélioration supplémentaire de la précision à 45,5 %, ou une amélioration de l'efficacité d'échantillonnage de facteur 5 par rapport à la méthode d'état de l'art longtemps dominante. Notre code est disponible à l'adresse suivante : \url{https://github.com/HKUNLP/subgoal-theorem-prover}.