La complexité mathématique est sans limites

La longueur des démonstrations est ce qui rend la mathématique intéressante, et elle constitue un fait d'une importance philosophique fondamentale. [...] Une astuce qui permet une démonstration très brève d'un résultat qu'on croyait difficile donnera lieu à un mélange de satisfaction et de déception (parce que le résultat se réduit finalement à une trivialité).

David Ruelle, Hasard et Chaos, Ed. O. Jacob 1991.

C'est clair, les mathématiciens attribuent de la valeur aux résultats qui, tout en s'énonçant facilement, nécessitent de longues démonstrations. Le blog précédent donnait l'exemple récent d'un résultat à l'énoncé très court qui exigeait une démonstration très longue (et il y a bien d'autres exemples). Cette complexité est pour le mathématicien une forme de beauté.

Sait-on s'il existe des résultats ayant une complexité (en ce sens) aussi grande qu'on le veut ?

Sait-on donner des définitions précises de « longueur de résultat » et de « longueur de démonstration » ?

La logique mathématique et particulièrement le domaine de la « théorie de la preuve » dispose d'outils permettant d'aborder ces notions, et elle a depuis longtemps formulé des théorèmes qui répondent bien à ce type d'interrogations. En deux mots : pour toute définition raisonnable de la notion de démonstration, on sait établir qu'il existe des théorèmes dont la taille de la démonstration est considérablement plus longue que la taille de l'énoncé. En mathématiques, c'est donc une certitude, la complexité est sans limites.

Formaliser, axiomatiser.

La rigueur va de pair avec les mathématiques et dès l'antiquité — chez Euclide par exemple — on a tenté de la définir, c'est-à-dire de préciser ce qu'est une démonstration juste. Ces efforts continus n'ont pleinement abouti qu'à la fin du XIXe siècle et au début du XXe avec les travaux de Gottlob Frege, Giuseppe Peano, Georg Cantor, Ernst Zermelo, Alfred Whitehead et Bertrand Russell. Ces derniers dans leur ouvrage Principia Mathematica proposaient une notion entièrement formelle (c'est-à-dire ramenant tout à des manipulations de symboles) de démonstration qu'ils utilisaient ensuite pour développer une partie des mathématiques. C'est d'ailleurs en se référant au formalisme des Principia que Kurt Gödel en 1931 formula et prouva ses célèbres résultats d'incomplétude.

Une démonstration, dans le système des Principia, est une suite finie de formules respectant des règles de construction purement mécaniques qui sont fixées une fois pour toutes. Vérifier une démonstration écrite dans le système des Principia ne demande aucune intelligence et c'est un travail qu'on peut confier à un programme d'ordinateur. À partir de cette époque, l'activité du mathématicien a donc pu être perçue comme purement mécanique : un mathématicien est une personne qui recherche des combinaisons de symboles conformes aux règles de son système et qu'il appelle démonstrations. Bien sûr, cette conception des mathématiques — qu'on appelle le formalisme — est réductrice. Elle oublie la phase de recherche des bonnes idées et la phase de mise au point de la démonstration, pour ne retenir que la phase de vérification. Sans adopter la version extrême du formalisme qui affirme que l'activité du mathématicien n'est que manipulation syntaxique, il apparaît cependant raisonnable d'en retenir certains éléments et par exemple de considérer que produire une démonstration mathématique se décompose en définitive en quatre étapes.

(a) Découvrir les idées de la démonstration (phase de recherche et de mise au point) ;

(b) Sélectionner un système formel acceptable (de manière implicite, la théorie classique des ensembles est souvent choisie) ;

(c) Travailler dans ce système pour y formuler ses idées et résultats (même si on n'explicite pas totalement les démonstrations formelles) ;

(d) Contrôler et faire contrôler (par des collègues et des machines éventuellement) que ce qu'on a proposé est correct.

Les mathématiciens s'accordent finalement sur l'utilité de la notion de système formel, tout en admettant qu'elle ne dit pas tout de ce que sont les mathématiques et surtout de la phase de recherche informelle précédant l'écriture des démonstrations. Cet accord nous suffit pour mener notre réflexion sur la longueur des démonstrations et nous permet d'éviter un premier piège qui serait de croire qu'un résultat peut être long à démontrer dans l'absolu, c'est-à-dire dans tout système formel.

Pas de résultat à la démonstration nécessairement longue

Dans la présentation des systèmes formels, on distingue les axiomes (qui sont les connaissances de base à partir desquelles on démarre les démonstrations) et les règles d'inférence qui décrivent les manipulations syntaxiques autorisées pour avancer pas à pas dans une démonstration. Soit un système formel donné (par ses axiomes et ses règles d'inférence), et soit un théorème T qui s'y démontre avec une démonstration d'une longueur de dix millions de symboles par exemple. Soit maintenant le système formel obtenu en prenant les mêmes règles d'inférence, et les mêmes axiomes auxquels on ajoute T lui-même comme axiome. Il est identique en tout point au précédent, sauf qu'il possède l'axiome T en plus. Ce nouveau système est non contradictoire si le premier l'était (car on a ajouté un axiome qui était démontrable dans le premier). Dans ce nouveau système, la démonstration de T est très courte, elle a le même nombre de symboles que T : puisque T est un axiome, la démonstration de T consiste juste en l'écriture de T. Aussi bête soit-il, ce petit raisonnement est fondamental : il montre qu'un théorème ne peut pas avoir une preuve longue dans tout système formel.

De cette remarque (qu'on peut toujours considérer un théorème comme un axiome), on pourrait conclure que tout est terminé, et que nous avons montré que la recherche d'une notion satisfaisante de longueur de démonstration est absurde. Oui ... sauf si on accepte de privilégier certains systèmes formels auxquels on se référera de manière constante, et dont on refusera de compléter les axiomes par n'importe quoi.

Démonstrations dans ZFC

Il se trouve justement que les mathématiciens s'accordent pour retenir et faire jouer un rôle privilégié à certains systèmes formels particuliers. Le système formel usuel de la théorie des ensembles (ZFC) est très puissant et sert fréquemment de référence. C'est d'ailleurs ce système que le grand traité de mathématiques de Nicolas Bourbaki prend comme base. À partir de maintenant, sauf mention contraire, lorsque nous parlerons de longueur d'une démonstration, il sera sous-entendu que nous nous référons à la longueur de cette démonstration dans le système formel usuel de la théorie des ensembles ZFC auquel nous ne touchons plus.

Le premier résultat que nous indiquons repose sur une idée simple mais importante.

Résultat 1. Pour tout entier (par exemple 100) il existe un entier (par exemple 1 000 000) tel que tous les théorèmes de longueur inférieure à 100 possèdent une démonstration de longueur inférieure à 1 000 000. Sous forme générale : pour tout entier n il existe un nombre Max(n) tel que tous les théorèmes dont l'énoncé a une longueur inférieure à n (dans ZFC) possèdent une démonstration dont la longueur est inférieure à Max(n) (dans ZFC).

Démonstration du résultat 1. En effet, soit n fixé et soient t(1) t(2) ... t(p) les théorèmes de la théorie des ensembles dont l'énoncé est de taille inférieure à n. Ces théorèmes sont en nombre fini, car avec un nombre fini de symboles de bases on ne peut écrire qu'un nombre fini de formules de longueur inférieure à n. Les mathématiciens utilisent un peu plus de symboles que le langage écrit usuel, mais ils n'en n'utilisent qu'un nombre fini, et de toute façon le système formel de la théorie des ensembles qui nous sert de référence nécessite moins d'une centaine de symboles. Désignons par l(1) la longueur de la plus courte démonstration de t(1). De même, désignons par l(2) la longueur de la plus courte démonstration de t(2) etc. jusqu'à l(p). Soit le plus grand des nombres l(1), l(2), ..., l(p). C'est lui que nous prenons pour Max(n). Quelques secondes de réflexion montre qu'il convient.

Cette démonstration laisse cependant insatisfait, car si elle montre que Max(n) est bien défini, elle n'en donne pas la moindre idée. Peut-on être plus précis ? Ce Max(n) est-il égal à 1000 n ? Ce serait bien pratique, car pour démontrer un théorème de longueur n, on saurait qu'il est inutile d'en chercher des démonstrations plus longues que 1000 n.

Ce Max(n) est-il égal à 2n ? Son utilisation serait déjà plus difficile. Ce Max(n) est-il égal à 1000 n! ? Ou encore à 101000 n! ?

La réponse est que Max(n) est bien pire que tout cela... et (vraisemblablement) que tout ce que vous pouvez imaginer. En effet, quelle que soit la fonction que vous définirez n —> g(n) avec des puissances, des factorielles, et tout ce qu'il vous plaira (pourvu que vous soyez précis et décriviez un moyen de calcul de g(n)) ce sera une fonction qui ne majorera pas Max(n).

Le résultat mathématique est le suivant :

Résultat 2. La fonction Max(n) prend des valeurs plus grandes que celles de toute fonction calculable par algorithme. Dit autrement : toute fonction g(n) tendant vers l'infini définissable à l'aide d'un programme d'ordinateur sera dépassée par Max(n) une infinité de fois.

Il en résulte immédiatement que la fonction Max(n) n'est elle-même pas calculable par programme. C'est une fonction croissante (cela résulte de sa définition), mais sa croissance est colossalement rapide. Cela signifie en particulier que le rapport entre la longueur d'une démonstration et celle de l'énoncé démontré peut être aussi grand qu'on le veut.

Démonstration du résultat 2. La démonstration repose sur un résultat classique de la théorie de la démonstration dû à Alonzo Church qui l'a établi en 1936 à peu près en même temps que le mathématicien anglais Alan Turing. Ce résultat n'est pas sans rapport avec le théorème de Gödel, mais ne doit pas être confondu avec lui. Le théorème de Church (énoncé et adapté à la théorie des ensembles) est : il n'existe pas d'algorithme qui pour tout énoncé de la théorie des ensembles indique s'il s'agit d'un théorème ou pas.

Nous ne démontrerons pas le théorème de Church qui n'est pas évident, mais l'argument est tellement simple pour en déduire notre énoncé concernant Max(n) que tout le monde devrait l'avoir en tête. Supposons qu'il existe une fonction g(n) calculable par algorithme qui ne soit jamais plus petite que Max(n) (dit autrement : qui majore Max(n)). Alors en utilisant g(n), je peux construire un algorithme qui m'indiquera pour chaque formule F de la théorie des ensembles si c'est un théorème ou pas de cette théorie (ce sera une contradiction avec le théorème de Church). Mon algorithme procède ainsi : il commence par mesurer la longueur de la formule F, soit n cette longueur; il calcule ensuite g(n) (ce que j'ai supposé faisable par algorithme) ; l'algorithme recherche alors toutes les démonstrations correctes de longueur inférieure à g(n). Il s'agit d'un travail très long, mais fini, et donc possible (en théorie). Si lors de cette exploration, il découvre une démonstration de F, mon algorithme s'arrête en m'indiquant que F est un théorème de la théorie des ensembles. Si lors de son exploration, jamais il n'arrive à une démonstration de F, alors après avoir tout exploré, mon algorithme m'indique que F n'est pas un théorème de la théorie des ensembles. Par hypothèse g(n) est toujours plus grand que Max(n) et donc mon algorithme ne peut pas manquer de démonstration, autrement dit, il ne se trompe pas quand il me dit que F est un théorème ou quand il me dit que ça n'en est pas un. Cet algorithme contredit le théorème de Church. En conclusion : g ne peut pas exister.

Parmi les conséquences de ce résultat 2 sur Max(n), il y a la suivante qui va répondre à la question principale que nous posions. Il existe des théorèmes de la théorie des ensembles dont la démonstration la plus courte est un milliard de fois plus longue que l'énoncé lui-même. On pourrait dire d'un tel théorème que son niveau de difficulté est un milliard. Bien sûr, il existe aussi des théorèmes dont le niveau de difficulté est un milliard de milliards, ou tout nombre que vous voudrez. La démonstration que des théorèmes de difficulté un milliard existent s'obtient en considérant la fonction calculable par algorithme g(n) = 1 000 000 000 n. D'après notre résultat sur Max(n) pour certaines valeurs de n, g(n) est plus petit que Max(n), ce qui signifie que pour de telles valeurs de n, il existe un théorème de la théorie des ensembles dont la longueur est inférieure à n et dont la plus courte démonstration a pour longueur Max(n) qui est plus grand que 1 000 000 000 n.

Remarquons que l'existence de théorèmes ayant un niveau de difficulté d'un milliard (ou plus) est valable pour d'autres systèmes formels que celui ZFC que nous avons considéré. La seule chose dont nous ayons eu besoin est le théorème de Church, or celui-ci est valable pour tous les systèmes formels puissants, qu'on pourrait envisager pour faire des mathématiques. Donc, même si on voulait utiliser une théorie plus forte que celle des ensembles, il y aurait encore des théorèmes de difficulté un milliard (ou plus) dans cette nouvelle théorie.

 

On trouvera des résultats plus avancés sur la complexité des démonstrations dans les références suivantes.

  • Stephen Cook, Phuong Nguyen, Logical Foundation of Proof Complexity, Cambridge University Press, 2010.
  • R. J. Parikh, Some Results on the Length of Proofs, Transaction of the American Mathematical Society, 177, 29-36, 1973.
  • Pavel Pudlak, Proof Complexity,  in "Logical Foundation of Mathematics and Computational Complexity", Springer Monographs in Mathematics, 2013.
  • Alma Steingard, A Group Theory of Group Theory: Collaborative Mathematics and the 'Uninvention' of a 1000-page Proof." Social Studies of Science 42/2, 185-213, 2012.
  • Nathan Segerlind, The Complexity of Propositional Proofs, The Bulletin of Symbolic Logic, 13/4, 417-481, 2007.
  • Richard Statman, Bound for Proof-Search and Speed-up in the Predicate Calculus, Annals of Mathematical Logic, 15, 225-287, 1978.

2 commentaires pour “La complexité mathématique est sans limites”

  1. Diziet Sma Répondre | Permalink

    Très franchement,j'ignorais que les mathèmaticiens accordaient plus de valeur à un théorème concis dans sa formulation,mais dont la démonstration est d'autant plus longue.
    Je pensais que le principe du " rasoir d'occam " s'appliquait aussi aux preuves,en privilégiant les plus économes.
    Si les machines assistent désormais l'homme dans l'éllaboration ou la vérification des démonstrations,peut-on imaginer qu'un gros calculateur à qui on fournirait un système formel non contradictoire,comme le ZFC,serait capable de produire des théorèmes non triviaux et j'usque là inconnus ?

    • Jean-Paul Delahaye Répondre | Permalink

      Si un mathématicien réussit à trouver une démonstration assez courte d'un résultat dont on ne connaît qu'une démonstration très longue, tout le monde est satisfait et l'admire. Cependant, si la démonstration est vraiment très courte (quelques lignes), alors on se dit que c'est sans doute parce qu'on n'avait pas vraiment cherché et que le théorème n'est sans doute pas très profond.
      Faire la recherche au hasard de théorèmes intéressants par des démonstrateurs de théorèmes (utilisant ZF ou autre chose) n'est pas une bonne méthode, et je crois qu'aucun résultat n'a jamais été obtenu ainsi. En revanche, en organisant la recherche, on trouve parfois des choses intéressantes. En 1995, Simon Plouffe en procédant par essais systématiques dans une classe de formules a trouvé une nouvelle série donnant Pi qui s'est révélée utile (l'ordinateur ne la pas démontrée, mais une fois que l'ordinateur l'a proposée, il a été facile de la démontrer). Voir : http://fr.wikipedia.org/wiki/Formule_BBP

Publier un commentaire