Preuves par IA : le paradoxe signalé par Terence Tao

Intervenant 10:00

Bienvenue dans le podcast du magazine Tangente. Alors, imaginons une seconde une situation un peu absurde. En fait, qu'arriverait-il si un assistant générait chaque soir des textes parfaits sur le fond, mais genre cinq fois trop longs, avec des paragraphes duplifiés à l'infini ?

Intervenant 20:17

C'est clair que le soulagement de ne plus avoir à écrire, ça se transformerait très vite en un

Intervenant 10:22

En un cauchemar absolu de lecture.

Intervenant 20:25

Exactement. C'est très paradoxal, mais c'est très précisément le mur que la recherche mathématique de pointe est en train de percuter aujourd'hui.

Intervenant 10:32

Et c'est ce qu'on va décortiquer dans notre plongée du jour. Notre mission, en gros, c'est de comprendre comment l'intelligence artificielle vient de bouleverser la création mathématique. Et pour explorer ça, on s'appuie sur des sources incroyables, notamment une alerte publiée fin juin 2026 par le célèbre médaillé Fields, Terence Tao, sur la plateforme Mestodon.

Intervenant 20:53

C'est un corpus vraiment fascinant. Et pour bien comprendre l'alerte de Terence Tao, il faut jeter un œil à son projet de recherche, le projet INATNN.

Intervenant 11:04

Ah oui, de la théorie analytique des nombres, c'est ça. Un domaine hyper exigeant où la moindre petite erreur arithmétique détruit tout l'édifice. Je suis toujours fascinée par la rigueur que ça demande.

Intervenant 21:16

C'est carrément ça. Et justement, pour éviter ces erreurs fatales, les chercheurs s'appuient sur un outil génial qui s'appelle Lean.

Intervenant 11:24

Lean, ouais. J'ai lu que c'est un assistant de preuves, donc en fait ça transforme une démonstration classique en un programme informatique.

Intervenant 21:31

Tout à fait. La machine vérifie ensuite mécaniquement que la logique est infaillible. Et historiquement, ce travail était découpé en petites tâches, ce qu'on appelle des lèmes.

Intervenant 11:41

Alors, pour ceux qui ont oublié leur cours de fac, un lème, c'est juste une étape intermédiaire, un petit tremplin technique pour ensuite démontrer un théorème beaucoup plus massif.

Intervenant 21:53

C'est le mot parfait, un tremplin. Et avant, des volontaires humains mettaient des semaines à traiter ces lèmes. Mais au printemps 2026, l'IA s'est mise sur le coup et…

Intervenant 12:02

Et boum ! Elle a vidé la file d'attente à une vitesse fulgurante. Les chiffres sont dingues. Entre le 18 et le 21 juin, le nombre de tâches en attente est passé de 22 à 7. Et au jour 153, 320 tâches étaient complétées.

Intervenant 22:20

Ouais, le projet a radicalement changé de nature en moins d'un mois. C'est une usine qui a multiplié sa production par mille.

Intervenant 12:26

Mais attends, je t'arrête deux secondes. Si l'IA produit une montagne de preuves parfaites, validées par l'outil Lean, en un temps record, en quoi c'est un problème au juste ? Ça ressemble au rêve absolu pour un chercheur, non ?

Intervenant 22:37

Ben, c'est là toute la subtilité. C'est ce que Tao appelle la désadaptation d'impédance. Le souci, c'est le style de l'IA. Ses preuves sont justes, Lean les accepte sans broncher, mais elles sont atrocement verbeuses.

Intervenant 12:50

Ah, je vois le genre. Là où un humain utiliserait une abstraction élégante ou un raccourci intuitif, l'IA utilise la force brute.

Intervenant 22:58

Exactement. Elle détaille chaque micro-étape de manière redondante. En théorie des files d'attente, on dit que le débit de génération a explosé, la vérification par la machine suit, mais le débit de digestion humaine, lui, il stagne.

Intervenant 13:12

Le cerveau humain sature face à ces blocs de codes illisibles, quoi. Le goulot d'étranglement a simplement muté.

Intervenant 23:18

C'est ça. L'humain n'arrive-tu à relire assez vite ?

Intervenant 13:21

C'est quand même super contre-intuitif. On entend souvent que l'IA est imbattable pour faire du code golf. Tu sais, optimiser un code pour qu'il soit le plus court possible. Pourquoi elle n'y arrive pas en maths ?

Intervenant 23:32

Alors, elle sait très bien le faire sur un LEM isolé, mais elle est complètement aveugle à l'échelle d'une bibliothèque entière. Un papier de recherche très éclairant, Lean Marathon, de Yuan Zhang, explique que l'IA échoue parce qu'elle ne s'est pas factorisée dans un graphe de dépendance.

Intervenant 13:48

Oula, factorisée dans un graphe de dépendance. Il va falloir m'aider avec une image là, parce que ça sonne très abstrait.

Intervenant 23:55

Pas de souci. Imagine une immense ville construite en Lego. Si tu veux créer une nouvelle forme de brique aux fondations d'un immeuble, pour qu'elle puisse aussi soutenir trois autres bâtiments plus loin, Il faut repenser toute l'architecture du quartier en même temps.

Intervenant 14:08

Ah oui, c'est un calcul d'une complexité gigantesque.

Intervenant 24:11

Voilà. Face à ça, l'IA préfère construire plein de petites tours isolées et identiques plutôt que de relier les fondations entre elles.

Intervenant 14:18

Ce qui explique cette explosion hallucinante de l'USIA. La grande bibliothèque de l'IN Matlib est passée de 15 000 à 140 000 lignes de code en un éclair. Donc en fait, le métier même de mathématicien est en train de muter radicalement.

Intervenant 24:32

Complètement. Le mathématicien devient un véritable ingénieur d'architecture. La compétence clé, ce n'est plus de rédiger la preuve, c'est de décomposer le problème.

Intervenant 14:41

C'est dingue ! On ne démontre plus ? On anticipe les structures pour encadrer le travail de la machine ? C'est concevoir tout le système d'indexation pour que l'IA range ses livres sans faire s'effondrer l'édifice ?

Intervenant 24:52

C'est une excellente façon de le résumer.

Intervenant 14:54

C'est fascinant et un peu vertigineux quand même. Ce qui amène une dernière réflexion assez troublante. Si un jour, l'intelligence artificielle développe la capacité de structurer d'elle-même cette immense architecture globale, les mathématiques deviendront-elles un édifice si vaste et si dense que l'esprit humain pourra seulement l'interroger sans jamais en comprendre pleinement les plans ?

Intervenant 25:16

C'est le grand mystère des prochaines années.

Intervenant 15:18

On laisse cette question en suspens. Merci de nous avoir suivis et à très vite pour une nouvelle Plongée mathématique.