IA et mathématiques : le véritable obstacle est la vérification des preuves, pas leur génération

Daniel Litt, mathématicien à l'Université de Toronto, a pris position dans un débat qui agite la communauté mathématique : les intelligences artificielles peuvent-elles véritablement faire des mathématiques ? Invité du podcast d'a16z consacré à la question « L'IA peut-elle apprendre l'intuition mathématique ? », il a formulé une critique à deux niveaux, à la fois technique et philosophique.

Sur le plan technique, Litt identifie un obstacle majeur : les modèles d'IA sont capables de générer des démonstrations, mais peinent à en vérifier la cohérence globale. Pour des preuves courtes, le problème est repérable — les modèles eux-mêmes reconnaissent leurs erreurs quand on les interroge. Mais lorsque la longueur augmente, avec ses enchaînements de définitions, de lemmes et de références, les incohérences se noient dans le texte et le modèle ne dispose pas de mécanisme fiable pour contrôler l'ensemble. Litt illustre ce point par un cas concret : un texte d'environ 800 pages, généré par IA, prétendrait résoudre le problème de résolution des singularités en caractéristique positive — un défi ouvert de longue date en géométrie algébrique, consistant à « lisser » les singularités d'un objet mathématique sans en modifier la structure birationnelle. S'il n'a pas localisé d'erreur précise, Litt juge la preuve invalide : une telle avancée constituerait une percée majeure, or ni les experts humains ni les IA existantes ne sont en mesure d'auditer une telle chaîne de raisonnement de façon rigoureuse.

Sur le plan philosophique, son argument va plus loin. Pour Litt, « le but des mathématiques n'est pas de produire des articles de mathématiques, c'est de produire une forme de compréhension ». Même si une IA encode une certaine forme de savoir dans ses paramètres, cela reste, selon lui, « insatisfaisant » : ce qui manque n'est pas la correction formelle des résultats, mais la curiosité orientée, la capacité à choisir les bons problèmes et à construire une compréhension qui évolue. Il distingue ainsi la maîtrise des artefacts — produire des preuves ou des articles — de la maîtrise réelle du domaine.

Cette prise de position s'inscrit dans un contexte de révision de ses propres anticipations : Litt avait parié que l'IA ne serait pas capable de publier un article de théorie des nombres au niveau des Annals of Mathematics avant 2030, avant de reconnaître avoir sous-estimé les progrès récents. Il maintient néanmoins que le raisonnement vérifiable sur de longues chaînes reste la frontière entre résolution locale de problèmes et recherche mathématique autonome.