Sites Inria

English version

Équipe de recherche

Charlotte Renauld - 28/10/2016

Georges Gonthier rejoint l’équipe SPECFUN du centre Inria Saclay – Île-de-France

Depuis sa thèse aux côtés de Gérard Berry, professeur au Collège de France, Georges Gonthier explore le domaine de la vérification informatique des théorèmes mathématiques. Après avoir travaillé pour le centre Inria Rocquencourt, le laboratoire de recherche Microsoft à Cambridge et participé à la création du laboratoire commun Inria – Microsoft Research, Georges Gonthier rejoint l’équipe SPECFUN du centre Inria Saclay – Île-de-France pour poursuivre ses projets de recherche et retrouver les équipes avec qui il collabore depuis plusieurs années. 

Retour sur l’un de ses résultats majeurs : la démonstration du théorème des quatre couleurs.

Georges Gonthier s’attache depuis le début de sa carrière à vérifier la justesse de théorèmes mathématiques grâce à l’informatique. Il s’est attaqué à des démonstrations qui représentent des centaines de pages de raisonnement et notamment le théorème des quatre couleurs avec Benjamin Werner, vérifié en 2005, et la théorie des groupes plus récemment.

Sélectionné cette année par le ministère de l'Éducation nationale, de l'Enseignement supérieur et de la Recherche comme faisant partie des découvertes majeures mises en avant dans un ouvrage « 25 découvertes pour les 25 ans de la Fête de la science », le théorème des quatre couleurs fait à nouveau parlé de lui.

« Je suis fier de faire partie de ces 25 découvertes majeures mais je me sens un peu petit à côté de certaines autres comme l’invention du Web. Ce n’est pas tout-à-fait la même portée » , souligne Georges Gonthier. « Il s’agit d’un théorème grand public au sens où il est facile à comprendre mais qui n’est pas tellement en prise avec les mathématiques modernes. Il m’a néanmoins permis de faire comprendre l’enjeu des systèmes informatiques de vérification. »

Ce théorème, qui stipule que quatre couleurs suffisent pour colorier toute carte sans que deux régions de même teinte ne se touchent, a marqué la carrière de Georges Gonthier.

« En 1979, j’ai participé, jeune lycéen, aux Olympiades de Mathématiques canadiennes et remporté un prix. Il s’agissait de passer une semaine à faire des mathématiques à l’Université de Waterloo. C’était l’occasion de mettre la main sur des ordinateurs, ce qui n’était pas aussi courant que maintenant. Durant cette semaine, j’ai découvert l’informatique, la programmation et le théorème des quatre couleurs car Waterloo était un grand centre de recherche en combinatoire. Beaucoup de mathématiciens étaient spécialistes de la question » , explique Georges Gonthier.

Ce théorème est un peu à l’origine de la vocation scientifique de Georges Gonthier, et c’est vers l’an 2000 qu’il a décidé de s'intéresser de nouveau au problème : « La preuve développée sur le sujet en 1976 avait quelque peu mal vieilli et avait été réactualisée et simplifiée en 1995. Ce qui en faisait un sujet plausible pour un éventuel travail de formalisation. » En utilisant la théorie des cartes, Georges Gonthier et Benjamin Werner ont résolu le problème en 2005.

Au sein de l’équipe SPECFUN, Georges Gonthier compte aujourd’hui poursuivre ses travaux de recherches mais également définir les contours de nouveaux objectifs. « Le travail effectué sur la théorie des groupes, par exemple, a permis de développer beaucoup de contenu en algèbre mais il reste des fondements non résolus. Nous allons reprendre le travail et définir où mettre les moyens pour faire avancer la recherche dans ce domaine. »

Mots-clés : Specfun Geroges Gonthier Théorème 4 couleurs INRIA Saclay - Île-de-France

Haut de page

Suivez Inria tout au long de son 50e anniversaire et au-delà !