Georges Gonthier est un chercheur en informatique Canadien. Il travaille actuellement en France au sein du département recherche de Microsoft. Il nous a présenté aujourd’hui son travail sur la preuve du théorème des quatre couleurs, et de ses recherches sur la théorie des groupes. Le plan de son oral est contenu dans le titre de la présentation, à savoir une première partie sur le théorème des quatre couleurs, et une seconde partie sur ses travaux autour de la théorie des groupes.
Le théorème des quatre couleurs
Le théorème des quatre couleurs spécifie que n’importe quelle carte planaire peut être coloriée avec seulement quatre couleurs, sans qu’aucune zone ait la même couleur qu’une zone adjacente.
Tout l’intérêt de ce théorème consiste à essayer de le prouver, ce qui a été un véritable casse- tête depuis la fin du dix-neuvième siècle.
Au fur et à mesure de l’avancement des recherches, il a été trouvé que la solution la plus réalisable était de vérifier chaque configuration séparément, mais il restait à prouver que pour chacun de ces cas, seulement quatre couleurs suffisent.
C’est avec l’arrivée de l’informatique, qu’il a été possible de prouver toutes ces configurations de manière non rébarbative. Georges Gonthier a écrit un programme dans un langage de programmation appelé Coq, qui permet de résoudre ce type de problèmes.
Coq a une syntaxe assez inspiré du langage de mise en forme latex. Il propose de très nombreux outils permettant d’écrire rapidement une théorie mathématiques complexe.
Une grande partie du problème informatique a aussi été de trouver le meilleur format de description du plan. Georges Gonthier a mis au point une structure de données sous forme de graphe appelée hypergraphe.
Il nous a ensuite été exposé un cas pratique de l’algorithme de coloriage par récurrence, sans rentrer dans les détails. Force de constater que ça fonctionne simplement et rapidement.
Ses travaux ont donc permis de prouver la théorie des graphes. Cela a mis au jour une vielle dispute entre mathématiciens et informaticiens. Les mathématiciens veulent tout prouver, en réfléchissant et en comprenant. Les informaticiens, dans ce domaine de recherche, pensent que les preuves peuvent être vérifiées par des machines, et que ce n’est pas la peine de tout vérifier.
La théorie des groupes
À la suite de son travail qu’il a mené avec succès sur la théorie des quatre couleurs, Georges Gonthier s’est tourné sur la théorie des groupes dans un domaine plus général. Son activité actuelle consiste à prouver de nombreux théorèmes du domaine de la théorie des groupes, à l’aide de la machine.
Il a été démontré le théorème de Sylow, l’isomorphisme canonique, les groupes de Frobenius, la factorisation de Thompson, la théorie des caractères, les représentations linéaires, la théorie de Galois, l’algèbre linéaire des polynômes. Bref, beaucoup de travail a déjà été réalisé.
Le groupe de chercheurs dans lequel travaille Georges Gonthier s’attaque actuellement au théorème de Feit-Thompson, qu’il juge complexe, pour s’attaquer ensuite à la théorie de classification des groupes simples finis, qu’il décrit comme monstrueux. Il présente rapidement comment il compte résoudre le théorème de Feit-Thomspon, mais passe rapidement par manque de temps.
Georges Gonthier profite cependant de la présentation de son travail pour parler du problème des bibliothèques d’outils en informatique. Ce problème bien connu des informaticiens est qu’il est parfois plus facile de tout réécrire dans son coin plutôt que de s’adapter à aux bibliothèques pré-existantes.
Il nous présente visuellement plusieurs théories décrites avec le langage de programmation Coq, qu’il décrit comme très pratique et très succinct pour décrire ces théories. Il déclare même qu’il est plus rapide d’écrire la preuve dans le langage Coq, que la preuve dans le langage Latex.
Conclusion
Georges Gonthier propose en conclusion différents points. Il dit tout d’abord qu’il est possible de programmer rigoureusement, d’un point de vue mathématique. Pour pouvoir faire cela, il fallait effectivement utiliser un langage de programmation spécialisé dans les mathématiques, ce qui a permis d’obtenir la rigueur nécessaire.
Il déclare aussi que les assistants de preuves permettent de prouver des théorèmes complexes, comme il l’a montré sur ses travaux de la théorie des groupes.
Il pense que les machines permettent de trouver de nouvelles idées mathématiques, mais que la formalisation du problème sur la machine relève surtout de l’ingénierie.
Une question du public a été de savoir si le langage de programmation Coq a été prouvé. Georges Gonthier a par la négative, mais que des travaux étaient en cours dans ce sens. Il faut tout de même savoir qu’une fois que le langage de programmation aura été prouvé, il faudra prouver tout les composants de la machine, un à un, ce qui est quasiment impossible.
Une autre question a été de savoir si le langage de programmation Coq était utilisable dans le niveau secondaire. Là encore, il a été répondu que non, ce n’était pas la finalité du langage.
Ce fut donc un Colloquium très intéressant, sur une méthode de preuve qui va peut-être être très courante dans quelques années.
Leave a Reply