Terence Tao : l’IA suggère, le mathématicien vérifie

Intervenant 10:00

Salut à tous et bienvenue dans cette nouvelle exploration pour le podcast du magazine Tangente. Aujourd'hui, on plonge dans un bouleversement total des mathématiques. Il faut imaginer un instant le plus grand joueur d'échecs au monde, un esprit ultra

Intervenant 20:14

brillant. Un maître qui a l'habitude de toujours calculer ses coups tout seul face à l'échiquier.

Intervenant 10:21

C'est ça. Et d'un coup, il décide de s'entraîner avec un partenaire qui propose des trucs parfois complètement absurdes.

Intervenant 20:27

Complètement fous.

Intervenant 10:28

Mais qui, de temps en temps, sort un coup de génie absolu capable de renverser la partie. Et bien, c'est exactement la dynamique actuelle de Terence Tao.

Intervenant 20:37

La médaille Phil de 2006.

Intervenant 10:38

Voilà le prix Nobel des maths en gros. Et le fait que Terence Tao utilise l'intelligence artificielle au quotidien, c'est un signal sismique pour la communauté scientifique.

Intervenant 20:48

Ah bah c'est clair, c'est pas juste un petit changement d'outil. C'est la structure même de la recherche mathématique qui est en train de se modifier.

Intervenant 10:55

Mais c'est hyper paradoxal, non ? Les maths exigent une précision absolue. Et on sait très bien que des modèles comme GPT-4, ça hallucine en permanence, ça invente des faits.

Intervenant 21:06

C'est le grand reproche qu'on leur fait, oui.

Intervenant 11:08

Du coup, comment c'est possible de concilier cette quête de vérité infaillible avec une machine qui affirme des erreurs avec un aplomb incroyable ?

Intervenant 21:17

Justement, c'est cette capacité à halluciner qui rend l'outil super précieux dans la phase d'exploration. L'IA n'entrevient pas du tout pour valider les preuves. Elle fait quoi alors ? Elle agit comme un partenaire de brainstorming totalement décomplexé. En fait, quand on est enfermé dans des schémas de pensée trop rigides, une suggestion inattendue de la machine, même si elle est fausse,

Intervenant 11:39

Ça permet de débloquer la situation.

Intervenant 21:41

Exactement. Ça permet de débusquer des structures cachées. C'est une façon de casser un problème massif en plein de petites sous-questions. L'erreur générée, elle agit comme une étincelle créative.

Intervenant 11:52

D'accord, donc l'IA génère des idées dans tous les sens, de manière un peu chaotique. Mais puisqu'elle hallucine, comment on transforme cette intuition sauvage en une certitude irréfutable ? Il faut bien un garde-fou derrière.

Intervenant 22:05

Et ce garde-fou, ce sont les assistants de preuves formelles. Des logiciels comme Lean4 ou Coq.

Intervenant 12:10

C'est quoi la différence avec les IA génératifs, du coup ?

Intervenant 22:13

Ben eux, c'est de la logique pure et dure. Faut voir ça comme un compilateur informatique qui refuse catégoriquement d'exécuter un programme s'il manque un seul point-virgule. Ah

Intervenant 12:23

oui, l'intransigeance totale, quoi.

Intervenant 22:25

C'est ça. Ils appliquent la même intransigeance au math. Ils valident l'enchaînement logique ligne par ligne, sans rien laisser passer du tout.

Intervenant 12:33

D'ailleurs, lors d'un récent projet de combinatoire, l'équipe de Tao a utilisé l'IN4 au lait d'écrire la preuve sur papier et l'ont codé dans le logiciel.

Intervenant 22:43

Tout à fait. Et l'effet immédiat, c'est que la machine a forcé l'équipe à expliciter chaque étape intermédiaire, ce qu'on appelle les LEM.

Intervenant 12:49

Parce que d'habitude, les chercheurs font des sauts logiques implicites, j'imagine.

Intervenant 22:54

Voilà, la déduction leur semble évidente, donc ils passent à la suite. Mais Lean4, il n'a aucune intuition. Le logiciel exige que chaque micro-étape soit justifiée.

Intervenant 13:04

Donc, ça met vraiment en lumière toute l'architecture invisible de leurs pensées.

Intervenant 23:08

Exactement. Et le grand objectif futur, c'est l'auto-formalisation, c'est-à-dire relier la fulgurance créative des IA génératives à cette validation implacable des assistants de preuves.

Intervenant 13:21

C'est fascinant. Si on combine un moteur à idées inépuisable et un vérificateur aussi strict, la recherche va s'accélérer de façon vertigineuse. Mais attends, quel est l'impact pour ceux qui apprennent les maths aujourd'hui ?

Intervenant 23:35

Ah, c'est une vraie question.

Intervenant 13:36

Avoir un tuteur algorithmique dispo 24 heures sur 24, c'est super, mais est-ce qu'on risque pas de court-circuiter l'apprentissage lui-même ?

Intervenant 23:44

Si, complètement. Le vrai risque, c'est pas la triche, c'est le phénomène de décharge cognitive. Parce que l'apprentissage rigoureux, ça repose sur le frottement cognitif en fait.

Intervenant 13:55

Le fait de galérer sur un problème, en gros ?

Intervenant 23:56

Ouais. Rester bloqué pendant des heures face à une équation, c'est pas un défaut du processus. C'est le mécanisme par lequel le cerveau construit ses connexions neuronales.

Intervenant 14:07

Donc, sous-traiter cette difficulté à une machine, ça empêche de développer la résilience intellectuelle.

Intervenant 24:13

Exactement. La vraie compétence aujourd'hui, c'est plus juste de résoudre l'équation brute, mais plutôt l'art de formuler le bon problème et d'avoir un esprit critique sur la réponse de la machine.

Intervenant 14:24

L'intuition et le sens du beau restent donc profondément humains. La machine propose plein de chemins, mais c'est l'esprit humain qui reconnaît la pertinence d'une direction.

Intervenant 24:34

C'est un très bon résumé.

Intervenant 14:36

Si une IA suggère une piste de recherche totalement inédite et qu'un humain la transforme ensuite en démonstration irréfutable, à qui appartient réellement la créativité mathématique de cette découverte ? C'est sur cette question vertigineuse qu'on se quitte. À très vite !