canard - Le génie mathématiques, du théorème des quatre couleurs à ...

Dieu

Description

canard - Le génie mathématiques, du théorème des quatre couleurs à ...

Sujets

• mathématiques
• mathématique

Informations

• Publié par: isybokom
• Nombre de lectures: 133
• Langue: Français

Extrait

Colloquium Jacques Morgenstern

Le 18 novembre 2010

Présentation de Georges Gonthier

Le génie mathématiques,

du théorème des quatre couleurs à la théorie des groupes.

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.

Compte rendu rédigé par Antoine Pultier

École Polytech de Sophia-Nice

Rédigé le 23 novembre 2010