Imaginez qu'un assistant ultra-rapide vous rende chaque soir une pile de dissertations correctes sur le fond, mais rédigées en cinq fois trop de mots, avec des paragraphes dupliqués et des détours inutiles. Vous seriez soulagé de ne plus avoir à écrire — et submergé de ne plus pouvoir lire. C'est exactement la situation que décrit Terence Tao, médaillé Fields et professeur à l'UCLA, dans un message publié sur Mathstodon fin juin 2026 : l'intelligence artificielle vient de franchir un seuil critique dans la formalisation automatique des preuves mathématiques. Et ce franchissement crée autant de problèmes qu'il en résout.
Un projet, une file de tickets, et soudain le vide
Pour comprendre ce qui s'est passé, il faut d'abord saisir ce qu'est le projet IEANTN — pour Integrated Explicit Analytic Number Theory Network (Réseau intégré de théorie analytique explicite des nombres). Comme le décrit la page officielle de l'IPAM, l'objectif est de construire un réseau vivant d'estimations en théorie analytique des nombres — un domaine où chaque constante numérique compte, où une seule erreur arithmétique peut rendre des dizaines de bornes ultérieures non fiables. Pour cela, Tao et ses collaborateurs formalisent des articles techniques dans Lean, un assistant de preuve développé par Leonardo de Moura et Sebastian Ullrich, décrit dans les actes de CADE 28 comme à la fois un langage de programmation et un vérificateur logique : une preuve Lean n'est pas un texte qu'on lit, c'est un programme que la machine contrôle mécaniquement.
Concrètement, Tao découpait les démonstrations en petits lemmes indépendants, les postait comme tâches ouvertes, et attendait que des volontaires les réclament. Résultat habituel : plusieurs semaines d'attente. Selon le journal de bord personnel de Tao sur le dépôt GitHub du projet, le 18 juin 2026, 22 tâches attendaient encore preneur. Le 21 juin : 7. Au jour 153 du projet, 320 tâches avaient été complétées — et le goulot d'étranglement avait changé de nature.
Ce qui s'est passé entre-temps ? Les outils d'autoformalisation — c'est-à-dire, comme le définissent Yuhuai Wu et ses collègues dans un article de Google Research, « le processus de traduction automatique depuis les mathématiques en langage naturel vers des spécifications et preuves formelles vérifiables par machine » — ont soudainement changé de régime. Presque toutes les tâches postées par Tao sont désormais traitées par l'IA en quelques heures. La file de tickets s'est vidée.
La digestion humaine bloquée
Sauf que voilà le paradoxe. Les preuves générées sont correctes — Lean les accepte, le vérificateur ne bronche pas. Mais elles sont verbeuses à un degré que les humains ne pratiquent jamais volontairement. Des centaines de lignes de plus que ce qu'un mathématicien écrirait. Des étapes redondantes. Des lemmes posés à un niveau d'abstraction inadéquat.
Tao nomme ce phénomène « désadaptation d'impédance » — un terme emprunté à l'électronique, où l'impédance désigne la résistance d'un circuit à recevoir un signal. Ici, le signal, c'est la preuve. Et les trois étages du circuit — génération, vérification, digestion — ne tournent plus à la même vitesse. L'IA a accéléré la génération de plusieurs ordres de grandeur. La vérification formelle par Lean reste rapide. Mais la digestion humaine — comprendre ce que fait la preuve, juger si elle est bien structurée, décider si elle mérite d'entrer dans Mathlib, la grande bibliothèque communautaire de mathématiques formalisées — cette digestion, elle, n'a pas accéléré d'un iota.
Chaque preuve verbeuse ajoute des dizaines de secondes au temps de compilation global du projet. Multipliez par des centaines de lemmes, et l'effet cumulatif devient un vrai problème d'ingénierie.
Ce que l'IA ne peut pas faire seule
Tao a identifié une frontière nette. L'IA excelle dans ce qu'on appelle le code golf local — compresser une preuve existante, éliminer des étapes superflues à l'échelle d'un lemme. Mais la reconstruction globale lui échappe complètement.
Prenez un exemple concret, documenté dans le journal de bord du projet : si un même argument apparaît à plusieurs endroits dans un fichier Lean, un mathématicien humain le reconnaîtra, l'abstraira en un lemme réutilisable, et cherchera si ce lemme n'aurait pas sa place dans Mathlib plutôt que dans un coin isolé du projet. L'IA, elle, peut exécuter cette restructuration si on la lui explique. Elle ne la découvre pas spontanément. Elle construit des mini-bibliothèques locales — autour de l'inversion de Laplace, par exemple — qui sont localement correctes et globalement mal rangées.
C'est exactement ce que pointe le papier LeanMarathon, publié sur arXiv par Yuanhe Zhang et ses collègues : « l'autoformalisation longue-horizon échoue non seulement sur les lemmes difficiles, mais à l'échelle » — par dérive des énoncés, enchevêtrement des dépendances, et réparations locales qui dégradent la cohérence à distance. Le problème de Tao a un nom dans la littérature, et il est systémique.
Vous voyez le renversement ? Avant, le mathématicien attendait que les preuves soient faites. Maintenant, il doit anticiper comment les poser pour que l'IA produise quelque chose d'intégrable. Le goulot d'étranglement s'est déplacé de l'exécution vers l'architecture. Tao le dit lui-même : il passe désormais plus de temps à planifier la portée des tâches qu'à en faire les preuves.
Un nouveau métier pour les mathématiciens ?
Ce basculement a des implications concrètes pour quiconque travaille avec ces outils — chercheurs, étudiants en master, contributeurs à des projets de formalisation. La compétence qui monte n'est plus seulement de savoir démontrer : c'est de savoir décomposer un problème de façon à ce que les sorties de l'IA soient révisables, modulaires, compatibles avec une architecture existante.
C'est une compétence d'ingénieur de bibliothèque autant que de mathématicien. Mathlib, comme le décrit le papier fondateur de la communauté mathlib, a grandi de 15 000 à 140 000 lignes de code en deux ans, portée par 73 contributeurs. Intégrer une preuve dans cet édifice, ce n'est pas juste la rendre correcte — c'est la placer au bon niveau d'abstraction, avec les bonnes interfaces, sans dupliquer ce qui existe déjà. L'IA produit des pièces de puzzle à une vitesse stupéfiante. Mais juger si la forme de la pièce correspond au dessin d'ensemble reste, pour l'instant, un travail humain.
Tao a présenté l'architecture de ce projet lors d'un exposé à l'ICERM le 15 mai 2026, dans le cadre du programme « Techniques and Tools for the Formalization of Analysis ». Moins d'un mois plus tard, le projet avait changé de nature. C'est la vitesse à laquelle ce domaine évolue en ce moment.
Concepts à emporter
L'impédance vue de l'intérieur : ce que mesure vraiment ce seuil
Le terme « désadaptation d'impédance » mérite qu'on s'y arrête, car il cache une structure mathématique précise. Dans un système de traitement de l'information, l'impédance désigne la résistance d'un composant à recevoir ou transmettre un flux. Quand deux composants ont des impédances incompatibles, l'énergie se dissipe à l'interface — c'est une perte, pas un gain.
Appliqué aux preuves, le modèle est le suivant. Appelons G le débit de génération (lemmes produits par heure), V le débit de vérification formelle (acceptations par Lean, par heure) et D le débit de digestion humaine (preuves comprises et intégrées par heure). Pendant des décennies, G était le facteur limitant : les humains produisaient lentement, Lean vérifiait vite, et la digestion suivait sans peine. Le seuil franchi par Tao correspond à un basculement brutal : G a été multiplié par plusieurs ordres de grandeur, V a légèrement augmenté (les preuves plus longues prennent plus de temps à compiler), et D est resté constant. Le goulot d'étranglement s'est déplacé de G vers D.
Ce type de basculement est bien connu en théorie des files d'attente — un domaine de la recherche opérationnelle qui modélise les flux dans des systèmes à ressources limitées. Quand on accélère une étape d'une chaîne, la file se déplace vers l'étape suivante. Ce n'est pas un progrès partiel : c'est un changement de régime complet. La bonne nouvelle, c'est que le système produit plus. La mauvaise, c'est que l'optimisation à faire maintenant est entièrement différente de celle d'avant.
Il y a aussi une dimension combinatoire dans le problème de reconstruction globale. Abstraire un argument répété en un lemme réutilisable, c'est résoudre un problème de factorisation dans un graphe de dépendances : trouver un sous-graphe commun à plusieurs preuves, le nommer, et relier tous les sites d'utilisation à ce nouveau nœud. Ce problème — trouver le « meilleur » facteur commun dans un graphe de preuves — est, dans sa forme générale, computationnellement difficile. Ce n'est pas un hasard si l'IA, optimisée localement, échoue à le résoudre globalement : elle ne dispose pas, par construction, d'une représentation du graphe entier. C'est précisément ce que les chercheurs de LeanMarathon appellent « l'enchevêtrement des dépendances » — et c'est là que l'architecte humain reste, pour l'instant, irremplaçable.
