Nous explorons l'usage de l'itération d'expert dans le contexte de la modélisation linguistique appliquée aux mathématiques formelles. Nous démontrons qu'avec un budget de calcul identique, l'itération d'expert — entendue comme une recherche de preuves entrelacée avec l'apprentissage — surpasse de façon significative une recherche de preuves seule. Nous observons également que, lorsqu'elle est appliquée à une collection de propositions formelles présentant une variété suffisante de niveaux de difficulté, l'itération d'expert parvient à identifier et à résoudre un curriculum de problèmes de difficulté croissante, sans nécessiter de preuves correctes associées. Enfin, en appliquant cette méthode à un ensemble de problèmes soigneusement sélectionnés manuellement, nous atteignons un état de l'art sur le benchmark miniF2F, en résolvant automatiquement plusieurs problèmes complexes issus des olympiades scolaires.