Trois scientifiques ont prouvé que la bicoloration des triplets de Pythagore n'était pas possible pour tous les entiers. Au-delà de la résolution d'un problème mathématique vieux de 35 ans, la méthode utilisée (solveur SAT) est très intéressante et laisse entrevoir de nombreuses possibilités dans tous les domaines scientifiques.
Les mathématiciens sont un peu joueurs et se posent parfois de drôles de questions, généralement bien difficiles à résoudre. Mais avec les ordinateurs modernes et les avancées dans le domaine de l'algorithmique, la solution est à portée pour certaines énigmes. C'est notamment le cas de... la bicoloration des triplets de Pythagore.
Deux couleurs, trois nombres et des milliards de milliards de possibilités
Le CNRS en donne la définition suivante : il s'agit de savoir s'il « est possible de colorier chaque entier positif en bleu ou en rouge de telle manière qu’aucun triplet d’entiers a, b et c qui satisfait la fameuse équation de Pythagore a² + b² = c² soient tous de la même couleur ? Par exemple, pour le triplet 3, 4 et 5, si 3 et 5 sont coloriés en bleu, alors 4 doit être rouge ».
Si la question parait simple en apparence, on se doute qu'elle se complique de manière exponentielle lorsque le nombre de triplets à prendre en compte augmente. En 2013, les chercheurs Joshua Cooper et Chris Poirel arrivaient à trouver une solution pour « colorier » des nombres entiers jusqu'à 1 344 sans avoir de triplets qui ne comportent que des nombres de la même couleur. Pour autant, cela ne permet pas de répondre à la question pour les nombres supérieurs. Simplement peut-on affirmer que la réponse est oui jusqu'à 1 344, sans que cela ne laisse présager quoi que ce soit de plus. Frustant pour les mathématiciens, mais un défi intéressant pour d'autres.
Dans un article soumis pour publication le 3 mai, et repris récemment par le journal du CNRS, trois scientifiques (Marijn J. H. Heule, Oliver Kullmann et Victor W. Marek) sont enfin parvenus à trouver la solution ce « problème mathématique ouvert depuis 35 ans ». Et leur réponse est sans ambiguïté : non, il n'est pas possible de colorier des entiers de cette manière.
Jusqu'à 7 824 tout va bien, à 7 825 c'est impossible
Leur étude montre tout de même qu'il est possible de colorier les entiers positifs jusqu'à 7 824 de manière à ce que tous les triplets de Pythagore aient des nombres des deux couleurs. Les scientifiques ajoutent qu'il existe même plusieurs manières d'y arriver. Les cases blanches dans la représentation ci-dessous sont sans contrainte et peuvent donc être indifféremment bleues ou rouges pour que les conditions du problème soient remplies. Néanmoins, cela devient impossible à partir de 7 825. Inutile d'aller plus loin donc.
Au-delà de cette réponse qui n'apporte rien de plus que la satisfaction de l'avoir trouvée (et qui est présenté à la conférence SAT 2016 à Bordeaux), la méthode utilisée par le trio de scientifiques est très intéressante à analyser. Laurent Simon, du Laboratoire bordelais de recherche en informatique (LaBRI), explique en effet que « pour le prouver, 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 ».
Une solution qui fonctionne pour les 7 824 premiers entiers (les cases blanches sont sans contrainte de couleur)Un supercalculateur à la rescousse
Et il y en a des combinaisons : 2^7825, soit environ 10^2355 possibilités à analyser, ou encore 1 suivi de 2 355 zéros. Afin de réduire le champ des possibilités, et donc gagner du temps de calcul (qui prendrait de toute façon trop temps), les chercheurs ont mis en œuvre différentes techniques issues de la théorie des nombres. Ils sont ainsi redescendus à 1 000 milliards (1 000 000 000 000) de combinaisons « seulement ». Sans commune mesure avec le nombre total de possibilités à analyser, mais cela reste tout de même important.
À titre de comparaison, il y a 5 x 10^20 coups possibles au jeu de dames (qui est résolu, c'est-à-dire que toutes les parties possibles et imaginables ont été calculées et enregistrées), tandis que le mathématicien Claude Shannon, estime qu'il y aurait environ 10^120 parties « intéressantes » à jouer aux échecs. Au jeu de Go, une partie comporte 1,4 x 10^768 coups possibles et les intelligences artificielles commencent seulement à prendre le dessus sur les humains, là encore sans calculer toutes les possibilités, mais en ayant recours à l'apprentissage profond et par renforcement. Nous avions détaillé tout cela au sein de cette actualité.
Daniel Le Berre, du Centre de recherche en informatique de Lens (Cril), explique que « l’astuce de l’équipe a ensuite été de découper tous ces cas possibles en un million de paquets différents pour pouvoir résoudre le problème plus facilement ». Les opérations ont ensuite été effectués sur le supercalculateur Stampede de l'université du Texas. Celui-ci comprend plus de 522 000 cœurs de traitement, peut effectuer un billiard (10^15) opérations par seconde et revendique la 116e place mondiale des supercalculateurs.
La solution « pèse » la bagatelle de 200 To
« Il aura fallu alors deux jours au supercalculateur [...] pour passer en revue toutes ces possibilités et apporter la preuve tant attendue, générant pour cela 200 téraoctets de données » indique le CNRS dans son journal. Une fois la « preuve » apportée sur un plateau d'argent par le supercalculateur, encore fallait-il la vérifier.
Le résultat est d'une « taille phénoménale, équivalente à tous les textes numérisés détenus par la bibliothèque américaine du Congrès ; c’est la plus grande preuve mathématique jamais produite » et « Il faudrait 10 milliards d’années à un être humain pour la lire » explique le centre de la recherche scientifique. Bref, c'est là encore un ordinateur qui s'est chargé de cette besogne, mais avec un programme différent.
Les solveurs SAT au cœur de la résolution de ce problème
Le CNRS ajoute que cette petite révolution a été possible grâce aux solveurs SAT, « de nouveaux algorithmes très efficaces pour résoudre ces problèmes [...] Dans le langage informatique, SAT signifie « satisfiabilité ». Il s’agit d’un formalisme logique qui capture toute la difficulté d’un problème combinatoire pour tenter ensuite de le satisfaire ». Emmanuelle Filiot, de l'université libre de Bruxelles, expliquait en 2012, qu'un « solveur SAT est un programme qui décide automatiquement si une formule de logique propositionnelle est satisfaisable ».
Deux exemples parmi d'autres : les jeux de Sudoku (voir ici pour un exemple pratique) ou un démineur, de « très simples problèmes qui peuvent être appréhendés et résolus très facilement par ce formalisme », même si cela peut aller beaucoup plus loin. Daniel Le Berre de l'université d'Artois, explique au CNRS que s'ils étaient pendant un temps réservé à l’informatique théorique, leur utilisation explose et ils permettent désormais « de résoudre des problèmes de plus en plus difficiles ».
Traitement rapide des problèmes avec de nombreuses variables et clauses
Dans les exemples d'applications actuelles, il est question de champs assez vastes allant du diagnostic d'erreur sur les circuits électroniques à l'intelligence artificielle. En 2012, Gilles Schaeffer, directeur de recherche au CNRS, ajoutait même que « l’utilisation de solveurs SAT génériques concurrence les algorithmes ad hoc pour certains problèmes d’optimisation combinatoire ».
C'est encore trop obscur pour vous ? En 2012 toujours, le blog d'Ozwald donnait quelques exemples pratiques (même si ces informations ont quatre ans, l'idée générale reste la même) : « Là où ça devient intéressant, c'est qu'on peut faire beaucoup plus que des mini problèmes. Parmi les fichiers cnf mis à dispositions ici on en trouve un qui compte 1 040 variables et 3 668 clauses que Minisat résout (comme "UNSATISFIABLE") en... 0m0.013s ! Dans la même catégorie on trouve un autre fichier de test contenant 1501 variables et 3575 clauses que Minisat résout (en "SATISFIABLE" avec une solution exemple) en 0m0.008s ». Un traitement des plus rapides donc, et les choses ont encore dû s'améliorer depuis.
Vous l'aurez compris : de manière générale, les solveurs SAT permettent parfois d'obtenir de bons résultats, surtout lorsqu'il n'existe pas d'autres options que la « force brute », ce qui est exactement le cas dans la bicoloration des triplets de Pythagore.
Pour ce dernier, c'est le programme Glucose qui a été utilisé, un solveur SAT développé par Gilles Audemard et Laurent Simon. Il a été récompensé à plusieurs reprises lors de compétitions internationales et le code source peut être téléchargé par ici. En 2014, c'est également Glucose qui avait déjà permis de construire la plus longue preuve mathématique de l'époque note le CNRS.
Microsoft et Intel utilisent déjà les solveurs SAT, d'autres applications en route
Ce dernier ajoute que, « aujourd’hui, Microsoft fait appel à ces algorithmes pour tester ses nouveaux systèmes d’exploitation. Il s’agit alors d’identifier une succession d’instructions parmi des millions susceptibles de causer un bug dans le logiciel ou au contraire de prouver qu’il n’y en aura pas. Même chose pour Intel qui vérifie grâce à ces outils le bon fonctionnement de ses microprocesseurs. Et le nombre d’applications ne cesse de croître en robotique, en bio-informatique ou encore en cryptographie ». L'intelligence artificielle et les solveurs SAT sont aussi étroitement liés, comme on peut facilement s'en douter.
Laurent Simon, coauteur du logiciel Glucose, explique que « ce dernier résultat [NDLR : la bicoloration des triplets de Pythagore] montre qu’il est possible de s’attaquer avec cette méthode à des problèmes mathématiques combinatoires extrêmement difficiles, pour lesquels aucune approche classique à la main n’est encore disponible. Il préfigure probablement la fin d’autres conjectures similaires qui résistent encore aujourd’hui aux mathématiciens ».
Il faut donc s'attendre à ce que les choses évoluent, que ce soit pour les mathématiques, l'informatique et les sciences de manière générale. Dans tous les cas, il reste une question, comme le note de manière ironique Gérad Villemin sur son blog : « Ce type de preuve établit des faits sans les expliquer. Pourquoi 7 824 ? ». On vous laisse méditer sur cette nouvelle question...
Commentaires (71)
#1
lol cette nouvelle change ma vie
" />
#2
« Ce type de preuve établit des faits sans les expliquer. Pourquoi 7 824 ? »
" />
Parce que 42.
A+
#3
Comme précisé dans l’actu, le plus important ce n’est pas la réponse à la question, mais la manière d’y arriver ;)
#4
Très intéressant, merci!
#5
Merci pour cet article très intéressant
" />
Et c’est sur que l’algorithme ne peut pas fournir une explication logique sur le chiffre “7824” il n’est pas la pour ça. Mais les chercheurs vont se pencher dessus, c’est peut-être lié à des problèmes combinatoires à partir de 3 éléments => 3 chiffres, 2 couleurs, 2 équations (jamais 3 bleus ou 3 rouges / a²+b²=c²).
#6
J’ai lu, mais à mon avis, il me faut le relire :)
" />
Parce que je ne suis pas sûr d’avoir tout compris.
#7
Ca n’a rien d’une preuve ni d’une démonstration, vu que ce n’est pas démontré pour TOUTES les combinaisons de nombre possibles. C’est juste une confirmation numérique que ca semble fonctionner jusqu’à un certain rang.
La preuve, c’est lorsqu’on aura démontré que c’est tout le temps vrai ou pas, ou pourquoi sur un certain rang
EDIT : ici on a juste montré qu’une propriété empirique fonctionne sur un intervalle donné, sans trop savoir pourquoi, mais on a poussé les calculs pour savoir jusqu’à quand “ca ne marche plus”
#8
non justement. Une (et même plusieurs) solution existe pour les 7824e premiers entiers, mais c’est impossible à partir du 7825e. Donc pas la peine de continuer 
" />
#9
#10
Il reste à en faire la démonstration
" />
" />
Le match déduction vs induction continue
#11
Pour montrer qu’une propriété est fausse un contre exemple suffit. La on a un contre contre exemple (trouvé de maniere empirique certe mais ça reste un contre exemple) ça suffit pour dire que la propriété est fausse, pas la peine de chercher plus loin.
#12
Non c’est suffisant pour une démonstration (qui infirme l’énoncé)
“Un nombre puissance 3 ne peut pas être négatif”
Heuuu … “-1”
Il est prouvé que c’est faux.
Pas besoin de chercher toute les combinaisons. C’est ce qu’ils ont fait.
Ils ont prouvé que c’est vrais dans un interval cependant.
#13
Et d’après l’article, ils ont également prouvé que c’est impossible au delà de 7824 (calcul de toutes les combinaisons pour 7825).
Je vais chercher un peu plus pendant mes vacances moi sur ce thème moi, ca va m’occuper ^^
#14
Balèze, on devrait soumettre la question des voyages en hyper-espaces, en lui refilant tout nos connaissance, on sait jamais.
" />
#15
Et la conjecture de Riemann, on est ou ?
" />
#16
J’attends toujours la résolution du mystère qu’est la femme via ces supercalculateurs
" />
#17
C’est un mystère sans solution.
" />
#18
#19
#20
Bon après avoir relus la définition du problème une bonne dizaine de fois, je crois (
" />) que j’ai compris pourquoi çà prend du temps : c’est principalement à cause “des cases blanches”. Dès qu’on a une case blanche il faut faire les tests en double… et si on croise une autre blanche rebelotte, ca fini par prendre de la place en mémoire forcément 
" />
Les vases blanches étant des nombres qui peuvent être bleu ou rouge, ou finir par être bloqué sur une couleur…
#21
J’ai même pas compris l’énoncé du problème 
" />
#22
#23
Ca va déjà plus vite avec la touche “Tab”
" />
#24
J’ai jamais penser qu’ils le trouverais en quelque jours, mais les calculateurs qui ne sont plus utiliser, peuvent se pencher dessus quelques dizaines d’années.
#25
j’ai absolument rien pigé au problème mais…
" />
" />
" />
200 To de données !
ça en fait du gribouillage High Tech
je vais refiler l’article a un pote matheux, il va avoir le kikitoudur
#26
on est deux …
" />
#27
#28
Au pif, un problème mathématique sans application concrète à priori.
#29
Grossièrement, les mecs ont 2 crayons de couleur et veulent savoir s’ils peuvent colorier des cases sans déborder
" />
#30
#31
c’est carrément ça
" />
#32
#33
#34
En gros, t’as des dominos bizarres (ils ont trois « côtés ») et un peu spéciaux (les numéros sur les trois côtés respectent une relation mathématique : a²+b²=c²) et tu veux savoir s’il est possible de colorer d’une seule couleur chaque numéro sur l’ensemble des dominos avec seulement un crayon bleu et un crayon rouge (par exemple tous les 4 en bleu, tous les 5 en rouge, etc.) , tout ça sans qu’il y ait un domino qui soit entièrement coloré de la même couleur.
#35
En relisant l’article de wikipédia, je me suis fait la réflexion que ça correspondrait à faire du surf sur une « vague » de l’espace-temps. Du coup je me suis posé la question suivante : est-ce qu’il serait possible de « surfer » sur une onde gravitationnelle ?
" />
Vu que tu as fait pas mal de recherches sur ce genre de sujet pour tes nouvelles, tu peux peut-être me répondre ?
#36
Je me réponds à moi-même puisque la réponse est toute bête : oui, puisque la gravitation est une déformation de l’espace-temps. Par contre, elle ne se déplace qu’à la vitesse de la lumière, donc ça ne devrait pas permettre d’aller plus vite…
#37
#38
pour le prouver, 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
News@11
Des chercheurs ont résolu un problème de dénombrement en testant toutes les combinaisons possibles.
/News@11
#39
Y a de grandes chances que ce problème soit indécidable.
#40
#41
Trop de variables aléatoires changeants d’états en permanence j’en ai bien peur en effet 
" />
#42
#43
Ils ont eu du bol que ce soit faux, si la conjecture avait été vraie le truc tournerait encore, et pour rien d’ailleurs… Je me demande s’ils avaient une intuition que ce serait faux aux alentours de 7800 ou s’ils avaient prévu de faire tourner le truc pendant les vacances pour voir en espérant qu’ils en tireraient de quoi faire un article.
#44
#45
#46
#47
Les mathématiciens cachent leur bornes sous des flots de formules
#48
#49
#50
#51
#52
#53
#54
Et bah c’est plus clair comme ça en tout cas =)
Le premier exemple était déjà trop nébuleux pour moi :p
#55
#56
Au contraire, les blanches tendent à simplifier le problème. Un certain nombre d’entre elles ne font pas partie de triplets pythagoriciens (il me semble que c’est le cas de 1 et 2), pour d’autres, elles font partie d’un triplet dont les deux autres membres sont de couleur différente. Cela tend à te simplifier ton problème.
Pour l’explosion combinatoire, c’est expliqué dans l’article : 2^7385 (chaque case peut être soit bleue, soit rouge). Après, un premier moyen simple, c’est de réduire ça aux seuls triplets pythagoriciens (tous les nombres entiers ne font pas partie d’un triplet) : ça doit déjà enlever quelques ordres de grandeur. Je suppose qu’ils ont fait en plus de ça d’autres simplifications moins triviales, et ensuite « use the (brute) force ».
#57
Car 7+8+2+4=21=42⁄2 
" />
CQFD JQCT.
#58
C’est efficace avec des problèmes de complexité NP ces solveurs SAT ?
#59
Oui, cf ici pour plus de détails (cours de Gilles Schaeffer) 
" />
#60
Merci beaucoup pour cet article.
Très franchement, je ne suis pas sur d’avoir tout compris. Mais, j’apprécie infiniment que les journalistes se décarcassent pour solliciter mon neurone sur un sujet qui n’avait à priori aucune chance de m’intéresser.
Merci à tous ceux qui collaborent à ce site et qui m’ont donné envie de rejoindre les abonnés.
#61
Euh non toutes les “cases” étant testés (pas forcement une valeur “c”, mais obligatoirement une valeur possible de a ou b), tu dois tester si çà marche en rouge, bleu (ce qui implique une couleur qui peut varier pour c du coup) et ainsi de suite.
#62
Merci !
" />
#63
Çaexiste mieux que la perfection déjà incarnée que nous sommes
" />
#64
Ah bah voilà, il ne me reste plus qu’à le commander et potasser tout ça
" /> Merci 
" />
#65
#66
Oh joli !!!!
" />
#67
Le compte est bon Michel ! On va maintenant passer aux lettre. Consonne ou voyelle ?
#68
Un domino à trois côtés est un Triomino.
#69
Les opérations ont ensuite été effectués sur le supercalculateur Stampede de l’université du Texas.
On n’a pas de calculateurs suffisants en France pour ce genre d’applications ?
#70
La liste d’attente pour traiter les problemes qui leur sont soumis peut etre longue. Un supercalculateur qui ne travaille pas est une perte sèche.
C’est comme les grues mobiles en france. Pour l’accident de brétigny, c’est une belge qui est venu. On en a en france, mais aucune n’était disponible immédiatement (/sous 7 jours).