En 2004, G. Gonthier a achevé la preuve formelle du théorèmes de quatre couleurs dans l'assistant à la preuve Coq. L'une des clefs de cette réussite est une utilisation intensive de techniques dites de ``réflexion à petite échelle'', soutenues par une extension du langage de tactiques de Coq. Cette extension, ainsi qu'une partie des bibliothèques développées pour la preuve, sont actuellement utilisées comme point de départ pour le projet de formalisation d'une somme substantielle de théorie des groupes finis, dans l'équipe Composants Mathématiques du centre commun INRIA MSR. Il s'agit cette fois de construire une preuve formelle du théorème de Feit-Thompson (1963), qui constitue un passage a l'échelle significatif pour les contributions issues de la preuve du théorèmes des quatre couleurs. Le but de cette expérience est de comprendre comment mener à bien le développement de bibliothèques de mathématiques formalisées, réutilisables et combinables. Nous tenterons d'abord de dégager les difficultés que présente la réalisation de telles bibliothèques, puis de présenter les solutions qui se dégagent de la preuve du théorème des quatre couleurs, et en particulier le langage de tactiques ssreflect. Enfin, si le temps le permet, nous présenterons brièvement les nouvelles questions soulevées par la formalisation de théorie des groupes finis, ainsi que l'état actuel de cette construction.