La clôture s’achète

1. Deux nombres pairs

Été 1954, à l’Institut d’études avancées de Princeton. On y trouve un ordinateur à tubes électroniques, l’un des tout premiers construits au monde. Sa mémoire contient en tout mille vingt-quatre mots machine. Le programme, les formules à traiter et tout ce que les calculs produiront en cours de route doivent tenir dans cet espace.

Un logicien de vingt-six ans lui écrit un programme. Il s’appelle Martin Davis.

À cette époque, les ordinateurs font presque tous du calcul numérique. Ce programme, lui, se prononce sur des énoncés. On lui soumet une phrase concernant les entiers ; il suit pas à pas des règles immuables. L’algorithme de décision sur lequel il repose garantit qu’une machine idéale, dont la mémoire ne serait pas limitée, finira par s’arrêter et donnera la bonne réponse. La machine réelle peut, elle, manquer de mémoire bien avant. L’expression « intelligence artificielle » n’a pas encore été inventée.

Bien des années plus tard, Davis écrira que le plus beau succès de son programme aura été de démontrer que la somme de deux nombres pairs est encore paire.

Il se moque de lui-même, mais il n’exagère en rien. Une machine qui remplit une pièce, et pour fait d’armes une vérité connue des écoliers.

Deux questions se présentent aussitôt. Dans toute l’étendue des mathématiques, pourquoi est-ce précisément ce petit territoire que l’on peut confier sans crainte au jugement d’une machine, avec la certitude que, si elle répond vrai, c’est vrai ? Et puisqu’elle sait trancher, pourquoi son meilleur résultat est-il si modeste ? À la seconde question, la machine apportera très vite sa propre réponse, bien plus lourde que la boutade de Davis. Pour la première, il faut remonter vingt-cinq ans en arrière, à Varsovie.

Mardi 24 septembre 1929, dix heures et demie du matin. Le premier Congrès des mathématiciens des pays slaves entre dans sa deuxième journée à Varsovie. La première communication de la première section est confiée à un étudiant qui n’a pas encore obtenu sa maîtrise. Il s’appelle Presburger, étudie les mathématiques à l’université de Varsovie et a vingt-quatre ans.

Arrêtons-nous un instant sur ce congrès. Fraenkel parle de Cantor à l’ouverture ; Tarski donne lui-même deux conférences. La plupart des participants sont polonais, mais certains sont venus du Japon, d’autres du Texas. Les actes acceptent cinq langues européennes, parmi lesquelles l’allemand et le français dominent. À la fin du congrès, un groupe prend le train de nuit, en voiture-lits, pour Poznań. Kuratowski y poursuivra les conférences avec la topologie.

La communication de Presburger paraîtra dans ces actes : dix pages de texte, suivies d’une page de supplément non numérotée. Le titre annonce un travail sur la complétude d’un système arithmétique des entiers dont l’addition est la seule opération. Au début, une note de bas de page presque invisible précise deux choses : le résultat a été obtenu en mai 1928 ; le problème a été posé par Tarski.

Ce problème venait de loin. Hilbert et son école poursuivaient alors une ambition immense : trouver un procédé mécanique unique capable de décider si une formule donnée de la logique du premier ordre est universellement valide. C’était le « problème de la décision ». Il n’y avait pas encore d’ordinateurs. Un procédé mécanique était une suite de règles sur le papier, assez strictes pour qu’une personne ignorant tout des mathématiques puisse les appliquer et parvenir à la bonne réponse. L’école de Hilbert voulait de telles règles pour l’ensemble des mathématiques.

Tarski en avait découpé un tout petit morceau pour le confier à un étudiant. La réponse rapportée par Presburger était : sur ce morceau, oui. Il existe un fragment de l’arithmétique des entiers dans lequel chaque énoncé peut être déclaré vrai ou faux, au moyen d’un procédé uniforme qui, quel que soit l’énoncé soumis, livre sa réponse après un nombre fini d’étapes. Vingt-cinq ans plus tard, c’est ce procédé que Davis installera dans des tubes électroniques. Avant de pouvoir être construite, la machine avait été construite sur le papier.

Les épisodes précédents racontaient presque tous l’histoire inverse. La théorie des ensembles avait engendré des contradictions ; la querelle des fondements avait duré vingt ans ; un théorème avait établi qu’une arithmétique dont un programme peut énumérer les axiomes, dès lors qu’elle est suffisamment forte, ne peut être à la fois cohérente et complète. Et voici un étudiant qui, dans une salle de cours bondée, apporte dix pages d’une arithmétique à l’abri de ces ennuis. Son résultat date de 1928, sa communication de 1929 : trois ans et deux ans, respectivement, avant la publication de ce théorème en 1931.

La question mérite donc d’être posée : jusqu’où faut-il affaiblir une arithmétique pour qu’elle soit complète et dispose d’une machine capable de tout y décider ? La réponse est bien plus compliquée, et bien plus intéressante, que la simple suppression de la multiplication.

2. Ce qu’on ne peut pas dire

Avec des pièces de trois et de cinq unités seulement, peut-on composer exactement une somme donnée ? Onze, oui. Sept, non. Et existe-t-il un montant à partir duquel toutes les sommes deviennent possibles ? Oui : à partir de huit, aucune ne manque.

Le langage de Presburger permet d’exprimer chacun de ces énoncés. Sa procédure permet de les décider tous.

Il s’agit d’une arithmétique des entiers où la seule opération est l’addition. Son langage dispose du signe plus, des constantes zéro et un, de l’égalité et de l’ordre, ainsi que de mots tels que « il existe » et « pour tout ». On peut parfaitement y parler du triple d’un nombre : il suffit d’additionner trois fois le même nombre. Presburger le précisait en présentant ses axiomes : faute de signe de multiplication, cette écriture doit se comprendre comme une addition répétée un nombre fixé de fois. Dire que plusieurs nombres ont pour somme un autre nombre, de combien l’un dépasse l’autre, qu’un nombre a pour reste trois dans la division par sept, ou que plusieurs entiers satisfont simultanément toute une série de ces conditions : tout cela s’exprime dans ce langage, et tout cela peut être décidé. Ce n’est pas un champ de ruines. C’est un monde petit, mais entier.

Ce qui manque, c’est la multiplication de deux variables. Certaines relations et propriétés deviennent donc impossibles à exprimer dans ce langage : qu’un nombre soit le produit de deux autres ; qu’il soit un carré ; qu’il soit premier ; qu’un nombre en divise un autre, lorsque les deux sont des variables.

« Impossible à exprimer » doit s’entendre dans toute sa force. Il ne s’agit pas d’une difficulté de démonstration : aucune formule du langage ne permet de dire cela de façon générale. Les ensembles de nombres que ce langage sait délimiter ont une forme très régulière : assez loin, leur disposition se répète périodiquement. Les carrés et les nombres premiers ne suivent pas ce régime. Ils n’ont donc même pas de nom dans ce monde. « Ce nombre est-il premier ? » est l’une des plus anciennes questions de la théorie des nombres. Dans le monde de Presburger, on ne peut pas la poser.

C’est une perte de pouvoir d’expression, et non de pouvoir de démonstration. Les deux ne se confondent pas.

Trois mots vont désormais suivre des chemins distincts. La complétude signifie que, pour chaque énoncé de son langage, la théorie tranche dans un sens ou dans l’autre. On n’y rencontre pas les phrases de l’épisode 17, impossibles aussi bien à démontrer qu’à réfuter. La décidabilité dit autre chose : il existe un procédé mécanique uniforme auquel on peut soumettre n’importe quel énoncé de ce langage, et qui s’arrêtera nécessairement après un nombre fini d’étapes en donnant la bonne réponse.

Un pont très court relie les deux. Supposons une théorie complète dont on puisse énumérer les axiomes un à un. On peut alors énumérer également toutes les démonstrations. Face à un énoncé, on poursuit cette énumération jusqu’à voir apparaître une démonstration de cet énoncé ou de sa négation. La théorie étant complète, l’une des deux finira par apparaître ; le procédé s’arrêtera donc. Presburger le dit dès le début de son article : le caractère effectif de sa preuve de complétude fournit en même temps une méthode pour déterminer si un énoncé est vrai. Une démonstration, et voici une machine livrée avec.

Il reste quelque chose à entendre dans le mot « complète ». Il ne signifie pas que la théorie sait tout. Il signifie seulement qu’elle peut trancher tout ce que son langage permet de dire. Ce qu’elle ne peut pas exprimer, elle ne peut même pas le demander. Moins un système a de choses à dire, plus il lui est facile d’être complet. Cela ressemble à un compliment. C’est en réalité la première ligne de la facture.

Le troisième mot est la faisabilité. Qu’une méthode existe est une chose ; qu’elle puisse réellement fonctionner avec le temps, la mémoire et les machines dont nous disposons en est une autre. Les deux premières notions sont logiques. La troisième oblige à regarder aussi la complexité et les ressources réelles. Un ordinateur doté de mille vingt-quatre mots de mémoire va bientôt rendre la différence tangible.

3. Faire disparaître un mot

La méthode au cœur de cette machine s’appelle l’élimination des quantificateurs. Pour l’arithmétique de Presburger, on commence généralement par enrichir le langage de prédicats de congruence à module fixé, ou de divisibilité par un entier fixé ; c’est dans cet enrichissement équivalent que l’on élimine les quantificateurs.

Un énoncé peut contenir des expressions comme « il existe un nombre » ou « pour tout nombre ». Éliminer le quantificateur ne consiste pas à deviner quel est le nombre en question. On remplace l’énoncé entier par un énoncé exactement équivalent qui ne mentionne plus ce nombre.

Prenons l’exemple le plus simple. Existe-t-il un entier qui, ajouté à lui-même, donne un nombre fixé ? La question contient « existe-t-il un entier ». Une fois ces mots éliminés, il ne reste qu’une condition portant sur le nombre donné : celui-ci doit être pair.

C’est tout. « Il existe un entier dont la somme avec lui-même est ce nombre » devient « ce nombre est pair ». La seconde phrase ne parle plus de l’entier à chercher ; sa condition se vérifie directement. L’article de Presburger contient de petits exemples de ce genre : une équation additive précédée de « il existe » se transforme en conditions qui ne portent plus que sur des restes et sur les autres nombres. Le plus beau succès de la machine de Davis concernait, lui aussi, des nombres pairs. Dans ses tubes électroniques, c’étaient précisément ces remplacements successifs qui s’effectuaient.

Passons dans un autre monde. Existe-t-il un nombre réel dont le carré soit égal à un nombre donné ? Une fois le quantificateur éliminé, il reste cette condition : le nombre donné est supérieur ou égal à zéro. Le nombre qu’il fallait chercher a disparu. Seul demeure un énoncé portant sur celui que l’on connaissait déjà.

En répétant l’opération, on finit par transformer un énoncé sans aucune variable libre en une condition dont on peut lire directement la vérité ou la fausseté. Voilà d’où vient la procédure de décision. Le pas décisif de Tarski a été de porter cette idée dans le monde des égalités et des inégalités polynomiales sur les réels. On y trouve l’addition, la multiplication, l’ordre et les quantificateurs. Et les quantificateurs s’éliminent encore.

Une discipline se trouve entraînée dans le mouvement : la géométrie. La géométrie élémentaire dont parle Tarski est celle des problèmes que l’on peut traduire, une fois des coordonnées choisies, en formules algébriques sur les réels. Dans un repère cartésien fixé, les points sont représentés par des coordonnées réelles ; distances, alignement, perpendicularité et cercles se décrivent par un nombre fini d’égalités ou d’inégalités polynomiales. Les propositions géométriques correspondantes entrent donc, elles aussi, dans la machine. Les énoncés généraux portant sur des ensembles de points ou des fonctions arbitraires n’y entrent pas. C’est le langage choisi qui fixe le périmètre, et non le nom de « géométrie ».

À première vue, rien ne devrait permettre ce tour de force. « Il existe » semble commander une recherche dans un domaine infini. Or une machine ne peut pas essayer les nombres un par un sans fin : si elle ne trouve pas, elle ne s’arrêtera jamais. Éliminer ces mots, c’est remplacer cette recherche interminable par un énoncé fini, immédiatement vérifiable. Voilà la moitié de la réponse à notre première question : ce petit territoire se prête à la machine parce que chacun de ses « il existe » peut être éliminé. La possibilité du remplacement dépend de la régularité du monde considéré. Là où la structure est suffisamment régulière, il réussit. Ailleurs, non.

La méthode livre une réponse, pas une compréhension. Le résultat du remplacement peut être gigantesque, et ne pas du tout ressembler à ce qu’un humain appellerait une belle démonstration. Mais l’élimination a une autre utilité, bien plus vaste que de répondre oui ou non : elle montre exactement quel ensemble un énoncé contenant « il existe » et « pour tout » délimite dans ce monde. C’est dans cette information sur la structure que la théorie des modèles verra par la suite sa valeur essentielle.

4. Où passe la frontière

Si renoncer à la multiplication permet d’obtenir une machine, la question suivante s’impose : la frontière passe-t-elle par le signe de multiplication ?

Non. Deux exemples venus d’horizons différents font tomber cette hypothèse. Le premier est l’arithmétique de Skolem : sur les entiers naturels, on garde la multiplication et on retire l’addition ; la théorie reste décidable. Le second est plus frappant encore : chez Tarski, les réels disposent de l’addition, de la multiplication et de l’ordre, sans que la décidabilité disparaisse.

L’addition seule se laisse apprivoiser. La multiplication seule aussi. C’est leur réunion sur les entiers qui change la nature de l’affaire.

La raison ne se trouve pas dans la liste des symboles. Ensemble, l’addition et la multiplication des entiers permettent des codages d’une extraordinaire richesse : suites finies, démonstrations, calculs déroulés étape par étape peuvent tous se récrire en relations entre entiers. C’est exactement la puissance requise par le codage de l’épisode 17. L’arithmétique de Presburger ne peut pas accomplir ce travail, puisqu’elle ne permet même pas de définir la multiplication de deux variables. Parmi les trois conditions de l’épisode 17, c’est donc la troisième qui la maintient en deçà du seuil. Elle n’échappe pas au théorème par un défaut de cohérence ni d’axiomatisabilité effective. C’est sa puissance d’expression qui n’atteint pas le niveau requis.

Tarski expose lui-même le contraste très directement dans son livre : dès qu’une théorie est assez forte pour embrasser tous les énoncés pertinents de l’arithmétique usuelle des entiers, avec addition et multiplication, elle ne peut plus disposer d’une telle méthode uniforme de décision.

Il fait aussi une expérience de frontière particulièrement élégante. Dans le langage algébrique des réels, on ne peut pas définir de façon générale la propriété « ce nombre est un entier ». Si, en revanche, on autorise les variables à ne parcourir que les entiers, des questions telles que « existe-t-il des entiers dont le cube du premier, ajouté au cube du deuxième, soit égal au cube du troisième ? » deviennent formulables. L’arithmétique des entiers entre avec elles, et la décision uniforme ne peut plus être garantie. L’expression reste la même. Il suffit de faire passer les variables des réels aux entiers pour que son destin logique change tout entier.

Le facile et le difficile ne se logent pas dans les symboles. Ils se logent dans le domaine où l’on fait courir les variables.

On finira par établir définitivement ce qui se passe de l’autre côté du seuil. Parmi ceux qui y contribueront figure un visage connu. Le dixième problème de la liste dressée par Hilbert en 1900 demandait une méthode pour décider si une équation polynomiale quelconque à coefficients entiers possède une solution entière. C’est précisément le genre de question où les variables se multiplient entre elles et prennent leurs valeurs dans les entiers. Depuis ses études de troisième cycle, Martin Davis ne pouvait plus lâcher ce problème ; il l’accompagnerait toute sa vie. Durant l’été 1954, à Princeton, quand il installait dans des tubes électroniques la machine de ce côté-ci du seuil, il cherchait déjà depuis plusieurs années de l’autre côté.

Avec Putnam et Julia Robinson, il y a ouvert le chemin pendant plus de dix ans. Matiiassevitch a posé la dernière pierre. Celui-ci se rappelait très précisément la date de son premier exposé public sur la solution : le 29 janvier 1970, à Leningrad. Tseïtine était dans l’assistance. La réponse était : il n’existe pas de méthode générale. Le même homme, Davis, avait construit une machine d’un côté du seuil et contribué, de l’autre, à démontrer qu’on ne pouvait pas en construire.

Le seuil ne dessine donc pas une ligne bien nette. En 1936, Church et Turing ont établi qu’il n’existait pas de procédure uniforme de décision pour la logique du premier ordre en général. Le rêve de Hilbert à l’échelle de toutes les mathématiques s’arrêtait là. Mais les domaines situés en deçà du seuil viennent de directions très différentes : l’arithmétique linéaire, l’algèbre des réels, les corps algébriquement clos, puis toute une famille de structures issues de la théorie des automates. Ils sont décidables pour des raisons diverses : l’ordre pour les uns, la clôture algébrique pour d’autres, les automates ou l’élimination des quantificateurs ailleurs. En 1950, Trakhtenbrot montrera que même la restriction aux structures finies ne donne pas de solution au problème général de la décision. Ce que l’histoire de la logique nous laisse n’est donc pas une droite menant du décidable à l’indécidable. C’est une carte : on y cherche, d’un côté, les plus grands fragments décidables ; de l’autre, les plus petites extensions qui cessent de l’être.

5. Varsovie et le livre qui ne paraissait pas

Presburger n’était pas un étudiant isolé qui aurait, par hasard, écrit un article aux marges de la discipline. Varsovie était alors l’un des foyers les plus denses de la logique européenne. Elle appartenait à un ensemble plus vaste, l’école de Lvov-Varsovie, fondée par Twardowski et représentée entre les deux guerres par Ajdukiewicz, Kotarbiński, Leśniewski, Łukasiewicz et Tarski. Son essor a épousé les vingt et une années de l’entre-deux-guerres, du rétablissement de l’État polonais au déclenchement du conflit. La logique en est devenue peu à peu la branche la plus visible. Si l’on resserre le regard sur le cercle des logiciens de Varsovie, on trouve au centre Łukasiewicz, Leśniewski et Tarski ; autour d’eux, Lindenbaum, Presburger et de nombreux étudiants.

Presburger participait au travail de ce cercle. C’est lui qui a mis en forme les leçons orales de Łukasiewicz pour en tirer son cours de logique mathématique.

Le réseau des publications était dense, lui aussi. Les mathématiciens polonais avaient une revue spécialisée, Fundamenta Mathematicae, et deux autres à Lvov et à Cracovie. Varsovie et Vienne n’étaient pas davantage deux îles sans relations : Tarski s’est rendu à Vienne en 1930, Carnap est venu à Varsovie la même année, et Tarski est retourné à Vienne en 1935. Les noms viennois des épisodes 15 et 17 et les noms varsoviens que nous rencontrons ici appartenaient, en ces années-là, au même réseau.

Quant aux conditions de vie de Tarski, les bases de données bibliographiques allaient les rendre entièrement invisibles. Né Teitelbaum, il avait pris le nom de Tarski en 1923, en même temps que son frère. Tous deux s’étaient aussi convertis au catholicisme, alors que lui-même n’était pas croyant. Ses raisons étaient multiples : il voulait être polonais et savait combien, dans la Pologne de cette époque, il était difficile à un Juif d’obtenir un poste universitaire. Après son doctorat à Varsovie en 1924, il a longtemps enseigné les mathématiques dans le secondaire, tout en n’occupant qu’un modeste poste à l’université de Varsovie. En 1939, il a posé sans succès sa candidature à une chaire à Lvov. Des résultats de logique d’envergure mondiale sortaient alors de la plume d’un homme qui, dans le même temps, faisait classe au lycée.

Sa méthode de décision pour l’algèbre des réels date de 1930. La note historique qui clôt son livre remonte encore un peu plus loin : une partie des résultats figurait déjà dans ses cours de 1926 à 1928. Les étudiants varsoviens assis devant lui en avaient donc entendu certains éléments. Ceux qui n’étaient pas dans la salle devraient attendre encore vingt ans pour les lire.

Le livre entame alors sa propre traversée. Un éditeur parisien devait le publier en 1939 ; la guerre a interrompu le projet. C’est une institution de recherche américaine qui le reprend : en 1948, le projet RAND de l’armée de l’air des États-Unis s’intéresse au problème de la décision. On ressort le manuscrit resté neuf ans en attente ; McKinsey contribue à sa mise au point et à sa révision ; il paraît sous la forme d’un rapport numéroté de RAND. Une nouvelle version révisée suit en mai 1951, date sous laquelle l’ouvrage sera généralement cité. Sept ou huit ans après la première publication, un ordinateur de cette même institution fera tourner un autre type de programme de démonstration de théorèmes.

Dix-huit ans séparent la découverte de la méthode par Tarski de la publication qui la rend accessible à l’échelle internationale. À partir de 1939, la cause de l’interruption est claire : la guerre. Pour les neuf années précédentes, de 1930 à 1939, on ne dispose toujours pas d’une explication à cette absence de publication.

Toutes les dates de cette histoire se vérifient. Une seule se dérobe.

Presburger est né à Varsovie le 27 décembre 1904. Il a terminé ses études secondaires en 1923, puis est entré à l’université de Varsovie. Une seule étude lui est spécifiquement consacrée : la biographie publiée par Zygmunt en 1991, fondée pour l’essentiel sur les dossiers d’étudiant conservés par l’université. Ces archives ont depuis été numérisées en haute résolution, classées et rendues publiques : fiches d’inscription, cours suivis, pièces relatives au diplôme. On peut encore aujourd’hui tourner les pages qui attestent l’obtention de sa maîtrise de mathématiques en octobre 1930.

Ensuite, la trace se rompt. Juif polonais, il a été tué dans la Shoah, probablement vers 1943. Dans la biographie savante, cette année porte encore un point d’interrogation. La date exacte, le lieu et les circonstances de ses derniers jours ne sont pas établis avec la même certitude que les détails de sa vie étudiante.

Dix pages écrites par un homme de vingt et quelques ans sont exécutées, de machine en machine, depuis plus de soixante-dix ans. Mais comment cet homme est mort, nous ne savons pas l’écrire.

6. Une autre voie

Revenons à la machine de l’été 1954.

La méthode de décision existe. La machine aussi. Pourtant, Davis rencontre très vite un mur. Sur le papier, la méthode tient en quelques étapes ; dans l’ordinateur, elle impose d’abord de ramener les formules à une certaine forme normale. Or cette réécriture les fait gonfler : les combinaisons de conditions s’empilent, et une ligne assez courte au départ peut devenir plusieurs fois plus longue. Les mille vingt-quatre mots de mémoire sont vite remplis. C’est là que prend naissance le peu d’espoir que Davis placera ensuite dans des procédures de décision plus complexes.

Pour la première fois, cette machine donne à voir la différence : pouvoir décider ne signifie pas avoir les moyens de décider.

Deux ans plus tard, d’autres abordent le problème par l’autre bout. Newell et Shaw, chez RAND, avec Simon, du Carnegie Institute of Technology, créent un programme de démonstration logique. Il travaille sur les premières propositions des Principia Mathematica de Whitehead et Russell. Il ne suit pas une méthode qui garantit un résultat ; il choisit ses recherches. Une voie semble rapprocher du but ? Il l’emprunte d’abord. Les branches se multiplient trop ? Il en coupe certaines. S’il trouve, il fournit une démonstration. S’il ne trouve pas, il peut seulement dire qu’il n’a pas trouvé. Entre « je n’ai pas trouvé » et « il n’existe pas de preuve », il manque précisément ce que la machine de Davis possédait : une garantie. L’expression « intelligence artificielle » a alors moins d’un an.

D’un côté, une réponse est garantie, mais la mémoire déborde très vite. De l’autre, on renonce à garantir que l’on trouvera toujours une preuve, afin d’éviter ce débordement ; les preuves effectivement trouvées doivent néanmoins obéir à des règles d’inférence sûres. C’est ici que les deux voies se séparent.

À leur bifurcation se tient un Chinois. Wang Hao est né en 1921 à Jinan ; il a achevé ses études à l’Université nationale associée du Sud-Ouest, à Kunming, avant de partir aux États-Unis travailler en logique mathématique. Durant l’été 1958, dans un laboratoire de recherche d’IBM à Poughkeepsie, dans l’État de New York, il écrit plusieurs programmes sur l’un des grands ordinateurs de l’époque. L’un d’eux démontre la totalité des deux cents et quelques théorèmes des cinq premiers chapitres des Principia Mathematica. L’opération prend environ trente-sept minutes. Les douze treizièmes de ce temps passent en lecture des données et en impression. Moins de trois minutes servent réellement à démontrer.

Il présente ces résultats dans un article dont le titre signifie « Vers une mécanisation des mathématiques ». On dirait le vœu de l’école de Hilbert formulé à nouveaux frais. Un passage n’a rien de courtois. Pour comparer les méthodes heuristiques aux algorithmes, observe Wang, Newell et ses collègues ont pris pour témoin un algorithme particulièrement obtus. Invoquer un algorithme singulièrement inefficace pour établir la supériorité des heuristiques sur les algorithmes n’est guère, selon lui, une comparaison équitable.

Il en tire aussi une leçon : même dans un domaine assez riche, la plupart des théorèmes effectivement démontrés n’utilisent qu’une petite fraction des moyens que ce domaine offre. Pour qu’une machine puisse décider, il faut limiter ce que l’on peut dire. Or les choses que l’on cherche réellement à démontrer n’exigent, le plus souvent, qu’une toute petite part de ces moyens.

En 1983, il reçoit le premier prix « Milestone » de démonstration automatique, décerné par la Conférence internationale conjointe sur l’intelligence artificielle. Près de vingt ans plus tard, quand Davis raconte cette histoire des débuts, il inscrit sous son titre : « À la mémoire de Wang Hao ».

7. Le prix se calcule à part

Après la bifurcation, chacune des deux voies avance de son côté pendant près de vingt ans.

Les programmes heuristiques se multiplient, les promesses grandissent. En 1973, le Science Research Council britannique demande à Lighthill, spécialiste de mathématiques appliquées, une évaluation générale de l’intelligence artificielle. Une expression revient dans son rapport : « explosion combinatoire ». Les programmes réussissent sur des problèmes petits et bien délimités. À l’échelle du monde réel, le nombre de possibilités à explorer devient tel que la recherche n’en finit plus.

L’année suivante, de l’autre côté, arrive un résultat plus glacial encore. En 1974, Fischer et Rabin ne demandent pas si la méthode de Presburger est rapide. Ils demandent si quelque méthode que ce soit pourrait être fondamentalement beaucoup plus rapide. La réponse est non. Pour cette arithmétique, quelle que soit la procédure générale inventée, il existe des formules pour lesquelles chaque petit accroissement de la taille de l’entrée oblige à porter de nouveau au carré le nombre d’étapes nécessaires. C’est une borne inférieure doublement exponentielle. En 1978, Oppen établit aussi une borne supérieure : le problème se trouve pris entre deux murs d’une hauteur vertigineuse.

Cela ne signifie pas que toute formule de cette longueur soit aussi difficile. Cela signifie que toute méthode générale rencontre de telles entrées défavorables. Ce n’est pas non plus le défaut d’un programme mal écrit : la difficulté appartient au problème lui-même. Fischer et Rabin examinent également la longueur des démonstrations. Sous des conditions appropriées, certains énoncés, quoique démontrables, ne peuvent avoir que des preuves extrêmement longues. Être décidable, être démontrable et fournir à quelqu’un une preuve qu’il puisse réellement lire jusqu’au bout deviennent ainsi trois choses distinctes.

Les deux voies se rejoignent devant le même mur. Lighthill décrit celui qu’un champ de recherche rencontre en passant à l’échelle du monde réel. Fischer et Rabin disent autre chose : même si l’on se replie sur ce fragment d’arithmétique minuscule, épuré et garanti, le mur est toujours là.

Sur les réels, l’histoire se répète. La méthode de Tarski prouvait l’existence d’une procédure de décision, mais ne donnait pas un algorithme que l’on puisse faire tourner en pratique. La première méthode complète réellement exploitable est généralement attribuée à Collins, en 1975. Il découpe l’espace réel à plusieurs dimensions en un nombre fini de cellules, de sorte que chacun des polynômes donnés conserve le même signe sur chaque cellule. Une question portant sur une infinité de points devient alors un ensemble fini de vérifications représentatives. Cette méthode est devenue l’un des fondements des systèmes de calcul formel. Mais le nombre de cellules peut croître doublement exponentiellement avec le nombre de variables. En 1988, Davenport et Heintz montrent que cette difficulté n’est pas entièrement imputable à la méthode : l’élimination générale des quantificateurs sur les réels est elle-même exposée à ce degré de complexité. Durant les décennies d’améliorations qui ont suivi, il s’est surtout agi, non de renverser cette borne inférieure, mais d’éviter le travail inutile : améliorer les projections, ne découper que les régions dont le problème posé a réellement besoin.

Du côté de la géométrie, quelqu’un négocie autrement le prix. En 1976 et 1977, à Pékin, Wu Wenjun commence à faire démontrer des théorèmes géométriques par ordinateur. Il écrira plus tard, dans une préface, que le théorème de mécanisation de Tarski embrasse certes une vaste part de la géométrie élémentaire, mais que son efficacité est trop faible. Sa propre méthode traduit les problèmes géométriques en systèmes d’équations polynomiales ; les propositions faisant intervenir l’ordre et les inégalités sont provisoirement laissées de côté. En resserrant un peu le champ des questions, on permet à la machine de fonctionner. Elle démontre ainsi une série de théorèmes géométriques qui n’ont rien de trivial.

Il appelle ce programme la « mécanisation des mathématiques » et dit en avoir trouvé l’inspiration dans les mathématiques chinoises anciennes. Les Neuf Chapitres sur l’art mathématique, ainsi que les commentaires que Liu Hui leur a consacrés en 263 de notre ère, sont à ses yeux les grands classiques d’une tradition orientale qui organise les mathématiques en algorithmes mécaniquement exécutables. Le Liu Hui de l’épisode 5 est ici reconnu comme un prédécesseur par un mathématicien du XXe siècle. Dans la même préface, Wu rappelle aussi les deux cents et quelques propositions que la machine de Wang Hao avait démontrées en trois minutes.

Il y a donc un écart entre être décidable et être utilisable. Au sens mathématique, la décidabilité pose une question : existe-t-il une méthode uniforme qui garantisse de finir par s’arrêter et de répondre juste ? Elle ne promet ni quelques secondes ni un siècle. Elle ne promet même pas de tenir dans les ressources disponibles dans cet univers. Pour l’ingénieur, l’utilité pose une autre question : sur les problèmes qui se présentent réellement, avec une machine donnée, un temps donné et une mémoire donnée, le programme fournit-il souvent assez vite des résultats utiles ? La réponse peut être oui à l’une et non à l’autre. C’est même fréquent.

L’inverse est tout aussi vrai. Un pire cas désastreux ne rend pas une méthode inutile. De nombreuses procédures de décision, dont le pire cas théorique est effroyable, sont très efficaces sur les problèmes qu’elles doivent effectivement traiter. La leçon de Wang Hao revient ici : la plupart des problèmes rencontrés en pratique ne relèvent pas des cas les plus défavorables.

8. Un compte à trois colonnes

Revenons au titre. La clôture s’achète-t-elle ? Oui. Elle a même été achetée deux fois, et ce n’était pas la même marchandise.

Presburger a obtenu un fragment complet et décidable de l’arithmétique des entiers. Le prix : une vaste part de la théorie des nombres ne peut pas s’y dire. Tarski a obtenu une méthode uniforme de décision pour l’algèbre des réels et, avec elle, pour la géométrie élémentaire. Il n’avait pourtant rien supprimé. Le prix se trouvait ailleurs : par sa nature même, ce langage ne peut pas dire « ce nombre est un entier ». Ni l’un ni l’autre n’a passé un marché. Chacun étudiait un objet mathématique précis et a découvert que cet objet présentait une remarquable régularité. L’« achat » est la forme que nous distinguons après coup. Sur le moment, personne ne payait.

Ces deux résultats ont surtout prolongé leur vie dans deux disciplines venues ensuite. L’élimination des quantificateurs de Tarski est devenue une technique fondamentale de la théorie des modèles ; les réels et les corps algébriquement clos, des exemples élémentaires de ses manuels. L’arithmétique de Presburger est entrée, elle, dans la vérification des programmes. La correction d’un programme dépend souvent d’indices de tableaux, de compteurs de boucles et de relations linéaires entre entiers : exactement le genre de choses que cette arithmétique sait dire. En 1972, Cooper transforme la méthode de Presburger en une version utilisable sur ordinateur. Son article, consacré à la démonstration de théorèmes dans l’arithmétique sans multiplication, paraît dans la collection Machine Intelligence. Certains des programmes qui aident aujourd’hui les mathématiciens à vérifier leurs preuves ligne à ligne comportent un module expressément intitulé « procédure de décision pour l’arithmétique de Presburger ». C’est la version de Cooper qui s’y trouve.

Que faut-il en retenir ?

Un système capable de répondre à tous les énoncés qu’il peut formuler semble faire la preuve de sa puissance. Il dresse aussi un inventaire : celui de tout ce qu’il ne peut pas dire. Pour juger un discours, commençons par compter les questions auxquelles il ne peut pas répondre, avant de compter celles auxquelles il répond. Quand toutes reçoivent une réponse, c’est généralement qu’on en a posé trop peu.

Depuis la machine de 1954, toutes les machines construites pour répondre à des questions peuvent figurer dans un même livre de comptes. Il comporte trois colonnes : ce qu’on peut demander à la machine ; si sa réponse est garantie ; le prix à payer pour chaque réponse.

Les dix pages de Presburger disent ceci : si la colonne des questions est assez étroite, celle des garanties peut être entièrement remplie. La remarque de Tarski, jointe aux résultats de Church et Turing en 1936, dit que, dès que l’on ouvre assez les questions pour accueillir l’addition et la multiplication des entiers, il devient impossible de remplir complètement la colonne des garanties. Fischer et Rabin disent enfin que, même en resserrant les questions autant que Presburger et en remplissant la colonne des garanties, le prix inscrit dans la dernière colonne peut rester hors de portée.

La machine de Davis remplissait la colonne des garanties et butait sur celle du coût. Le programme de 1956 laissait vide la colonne des garanties pour réduire le coût. Dans le même secteur, Wang Hao a pu remplir les deux colonnes, parce que le secteur était assez petit. Wu Wenjun a retranché une partie des questions de la géométrie, et le coût est devenu supportable. Les machines suivantes n’ont cessé de déplacer le compromis entre ces trois colonnes. Certaines conservent la garantie et élargissent peu à peu le champ des questions. Davis a ainsi élaboré plus tard, avec Putnam et d’autres, une méthode pour décider si un ensemble de conditions logiques peut être satisfait simultanément ; ses descendantes seront largement employées pour vérifier des circuits intégrés et des logiciels. D’autres ouvrent très largement les questions et laissent vide la colonne des garanties. Une grande part de ce qui prendra le nom d’intelligence artificielle tient ses comptes de cette façon.

Personne n’a jamais présenté la page où les trois colonnes seraient remplies à la fois. Que le champ des questions et la garantie ne puissent être tous deux sans lacune, c’est un théorème qui le dit.

Dans cet épisode, la guerre a arrêté un livre à la porte de l’imprimerie. Elle a aussi interrompu la vie d’un homme. Le manuscrit a été retrouvé ; des derniers jours de Presburger, il ne reste qu’une année suivie d’un point d’interrogation. Le prochain épisode remontera à 1933, dans une université.

On continue à compter les nombres. Ce qui compte comme mathématiques, en revanche, n’a jamais été définitivement réglé.

Sources historiques et lectures complémentaires

Les références ci-dessous éclairent les détails historiques et les divergences d’interprétation évoqués dans le texte. Les notices de collections, la littérature ancienne et les reconstitutions modernes ne constituent pas le même type de preuve.

• L’article original de Presburger, traduit et annoté
• Tarski dans la Stanford Encyclopedia of Philosophy
• Le rapport RAND de Tarski sur une méthode de décision
• L’article de Wang Hao, « Vers une mécanisation des mathématiques »
• La borne supérieure de complexité établie par Oppen en 1978
• Brown et Davenport sur la complexité de l’élimination des quantificateurs
• Préface de Wu Wenjun à la collection sur la mécanisation des mathématiques