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

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).

« 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 02/12/2020 à 09h45
Soyez toujours courtois dans vos commentaires.
Respectez le réglement de la communauté.
0
0

Actualités récentes

Comparatif des meilleurs VPN (2021)
Meilleurs jeux mobiles gratuits : découvrez notre Top 10
Bon plan gaming : le casque filaire HyperX Cloud Alpha S disponible à moins de 100€
Genshin Impact : la version PS5 arrive le 28 avril avec plusieurs améliorations
Acer Nitro 5 : un PC portable gaming 17.3
Votre nouvelle Smart TV Samsung à moins de 30€ avec la fibre Bouygues Telecom
Mercedes dévoile EQS, sa berline électrique de luxe et ses 770 km d'autonomie
L'excellent casque Bose 700 profite d'une promo immanquable chez Cdiscount
Bon plan VPN : Top des bons plans à saisir chez CyberGhost, NordVPN et Surfshark
Amazon revendique 200 millions d'abonnés à Prime
Haut de page