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.