Quand le meilleur mathématicien du monde change sa façon de penser

Imaginez un grand maître d'échecs qui, après des décennies à jouer seul face à l'échiquier, se retrouve soudain avec un partenaire capable de suggérer des coups inédits — parfois brillants, parfois absurdes, mais toujours surprenants. C'est à peu près ce que vit Terence Tao depuis qu'il a intégré l'intelligence artificielle dans sa pratique quotidienne des mathématiques. Et quand Tao parle, la communauté mathématique mondiale tend l'oreille.
Qui est Terence Tao ? En deux mots : le mathématicien vivant le plus admiré de sa génération. Australo-américain, né en 1975, il a reçu la médaille Fields en 2006 — l'équivalent du prix Nobel en mathématiques, décerné tous les quatre ans à des chercheurs de moins de quarante ans pour des travaux jugés exceptionnels. Tao travaille sur des domaines aussi variés que la théorie des nombres, l'analyse harmonique ou les équations aux dérivées partielles. Ce n'est pas un mathématicien spécialisé dans un seul couloir : c'est quelqu'un qui traverse les murs entre disciplines avec une aisance déconcertante.
Depuis plusieurs années, il est aussi l'une des voix les plus sérieuses et les plus nuancées sur l'intégration de l'IA dans la recherche mathématique. Récemment, il a publié une synthèse de ses expériences et accordé plusieurs interviews pour détailler ses observations. Le tableau qu'il brosse est loin d'être celui d'un enthousiaste naïf — ni d'un sceptique réfractaire.

L'IA comme assistant de recherche : ni oracle, ni outil banal

Pour comprendre ce que l'IA change dans le travail d'un mathématicien, il faut d'abord comprendre à quoi ressemble ce travail. Contrairement à ce qu'on imagine souvent, un mathématicien de haut niveau ne passe pas ses journées à calculer. Il cherche des structures, des régularités cachées, des chemins logiques qui relient des vérités entre elles. Une démonstration mathématique, c'est une chaîne d'arguments où chaque maillon doit être irréfutable — une seule faille, et tout s'effondre.
Dans ce contexte, les grands modèles de langage — ces systèmes d'IA entraînés sur d'immenses corpus de textes et capables de produire du langage cohérent, comme GPT-4 ou ses équivalents — ont d'abord semblé peu adaptés aux mathématiques. Les mathématiques exigent une précision absolue ; ces systèmes, eux, sont connus pour « halluciner », c'est-à-dire produire des affirmations fausses avec une confiance imperturbable.
Pourtant, Tao rapporte quelque chose d'inattendu : utilisés correctement, ces outils peuvent agir comme un sparring partner intellectuel — un partenaire d'entraînement. Pas pour valider des démonstrations (ils ne sont pas fiables pour ça), mais pour explorer rapidement des pistes, reformuler un problème sous un angle différent, ou identifier des analogies avec des résultats connus dans d'autres domaines. En somme : pour accélérer la phase d'exploration, avant même que la rigueur entre en jeu.

« L'IA ne remplace pas la démonstration. Mais elle peut changer la façon dont on cherche quoi démontrer. »

—

Ce que l'IA fait à la cognition mathématique

Là où Tao devient vraiment fascinant, c'est quand il parle non pas de ses résultats, mais de ses processus mentaux. Travailler régulièrement avec des outils d'IA, dit-il, modifie la façon dont on formule les problèmes. On apprend à décomposer une question complexe en sous-questions plus précises — parce que l'IA répond mieux à des requêtes bien ciblées qu'à des demandes vagues. Ce faisant, on affine sa propre pensée.

C'est un phénomène bien connu en psychologie cognitive : l'outil façonne l'utilisateur autant que l'utilisateur façonne l'outil. La calculatrice a changé la façon dont on pense au calcul numérique. Les logiciels de géométrie dynamique ont changé la façon dont on explore les figures. L'IA générative est en train de changer la façon dont on explore les espaces de possibilités mathématiques.

Mais cette transformation soulève aussi une question inconfortable : si l'IA suggère une direction de recherche, et que le mathématicien la suit jusqu'à une démonstration valide, à qui appartient l'intuition ? La créativité mathématique est-elle encore entièrement humaine ? Tao ne tranche pas — et c'est précisément ce qui rend sa position intéressante. Il ne cherche pas à rassurer. Il observe.

La démonstration formelle assistée : un chantier en cours

Au-delà des grands modèles de langage, Tao s'intéresse aussi à une autre famille d'outils : les assistants de preuve formelle, comme Lean ou Coq. Ces logiciels permettent de vérifier mécaniquement chaque étape d'une démonstration mathématique — un peu comme un correcteur orthographique, mais pour la logique pure. Si une étape est fausse ou incomplète, le système le signale immédiatement.

Tao a participé à des projets collaboratifs utilisant ces outils, notamment pour formaliser des résultats complexes avec l'aide de dizaines de contributeurs en ligne. L'expérience lui a montré que la formalisation force à expliciter des hypothèses qu'on laisse habituellement implicites — ce qui peut révéler des lacunes insoupçonnées, même dans des démonstrations réputées solides.

L'enjeu à long terme est considérable : si l'on pouvait combiner la puissance exploratoire des grands modèles de langage avec la rigueur vérificatrice des assistants de preuve formelle, on disposerait d'un outil capable à la fois de proposer des pistes et de les valider. Nous n'en sommes pas là — mais la trajectoire est visible.

Ce que ça change pour les étudiants et jeunes chercheurs

Pour un étudiant en mathématiques ou un jeune chercheur, les implications sont immédiates et pratiques. Premier point : l'IA peut être un tuteur disponible vingt-quatre heures sur vingt-quatre, capable d'expliquer un concept sous dix angles différents jusqu'à ce que l'un d'eux fasse tilt. C'est précieux, surtout dans les moments où l'on hésite à déranger un directeur de thèse pour une question qui semble « trop basique ».

Deuxième point, plus délicat : le risque de court-circuiter l'effort cognitif. Apprendre les mathématiques, c'est en grande partie apprendre à rester bloqué — et à s'en sortir par ses propres moyens. Ce frottement inconfortable est le moteur du développement intellectuel. Si l'IA fournit systématiquement la sortie de secours, elle peut priver l'apprenant du bénéfice de l'obstacle. Tao insiste sur ce point : l'outil doit amplifier la pensée, pas la remplacer.

Troisième point : les compétences qui comptent sont en train de changer. Savoir poser les bonnes questions à un système d'IA — ce qu'on appelle le prompting, l'art de formuler des requêtes efficaces — devient une compétence à part entière. Savoir évaluer critiquement une réponse générée par une IA, identifier ses erreurs, en extraire ce qui est utile : voilà des aptitudes que les formations mathématiques vont devoir intégrer explicitement.

Ni utopie, ni dystopie

Ce qui ressort du bilan de Tao, c'est une posture rare dans les débats sur l'IA : ni l'enthousiasme béat qui annonce la fin du travail humain, ni la résistance crispée qui refuse de voir ce qui change réellement. Les mathématiques, dit-il en substance, restent une activité profondément humaine — mais le contexte dans lequel cette activité se déroule est en train de se transformer à une vitesse sans précédent.

La vraie question n'est pas « l'IA va-t-elle remplacer les mathématiciens ? » — la réponse est non, du moins pour tout ce qui touche à la créativité, à l'intuition profonde, au sens de ce qui est beau ou important en mathématiques. La vraie question est : « Comment former des mathématiciens capables de travailler avec ces outils sans en devenir dépendants ? » Et à cette question, même Terence Tao n'a pas encore de réponse définitive. Ce qui, quelque part, est rassurant.

Concepts à emporter

  • Terence Tao est médaillé Fields — le « Nobel des maths » — et il utilise l'IA dans sa recherche depuis des années : si lui le fait sérieusement, c'est que le sujet mérite vraiment d'être pris au sérieux.
  • L'IA ne démontre pas à la place du mathématicien : elle aide à explorer les pistes avant que la rigueur entre en jeu — comme un GPS qui propose des itinéraires, mais c'est vous qui conduisez.
  • Utiliser l'IA régulièrement change la façon dont on pense les problèmes — pas seulement la façon dont on les résout. L'outil modifie le cerveau qui l'utilise.
  • Il existe des logiciels capables de vérifier chaque étape d'une démonstration mathématique comme un correcteur orthographique vérifie chaque mot — et ils révèlent parfois des failles dans des preuves que tout le monde croyait solides.
  • Pour les étudiants, le vrai danger de l'IA en maths n'est pas la triche : c'est de ne plus jamais rester bloqué — et donc de ne plus apprendre à se débloquer seul.

Pour les matheux

L'une des applications les plus rigoureuses de l'IA en mathématiques concerne la vérification formelle de preuves. Dans ce cadre, une démonstration n'est pas écrite en langage naturel mais dans un langage formel compris par un logiciel — par exemple Lean 4. Chaque étape de la preuve est une instruction que le système vérifie mécaniquement selon les règles de la logique et les axiomes choisis (généralement ceux de la théorie des types dépendants, ou de la théorie des ensembles de Zermelo-Fraenkel). Tao a contribué au projet Polynomial Freiman-Ruzsa (PFR), où une preuve combinatoire complexe a été entièrement formalisée dans Lean en quelques semaines grâce à une collaboration distribuée. Ce qui est mathématiquement remarquable : la formalisation a forcé les auteurs à expliciter des lemmes intermédiaires qui étaient implicites dans la preuve originale, révélant la structure fine du raisonnement. À terme, l'enjeu est de coupler ces assistants de preuve avec des modèles de langage capables de générer des candidats de preuve — ce que certains appellent l'autoformalization : la traduction automatique d'énoncés en langage naturel vers des preuves formelles vérifiables.
Source : article en allemand dans Der Standard