Comments on Sur la destruction des maths par les boîtes d'IA

Post intéressant ! Eh oui : l'IA c'est bien le grand stérilisateur, le Midas à l'envers qui transforme tout en plomb. Même si ça a du sens, c'est fait par quelque chose qui n'a aucune ouverture à ce qu'est le sens pensé et c'est une aliénation totale de devoir se plonger dans le capot de ce qui pond des résultats dont il n'a cure, ça je vois tout à fait. Vivement que l'IA régresse si c'est possible, peu de mouvements sociaux récents m'ont aussi intéressé que la fronde américaine contre les datas centers.

Rassuré de voir qu’effectivement, L’IA ne parvient pas à faire ce que fait Grothendieck :

https://gilkalai.wordpress.com/2026/09/22/be-a-grothendieck-on-ai-and-mathematics/

Ça ne résout pas les problèmes concrets immédiats, mais ça résout quand même le problème existentiel.

Tout ça est quand même hyper pessimiste ! On a maintenant accès à un outil qui permet de faire des progrès formidables. Oui, on peut toujours trouver des problèmes et s'apitoyer, mais comment prétendre que ça va ralentir la recherche ? Est-ce que des médecins se plaindraient si l'on accélérait la découverte de médicaments, ou des physiciens si l'on permettait une meilleure compréhension du monde ?

Quant aux préoccupations bien plus mondaines sur le sort des mathématiciens professionnels, là aussi les réactions sont totalement exagérées. Qui attribue les doctorats, les postes universitaires, les financements, voire les prix ? Ce sont d'autres mathématiciens ! Ils vont continuer à perpétuer leur système, peut-être au prix de quelques reframings de circonstance.

On voit mal aussi pourquoi les financements publics devraient soudainement se tarir. Si l'on donnait de l'argent à des chercheurs pour chercher la preuve de théorèmes abstraits pour la gloire de la connaissance, on leur donnerait exactement la même chose pour comprendre les preuves générées par IA, ou pour trouver de nouvelles questions et faire avancer la science en s'épaulant sur ces outils.

Et même si les financements de recherche en maths se voyaient soudainement réduits, qu'est-ce que la société y perdrait vraiment ? Les jeunes mathématiciens pourraient se réorienter vers des thématiques un peu plus appliquées, ou faire les maths qu'ils veulent sur leur temps libre, à côté d'un travail alimentaire (au hasard, l'enseignement des maths, ce qui n'est d'ailleurs pas très différent de ce qu'on demande déjà aujourd'hui aux enseignants-chercheurs).

Tout ça c'est de la discrimination contre les IA. Elles ont le droit de faire des mathématiques connement autant que nous. Et on n'a jamais jeté de pierres à Ramanujan parce qu'il trouvait des formules sans les comprendre - et elles étaient parfois même fausses.

On vient de se prendre Ramanujan puissance Oméga sur la tête. Bah, on n'a qu'à retourner le poison contre lui-même et obliger les IA à nous aider à comprendre les preuves, voire les minimiser, encore plus cruel les beautifier.

Je pense il y a beaucoup à dire sur le sujet de "Combien de confidence doivent on apporter aux preuves Lean?" surtout si c'est un preuve imbitable pondu par un LLM.

Sur tout que de de point de vue d'un IA entraîné à être très fort en Lean, elle n'est pas directement entraîné à être fort en math en genèrale, et il y a un petit différence. Di elle trouve un preuve du faux cause par un bug où simplement le fait que la logique est incohérente, elle a intérêt à le bien cacher pour pouvoir démontrer tous ce qu'elle est demandé avec.

Au faite des preuves faites en Lean par des humains sont plus digne de confiance car en général les mathématiciens n’essaient pas de trouver une faille dans Lean ou sa logique, on peut plus appuyer sur leur réputation etc.

Autre que ça, il paraît que la la logique même du Lean repose sur un fondement étonnamment fragile et mal-maîtrisé: <URL: https://www.lesswrong.com/posts/zHhGa3iQBQcdSifFL/a-critical-look-at-lean4-1> . Peut être un peut moins maîtrisé qu'on peut espérer pour LE assistant de preuve choisi pour formaliser les maths *~*

P.S. Je pense que 100% Hilbert aurait été un AI bro xD. (Nan en vrai j'en sait rien, mais ça aurait été drôle)

J'essaye de propager un meme (en espérant bien être le premier à en avoir eu l'idée) :

Wir müssen uns anpassen, wir werden uns anpassen.

@Apocalypse: ben non mdr: http://www.madore.org/~david/weblog/d.2006-09-19.1360.html

Est-ce qu’Apokrif est Apocryphe ?

Je n'avais pas compris que c'était toujours la même personne, Levent Alpöge, qui était impliquée du côté d'Anthropic. Bien fait pour lui.

Ce que tu dis résonne beaucoup avec mes interrogations en ce moment : je viens de commencer mon doctorat, est-ce qu'il y aura encore de la recherche quand je l'aurais terminé ? Franchement, je ne sais pas si j'ai envie de continuer après… Et vu les angoisses de la plupart de mes collègues, même en informatique, l'avenir n'est pas très lumineux.

Sinon, je trouve ta position sur l'utilisation de l'IA très sensée, parce que j'ai vraiment l'impression qu'autour de moi on est sur du tout ou rien (et surtout, mais pas uniquement, du rien).

Utiliser https://www.lesnumeriques.com/intelligence-artificielle/c-est-un-cataclysme-cedric-villani-et-24-autres-medailles-fields-se-disent-secoues-par-la-percee-mathematique-de-l-ia-n262074.html plutôt que l'URL horrible fournie par Lucien ;-)

@Lucien: pourquoi se compliquer la vie en passant inutilement par un site Google utilisant une URL illisible ?

"C'est un cataclysme" : Cédric Villani et 24 autres médaillés Fields se disent secoués par la percée mathématique de l'IA - Les Numériques https://share.google/dV7jms8pQLnaNi8kZ

Billet qui contient des sujets intéressants. Mais j'ai l'impression que tu ne proposes pas grand chose, au final, après c'est peut-être pas forcément une critique, on a le droit d'avoir un diagnostic, sans forcément proposer un traitement.

Un point quand même : je ne vois pas pourquoi le fait qu'un modèle de langage ait pu obtenir la réponse à telle ou telle conjecture soit fondamentalement différent de la situation où un humain très fort trouve à la force de son travail acharné, dans son coin, la solution à un problème très difficile.

En général, un mathématicien qui travaille seul (ça existe encore), on lui en tient pas rigueur (et heureusement). Il ne divulgue pas toutes les étapes infructueuses de son travail, et on lui en tient pas rigueur. Pourquoi ce double standard ?

Tu parles du problème de la création de question : mais en quoi le fait d'avoir la solution empêche ou bloque la création de questions ? Si un humain se donne la peine de comprendre la solution, il aura très certainement des nouvelles questions (du genre, est-ce que cette méthode marche sous telle nouvelle hypothèse, etc.)

Par exemple, tu sembles mécontent du fait qu'une IA ait pu construire une structure complexe sur S^6 car du coup personne ne va se donner la peine d'en construire une (?)

En quoi le fait d'en avoir une d'origine non-humaine bloquerait la curiosité d'en construire une autre, ou même de comprendre celle qui a été construite ? Est-ce parce que c'est du "slop", ou parce que ça vient d'une machine ? C'est assez limité comme argument. Et surtout, il est assez bancal, parce qu'on pourrait l'appliquer à n'importe quel article correct d'origine humaine un peu imbittable ou mal écrit résolvant n'importe quelle conjecture.

Dans la même veine :

Tony Padilla dans Numberphile parle de Navier-Stokes.
https://www.youtube.com/watch?v=3geDF-DAwpg
https://www.youtube.com/watch?v=aom4269UgSM
Trop Long; Donne Résumé :
Même idées que David Madore, et une petite explication de comment fonctionne la solution proposée.

Et Pravesh Kothari, Raghu Meka, Prasad Raghavendra sur le blog de Scott Aaronson : https://scottaaronson.blog/?p=10116

TL;DR :

Il faudrait créer un nouveau type de publication mathématique, centré sur les définitions proposées. Un tel article ne serait pas évalué sur la longueur ou la difficulté des démonstrations (qui pourraient être de simples certificats Lean fournis avec l'article), mais sur l’intérêt des nouvelles définitions proposées, et la profondeur des nouveaux objets proposés à l'étude.

Citation : «The papers in this track should be judged exclusively on the conceptual merits, completely agnostic to the difficulty of the proofs.»

Ça rejoint pas mal de commentaires que j'ai lu et entendus à divers endroits (dont ici dans le commentaires) comme quoi l'IA met à mal un système de publication qui était déjà mauvais depuis très longtemps.

@Ruxor, pourrais-tu nous expliquer comment @jeanas et toi vous êtes retrouvés dans Le Monde (<URL: https://www.lemonde.fr/sciences/article/2026/09/18/les-avancees-de-l-ia-provoquent-une-crise-inedite-chez-les-mathematiciens_6776810_1650684.html>) ?

@Jany: j'ai passé pas mal de temps à essayer de comprendre Lean dernièrement, avec un regard extérieur (je ne connaissais pas la théorie des types avant), j'en ai fait une petite série de vidéos que je mets en lien sur mon pseudo ci-dessus.

Cette aventure m'a aussi amené à la conviction qu'il faut investir dans des projets similaires à Lean mais explorant d'autres approches et qu'il y avait là une tâche importante pour la recherche académique.

Concernant les questions sur l'IA elle-même, je suspends mon jugement (non pas que quelqu'un en ait quelques chose à faire) tant j'ai du mal à me positionner sur un sujet en évolution aussi rapide. Je ferai juste remarquer que cette entrée se focalise sur le point de vue des mathématiques, mais il faut voir aussi comment le développement logiciel est impacté !

De la même façon que PISA n'est pas infaillible (traduction mot à mot des énoncés de l’anglais vers le français, par ex.), j’ai tendance à penser que Lean (Lean Tower) peut bugger. Et tout l’édifice du slop repose sur Lean.

Les dates que tu donnes ne prouvent rien. Si tu es une IA, il est clair que tu es une IA codée en LISP qui tourne sur une machine antédiluvienne (avec un nom de bateau, genre 𓅱𓇋𓄿𓊞𓈖𓁨𓏤𓏪) oubliée dans un placard au 45 rue d'Ulm.

Pour Navier-Stokes, si j'ai bien compris, la vitesse devient infinie mais pour une quantité de fluide infime. Ca rappelle le paradoxe de Zénon, en version spatiale. A-t-on fait l'expérience?

J'ai souvent l'impression que les IA sont des débiles avec une mémoire quasi-infinie qui se sont entraînés pendant des (milliers de) milliards d'années. A ma connaissance, toutes les preuves sont au ras des pâquerettes: pas de concept nouveau (ce qui peut être intéressant). Je me demande si l'IA fait plus qu'optimiser la recherche combinatoire exhaustive et limiter l'explosion combinatoire. Un système de preuve automatique bien guidé par un humain serait-il parvenu au résultat?

J'imagine qu'il y a déjà des méta-IA qui se chargent d'optimiser les IA afin d'améliorer leurs performances. Cependant, dans l'Evolution, l'intelligence ne semble pas si facile à atteindre. Il se peut donc qu'il faille attendre encore quelques décennies avant d'obtenir une véritable IA, générale. Un bon test serait de (e.g.) vaincre AlphaGo Zero avec un entraînement bien moindre.

Je crois me souvenir que tout système S contenant l'arithmétique est Gödel-indécidable certains (notamment ZF?) sont partiellement décidables au sens où S(n) est démontrable par S(p) pour quelque p>n, S(p) contenant strictement S(n), S(n) étant une partie de S avec une limitation sur la complexité de la formule. On aurait alors pour S une sorte d'oméga-décidabilté.

Pfff, vu la longueur des posts et leur délayage, je te soupçonne d'avoir recours de plus en plus massivement à des IA.

Je trouve que ce billet touche du doigt un fait essentiel (ce qui explique son succès) tout en ne le disant pas explicitement : cette manière qu'a le système actuel de farcir d'IA tout notre quotidien nous met en état de dépossession. Après le travail physique, les capitalistes ont quasi réussi à s'accaparer le travail intellectuel. Je suis informaticien et je commence à me demander s'il y aura encore des personnes qui sauront programmer dans 30 ans. Comme pour les maths, une application informatique est bien plus que la somme des instructions contenues dans ses fichers sources. C'est une manière de voir le monde.

Comme il existe toujours des fabricants de chaussures artisanaux ou des micro-brasseurs, tout n'est pas perdu, mais ça suppose une forme d'entrée en résistance qui va demander courage et énergie. La crise majeure à venir prophétisée par certains sera un moment clé pour rebattre les cartes et tenter de reprendre la main.

Je viens aussi de le voir passer sur le blog de Peter Woit !

En tout cas ce billet a un grand succès, il a été relayé sur pas mal de canaux, notamment les-mathematiques.net, la liste de diffusion de l'UPS (= asso de prof de prépa), etc.

Une lettre ouverte des matheux du Caltech, qui va dans le même sens: "These companies appear guided by an unhealthy instinct to claim certain results before competitors at all costs, regardless of the collateral damage to mathematical understanding".

https://proofsandprompts.com/2026/09/10/open-letter-about-the-mathathon/

Au fait, connais-tu les détails concernant le certificat Lean pour Navier-Stokes ? Déjà, la preuve en Lean a-t-elle été publiée ?

Et notamment, qu'en est-il de la question de savoir si la formalisation de l'*énoncé* est correcte ? Y a-t-il un mathématicien humain qui l'a confirmé ?

Pour un truc comme, disons, la conjecture de Goldbach, formaliser l'énoncé en Lean ne serait sans doute pas un gros problème. Mais avec Navier-Stokes, il est quand même question de nombres réels, d'équations différentielles etc. Cette partie-là des mathématiques dispose-t-elle déjà d'une bibliothèque Lean ?

Billet très intéressant mais il reste une question qu'on est en droit de se poser.

Supposons qu'à l'avenir une large majorité des acteurs adhère à cette position sur la recherche mathématique (utopique mais faisons l'exercice). On peut tout de même arriver à un système dans lequel les LLMs contribuent à la majorité des résultats mathematiques au travers d'un procédé qu'on aurait au préalable validé pour correspondre à la vision du billet (que je caricature):
- des agents de vulgarisation afin de rendre les résultats accessibles à la communauté scientifique et permettre la réécriture d'articles en Lean en langage humain
- des articles détaillés qui expliqueraient le cheminement naturel ainsi que les difficultés rencontrées lors de la découverte de nouvelles preuves.
- des agents qui contribuent à proposer des idées nouvelles en s'entraînant sur les endroits où d'autres agents ont bloqué dans les preuves etc
- et soyons fous imaginons que tout se fasse à vitesse humaine et donc que chaque chercheur s'il le souhaite puisse aussi prendre le temps de s'approprier les nouveaux concepts, les outils, les preuves etc…

Le mathématicien devient juste un rat de bibliothèque à qui l'on offre des livres dans lesquels il peut se plonger. Au meme titre que peu de personne aujourd'hui se refuseraient à utiliser les résultats existants en invoquant le fait qu'ils veuillent les retrouver par eux-mêmes, on peut imaginer la grande bibliothèque des mathématiques se remplir toute seule sans intervention humaine. Dans un tel système, quel fou continuerait à écrire des choses nouvelles? Qui s'amuse à refaire à la maison de son côté toute la géométrie algébrique sans s'inspirer de ce qui existe déjà ?

Et tout cet écosystème reproduirait plus ou moins l'écosystème actuel de la recherche mathematique sous format purement LLMique. Serait-ce acceptable?

Ajoutons à cela la logique de marché. Les mathématiciens déjà bien mal payés seront en compétition avec des LLMs surperformants qui coûteraient potentiellement bien moins cher tout en faisant un travail qu'on estime acceptable vis-à-vis de la vision proposée de la recherche mathématique globale.

Et puis on peut aussi réévaluer l'utilité d'un professeur, d'une discipline dans son ensemble. Force est de constater que la technologie a déjà détruit des pans entiers de la recherche dans bien des domaines. Les mathématiques étaient encore épargnées et encore louées pour leur caractère science dure qu'on estimait hors de portée de la technologie. Or on constate que ce n'est plus le cas. Et le scénario proposé au-dessus suppose en plus qu'on adhère à cette vision déjà bien optimiste dans laquelle on a contraint le système par un meta prompt magique à se conformer à des attentes raisonnables. Il n'y aura peut-être plus de mathématiciens, juste des hommes qui aiment les maths.

(sur la digression finale)
De toute façon la réponse est 42, on le sait depuis un moment déjà, l'IA n'apportera rien de plus!

IMO the focus on the related energy/environmental issues as a argument in the US as a narrative that is global is tied to data centers, and sociologically/psychologically it’s simply something that everyone who will never read anything like this enjoyable post or the NYT article on this matter etc. can understand because it’s in their backyards and communities. And I mean literally a row of upper-middle-class townhouses will end and tech companies will pop up another fast data center right next to it, and the residents didn’t even know that land was available for that kind of development when they first purchased. This goes back twenty years when tech corridors were developed inside high-growth suburbs, and the local legislature is way behind now on regulation. In this sense, politically and narratively it is the strongest argument because people understand it and have thoughts about it or at least an approach to thinking about it. I am from the area in the US where these things are most concentrated (MAE-east), and also a member of the Anthropic class action settlement. Everyday people I talk to understand the issues with the former immediately, and not the latter.

Energy/environ argument (local residential energy bills/energy availability, noise, pollution, erosion of communities) is, because people understand it, also a place for people to put what unease they sense but don’t fully understand from other issues which are the better arguments to explore if you understand them (labor, education, societal decline, tech lobbying/attacks on the USG, surveillance) with prediction tech and surrounding false-prophet hype (many thanks to Dr. Carissa Veliz for professorially equating Sam Altman to Rasputin in the opening of her recent book). It has a physical presence rather than being abstract. Also a major nexus for this public reaction is right by DC and where politicians live.

I had to read this all in translation (English), so please pardon that.

Thank you for your post: I’m really trying to understand what mathematicians think about this sub-culturally, both as it relates to the labor movement from writers/artists, and as a scifi writer who contemplates how to approach writing the future. Still a lot to learn/think about on my end. https://about.me/JSto

Vous dites "Si vous n'êtes pas mathématicien, imaginez les mauvaises images produites par les IA génératrices d'images qu'on voit partout jusqu'à la nausée : ben c'est pareil mais ce sont des preuves mathématiques correctes, qui résolvent de vrais problèmes, de façon formellement correcte mais quand même profondément merdique. "
J'ai du mal à suivre. Moi, j'adore les images générées par IA, je les trouve super belles, souvent bien plus que des images générées par humain. Et quelque part, si on n'a plus besoin de travail humain pour avoir de belles images, et que la création derrière se limite à quelques lignes de prompt, je trouve que c'est un progrès pour l'humanité.

J'ai vraiment adoré l'anecdote de fin (euhh digression, euuh parabole…)

@Globule Je dirais surtout que c'est comme lire un roman policier dont on s'est fait spoiler la fin.

Allez convaincre les pouvoirs publics de financer une recherche fondamentale dont la principale motivation serait de formaliser des preuves élégantes de théorèmes mathématiques déjà démontrés par des ordinateurs…

> ce sont des preuves formellement correctes qui démontrent (ou souvent, réfutent) effectivement des conjectures souvent anciennes et très respectables. Mais en même temps, c'est quand même de la bouillie

Il y a 1 ans, on disait que l'IA faisait des erreurs débiles. Il y a 6 mois, on disait que les preuves étaient plausibles mais couteuses à vérifier (denial of service). Maintenant on a des preuves correctes avec Lean, mais dur à comprendre. A ce rythme, peut-être qu'on peut espérer des preuves exploitables. Si c'est le cas, est-ce que ça changera les conclusions ?

Sur ce même sujet, j'ai bien aimé cette émission sur France Culture

https://www.youtube.com/watch?v=nq361IRxpxc

C'est sûr qu'il y a de quoi être inquiet et que l'IA va chambouler la façon dont on fait de la recherche en mathématiques, mais peut-être que ce n'est pas une mauvaise chose. Déjà, les mathématiciens n'ont pas attendu OpenAI pour le "concours de bites". Si l'introduction d'un nouvel outil met en péril le système, c'est que le système n'était peut-être pas bon et qu'il ne mesurait pas les bonnes choses.

Merci pour ce texte qui me donne un bon lien à partager pour faire part de l'ambiance dans les labos en ce moment.

Est-ce que ce qui est détruit, ce n'est pas tout d'abord les critères actuels d'évaluation de la recherche, qu'on savait déjà mauvais bien avant que les LLM fassent des maths ? Si l'intérêt des maths, c'est d'inscrire les résultats dans des théories élégantes, bien comprises et fructueuses et que les LLM ne font pas ça bien, alors ça ne devrait pas être tant un péril pour les mathématiciens. Le fait que Fermat-Wiles soit démontré n'a pas empêché de chercher et de trouver une démonstration plus moderne et éclairante ensuite.

Les LLM ont vidé de son sens l'organisation de compétitions autour de grands résultats à démontrer, mais ces compétitions n'étaient sans doute pas très saines à la base. Maintenant que les LLM sont champions dans ces compétitions, j'ai l'impression que beaucoup s'accordent à dire que ce n'est en fait pas ça faire des mathématiques. Ça veut donc dire qu'il reste des mathématiques à faire. Et plus généralement, il faudrait arrêter de donner autant d'importance au fait que quelqu'un ait démontré un truc avant tout le reste du monde.

Qu'est-ce qui empêche un mathématicien de travailler à l'ancienne sur une question déjà résolue ? Sa vanité blessée ?

"l'hypothèse implicite que c'est le dernier besoin venu qui est le moins légitime est stupide"

Je suis d'accord qu'il faut être précautionneux avec ce genre d'arguments. Je suis d'accord que c'est stupide si on le dit comme ça, mais je pense que la question est plus compliquée.

Je lis ce que tu écris comme "quand une nouvelle technologie arrive, il faut se demander ce qu'elle apporte à l'humanité, se demander quel est son impact prévisible, et voir si du coup il faudrait soit la rejeter, soit la prendre et réduire la consommation d'autres choses existantes à la place".

Mais pour moi il y a des raisons sérieuses pour lesquelles une nouvelle technologie ne peut pas être traitée de la même manière que les technos existantes:

* On n'a globalement pas trop d'idée de ses bénéfices futurs (ni le signe de s'il est positif ou négatif, ni la valeur absolue)
* On n'a pas non plus d'idée de son impact prévisible (notamment par rapport à l'effet rebond, on ne sait pas combien on va s'en servir)

En gros j'ai l'impression que l'heuristique que je suis (mais dont je suis d'accord qu'elle est critiquable) c'est : on a un monde qui contient déjà globalement déjà pas mal de technologie, et où l'urgence ça semble être d'éliminer des choses dont on sait qu'elles ne sont pas bénéfiques et trop impactantes (et de faire davantage de redistribution). En gros l'image de la trajectoire vers un monde soutenable, c'est un monde qui serait construit sur ce genre d'améliorations anticipables de la situation actuelle.

Dans ce modèle, voir qu'on est parti pour déployer à outrance une technologie dont le bénéfice est très incertain (pour être charitable), ça semble être une très mauvaise idée.

(Pour la clim, je suis d'accord avec toi, mais je trouve la situation est très différente : on connaît la technologie, on peut anticiper à quoi un déploiement réussi pourrait ressembler… Ça permet justement de se poser les questions utiles, qu'on ne peut juste pas utilement se poser pour l'IA pour l'instant à mon avis.)

Un peu de borgisme.

Le Théorème (que d’autres appellent la Bibliothèque de Gödel) se compose d’un nombre infini de galeries hexagonales avec au centre de vastes puits d’aération bordés par des rangées de tiroirs très bas. Vingt longues étagères, à raison de cinq par côté, couvrent tous les murs moins deux. Chaque étagère comprend trente-deux livres, tous de même format. Chacun des pans libres donne sur un couloir étroit, lequel débouche sur une autre galerie.

Les livres sont couverts de lignes cacophoniques, de galimatias et d’incohérences apparentes. Il y a cinq cents ans, le chef d’un hexagone supérieur mit la main sur un livre aussi confus que les autres, mais qui avait deux pages, ou peu s’en faut, de texte homogène et vraisemblablement lisible. Il montra sa trouvaille à un mathématicien ambulant, qui lui dit qu’il s’agissait de notions d’analyse combinatoire, illustrées par des exemples de variables à répétition constante.

Cette découverte permit à un mathématicien de génie de découvrir la Loi Fondamentale de la Bibliothèque : tous les théorèmes sont démontrés, ils sont produits par la Machine, et leur réunion infinie constitue le Théorème.

Mais depuis le fond obscur de l’hexagone que j’occupe, je crois, moi, qu’il n’est rien de tout cela. Mon raisonnement est le suivant. Il existe un théorème des théorèmes, qui désigne parmi les autres théorèmes ceux qui sont démontrés. Ce théorème, s’il est lui-même démontré, doit se trouver à l’intérieur de lui-même, dans un livre itératif infini qui ne peut figurer dans aucun hexagone fini. S’il n’est pas démontré, il contrevient à la Loi Fondamentale. Il doit en résulter que le théorème des théorèmes ne peut se trouver dans le Théorème.

Mon raisonnement est fragile, mais il y a, dans les tiroirs adossés aux puits, de l’encre et du papier que la Machine a négligé de détruire, ou d’utiliser. Avec ces armes antiques, je prouverai proprement mon théorème, et je casserai la Machine. Ma solitude se console à cet élégant espoir.

@Sty, @Ruxor: combien de mois avant que les emplois manuels ne soient eux aussi menacés, par des robots ?

@Ruxor Le point est justement que ce n'est *pas* un argument faible. Ce n'est certes pas le seul argument non plus mais c'est l'un des problèmes centraux, au moins symboliquement.

Si tu veux éviter de provoquer ce genre de discussions pénibles, il y a une solution simple : arrête de policer la façon dont les gens défendent des causes avec lesquelles tu es plutôt d'accord sous prétexte que tu trouves leurs arguments pas assez forts (surtout quand ça résulte d'une incompréhension de ta part).

(Je dois quand même préciser que je suis entièrement d'accord avec le reste de ce que tu dis dans le billet.)

@Ruxor

Tout dépend ce que tu appelles « bienfaits pour l'humanité ». Si l'IA permet de travailler 10 fois moins pour produire la même chose (que ce soit des théorèmes de maths ou des pièces de moteurs électriques), tout le monde (peut-être pas pour les maths, si j'ai bien suivi) va dire que c'est positif. Sauf qu'on va très certainement faire le choix de travailler autant et produire 10 fois plus (ne serait-ce que parce que nos sociétés ne sont pas conçues pour fonctionner sans le travail). Ça n'est pas soutenable sur le plan environnemental.

Il faut aussi s'attendre à ce que l'IA apporte des progrès spectaculaires contre les maladies, infectieuses ou non. C'est objectivement un « bienfait pour l'humanité ». Mais idem, ça s'accompagnera d'une augmentation majeure de notre impact sur l'environnement.

Donc du point de vue environnemental ça n'est pas tellement la consommation énergétique primaire des ordinateurs de l'IA qu'il faut questionner, mais l'impact du développement incroyablement rapide, presque exponentiel, que l'IA est en train de fournir à nos sociétés qui ne savent pas fonctionner de manière soutenable.

>>>Kévin Buzzard avait lancé un vaste projet de recherche récemment sur cette formalisation

Il faut noter que le projet de Buzzard a été lancé essentiellement pour enrichier la bibliothèque de Laan avec des définitions bien propres et mitonnées aux petits oignons. Après tout Mathlib est le socle sur lequel tout repose donc il est important de formaliser ça avec le plus grand soin.
Comme Buzzard le dit, son projet c'est "formalize in a gold-standard way (i.e. suitable for mathlib)".

Le travail qu'à produit Anthropic n'a pas du tout ce but. Il s'agit juste d'autoformaliser la preuve et de profiter de la mousse marketo-médiatique à ce sujet.

Buzzard ne semble pas amer parce qu'il explique bien que son projet à lui n'est pas celui d'Anthropic : "I would be making pull requests to Lean’s mathematics library, adding fundamental objects from modern number theory; this is ongoing. And secondly, and perhaps most importantly, that I would be creating a dynamic document enabling humans to explore the modern proof. My guess is that it is unlikely that Anthropic are going to do this; they will feel that their job is done with the formalization (and they did not formalize the modern proof anyway)."

Il y a une chose que l’IA ne sait pas faire : c’est sortir du cadre. De même qu’une calculatrice super puissante ne fera pas de calculs en nombres complexes si elle n’est pas programmée pour, de même qu’un logiciel de géométrie dynamique ne sortira pas du cadre euclidien s’il n’est pas programmé pour, de même une IA ne sortira pas du cadre conceptuel à l’intérieur duquel elle a été entraînée.

La solution est donc de hisser l’ensemble de la communauté mathématique au niveau de Grothendieck, où elle sera totalement à l’abri des assauts de l’IA. 😃

Ne peut-on pas penser que dans 1 ou 2 ans ces entreprises seront passées à autre chose. Et qu'on pourra toujours faire de la recherche nouvelle. On digèrera ce qu'ils ont fait de façon intelligible, puis posera des questions, les IA académiques repondront en partie, etc. C'est la période de transition qui est compliquée.

Merci d'avoir exprimé aussi limpidement ce que je pensais intérieurement de façon plus confuse. Chacun de tes billets est un petit joyau de réflexion, d'originalité, d'humour, de littérature, de philosophie, d'érudition… La lecture de ce blog me procure une joie que jamais une discussion avec un chatbot ne remplacera. Encore bravo pour ton talent et le temps que tu consacres à nous éclairer, et bonne chance pour ces temps à venir qui s'annoncent troubles.

+1 a3nm : voir l'argument écologique sous un angle comptable/utilitariste c'est rater la forêt pour les arbres.

Je me permets de signaler l'Association for Human Mathematics <URL: https://www.ahmath.org/ > et l'essai adjacent "The crisis of AI-generated mathematics" de Max Weinreich.

Mes condoléances aux chercheurs en mathématiques, qui vivaient dans une niche métastable où ils pouvaient vivre de leur passion, dans des circonstances financières il est vrai assez variables. Il demeure vrai que c'est (c'était) un domaine privilégié où des gens essentiellement issus de milieux favorisés pouvaient continuer de s'intéresser exclusivement aux choses abstraites, voire prendre fierté dans la futilité de leur travail, et pourtant gagner de quoi subsister. Cela s'opposait notamment à la situation de la plupart des artistes. Mais j'avoue que mon envie caustique de jouer à comparer les souffrances de chacun se heurte à la réalité d'une IA bientôt superintelligente, déjà terrifiante, qui risque peut-être de provoquer des désastres très directs avant même de mettre tous les travailleurs intellectuels de l'humanité au chômage. Le sort des mathématiciens doit s'ajouter à celui des programmeurs et graphistes pour alerter le reste du monde, pas "on risque de perdre nos emplois à long terme" mais "c'est en train d'arriver là maintenant tout de suite, et dieu sait si on aura le temps de nous réorganiser autour de l'IA avant qu'elle ne mène à notre perte".

Les choses vont tellement vite… Tu as raison de souligner que l'argument anti-slop qui consiste à dire que la formalisation (en Lean notamment) empêcheles dérives (= une avalanche de papiers faux) et qui était sans doute valable il y a quelques mois est complètement mort.

On a complètement sous-estimé la capacité des IA à formaliser, ce qui a l'air d'être devenu une tâche relativement trivial pour elles. L'exemple le plus frappant est Anthropic qui a réussi à formaliser la preuve du théorème de Fermat-Wiles (13,4 millions de lignes de code…) alors qu'en parallèle Kévin Buzzard avait lancé un vaste projet de recherche récemment sur cette formalisation (avec financement !) en pensant que ça allait prendre des années.

Merci pour ce billet de blog qui résume si bien la triste situation dans laquelle nous sommes.

En ce qui concerne le programme de Hilbert, je me disais déjà depuis quelques années (avant que les progrès des LLM en mathématiques ne deviennent aussi spectaculaires) qu’au-delà de la calculabilité, la théorie de la complexité avait elle-aussi une portée assez limitée pour prédire la difficulté *pratique* des problèmes réels, en particulier depuis que les solveurs SAT sont capables de résoudre des instances concrètes avec un nombre de variables qui devrait pourtant les rendre trop complexe *dans le pire des cas*. Clairement, nous ne comprenons pas suffisamment la complexité *moyenne* des problèmes intéressants. Il y a bien une théorie de la complexité-en-moyenne, mais mais une grande partie de ses résultats repose sur des hypothèses ou des choix de distributions qui ne semblent pas nous dire grand-chose à propos de la complexité empirique des problèmes rencontrés à l’état sauvage, pour ainsi dire. (Et les méthodes opaques des boîtes d’IA ne nous en apprennent malheureusement pas davantage ! Il serait intéressant de savoir quels problèmes elles ont essayé de résoudre sans succès, par exemple---ce qu’elles feraient si elles avaient vraiment à cœur de faire progresser les mathématiques et de collaborer avec la communauté scientifique).

Un autre point : ton billet (et nombre d’autres réactions de personnes sensées) explique bien les dommages de l’IA en maths *d’un point de vue interne*, mais on parle assez peu de ce que les maths apportent *d’un point de vue externe*, c’est-à-dire aux autres sciences et à la société de manière générale, et de ce que l’usage des LLM comme ersatz risque de nous faire perdre. Il me semble clair -- pour tout un tas d’arguments que tu résumes bien -- que les LLM et leurs maîtres capitalistes sont un danger pour la discipline. En revanche, dans un contexte où un grand nombre de scientifiques, d’ingénieurs, etc. (sans parler du grand public) ne voient déjà les mathématiques que comme une grosse boîte à outils dans laquelle il faut piocher le bon marteau pour attaquer son problème du moment et en tirer la solution toute faite, les LLM donnent l'illusion d'être un outil généraliste qui permettrait de ne plus s’embarrasser de mathématiques. J’imagine que bon nombre de personnes s’en réjouissent ! Bien sûr, ce n’est pas mon cas---il suffit de constater le grand nombre de résultats bidons (je pense par exemple aux crises de la reproductibilité en biologie, en médecine, en sciences sociales, etc.) dus à la mécompréhension des méthodes statistiques pour se convaincre que le choix du bon outil et son application correcte requièrent une compréhension à laquelle les LLM ne peuvent pas se substituer pour l’instant.

On me répondra que les LLM seront bientôt capables de s’assurer de la bonne application des outils mathématiques à toute question scientifique (!), et qu’il suffira de leur fournir suffisamment de contexte pour qu’ils choisissent et appliquent la bonne méthode. Peut-être… Mais cela me semble être un problème autrement plus compliqué que de produire des démonstrations mathématiques. S’assurer qu’un nombre (ou toute autre abstraction mathématique) ait un sens n’est pas une affaire dont la cohérence peut être vérifiée en Lean ! Il s’agit d’une activité que l’on pourrait qualifier de « méta-rationnelle » ou du moins de synthétique (comme le choix de questions intéressantes en maths d'ailleurs), dont les ressorts restent relativement mystérieux et dont je doute qu’ils soient totalement automatisables ("famous last words" de nos jours, je sais).

Je trouve le billet super intéressant mais il y a juste une distinction qui m'a manqué : quand on dit que sortir une preuve formelle opaque d'un résultat tue la recherche autour de ce résultat, je trouve que ça mélange à la fois (1.) une observation sur ce qui motive intrinsèquement des gens à réfléchir à un problème, et (2.) une observation sur comment la communauté mathématique est structurée actuellement et comment la reconnaissance est distribuée.

Je suis d'accord que (1.) existe : personnellement en tout cas si je réfléchis à un problème et qu'une solution formelle opaque du problème sort alors je ne vais pas être très motivé à continuer à y réfléchir ou à essayer de la décortiquer. (Mais c'est vrai aussi d'une preuve humaine -- à part que vu qu'elle est parfois moins opaque il y a davantage de motivation à comprendre ce que j'avais raté.)

Et je suis d'accord que (2.) ne justifie pas complètement le comportement des boites d'IA : si on prétend faire des maths c'est quand même bien de s'intéresser aux règles de la communauté des matheuxses et à l'impact de ce qu'on fait sur celle-ci.

Mais : je trouve quand même que c'est important de soigneusement distinguer (1.) et (2.). Parce que (2.) c'est quand même quelque chose qu'on peut espérer changer, et qu'on devrait de toute façon changer pour tout un tas de raisons. Et (1.) je trouve que ça mérite d'être examiné : certes l'existence d'une preuve opaque va décourager certaines personnes, mais elle va peut-être aussi en motiver d'autres à déslopifier le slop comme tu dis, ce qui peut avoir un impact positif à terme. Il y a aussi le fait que publier des preuves formelles opaques c'est quand même un peu un victimless crime si on ne regarde pas (2.) : c'est difficile de qualifier en quoi l'existence d'une preuve formelle est quelque chose qui cause du tort à des gens qui réfléchissaient au problème et ne sont aucunement empêchés de continuer à y réfléchir.

Sinon : sur l'empreinte environnementale des LLM, je suis sensible à l'argument mais pas tant pour l'impact marginal (je suis d'accord qu'il est faible) que pour la symbolique de la situation. En gros : sachant qu'on est depuis longtemps sur une trajectoire non soutenable environnementalement, je trouve ça vraiment intolérable de voir l'humanité (en termes d'attention collective, de perception du progrès, et surtout de capitaux) se ruer en courant dans une direction complètement haute qui (en dehors des rêves douteux des AI-optimists) n'aide pas à régler la crise climatique et même l'aggrave sévèrement en terme d'impact global…