Composants mathématiques pour la théorie des groupes

Formal proof systems have evolved considerably in recent years. Success stories like formal proofs of the four color theorem or the prime numbers theorem have shown that formal proof systems have reached a level of maturity that enables them to tackle non-trivial mathematical problems. Nevertheless, the use of formal proof systems in mathematics is very limited. One of the reasons that explains this situation is the lack of formal proof libraries. This thesis focuses on the development of mathematical components for finite groups theory. It is part of a project that aims to formalize the Feit-Thompson theorem on the classification of finite groups. The main goal of this work is to apply software engineering techniques to facilitate the reuse and organization of large scale formal mathematics developments like the formalization of the Feit-Thompson theorem. This thesis presents the first formalization of the Cayley-Hamilton theorem on polynomials and matrices. It presents also developments on the representation theory of finite groups which is a necessary component for the formalization of the Feit-Thompson theorem. In particular, it presents a formalization of the theory of modules over a field or an algebra and a formalization of the Maschke theorem. These developments have been done in the Coq system and with the SSReflect extension.Les systèmes de preuves formelles ont connu ces dernières années des évolutions importantes. Des travaux récents, comme la preuve formelle du théorème des quatre couleurs ou celle du théorème des nombres premiers, ont montré que ces systèmes ont atteint un niveau de maturité leur permettant de s'attaquer à des problèmes mathématiques non triviaux. Malgré cela, l'utilisation des systèmes de preuves formelles en mathématique reste très limitée. Un des arguments qui est avancé pour expliquer cette situation est le manque de bibliothèques de preuves formelles. Cette thèse s'intéresse au développement de composants mathématiques pour la théorie des groupes finis. Elle entre dans le cadre du travail de formalisation du théorème de Feit-Thompson sur la classification des groupes finis. L'objectif principal dans ce travail est d'appliquer les techniques de génie logiciel pour faciliter la réutilisation et l'organisation des développements mathématiques formelles de grande échelle, comme la formalisation du théorème de Feit-Thompson. Cette thèse présente une première formalisation du théorème de Cayley-Hamilton sur les polynômes et les matrices. Elle présente aussi des développements sur la théorie des représentations des groupes finis qui est une composante nécessaire à la formalisation de la preuve du théorème de Feit-Thompson. En particulier, elle présente une formalisation de la théorie des modules sur un corps ou sur une algèbre ainsi qu'une formalisation du théorème de Maschke. Ces développements ont été faits dans le système Coq et avec l'extension SSReflect