Comments on Les LLM vont-ils tuer les mathématiques ?

Justement, une vidéo de monsieur phi sur ce sujet https://youtu.be/AYPQIntoJeE?si=J_XUHTm8vMvBlRlN

Tu dis que les LLMs seraient adaptés pour "autoformaliser" les preuves existantes en langage naturel. Je ne suis pas tout à fait sûr. Une grosse partie d'un travail de formalisation, c'est de développer des abstractions utiles "informatiquement" (pas juste mathématiquement), des tactiques, etc. J'ai cru comprendre que les LLMs produisent des formalisations correctes mais de piètre qualité. Se reposer uniquement sur les LLMs pour la formalisation présente d'après moi le même risque que de tout coder avec des LLMs : une base de code immaintenable grevée de dette technique.

Sinon, je suis d'accord avec toi pour les risques des LLMs pour la recherche en maths pures. Enfin le volet "LLMs trop puissant". Le volet "LLMs trop faibles" ne risque pas de l'annihiler, juste de la rendre *très* pénible, c'est un peu différent. Et pour les maths pures, contrairement à la physique la plus théorique, même sans application tout le monde veut savoir ce qu'il y a dans l'univers ou de quoi est composée matière, alors que le programme de Langlands, bon, ça ne fait pas rêver grand monde.

Par contre je serais un peu plus sceptique par rapport à l'art. J'ai l'impression que l'immense majorité des boîtes s'en fichent d'avoir "de l'art" dans leurs produits tant que c'est "suffisant". Pour faire un logo ou une charte graphique, ou même pour une couverture de livre ou pour des éléments graphiques de jeux vidéos, qui va encore payer pour une prestation professionnelle "sans IA" forcément beaucoup plus chère qu'un résultat, même médiocre, produit soi-même beaucoup plus rapidement et moins cher ? Ou même si on passe par un professionnel, on s'attendra à ce qu'il soit plus rapide, ou baisse ses prix en conséquence. Ils ont encore de la chance que les modèles pour vidéos semblent pourris et les modèles pour images restent assez bof et doivent coûter super cher aux entreprises, mais je ne pense pas que sauf pour les "happy few" il y ait tant d'espoir que ça.

@Abie: plan cliquable en haut ?

@Abie : Très bonne suggestion. En attendant, avec Firefox, dom.text_fragments.create_text_fragment.enabled=true puis Menu contextuel > Copy Link to Highlight.

Merci pour cette lecture intéressante, mais que j'ai répartie sur plusieurs jours.
Requête d'accessibilité : il serait utile retransformer tes intertitres en liens /anchors cliquables : il y a des gens à qui j'enverrais bien une partie en particulier pour étayer nos discussions, mais à qui je ne peux pas demander une lecture complète.

https://zenodo.org/records/20302944
"Leiden Declaration on Artificial Intelligence and Mathematics"

Merci pour ce billet, dont je viens d'achever la lecture.

Voici quelques commentaires qui me viennent :

#23, inessentiel au propos général mais je suis curieux : Sans que tu ne précises ton propos par cette footnote, il me semblait que tu parlais de l'existence classique d'énoncés indécidables dans ZFC mais qu'on voit vrais depuis l'extérieur de ZFC. Mais la footnote 23 suggère que tu as en tête une indécidabilité spécifique à tels modèles. Qu'as-tu en tête ? En gros, ce qui me perturbe, c'est qu'avec l'aspect stochastique des modèles, j'ai spontanément envie de croire qu'ils peuvent potentiellement tout produire (mais peut-être y a-t-il néanmoins des bornes provenant de la simple taille des modèles ???).

#25 : Je trouve cela positif et sain que ce ne soit pas un problème d'ego pour toi. J'ignore toutefois si c'est, ou non, généralisable à la communauté mathématique dans son ensemble. Sur ce terrain, je ne peux que fournir mon propre exemple (mathématicien aussi), et je n'en suis pas fier mais l'ego dont tu parles fait pour moi partie du problème.

#29 : ni le beurre ni l'argent du beurre ? ou bien est-il vraiment préférable que ce soit "présence de A et présence de B" ? du beurre rance payé bien cher ?

Dans le scénario où une IA mathématiquement surpuissante serait disponible, je me demande quel serait l'usage préférable. Si on veut comprendre A, deux attitudes sont naturelles : (a) se ruer sur l'IA pour demander un cours sur A ; (b) réfléchir longtemps pour digérer A autant que possible, demander un indice à l'IA si on est bloqué très longtemps, reréfléchir puis, une fois une le problème résolu, demander à l'IA son approche et confronter pour étoffer.

Si on remplace "IA" par "corrigé", ce qu'on recommande à nos étudiants est (b). Appliquerait-on soi-même cela ? Que la réponse soit oui ou non : pourquoi ? La réponse doit-elle ou non être la même selon qu'on parle d'un amateur de mathématiques ou d'un chercheur rémunéré ? En quel mesure le chercheur médian l'applique-t-il déjà si on remplace "IA" par "livre de référence" ou "article existant" ?

Tu dis :

[#9] Modulo, évidemment, des bugs dans l'assistant de preuve (conduisant à la possibilité de prouver ‘⊥’, c'est-à-dire une absurdité). Mais ce serait difficile d'exploiter ce genre de bugs et de faire simultanément une preuve crédible. Si l'IA (supposée non malicieuse) produit une preuve utilisant un bug de l'assistant de preuve, ça va se voir comme le nez au milieu de la figure (à moins qu'elle essaie de le cacher, mais on ne voit pas pourquoi elle ferait ça, du moins tant que le processus d'entraînement n'est pas entièrement automatisé autour du but "faire dire oui à l'assistant de preuve").

Aujourd'hui cela relève de la SF, mais si demain Lean devenait l'outil de contrôle de l'alignement des IA (je ne sais pas vraiment ce que ça veut dire, mais c'est plus ou moins ce que dit Leo de Moura dans ses présentations / comm. autour de Lean) et était utilisé massivement, il est tout à fait possible que les utilisations malveillantes se multiplient. Si les gens se mettent à vibe-Leaner et prennent tout ce qui compile pour démontré on peut imaginer plein de problèmes potentiels difficiles à détecter (car personne n'aura le temps de tout relire, et les IA seraient (supposément) de plus en plus capables).

Sur la question de l'utilisation des LLMs pour générer des preuves formelles : un autre défi c'est que cette utilisation des LLMs ne marche que si on est d'accord sur l'énoncé formel de l'énoncé à prouver.

Or, quand cet énoncé fait appel à des définitions qui ne sont pas basiques, il y a besoin de formaliser ces définitions avant de pouvoir faire quoi que ce soit. Et pour le coup, ce travail de formalisation (= écrire des définitions formelles et établir un consensus collectif sur le fait que ce sont des définitions qui capturent les concepts qu'on a l'habitude de manipuler, qu'elles sont les plus commodes à utiliser possible pour éviter les désagréments formels, etc.), c'est un travail qui n'est pas automatisable et qui nécessite que les humains se mettent d'accord.

Je suis d'accord que l'utilisation des preuves formelles a d'autres inconvénients, notamment si elles tuent les preuves informelles comme tu l'expliques. Mais je me demande si l'effort collectif de formalisation n'a pas aussi quelques bénéfices indirects, par exemple en faisant travailler des matheux de divers horizons à un projet commun dans un langage commun.

Quel excellent billet amha, plein de discernement, et c'est ce dont nous avons besoin à l'ère de l'IA.

La dernière phrase du commentaire signé Armand "Les maths, c'est pour beaucoup un plaisir, comme faire du sport, ou de musique. En quoi les IA pourraient enlever ce plaisir ? la discipline n'a pas besoin d'être professionnalisée pour exister."

m'évoque le cas des échecs. La suprématie de l'IA sur les échecs a dans un premier temps, j'ai l'impression, réduit leur popularité, puis elle est revenue, y compris chez les plus jeunes. Il reste intéressant de faire des choses qu'une machine fait mieux que toi, tout comme il reste intéressant de courir moins vite qu'une Formule 1, ou de plonger moins vite que le faucon.

Quant à la dernière phrase, un peu LLM-style, d'OpenAI, elle mérite un peu mieux que la conclusion du billet principal. C'est un propre des LLM, même bien promptés et harnachés, que de réfléchir en rateau, en donnant a priori un poids similaire à tout ce qu'ils voient du contexte de leur sollicitation d'une part, de leur corpus d'entraînement d'autre part. Il peut rester de l'emploi de mathématiciens pilotes de Formule 1, ou dresseurs de faucons.

D'ailleurs - il y a 45 ans de ça, j'ai défriché ce qui me semblait être un petit bout de maths (sur une façon de parcourir l'espace des permutations circulaires) non traité dans mon programme de 1ère C - et depuis, je n'ai pas trouvé de source google ou de matheux intéressé pour me l'expliquer. Je n'avais même pas pensé à poser la question à l'IA mais c'est le moment !

> pas de trace d'intuition fulgurante, de technique nouvelle, encore moins de génie surhumain (à ce stade)

On peut déjà faire des expériences instructives.
Si on entraîne cette IA avec Gauss et Lagrange, est-ce qu’elle trouve Galois ?
Et si on l’entraîne avec Euclide, est-ce qu’elle trouve Riemann ?
Et si on lui donne les tablettes mésopotamiennes, est-ce qu’elle retrouve tout ce qu’on sait en 2026 ?

>un équivalent de l'expression le beurre et l'argent du beurre, mais en négatif

Ni le beurre, ni l’argent du beurre ?

Un bon LLM c'est un "collègue" qui

1. est prêt à t'écouter inlassablement parler de ton problème préféré
2. a une connaissance énorme de la littérature mathématique
3. travaille 24 heures sur 24
4. est très bon pour le codage de base, les maths de licence/master et le calcul littéral ou numérique
5. dit énormément de bêtises, mais est prêt à les reconnaître comme telles quand tu lui expliques gentiment
6. une fois sur cent, te donne une idée 'bingo!'

Pas mal pour un début.

Au risque d'être pénible, j'aurais aimé que l'introduction de ce billet soit différente. Je trouve le premier paragraphe particulièrement confus et désagréable.

Si personne n'utilisait les LLMs, leurs impacts négatifs sur la société disparaîtraient : l'urgence principale est donc de réduire leur utilisation (comme pour la voiture, l'avion, etc.). Je ne suis pas sûr que culpabiliser les utilisateurs soit un moyen d'y arriver, mais il faut au moins essayer de sensibiliser les gens à ces questions et ne pas faire comme si les LLMs étaient une technologie « neutre » dont on peut évaluer l'utilité dans tel ou tel domaine indépendamment de son impact sur la société.

Lecture recommandée :

Ali Alkhatib, "Defining AI" <URL: https://ali-alkhatib.com/blog/defining-ai >

Clar Fon, "Testing the limits of kindness" <URL: https://txt.ltdk.xyz/testing-the-limits-of-kindness/#a-trap >

Anthony Moser, "I Am An AI Hater" <URL: https://anthonymoser.github.io/writing/ai/haterdom/2025/08/26/i-am-an-ai-hater.html >

Phillip Rogaway, "Radical CS" (un peu plus général) <URL: https://web.cs.ucdavis.edu/~rogaway/papers/radical.pdf >

Jusqu'à hier je partageais ton constat que les LLM servaient surtout à chercher dans la littérature, interpoler les techniques, etc, mais qu'ils ne produisaient rien de vraiment nouveau.

Mais avec un LLM facilement accessible (chatGPT 5.5 thinking à 20€ par mois, peu regardant sur le partage de compte donc on est loin de l'inabordable), je suis récemment tombé de haut.

Je copie le problème ici car il est simple et rigolo: Est-ce qu'une grammaire avec des règles context-free + des règles AA->A peut générer un langage non context-free ?
J'avais réfléchi à ce problème assez longtemps (1 mois ou 2, avec également d'autres chercheurs intéressés), produit une preuve fausse que ça reste CFL, et finalement péniblement construit un contre-exemple dont j'étais plutôt content et que je me disais que les LLM étaient pas près de trouver. Hier ChatGPT a produit un meilleur contre-exemple avec quasiment zéro guidage, à part commencer avec une question intermédiaire naturelle qui ne demande aucune compréhension particulière du problème (commencer avec des règles AB->A). Probablement que ça reste une combinaison d'interpolation de techniques existantes et de bruteforce, mais ça commence à être dur de dire que nous on fait vraiment autre chose. Evidemment je me dis que finalement le problème était plus simple que je croyais et que ça en dit surtout long sur nos blind spots, mais quand même… Et histoire similaire le même jour avec un membre de mon équipe, spécialiste de son domaine (logique linéaire), ChatGPT a "inventé" rapidement un exemple plus simple que celui qu'il avait trouvé un peu laborieusement.

Du coup je ressens un décalage quand tu dis qu'il faut (ou faudra) des IA hors de prix pour avoir une aide qui ne se résume pas à une revue de littérature.
Je partage plutôt ton pessimisme sur l'effet que ça va avoir sur les maths comme activité humaine. A cause de ces quelques data point j'ai l'impression qu'on est en train de vivre un point de bascule, mais bon je ne me risquerai à aucun pronostic tant l'avenir est incertain à tous les points de vue.

Remarques éparses sur http://www.madore.org/~david/weblog/d.2026-05-22.2853.ai-and-math.html#d.2026-05-22.2853

Concernant les mensonges d'OpenAI, je ne vois pas de raisons de penser qu'ils seraient seulement "par omission". Ils ont largement menti concernant les capacités de Sora, leur système de génération de vidéos (<URL: https://futurism.com/the-byte/openai-sora-demo >

Concernant la création de preuves formalisées via des LLM, un point sur lequel je m'étonne que tu ne penche pas plus, c'est la correspondance entre ce que dit le LLM en langage naturel et ce qu'il produit comme code formel. *Rien* ne garantit qu'un LLM qui produit une preuve formelle peut correctement la "traduire" ou la résumer en langue naturelle de façon fiable, et réciproquement une traduction d'une preuve en langue naturelle a aussi des bonnes chances d'être inexacte. Ce que ça veut dire c'est qu'il faut vérifier manuellement que la preuve formelle elle-même, vérifiée par l'assistant de preuve, correspond à ce qu'en dit le LLM. Je pense que c'est un problème qui a notamment des bonnes chances d'apparaître avec une méthode de travail "agentique" où le LLM se relancerait lui-même jusqu'à ce que l'assistant de preuve lui renvoie un OK.

Quand tu dis « soit il produit quelque chose de correct, que l'assistant de preuve accepte, et alors peu importe que la preuve formalisée ne soit pas exactement celle qu'on lui a demandé de traduire, tant qu'elle est bonne », je pense que tu as tort, parce que rien ne dit qu'il n'a pas inclus dans le code accepté une hypothèse qui rend la démonstration triviale (ou en tout cas qui dévierait significativement la problématique qu'on lui aurait posée), et que ça ne peut se voir qu'avec une vérification manuelle de la preuve formelle.

Concernant de futures décisions de moins financer la recherche en maths, je crois qu'il ne faut pas tant y voir une conséquence de progrès réels ou supposés des IA. Ce ne sera au mieux qu'un prétexte. Ce n'est pas comme si nous vivions une période faste de financement pour la recherche fondamentale et c'est assez manifeste que tous les gestionnaires tant dans le public que dans le privé considèrent qu'il ne faut pas payer de gens. C'est pratiquement axiomatique chez eux. Il ne faut jamais prendre au sérieux les justifications à base de conjoncture défavorable ou autre problème budgétaire : ça peut être vrai comme ça peut être faux mais la conclusion préétablie dans tous les cas c'est que rémunérer des personnes est un espèce de tabou et que n'importe quoi vaut mieux (acheter des machins, louer des trucs, acheter des prestations). Si les IA ne fournissent pas un prétexte crédible, on trouvera autre chose.

Concernant les perroquets stochastiques, je pense que tu devrais probablement lire le papier qui a introduit cette expression avant d'affirmer que les LLM n'en sont pas ou que le résultat récent d'OpenAI prouve quoi que ce soit sur cette question.

Enfin : Il me semble que pas mal d'aficionados des LLMs pratiquent une espèce d'aller-retour parfois assez long pour parvenir aux résultats qu'ils désirent. D'une part ça complique pas mal les arguments sur l'automatisation (si un LLM nécessite cinquante étape de promptings et qu'on lui tienne tout le temps la main, y a peu de risque d'une automatisation complète du système), mais aussi ça veut dire que les humains qui prétendent tester les capacités des LLMs leurs fournissent continument des nouvelles information qui compliquent leur évaluation : la capacité des chatbot à faire de la lecture froide est ancienne puisque ça remonte quasiment à ELIZA qui jouait un psy précisément parce que c'est un rôle où le patient amène toute l'information). De là à dire qu'un mathématicien qui trouve de nouveaux résultats avec un LLM est essentiellement en train de pratiquer une forme de Rubber Ducky Debugging sans s'en rendre compte il n'y aurait qu'un pas ( <URL: https://en.wikipedia.org/wiki/Rubber_duck_debugging >).

Il y a des mathématiciens de grand talent chez OpenAI, comme Meehtab Sawhney, co-auteur ne nombre gros résultats avec Ben Green. Le problème n'a pas été choisi au hasard.

Il est clair que le nombre de chercheurs en math va fortement chuter d'ici 20 ans, mais oas d'ici 5 ans. Il va y avoir un période de vibe mathematics, où on guide des agents qui vont faire pour nous, y compris pour les doctorants. Puis à un moment le corpus sera devenu si gros que d'une part tous les trucs auxquels on peut penser assez rapidement auront déja trouvés, et que les choses nécessitant de très longues ruminations subtiles seront sans ceses remisesen cause et donc impossibles.

> Ce n'est pas terriblement compliqué au sens où les outils utilisés sont des techniques et théorèmes habituels de théorie algébrique des nombres (corps CM, théorie du corps de classes, théorème de densité de Čebotarëv, inégalités de Minkowski ; le maximum de technicité étant sans doute ce qui tourne autour de l'inégalité de Golod-Šafarevič[#19]).

Pas terriblement compliqué… je ne sais pas bien où il faut mettre la barre, mais si on nous avait dit il y seulement quelques années qu'une IA nous aurait produit un tel résultat, pas grand monde y aurait cru.

A un niveau moindre, je trouve que l'IA est un formidable outil d'apprentissage, et je pense que ça va créer de meilleurs mathématiciens parce que ça va rendre la connaissance bien plus accessible. C'est peut-être aujourd'hui que les maths sont pour les "happy few".

Les maths, c'est pour beaucoup un plaisir, comme faire du sport, ou de musique. En quoi les IA pourraient enlever ce plaisir ? la discipline n'a pas besoin d'être professionnalisée pour exister.