Une démonstration mathématique qui occupe 200 To, un nouveau record

06 juillet 2016 à 14h50
0
Trois informaticiens américano-britanniques viennent de réaliser la plus longue démonstration mathématique de l'histoire. Cette dernière occupe quelque 200 To d'espace disque et résout un problème vieux de 35 ans.

Vous ne connaissez sans doute pas le problème de la bicoloration des triplets de Pythagore, et il n'y a pas de mal à ça. Cette énigme est réservée à quelques mathématiciens chevronnés adeptes du dénombrement et de combinatoire.

Pourtant, son énoncé n'est pas si complexe à première vue : si l'on attribue une couleur parmi deux aux nombres entiers positifs, est-il possible que les trois nombres impliqués dans un triplet de Pythagore ne soient pas de la même couleur. En résumé, dans la fameuse formule a² + b² = c², si a et c sont de couleur bleue, b doit être rouge. Un problème auquel se butent les mathématiciens depuis des décennies.

Il y a trois ans, deux chercheurs sont parvenus à s'assurer de cette possibilité jusqu'à 1 344. Les trois scientifiques à l'origine de la publication évoquée aujourd'hui ont montré qu'au-delà de 7 824, il était impossible d'assurer une telle relation.

Pour y parvenir, Heule, Kullmann et Marek ont sollicité le supercalculateur Stampede de l'université du Texas et ses 800 processeurs, qui a cravaché durant deux jours. Un dispositif nécessaire à un dénombrement pur et dur qui a vu le supercalculateur essayer les 1 000 milliards de possibilités offertes par le problème (déduction faite des solutions trouvées par symétrie et autres artifices mathématiques).

01F4000008493652-photo-triplets-bicolor-s-de-pythagore.jpg

« Les chercheurs n'ont pas eu d'autres choix que d'y aller « en force » en énumérant et en vérifiant toutes les combinaisons possibles », explique au Journal du CNRS Laurent Simon, du Laboratoire bordelais de recherche en informatique.

Conséquence : un résultat qui occupe la bagatelle de 200 To d'espace disque. Une quantité d'information que personne ne pourra lire à moins d'avoir plusieurs milliards d'années devant soi, et qu'un logiciel spécialisé s'est chargé de décortiquer.

Ce qui a permis aux chercheurs de résoudre enfin ce problème ? De nouveaux algorithmes, regroupés au sein de ce qu'on appelle les solveurs SAT (pour satisfiabilité). Cantonnés initialement à l'informatique théorique, ces algorithmes commencent à être utilisés pour chercher des bugs dans un système d'exploitation (chez Microsoft) ou un éventuel défaut de conception dans les processeurs (chez Intel). D'où l'intérêt de ces travaux de recherche, qui peuvent paraître bien inutiles d'un premier abord.

Modifié le 01/06/2018 à 15h36
0
0
Partager l'article :

Les actualités récentes les plus commentées

Emmanuel Macron se moque des opposants au déploiement de la 5G
L'attaque d'un hôpital par ransomware pourrait tourner en homicide après la mort d'une patiente allemande
L'UE envisage de renforcer les limites d'émission de CO2 pour le secteur automobile
Clubic évolue (en douceur)
Allongé et endormi
AMD dévoile le design de sa Radeon RX 6000 sur Twitter
Le data center sous-marin de Microsoft refait surface après deux ans d'immersion
Après Bouygues, au tour de RED by SFR d'augmenter des forfaits sans possibilité de refus
Les satellites SpaceX, même peints, gâchent les nuits des astronomes
Déjà en rupture de stock, les NVIDIA RTX 3080 se vendent à prix d'or sur eBay
scroll top