David Madore's WebLog: 2026-06

(Plan :)

• Les preuves erronées
• La difficulté de vérifier
• Le positif et le négatif
• La difficulté n'est pas une grandeur unique
• Le problème de l'arrêt des exponentielles
• Les maths comme benchmark
• Preuves humaines, trop humaines ?
• Inventivité ?
• Paternité des idées
• Préoccupations pour l'avenir
• Le but des maths n'est pas de résoudre des problèmes
• Le rêve de « résoudre » les maths
• La déclaration de Leiden

☞ Les preuves erronées

D'abord, ça me semble important de souligner que les LLM actuels continuent à l'heure actuelle à produire énormément de démonstrations fausses (théorèmes hallucinés, appliqués avec les mauvaises hypothèses, confusions quand un terme a plusieurs sens, etc.). Même les « bons » modèles. (Oui, les bons en font moins, mais on leur demande des choses plus compliquées, et là ils en font encore beaucoup.) On peut parfois détecter ces erreurs, certainement les réduire, en demandant au LLM de vérifier sa propre preuve, mais même ainsi, la confiance n'est pas terrible. Du coup, si on veut quelque certitude, soit il faut formaliser la preuve en Lean[#2], ce qui n'est possible qu'avec un tout petit bout de la recherche en maths (dont beaucoup de problèmes d'Erdős[#3], qui ont la spécificité d'être très élémentaires), soit la faire vérifier par un expert humain, et là on a un bottleneck, parce que les experts ont autre chose à foutre que vérifier N preuves générées par IA dont beaucoup sont du bullshit.

[#2] Comme je l'explique dans un bout de mon précédent billet sur le sujet, Lean est un outil informatique dans lequel on peut exprimer des preuves mathématiques de façon formelle, et qui vont alors la vérifier (de façon complètement automatisée, et fiable). On peut demander à un LLM d'écrire ou de convertir la preuve en Lean. Mais pour que la preuve soit effectivement formalisable en Lean, il faut que tous les outils qu'elle utilise aient été eux-mêmes préalablement formalisés en Lean, ce qui, à l'heure actuelle, est loin de couvrir la totalité du spectre des mathématiques connues.

[#3] Paul Erdős était grand collectionneur de problèmes mathématiques, et ses problèmes sont devenus une sorte de défi pour les boîtes d'IA (je me demande ce qu'Erdős lui-même aurait pensé de cette situation, d'ailleurs). Mais il faut souligner que les problèmes d'Erdős représentent les intérêts du collectionneur, et qu'ils ont notamment un biais très important en faveur des énoncés élémentaires, souvent sans grande théorie derrière, et de certains domaines particuliers des maths (grosso modo : la combinatoire, la théorie des graphes, la théorie des nombres « élémentaire » / combinatoire / additive, éventuellement la théorie descriptive des ensembles).

En fait, c'est complètement con : on a automatisé une partie intéressante de la résolution de problèmes mathématiques (trouver une preuve), mais pas vraiment la partie chiante (vérifier les preuves), qui est pourtant, du point de vue théorique, parfaitement automatisable. (Un peu comme on préférerait que les IA nous débarrassent des choses chiantes de la vie, comme le ménage, et pas des choses créatives et intéressantes.)

☞ La difficulté de vérifier

Et en pratique, ce qui est en train de se passer en ce moment en maths, ce n'est pas tant que les problèmes ouverts tombent les uns après les autres (à part les problèmes d'Erdős), c'est que tout le monde est noyé par les preuves bidon produites par IA : avant, pour reconnaître un crackpot en maths c'était très facile (juste au style), maintenant, comme les preuves bidon produites par IA sont superficiellement hyper plausibles, c'est devenu extrêmement difficile de savoir sauf à tout lire en détails. Là on a un vrai problème.

(Et à moins de tout formaliser, ce n'est pas clair que le progrès des LLM nous tire d'affaire, parce que ce qui compte est le rapport entre leur capacité à générer du bullshit avancé et leur capacité à en détecter, et c'est pas évident comment il évolue.)

☞ Le positif et le négatif

C'est pour ça que je souligne que, à l'heure actuelle, il n'est pas du tout clair que la contribution des IA aux maths soit positive (même en ignorant totalement leurs coûts !). Il y a des termes >0 et des termes <0, et j'ai personnellement tendance à penser que la somme est <0.

Je peux aussi mentionner l'impact négatif qu'ont les LLM sur le site MathOverflow (une sorte de réseau social des mathématiciens, sous forme de questions-réponses); on peut toujours rêver qu'elles vont remplacer ça en mieux, mais pour l'instant ce n'est pas clair (ni gratuit !).

Donc je trouve assez fallacieux de ne parler que des progrès que les LLM ont apportés pour certains problèmes et de taire complètement tous les aspects négatifs sur la discipline. Peut-être que les contributions >0 vont augmenter à l'avenir, mais les <0 risquent d'empirer aussi ! Bref, bien malin qui saura dire à quoi ressemblera la somme.

L'enthousiasme (d'ailleurs assez relatif) de gens comme Terry Tao[#4] n'engage qu'eux : ce n'est pas parce qu'il est très fort que son avis est plus important que n'importe quel autre mathématicien. Et je trouve d'ailleurs significatif que la vidéo ne retienne, des commentaires de 9 mathématiciens sur la preuve d'OpenAI du unit distance problem, que les plus positifs : j'encourage beaucoup à lire ceux de Melanie Matchett Wood, avec lesquels je me sens très en phase.

[#4] Terence Tao est professeur à UCLA, médaillé Fields, et considéré par beaucoup comme un des plus brillants mathématiciens vivant actuellement (voire le plus brillant, parce qu'il a un fan-club franchement pénible ; mais indiscutablement il est très fort pour résoudre des problèmes, et aussi capable de comprendre un nombre impressionnant de domaines différents des mathématiques). Il fait preuve d'un certain enthousiasme pour le rôle que les IA vont jouer dans l'avenir des mathématiques, ce qui agace parfois certains collègues, surtout que ses propos sont pas mal utilisés par les zélotes de l'IA. (Mais bon, il est aussi signataire de la déclaration de Leiden, donc ce n'est certainement pas un enthousiasme sans réserves.)

☞ La difficulté n'est pas une grandeur unique

Beaucoup de spéculations (notamment dans la vidéo de Monsieur Phi) se fondent sur l'idée implicite que la difficulté d'un problème mathématique est une sorte de valeur objective, et notamment qu'elle serait la même pour les LLM et pour les humains. Vu qu'elle est déjà hyper différente d'un humain à l'autre, ça me semble particulièrement audacieux, comme hypothèse. Mais en tout cas, l'idée que les LLM deviennent très bons pour certains problèmes très durs pour les humains donc ils vont dépasser les humains en tout (je ne dis pas que la conclusion est fausse), elle repose sur une hypothèse très douteuse sur la nature linéaire de la difficulté mathématique.

Évidemment, c'est difficile de tester l'hypothèse il y a des problèmes de maths faciles pour les humains et difficiles pour les LLM parce que tout ce qui a jamais été écrit par un humain est connu des LLM (donc par définition elles savent faire), et qu'on ne sait même pas dans quelle direction chercher. Mais le fait est que certains collègues trouvent les LLM vraiment mauvais et d'autres spectaculairement bons, et on ne comprend pas bien la raison de ces différences (nature des problèmes ? qualité des modèles ? capacité à prompter efficacement ? effet placebo/nocebo dû aux préjugés sur les IA ?), mais pour l'instant on n'a vraiment aucune mesure scientifique sérieuse, juste plein d'anecdotes. En tout cas il est probable que les problèmes d'Erdős ne soient pas hyper représentatifs.

Je résumerais un peu la situation actuelle à celle où une boîte pharmaceutique aurait un produit à vendre et on mettrait en avant plein de témoignages de gens qui ont été guéris par ce médicament : je ne dis pas que ça ne dit rien, mais ça ne remplace pas une étude scientifique.

☞ Le problème de l'arrêt des exponentielles

La spéculation puisque les progrès sont très rapides, ils vont forcément aller extrêmement loin me semble particulièrement infondée : je ne sais pas quel mur les LLM peuvent risquer de heurter (économique ? énergétique ? technologique ? du processus d'entraînement ? de la nature même du modèle ?) mais je ne vois aucune raison particulière de penser que la position de telle ou telle barrière (si elle existe) est corrélée à la vitesse à laquelle on fonce dessus. Comme je le dis tout le temps (et comme j'ai passé toute la pandémie de covid à expliquer) : observer une exponentielle ne dit rien sur la manière dont elle s'arrêtera.

☞ Les maths comme benchmark

En tout état de cause, les développements ultra-rapides de ces derniers mois me semblent largement dus à une décision stratégique : OpenAI et les autres boîtes d'IA ont décidé d'utiliser les maths comme « benchmark »[#5] censément objectif pour montrer leur supériorité les unes sur les autres (notamment dans le contexte de l'introduction en bourse d'OpenAI). Évidemment, ce qui les intéresse n'est pas de faire des maths ni d'aider la science ou les mathématiciens, mais de vendre leurs produits. OpenAI a clairement décidé d'investir massivement pour une annonce spectaculaire, en ciblant les problèmes d'Erdős spécifiquement. Je ne dis pas que les LLM ne peuvent pas progresser plus généralement, mais il faut une certaine naïveté pour s'imaginer que ce développement est représentatif de quelque chose qui pourra être soutenu, ou qu'il est représentatif des maths en général, pire, de l'intelligence en général.

[#5] Comprendre : comme moyen d'évaluation, comme test pour se comparer les unes aux autres.

(Et là je me dois de citer la loi de Goodhart comme je le fais souvent : utiliser les maths / problèmes d'Erdős comme benchmark pour les IA avait peut-être un sens, mais dès que les boîtes s'en sont aperçu, ça a cessé d'être un bon benchmark.)

C'est donc notamment à cause de ça que beaucoup de mathématiciens sont exaspérés de la manière dont les boîtes d'IA font leur pub sur leur dos et leur donnent un rôle quasiment de prospectus publicitaire, au détriment de la discipline.