le mercredi 06 juillet 2016

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

Triplets bicolorés de Pythagore

« 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 06/07/2016 à 16h29
Commentaires