• Informatique
  • Internet
    • Référencement
    • Réseaux sociaux
    • Site internet
    • WordPress
  • Marketing
  • Science
  • Technologie
  • Entreprise
  • Maison & Jardin
    • Immobilier
    • Intérieur
    • Travaux
  • Musique & Art
Blog Jaune – L'actualité du web
Le magazine nouvelle génération du web !
  • Informatique
  • Internet
    • Référencement
    • Réseaux sociaux
    • Site internet
    • WordPress
  • Marketing
  • Science
  • Technologie
  • Entreprise
  • Maison & Jardin
    • Immobilier
    • Intérieur
    • Travaux
  • Musique & Art
Science

Le génie mathématiques, du théorème des quatre couleurs à la théorie des groupes.

Posted on06/06/201506/06/2016 No Comments Yet
Home  >  Science  >  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.

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.

Previous Article Les coques Galaxy S4 arrivent
Next Article Ce que Google sait sur ses utilisateurs

Leave a Reply

Annuler la réponse

Ce site utilise Akismet pour réduire les indésirables. En savoir plus sur la façon dont les données de vos commentaires sont traitées.

ARTICLES RÉCENTS

  • Ouvrir un compte bancaire en ligne : simplifiez vos démarches 06/09/2023 Internet
  • Les services de l’entreprise PROGRESSIUM 23/02/2023 Entreprise
  • Achat voiture occasion Leboncoin : la bonne méthode
    Achat voiture occasion Leboncoin : la bonne méthode 02/08/2022 Internet
  • Focus sur ou acheter voiture occasion
    Focus sur ou acheter voiture occasion 31/07/2022 Internet
  • Simplifiez votre comptabilité grâce à la dématérialisation des factures
    Simplifiez votre comptabilité grâce à la dématérialisation des factures 20/06/2022 Entreprise
  • Quels critères considérer pour dénicher une entreprise de conception de cartes électroniques ? 04/05/2022 Informatique
  • ODM et OEM : quelles sont les différences entre ces modes de fabrication  ? 09/01/2022 Entreprise
  • Quelle stratégie utiliser pour une meilleure distribution et vente de vos produits 05/01/2022 Entreprise
  • Que faire pour augmenter ses performances vis-à-vis des clients 01/01/2022 Marketing
  • Comment décorer sa maison pour Noël ? 19/12/2021 Maison & Jardin

Commentaires récents

  • El ahmadi Ahmed dans Liseuse électronique les modèles Kindle
  • Lucie dans Pourquoi auriez-vous besoin d’un brise-vue ?
  • Lois dans Les avantages de l’auto-entreposage (self-stockage)
  • Johanna dans Tout ce qu’il faut savoir sur l’installation d’une piscine de jardin
  • blateil dans Liseuse électronique les modèles Kindle

Catégories

  • Entreprise
  • Immobilier
  • Informatique
  • Intérieur
  • Internet
  • Maison & Jardin
  • Marketing
  • Musique & Art
  • Non classé
  • Référencement
  • Réseaux sociaux
  • Science
  • Site internet
  • Technologie
  • Travaux
  • Wordpress

Nos articles préférés

  • Trouver des associés pour créer mon entreprise ? 10/03/2019 Entreprise
  • Comment vérifier si son annonce Adwords est visible sans pénaliser sa campagne ! 04/01/2017 Internet, Référencement
  • Pourquoi construire un tunnel de vente 14/10/2019 Non classé
  • Redaction
    Un rédacteur web : l’incontournable de la sous-traitance informatique 26/09/2016 Internet, Marketing, Référencement
  • ODM et OEM : quelles sont les différences entre ces modes de fabrication  ? 09/01/2022 Entreprise
  • L’essentiel à savoir sur la maintenance d’un site wordpress 12/10/2016 Internet, Wordpress
  • Tout savoir pour profiter des avantages de la retranscription audio 26/09/2016 Internet
  • Les services de l’entreprise PROGRESSIUM 23/02/2023 Entreprise

Tags

acheter agence appel avantages avec bien blog choisir choix comment communication conseils d'entreprise d'un dans e-commerce entreprise erreurs faire google informatique internet ligne lors maison marketing monde pour pourquoi profiter quand quel quelle quels raisons sans savoir site sont tampon toiture tout trouver utiliser votre
© Copyright 2016. BlogJaune.fr