Une machine peut-elle vraiment démontrer un théorème ?

Intervenant 10:00

Bienvenue dans le podcast du magazine Tangente. C'est vraiment un plaisir de vous retrouver pour cette nouvelle exploration approfondie. Et aujourd'hui, on va aborder un sujet assez fascinant.

Intervenant 20:11

Salut à tout le monde. Un très beau sujet qui nous vient d'un ancien numéro de la revue d'ailleurs.

Intervenant 10:16

Absolument. C'est inspiré d'un dossier du numéro 8, qui a 30 ans, mais qu'on a bien sûr mis à jour avec les avancées récentes. La grande question du jour, c'est la machine peut-elle démontrer ? Parce que d'habitude, quand on pense à un ordinateur ou à une calculatrice, on s'attend à une rigueur absolue. Une

Intervenant 20:34

précision glaciale même.

Intervenant 10:36

Voilà, 2 plus 2 font 4, l'écran affiche le masulta et on se sent en terrain sûr. Mais en fait, dès qu'on plonge dans les mathématiques fondamentales, la machine montre un visage bien plus complexe. La frontière entre la créativité humaine et la validation par la machine devient super trouble.

Intervenant 20:55

Et c'est justement l'objectif de notre discussion aujourd'hui. On va essayer de comprendre comment l'ordinateur est passé de ce statut de simple calculatrice à celui d'un assistant de preuve indispensable.

Intervenant 11:06

Un vrai partenaire de travail, quoi.

Intervenant 21:07

Tout à fait. Un outil qui peut prendre une démonstration humaine, avec ses éclairs de génie, mais aussi ses petites failles, pour la transformer en une preuve formelle absolue. La question de fond, elle est vertigineuse. C'est une machine peut-elle vraiment démontrer un théorème à notre place ?

Intervenant 11:23

Bon, décortiquons un peu tout ça. Avant de confier la vérification aux machines, il faut déjà qu'on s'accorde sur ce qu'est fondamentalement une démonstration mathématique.

Intervenant 21:33

Ah bah oui, c'est la base. La vérité mathématique, elle repose sur une architecture très codifiée. Chaque théorème vit dans ce qu'on appelle une théorie.

Intervenant 11:41

Genre l'arithmétique pour les nombres entiers, ce genre de choses ?

Intervenant 21:44

Exactement, ou la géométrie eclidienne qui nous donne le fameux théorème de Pythagore. Mais pour bâtir ça, il nous faut un point de départ. Ce socle, ce sont les définitions, pour savoir de quoi on parle, et surtout les axiomes.

Intervenant 11:56

Les axiomes, ce sont ces vérités qu'on dit primitives, non ?

Intervenant 22:00

C'est ça. Ce sont des propriétés évidentes mais indémontrables. On les accepte comme les règles du jeu initial.

Intervenant 12:06

D'accord. On accepte que, par deux points, il ne passe qu'une seule droite, par exemple. Et à partir de là, on construit. Et ça me fait penser, au début du XXe siècle, il y avait cet optimisme de dingue, notamment avec le mathématicien David Hilbert.

Intervenant 22:21

Hilbert, oui, une figure incontournable. Son ambition était démesurée, en fait.

Intervenant 12:26

Il voyait un peu les mathématiques comme un énorme mur de briques infinies, non ? À l'étape 0, tu poses tes fondations, donc tes axiomes, et à l'étape 1, tu ajoutes ta première rangée de briques.

Intervenant 22:36

Voilà, les briques de l'étape 1 étant les théorèmes déduits directement des axiomes, par une logique super simple.

Intervenant 12:43

Et ensuite, étape 2, on s'appuie sur la rangée 1 pour déduire d'autres théorèmes, et ainsi de suite. Hilbert pensait vraiment pouvoir générer toutes les vérités mathématiques en empilant ses briques, mécaniquement.

Intervenant 22:54

Il voulait mécaniser la pensée logique, prouver que les mathématiques formaient un système parfait, sans aucune faille. Sauf que, en 1931, Kurt Gödel est arrivé avec une énorme douche froide.

Intervenant 13:07

Aïe, le fameux théorème d'incomplétude.

Intervenant 23:09

Exactement. Gödel a prouvé que dans tout système logique de base, il y aura toujours des propositions qui sont vraies, mais impossibles à démontrer à partir des axiomes de départ.

Intervenant 13:19

C'est un truc de fou quand on y pense. Si on reprend l'analogie du mur, Gödel prouve qu'il manquera toujours des briques pour le finir. Le mur parfait, il ne peut pas exister.

Intervenant 23:28

L'onde de choc a été terrible à l'époque. Ça ruinait l'idée du circuit mathématique fermé.

Intervenant 13:33

C'est le coup de grâce philosophique. Mais en fait, même si on met Gödel de côté deux minutes et qu'on essaye de construire notre mur brique par brique, on se heurte à un autre problème, purement physique.

Intervenant 23:43

Le cerveau

Intervenant 13:43

humain, tout simplement. Bah oui, construire des preuves par toutes petites étapes formelles, ça crée une complexité vertigineuse. Retenir et vérifier des millions de micro-déductions sans jamais faire une erreur d'inattention, pour nous c'est juste physiologiquement impossible.

Intervenant 23:58

Totalement. L'humain est génial pour l'intuition globale, pour faire des liens inattendus. Mais pour vérifier un million de petites étapes répétitives, on est des processeurs épouvantables.