Les médaillés Fields avertissent : les mathématiques et les entreprises d'IA n'ont pas les mêmes objectifs

La tension entre la communauté mathématique et les entreprises d'intelligence artificielle n'est plus une discussion de couloir. Dans « Le Monde », vingt-cinq lauréats de la médaille Fields, la plus haute distinction en mathématiques, signent un texte. Ils y écrivent que les objectifs des entreprises d'IA et ceux de la communauté mathématique divergent profondément. Le reproche ne porte pas sur la capacité des modèles à résoudre des exercices. Il porte sur la raison pour laquelle on les résout et sur la manière dont on en parle.

Une preuve n'est pas un produit

Quelques jours plus tard, « Le Monde » a publié un entretien avec Stéphane Mallat, mathématicien à l'ENS, médaille d'or du CNRS en 2025 et coauteur de l'algorithme de compression JPEG 2000. Sa phrase sert de fil conducteur à tout le débat : les preuves produites par l'IA ont peu de valeur en elles-mêmes si nous n'avons pas la préparation nécessaire pour les comprendre. Mallat travaille entre autres sur la malédiction de la dimensionnalité. Dans ce problème, le nombre de configurations possibles croît si vite qu'il n'a plus de sens de se forger une intuition à partir des dimensions basses.

L'argument se formule concrètement. Les mathématiques ne sont pas seulement un ensemble de théorèmes vrais, elles sont aussi une technique pour comprendre pourquoi ils sont vrais. Un vérificateur confirmera la validité d'une écriture formelle. Il ne transmettra à l'élève aucune de ces compétences tant qu'elles n'auront pas été exposées et discutées.

Ce que sait faire aujourd'hui la vérification automatique

En parallèle paraissent des travaux qui montrent à quoi ressemble une collaboration sérieuse entre l'humain et la machine. Dans un article sur arXiv, Mario Carneiro démontre que, dans la théorie des types de l'assistant Lean, le principe du tiers exclu suffit à prouver la cohérence de la théorie des ensembles ZF, sous une forme entièrement formalisée. Sans axiome du choix, sans extensionalité des propositions, sans quotients. C'est un résultat technique, mais il a un poids philosophique : on pouvait jusqu'ici penser que sans opérateur de choix, la force de la théorie des types tombait bien en dessous de ZF.

Le second courant est la recherche assistée par vérification. Un modèle propose des programmes dans le style de FunSearch, un évaluateur strict les note, et la sélection retient les meilleurs. Les auteurs d'un de ces travaux ont mené l'expérience sur un simple ordinateur portable, avec un modèle local de trente milliards et de 120 à 600 échantillons vérifiés par passe. Le résultat est ambigu, et c'est ce qui le rend précieux. La recherche s'est arrêtée après avoir comblé un peu plus de 90 pour cent de l'écart au record sur la tâche phare. Et lorsqu'une indication sur la famille de constructions a été donnée au modèle, la boucle a optimisé l'idée fournie. Aucune des exécutions autonomes ne l'avait découverte.

La question des incitations reste en arrière-plan. Si le critère principal devient le record dans un tableau, les mathématiques se transforment en un ensemble de benchmarks, et non en une pratique de compréhension. La prudence face à une telle simplification n'est pas de l'hostilité envers les outils. C'est la condition pour que ces outils servent durablement à quelque chose.