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

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

Frédéric Cuvelier

Mes domaines de prédilection ? Les ordinateurs portables et les SSD ! Mais de temps à autre, je m'autorise quelques infidélités pour des boîtiers, des alimentations ou des solutions de refroidissement...

Lire d'autres articles

Mes domaines de prédilection ? Les ordinateurs portables et les SSD ! Mais de temps à autre, je m'autorise quelques infidélités pour des boîtiers, des alimentations ou des solutions de refroidissement, tests dont je suis particulièrement friand. Je déteste l'expression "Le mieux est l'ennemi du bien" (notamment lorsqu'il s'agit de rendre mon PC silencieux), les livreurs qui arrivent sans bordereau et les coups de pieds de Polo sous le bureau. J'aime réussir mes photos-produit, améliorer les protocoles de test et cocher la case "Public" de notre interface d'édition. Féru de football, je m'essaie également à la photographie à mes heures perdues et ne recule jamais devant une petite partie de poker. Le tout saupoudré de beaucoup, beaucoup de musique.

Lire d'autres articles
Vous êtes un utilisateur de Google Actualités ou de WhatsApp ? Suivez-nous pour ne rien rater de l'actu tech !
google-news

A découvrir en vidéo

Rejoignez la communauté Clubic S'inscrire

Rejoignez la communauté des passionnés de nouvelles technologies. Venez partager votre passion et débattre de l’actualité avec nos membres qui s’entraident et partagent leur expertise quotidiennement.

S'inscrire

Commentaires

Haut de page

Sur le même sujet