L' Entscheidungsproblem ou la fin des mathématiques ? | Voyages au pays des maths | ARTE

L' Entscheidungsproblem ou la fin des mathématiques ? | Voyages au pays des maths | ARTE

ARTE10 min11 nov 2023
7 capitulos
  • Le rêve de Leibniz : une machine à calculer la vérité(0'051'15)
    Au 17e siècle, le philosophe et mathématicien Gottfried Wilhelm Leibniz a envisagé un monde où l'on pourrait calculer mécaniquement la vérité.
    Leibniz a imaginé le calculus raciocinator, une machine capable de soumettre toutes sortes d'affirmations et de répondre vrai ou faux sans se tromper.
    • Éliminer les débats d'opinion interminables • Créer un langage universel permettant de statuer sur toutes les affirmations • Atteindre une rationalité absolue
    Une telle machine est-elle possible ? C'est la question centrale qui guidera les mathématiques du 20e siècle.
  • Le problème de la décision de Hilbert(1'152'17)
    En 1928, David Hilbert et Wilhelm Ackermann posent une question : existe-t-il un algorithme capable de déterminer si un énoncé mathématique donné est démontrable ou ne l'est pas ?
    Un tel algorithme s'appelle un algorithme de décision, et l'existence d'un tel algorithme constitue le problème de la décision (Entscheidungsproblem en version originale).
    Pour Hilbert, résoudre l'Entscheidungsproblem est un objectif majeur pour rendre plus rigoureux les fondements des mathématiques.
    Au lieu de chercher un langage universel comme Leibniz, on se concentre uniquement sur les énoncés mathématiques déjà exprimés en termes exacts.
  • La méthode énumérative : lister tous les énoncés démontrables(2'174'00)
    Il existe un procédé simple pour lister tous les énoncés démontrables : faire taper au hasard tous les textes possibles d'une page, puis deux pages, puis trois pages, et ainsi de suite.
    • Une machine à écrire et un mathématicien infiniment patient (ou un robot) tapent aléatoirement • Parmi les textes générés, certains sont des preuves de théorèmes • Ces preuves sont ajoutées à la liste des énoncés démontrables
    Bien que mécanisable, ce procédé ne résout pas l'Entscheidungsproblem : si aucune preuve n'apparaît après 100 pages ou 1000 pages, on ne peut pas conclure si l'énoncé est indémontrable ou si sa preuve est simplement plus longue.
    C'est comme attendre un bus sans horaire : l'arrivée du bus confirme que l'arrêt est desservi, mais son absence ne permet pas de conclure.
  • Vers une théorie rigoureuse du calcul(4'005'55)
    Au cours des années 1930, pour prouver qu'il n'existe pas d'algorithme de décision, les mathématiciens doivent d'abord définir rigoureusement ce qu'est un algorithme.
    • Un algorithme devient un processus qui à certains nombres en associe d'autres • En termes mathématiques, c'est une fonction • On peut coder numériquement les formules et remplacer oui/non par 1/0
    Une fonction est calculable si on peut obtenir chaque résultat avec une recette explicite. Par exemple, la fonction f(x) = x + 1 est calculable, tandis qu'une fonction décrite uniquement par une liste infinie ne l'est pas.
    Cette réflexion crée la base de la théorie du calcul et de l'informatique, disciplines qui n'existaient pas avant.
  • Trois approches convergeantes : Gödel, Turing, Church(5'559'01)
    Kurt Gödel propose la notion de fonctions récursives : une fonction est calculable si elle peut être construite en combinant des fonctions de base selon des règles bien définies. En 1934, il établit que calculable signifie récursif.
    Alan Turing envisage le problème mécaniquement : il imagine une machine avec un ruban infini et une tête de lecture-écriture qui exécute des instructions. Il démontre qu'il existe des machines universelles pouvant remplacer n'importe quelle autre machine, tout comme un ordinateur programmable.
    Alonzo Church invente un ancêtre des langages de programmation : les lambda termes, des programmes abstraits qui peuvent manipuler d'autres programmes. Une fonction est calculable s'il existe un lambda terme pouvant calculer ses valeurs.
    • Les trois définitions utilisant des intuitions très distinctes recouvrent le même ensemble de fonctions • Turing-calculable égale Gödel-récursif égale Church-lambda-définissable • C'est comme trois alpinistes venant de pentes différentes qui atteignent le même sommet
  • Le problème de l'arrêt et la résolution négative(9'019'51)
    Turing pose une question piège : existe-t-il une machine capable de décider si une autre machine va s'arrêter ou rester bloquée dans une boucle infinie ?
    • Turing démontre qu'une telle machine n'existe pas : le problème de l'arrêt ne peut pas être décidé par une machine de Turing • Il montre que si une machine de Turing pouvait résoudre le problème de la décision, elle pourrait aussi résoudre le problème de l'arrêt • Puisque le problème de l'arrêt est indécidable, le problème de la décision l'est aussi
    Comme tout calcul est modélisable par une machine de Turing, il n'existe pas d'algorithme de décision pour les énoncés mathématiques. L'Entscheidungsproblem a une réponse négative.
    Il existe des mathématiques qui ne pourront jamais être réduites au calcul : les mathématiciens resteront nécessaires pour explorer l'infini des nombres.
  • Les conséquences positives : naissance de l'informatique(9'5110'40)
    De la réponse négative à l'Entscheidungsproblem sont nées de nombreuses choses positives, en commençant par la théorie du calcul.
    • Les algorithmes gèrent les flux financiers, les playlists, les albums photos • Ils calculent les primes d'assurance et les rencontres amoureuses • Ils imitent Jean-Sébastien Bach, Picasso, Proust et même Céline Dion
    Les algorithmes ne peuvent calculer que ce qui est calculable. On sait depuis près d'un siècle qu'on ne peut réduire au calcul ni la décision ni la recherche mathématique.
    Pour rêver à l'infini des nombres, il faudra toujours des mathématiciens. La connaissance d'une impossibilité a paradoxalement ouvert des horizons infinis.