George Gonthier - Le génie mathématique, du théorème des quatre couleurs à la classification des groupes

12:00
Thursday
4
Oct
2012
  • Keynote Speech
Place: 
Organized by: 
L’équipe "Keynotes" du LIG
Speaker: 
George Gonthier (Microsoft & INRIA)

Georges Gonthier est depuis 2003 chercheur au laboratoire de Cambridge de Microsoft Research, après treize ans à Inria et deux aux Bell Labs d’AT & T. G. Gonthier a reçu en 1988 un Doctorat de l’Université Paris XI pour son travail sur la conception, sémantique et implémentation du langage Esterel. Il a par la suite obtenu des résultats sur l’évaluation optimale des programmes fonctionnels, la conception et la vérification formelle d’un algorithme de gestion de mémoire parallèle. Il a conçu un modèle abstrait de la programmation parallèle, le join-calcul, qui a été repris par plusieurs langages de programmation (dont Visual Basic), et a été à la base de ses travaux sur la modélisation complètement adéquate (full abstraction) de propriétés de sécurité ; il a participé à la mise au point des logiciels de vol de la fusée Ariane. En 2005 il a complété la formalisation et la vérification sur ordinateur de la preuve du célèbre théorème des Quatre Couleurs ; depuis il a poursuivi cette voie de recherche en créant l’équipe "Composants mathématiques" au sein du laboratoire de recherche commun Microsoft Research-Inria, où il a développé une bibliothèque étendue de théories algébriques formelles, et qui vient tout juste d’achever son projet-phare, a preuve du théorème de Feit-Thompson. L’Académie des Sciences lui a décerné en 2011 le Grand Prix d’informatique de la Fondation EADS.

"Réalisation technique : Djamel Hadji | Tous droits réservés"

Voilà plus de trente ans que l’informatique et les ordinateurs ont fait irruption dans les mathématiques, avec la célèbre preuve du théorème des quatre couleurs par Appel et Haken. Leur rôle s’est amplifié récemment, car ils permettent maintenant de maîtriser non plus seulement des calculs, mais aussi des raisonnements dont la complexité dépasse les capacités de l’esprit humain (ou du moins, de la plupart), comme la preuve de la conjecture de Kepler ou la classification des groupes simples finis. Cependant, ces preuves "machine" exigent un changement profond de la pratique des mathématiques : un passage de l’artisanat, où chaque argument est un tribut à l’ingéniosité du mathématicien qui l’a ciselé, à une forme d’ingénierie, où les preuves sont construites à l’aide de techniques plus systématiques. On substitue ainsi des interface rigoureuses aux conventions d’usage malléables, et des algorithmes précis à l’apprentissage de méthodes par des exercices. Parvenir à codifier ainsi une part de l’état de l’art mathématique assez importante pour permettre de coder des preuves intéressantes, représente un défi considérable ; nous montrerons comment nous avons réussi à le relever, en complétant la preuve du théorème de Feit-Thompson, la première étape majeure de la classification des groupes finis.