How Terry Tao Became an Evangelist for AI in Math | Quanta Magazine
- Auteur
- Quanta Magazine
- Thème
- IA
- Mots-clés
- Terry Tao, IA mathématiques, preuves formelles, Lean, collaboration
- Ton
- news
Résumé
Quanta Magazine retrace le parcours de Terry Tao — considéré comme l'un des plus grands mathématiciens vivants — devenu un promoteur actif de l'IA dans la recherche mathématique. En 2014, il prédisait (sous des regards incrédules) que les mathématiciens travailleraient en larges collaborations vérifiées par ordinateur. En 2026, cette vision se concrétise avec les assistants de preuve formelle et les LLMs, et Tao explique où l'IA aide vraiment et où elle bute encore.
💡 Pourquoi ça compte
Terry Tao offre un point de vue rare : celui d'un expert de niveau mondial qui utilise effectivement l'IA dans sa pratique quotidienne et peut donc distinguer le signal du bruit dans les promesses de l'IA pour la recherche scientifique de haut niveau.
Analyse approfondie
De la prophétie à l'évangélisme
En 2014, devant un panel de lauréats du Breakthrough Prize, Tao décrit un futur où des centaines de mathématiciens collaborent et où les preuves sont vérifiées par ordinateur. L'audience trouve l'idée absurde. En 2026, il est devenu l'un des promoteurs les plus actifs de cette vision — parce qu'il la vit dans sa propre pratique.
Où l'IA aide vraiment en mathématiques
Tao distingue plusieurs niveaux d'utilité. Niveau 1 — exploration : les LLMs peuvent générer des idées, suggérer des approches, rappeler des lemmes pertinents. Ils ne sont pas fiables sur la vérité des assertions, mais utiles comme partenaires de brainstorming. Niveau 2 — vérification formelle : les assistants de preuve (Lean, Coq) permettent de vérifier mécaniquement chaque étape d'une preuve. L'IA aide à traduire des preuves informelles en langage formel, accélérant un processus autrefois prohibitivement coûteux en temps. Niveau 3 — rédaction : les LLMs peuvent aider à écrire des sections de papiers mathématiques dans un style formel, sous supervision experte.
Où l'IA bute encore
Tao est explicite : les sauts conceptuels non triviaux — le moment où un mathématicien identifie la bonne structure, la bonne analogie, le bon outil pour attaquer un problème — restent hors de portée de l'IA actuelle. L'IA peut valider des chemins déjà identifiés, pas en trouver de nouveaux de manière autonome sur des problèmes ouverts difficiles.
La vision des grandes collaborations
Le Polymath Project (grandes collaborations mathématiques ouvertes en ligne) était une autre prédiction de Tao en 2014. Les outils IA accélèrent ce modèle : ils permettent de formaliser et vérifier les contributions de nombreux participants, de détecter les erreurs rapidement, et de maintenir une vue cohérente d'un effort distribué. La mathématique devient moins solitaire.