La presse s'est faite l'écho de la publication de « la plus longue preuve des mathématiques » — attention surprenante pour un domaine, la preuve mathématique formelle assistée par ordinateur, qui n'est pas franchement grand public. Il se trouve que j'assistais à la conférence où résultat a été présenté ; j'aimerais ici en donner un résumé accessible et quelques commentaires.

Un public plus averti pourra se rapporter à l'article de recherche publié aux actes de la conférence ; mentionnons aussi la page « everything's bigger in Texas » où les auteurs ont rassemblé diverses informations et articles de presse.

Le problème du coloriage des triplets de Pythagore

Le problème qui se posait est de savoir si l'on peut colorer (disons, en bleu ou en rouge) les nombres entiers en respectant certaines règles. Par exemple, on peut imposer qu'on ne peut colorer de la même couleur les nombres 3, 4 et 5, au motif qu'il s'agit d'un « triplet de Pythagore » : 5 est la longueur du plus long côté d'un triangle rectangle dont les deux autres côtés sont de longueur 3 et 4. En d'autres termes, si on prend a=3, b=4, c=5 alors on a la relation a²+b²=c². On va s'interdire de colorer de la même couleur les triplets de Pythagore, et on va tenter de colorier les entiers 1, 2, 3… en respectant ces règles. La question est alors de savoir jusqu'à quel entier on va pouvoir colorier, ou en d'autres termes jusqu'où on pourra aller jusqu'à rencontrer une impossibilité. Bref, il s'agit de savoir à partir de quand on sera forcé d'avoir un triplet de Pythagore d'une seule couleur.

(Petite parenthèse. Je n'ai pas la moindre idée de pourquoi les gens s'intéressent à ce problème, s'il sert à quelque chose, s'il a des ramification ailleurs en mathématiques. Voir à la fin de l'article pour plus de discussion sur l'impact et la position de ce résultat.)

La force brutale ?

Une approche « par la force brutale » serait d'énumérer tous les cas de coloriage. Par exemple, si on essaye de colorier tous les entiers de 1 à 5, alors on a deux choix (bleu ou rouge)pour 1, deux choix pour 2, deux choix pour 3, deux choix pour 4, deux choix pour 5, et donc 2×2×2×2×2, soit 32, choix au total. Si on avait voulu colorier de 1 à 16, on aurait eu 2×2×2×2×2×2×2×2×2×2×2×2×2×2×2×2, soit 65 536, choix au total. Et pour 1 à 40, on aurait 1 099 511 627 776 possibilités. Le nombre de combinaisons croît vertigineusement !

Oh, certes, on peut y faire quelque chose. Un constat : si on a un coloriage en bleu et rouge, alors on en obtient un autre « opposé » en intervertissant le bleu et le rouge. On peut donc s'économiser un peu de travail en décidant qu'un nombre (par exemple 42) sera coloré en bleu, puisque s'il existe une solution où il est coloré en rouge, alors il existe la solution « opposée » où il est coloré en bleu. Ceci ne nous change cependant pas la vie, car il y a toujours un nombre vertigineux de combinaisons.

(Petite parenthèse de vocabulaire. Le nombre de coloriages possibles des entiers de 1 à n c'est 2×…×2 n fois, c'est-à-dire « 2 puissance n », noté 2n. On dit aussi « 2 exposant n », d'où le terme de « croissance exponentielle ». On entend parfois dans les médias ce terme appliqué à toute croissance rapide, mais le sens mathématique est celui que j'explique ici.)

En l’occurrence, les chercheurs cités on démontré que l'on peut colorier les nombres de 1 à 7824 avec deux couleurs de façon à ce qu'aucun triplet de Pythagore ne soit colorié d'une seule couleur, mais que cela est impossible pour 7825. Il est clair qu'il ne peut s'agir d'une preuve par la seule force brute : en effet, il faudrait alors énumérer 27825 combinaisons, soit un nombre à 2356 chiffres. Même en employant tous les ordinateurs disponibles actuellement pendant un temps égal à l'âge de l'Univers, on est très, très loin du compte. Pareil nombre pourrait paraître « astronomique » mais est même au-delà de tout ce que l'on peut envisager dans le monde astrophysique…

Un peu plus astucieux

On peut tenter d'être plus adroit. Si l'on sait, par exemple, que l'on doit colorier 3 et 4 en bleu, alors on peut immédiatement en conclure que 5 doit être coloré en rouge. On peut ainsi propager facilement des informations… un peu comme le joueur de Sudoku qui dit « la seule possibilité pour cette case, vu les cases déjà remplies, c'est de valoir 7, mais alors je sais que cette autre case doit valoir 8… ».

Toutefois, comme le savent les joueurs de Sudoku qui s'attaquent aux grilles « difficiles », cette propagation simple ne suffit pas. Il est parfois nécessaire de faire une hypothèse (« cette case peut être 5 ou 6, alors j'essaye 5 »), et de travailler ensuite sous celle-ci. On peut alors aboutir à une contradiction : une case pourrait n'avoir aucune valeur possible ! Il faut alors rétracter l'hypothèse faite (« comme ce ne peut pas être 5, j'essaye 6 »). Dans le problème du coloriage, on va donc être amené, lorsque la simple propagation ne suffit pas, à décider d'essayer qu'un nombre soit bleu, et si on aboutit à un conflit (une propagation conclut qu'un nombre doit être colorié en bleu et une autre propagation conclut que le même nombre doit être colorié en rouge) on se dit qu'on aurait dû choisir le rouge.

On explore ainsi une sorte d'arbre de choix : de la racine partent deux branches correspondant au premier choix (p.ex. branche de gauche, « 5 est colorié en bleu », branche de droite « 5 est colorié en rouge »), puis dans la première branche on trouve deux sous-branches (p.ex. branche de gauche, « 7 est colorié en bleu », branche de droite « 7 est colorié en rouge »), dans la deuxième deux sous-branches (p.ex. branche de gauche, « 8 est colorié en bleu », branche de droite « 8 est colorié en rouge »).

Ce que je viens de décrire est l'algorithme de Davis, Putnam, Logemann & Loveland (DPLL) (par algorithme, on entend « description d'un procédé de calcul automatique »). Mais il y a mieux !

L'apprentissage

Imaginons qu'il soit impossible d'avoir à la fois 47 et 49 en rouge et 70 et 5 en bleu. Cette règle n'apparaît pas dans les règles données initialement, qui ne parlent que de triplets de Pythagore, mais en est une conséquence. Malheureusement, l'algorithme DPLL ne s'en rendra pas compte, et pourra essayer plusieurs fois des combinaisons du style « 4, 47 et 49 en rouge et 99, 70 et 5 en bleu » ou « 3, 47 et 49 en rouge et 122, 70 et 5 en bleu ».

L'algorithme DPLL rétracte sa dernière hypothèse lorsqu'il rencontre un conflit. Ce conflit peut être analysé : « si je voulais colorier 84 en rouge, c'est parce que j'ai une règle qui dit que je n'ai pas le droit de colorier le triplet de Pythagore 80, 84 et 116 de la même couleur, or j'ai déjà colorié 80 et 116 en bleu ; j'ai colorié 80 en bleu parce que j'avais fait l'hypothèse que 60 et 100 étaient rouges, or 60, 80 et 100 forment un triplet de Pythagore ; et j'ai fait l'hypothèse que 116 était bleu. Par ailleurs, j'avais fait l'hypothèse que 84 était bleu. ». Ainsi, on est arrivé au conflit en raison des hypothèses « 84, 116 sont bleus, 60 et 100 sont rouges ». On peut donc apprendre une nouvelle règle : on ne peut jamais avoir à la fois 84 et 116 en bleu, 60 et 100 en rouge. Cette règle n'était pas initialement connue, mais je l'ai obtenue en analysant un conflit.

Ici, nous avons appris une règle supplémentaire à partir seulement de quelques étapes de raisonnement, mais en général, on peut ainsi déduire des règles qui « résument » une exploration assez fastidieuse, qu'on n'aura donc pas à refaire par la suite. Ici, une fois cette règle connue, on sait, une fois avoir sélectionné 84 en bleu, 116 en bleu, 60 en rouge, que 100 doit être bleu.

Ceci est la base de l'algorithme conflict-driven clause learning (CDCL). Je n'ai d'ailleurs pas évoqué diverses subtilités, comme par exemple comment éviter d'avoir à rechercher dans toutes la listes de règles celles qu'il faut considérer…

Je n'ai pas non plus évoqué comment les auteurs de l'article cité ont décomposé leur problème d'origine en un million de sous-problèmes, chacun résolu par CDCL, et comment ils ont réparti le million de problèmes sur 800 unités de calcul (ils travaillaient sur un super-calculateur composé de milliers d'unités de calcul, dont ils n'avaient loué que 800).

La preuve

On peut objecter qu'une telle preuve « par ordinateur » n'a guère de valeur, parce que le logiciel utilisé peut contenir des bugs.

Sur l'aspect « il est possible de colorier jusqu'à 7824 », il n'y a pas de problème. En effet, le logiciel, lorsqu'il répond positivement, produit le coloriage, qu'il est alors très aisé de vérifier.

Le problème est sur « il est impossible de colorier jusqu'à 7825 ». En effet, a priori, la correction de cette réponse repose sur le fonctionnement d'un logiciel très complexe. Il arrive que des logiciels mathématiques donnent des réponses fausses ou douteuses ; par exemple j'ai eu affaire à des logiciels qui, suivant leur version et la façon dont le même problème était présenté, répondaient « vrai » ou « faux ». On peut difficilement croire sur parole un logiciel qui se contente de répondre « il n'y a pas de solution ».

C'est là qu'intervient la fameuse « plus grosse preuve des mathématiques ». En effet, l'outil utilisé note les étapes de déduction qu'il effectue. Il produit ainsi une preuve (certes très longue, encore qu'on puisse la simplifier et la compacter) que l'on peut vérifier avec un logiciel indépendant. Il semblerait assez improbable que le logiciel ayant rédigé la preuve et le logiciel de relecture (voire les logiciels de relecture) aient tous des bugs qui laissent passer cette preuve, si elle était incorrecte, tandis qu'ils ont été abondamment testés par ailleurs.

Futile ?

On peut se dire que colorier des triplets de Pythagore est bien futile. En réalité, savoir « colorier » de deux couleurs suivant des règles d'incompatibilité, c'est extrêmement utile industriellement, car cela sert notamment à la recherche de bugs dans des circuits électroniques. Un « coloriage » réussi correspond alors typiquement à des valeurs électriques dans le circuit qui font que celui-ci produit un comportement indésirable. On dit souvent qu'un bug dans un circuit découvert uniquement après réalisation d'un prototype matériel coûte de l'ordre d'un million d'euros ; et un bug découvert après livraisons chez les consommateurs peut coûter largement plus (la société Intel, en 1995, avait dû organiser un rappel de microprocesseurs défectueux au coût de 475 millions de dollars des États-Unis).

Le tour de force des chercheurs ici a été non pas de développer un nouvel algorithme ou nouveau logiciel (encore qu'il y a eu certainement des développements spécifiques liés au découpage en un million de sous-problèmes), mais de tout mettre en œuvre pour résoudre un problème mathématique existant. On pourra objecter qu'il s'agit alors d’ingénierie ou du moins de recherche technologique et non de recherche scientifique.

Est-ce que cela en valait la peine ? Des mathématiciens comme Timothy Gowers objectent que, certes, on a une preuve d'impossibilité de coloriage en deux couleurs pour 7825, mais que cette preuve ne nous apprend rien sur le problème mathématique sous-jacent. Une vision naïve des mathématiques est que les mathématiciens cherchent à démontrer des théorèmes et que ce sont ceux-ci qui sont le but final, comme une sorte de grand prix. En réalité, avec la recherche de la preuve d'un grand théorème vient toute une réflexion, une compréhension, une théorisation ; pour reprendre une analogie assez cliché, ce n'est pas le but final qui fait l'intérêt du voyage, mais le trajet. De ce point de vue, la « grosse preuve » évoquée est assez pauvre : la produire n'a nécessité aucune compréhension de la structure des triplets de Pythagore.

Bien entendu, on peut rappeler que l'objectif posé par le président Kennedy d'aller sur la Lune, peut-être futile voire puéril en lui-même (allons-y pour montrer qu'on est plus fort que les Russkis !), a eu de nombreuses retombées technologiques, qui ne seraient peut-être pas arrivées, ou du moins pas aussi vite, s'il n'y avait pas fallu répondre au défi. Un défi peut lui aussi être intéressant non tant par son objectif final que parce qu'il a fallu réfléchir à comment le surmonter.

De ce point de vue, on pourra objecter que ni les approches ni les outils logiciels mis en œuvre n'étaient vraiment nouveaux pour cette preuve. Le logiciel CDCL utilisé, Glucose, de Laurent Simon (professeur à Bordeaux-INP) et Gilles Audemard (professeur à l'Université d'Artois), préexistait ; celui-ci met en œuvre plusieurs décennies d'idées et d'algorithmes dans le domaine de la satisfiabilité propositionnelle. L'approche cube-and-conquer de division en millions de sous-problèmes préexistait également.

Je pense cependant qu'avoir un résultat défi, identifié, visible, et qui parle aux mathématiciens professionnels, est une bonne chose pour la communication entre domaines scientifiques (je suppose que l'immense majorité des mathématiciens n'ont jamais entendu parler de preuve automatique, ou ont de fausses idées dessus ; encore que ce soit moins vrai de nos jours). Par ailleurs, du point de vue des mathématiciens, il est utile de savoir si un théorème est vrai ou faux avant de tenter d'en chercher une preuve élégante.

La couverture médiatique

Il est inhabituel qu'un résultat assez technique de mathématiques ou d'informatique sorte dans les médias grand public. Il semble qu'ici, l'origine de cette attention ait été un article dans la partie magazine de la revue Nature. J'ignore pourquoi Nature s'est penché sur le sujet (un communiqué des auteurs ? du service communication de leur université ?). Le Journal du CNRS a, avec un certain retard il est vrai, lui aussi évoqué le sujet, puis l'AFP et les médias qui suivent l'AFP. On a ici une illustration du suivisme des journalistes, qui parlent d'une chose parce que d'autres en ont parlé.

Ce qui, semble-t-il, a marqué les esprits, c'est qu'il s'agisse de « la plus grosse » ou « la plus longue » preuve des mathématiques. On pourra ironiser sur l'aspect « c'est moi qui a la plus grosse » de ces titres. On pourra également rappeler comment Richard Feynman se moquait de ces journalistes qui, pour évoquer une expérience de physique des particules, se concentraient sur un détail comme le fait que l'appareillage expérimental pesait 7 tonnes plutôt que sur le fond scientifique. Bref, ici, c'est le « record » qui est le motif.

Certains médias français ont évoqué « un algorithme de conception française » au sujet du logiciel Glucose (passons sur la différence à faire entre logiciel et algorithme). L'aspect « bien que cela ait été fait en Amérique, le fond est français » est important, un peu comme on souligne que telle ou telle région vinicole dont son succès en partie à l'expertise française exportée.

La théorie

J'ai dit l'importance des problèmes de « coloriage » (en réalité, des problèmes de satisfiabilité propositionnelle) pour l'industrie. Ces problèmes sont également très importants à titre théorique.

On l'a vu, la méthode naïve pour les résoudre consiste à énumérer un nombre exponentiel de possibilités. Les méthodes que j'ai évoqué plus bas (DPLL, CDCL) ne font pas mieux dans le pire cas. Une question légitime est donc de savoir si l'on pourrait trouver une méthode dont la croissance du coût du calcul avec la taille du problème soit seulement polynomiale (je ne définirai pas ce terme ici, mais, d'une certaine façon, ça croît bien moins vite qu'un exponentielle) — ou, à l'inverse, si l'on pourrait démontrer mathématiquement que cela est impossible. Cette question n'a pour le moment pas de réponse. On conjecture qu'il n'y a pas de méthode polynomiale, mais on ne sait pas le démontrer.

Cette question, aussi connue sous le nom de « P=NP ? » est considérée comme un problème central en informatique théorique. L'Institut Clay l'a listé parmi une liste de sept grand problèmes mathématiques « du millénaire », chacun doté d'un prix d'un million de dollars.

Le problème de la satisfiabilité propositionnelle est particulièrement important parce qu'un très grand nombre de problèmes lui ont été démontrés comme étant équivalents en un certain sens — si l'on trouve un algorithme polynomial pour l'un, alors il existe un algorithme polynomial pour les autres, et vice-versa. On peut dire (même si cette formulation est très discutable et doit être prise avec un grand de sel) qu'il s'agit de séparer ce qui est infaisable dans le pire cas, car trop coûteux, de ce qui est faisable.

Ces questions sont particulièrement importantes parce qu'elles ne dépendent pas de la technologie précise de calcul (sauf d'éventuels ordinateurs quantiques) et notamment ne se démodent pas avec le temps. Contrairement à un cliché répandu, les questions de science informatique ne sont pas forcément dépendantes d'une technologie en perpétuelle évolution à court terme je dirais même, le sont rarement.