L'essentiel
OpenAI a publié cette semaine près de 400 résultats mathématiques générés par IA, répartis sur plus de 700 manuscrits couvrant la combinatoire, plusieurs branches de la géométrie, la théorie des nombres, l'informatique théorique, l'algèbre, la topologie, les probabilités, la mécanique statistique et la physique mathématique. Le volume est tel qu'OpenAI a jugé nécessaire de publier un guide pour naviguer dans le dépôt GitHub qui héberge l'ensemble.
Plus de trois douzaines de mathématiciens interrogés par The Verge ont employé des mots comme « stupéfiant », « accablant », « sans précédent », « surréaliste » ou « pure folie » pour décrire la livraison. Beaucoup estiment qu'il faudra des années rien que pour comprendre ce qui a été publié, et craignent qu'OpenAI ne passe à autre chose — ou ne publie davantage — bien avant.
Les détails
Vérification partielle et inégale
Parmi les manuscrits figurent des formalisations en Lean, un langage de programmation et assistant de preuve qui permet de vérifier les résultats par calcul. Ces formalisations ont déjà servi à évaluer certaines affirmations mathématiques antérieures d'OpenAI. Mais le degré de vérification varie fortement : sur GitHub, OpenAI reconnaît que les résultats sont « à différents stades de vérification » et que « beaucoup, mais pas tous, des manuscrits ont été formalisés ». L'entreprise indique que seuls 300 résultats principaux sur 719 manuscrits ont été formalisés, soit environ 42 %, et qu'elle « mettra à jour le dépôt avec davantage de formalisations » au fur et à mesure.
Plusieurs mathématiciens déplorent ce manque de formalisation, d'autant que même lorsqu'un code Lean accompagne un résultat, l'évaluation n'est pas instantanée : il faut vérifier que la formalisation prouve bien ce que le résultat prétend. Plusieurs chercheurs ayant épluché les articles rapportent une qualité inégale et des énoncés vérifiés qui ne correspondent pas toujours aux affirmations des manuscrits.
Qualité et attribution en question
Kevin Buzzard, professeur à l'Imperial College London, dit avoir identifié de nombreux théorèmes dans son domaine (théorie algébrique des nombres) dont seulement environ six lui ont immédiatement « sauté aux yeux ». Presque aucun ne semblait formellement vérifié en Lean. « Je dois donc soit lire du slop potentiellement incorrect, soit attendre que d'autres le fassent, soit attendre que quelqu'un les formalise avant de pouvoir dire que les résultats sont même corrects », résume-t-il.
Le terme « slop » désigne du contenu généré par IA de faible qualité et souvent erroné. Les mathématiciens interrogés disent constater une forte hausse de ce type de matériel produit avec des outils comme ChatGPT et Claude, difficile à lire et peu rigoureux sur le crédit aux autres chercheurs. Les précédents écrits mathématiques d'OpenAI avaient été largement critiqués pour leur négligence, notamment leur attribution défaillante. Avant la publication, certains chercheurs parlaient de « slopocalypse ».
Brendan Hassett, professeur à Brown, raconte que « la rédaction du problème que je connais le mieux n'avait guère de sens après une lecture rapide » et qu'il n'aurait pas insisté s'il avait été écrit par un humain. Nalini Joshi, de l'université de Sydney, note que certains articles examinés « ont des bibliographies courtes » et se dit « méfiante quant au fait que l'attribution dans les articles puisse manquer une partie de l'histoire ». D'autres relèvent l'extraordinaire brièveté de travaux qui auraient normalement occupé des centaines de pages.
Des résultats jugés de haut niveau
Malgré ces réserves, le consensus est que la publication contient des travaux genuinely impressionnants. Dans un monde sans IA, beaucoup de ces résultats auraient mérité des revues de premier rang et auraient pu suffire à asseoir une carrière académique. Quelques-uns sont décrits comme le genre de travail qui pourrait faire d'un mathématicien un sérieux candidat à une médaille Fields.
Jared Duker Lichtman, de Stanford, cite « des dizaines » de résultats dans cette catégorie, dont des progrès vers l'hypothèse de Riemann, un cas particulier de la conjecture de Hodge et une solution à la conjecture de Kakeya en dimension quatre. Riemann et Hodge figurent parmi les sept problèmes du prix du millénaire. Scott Armstrong souligne qu'« il ne s'agit pas de problèmes farfelus que personne n'a jamais entendus » et que beaucoup sont « des problèmes très connus que beaucoup de gens ont tenté de résoudre pendant des décennies ».
Un paysage bouleversé
De nombreux chercheurs ont vu des années de travail et des plans de recherche soigneusement établis s'évaporer d'un coup. Tristan Buckmaster, de NYU, dit avoir entendu parler de « trois personnes dont des programmes de recherche entiers ont été anéantis ». Colva Roney-Dougal, de l'université de St Andrews, évoque une ambiance sombre et des collègues dont « les demandes de subvention viennent d'être anéanties ». Francesco Fournier-Facio, de Heriot-Watt, observe que les chercheurs en probabilités, combinatoire et informatique théorique semblent « particulièrement sous le choc », certaines régions de la théorie des groupes ayant été « rasées ».
Pourquoi c'est important
Pour un développeur ou une équipe qui travaille avec des modèles génératifs, cette séquence illustre un problème qui dépasse les mathématiques : produire massivement du contenu plausible est désormais facile, le vérifier ne l'est pas. Le taux de 42 % de formalisation rapporté par OpenAI montre que même l'éditeur ne peut pas garantir la validité de tout ce qu'il publie. Cela suggère que les pipelines de vérification automatique — ici Lean — deviennent un maillon critique dès qu'on automatise la production de résultats techniques.
À surveiller : la manière dont les communautés scientifiques s'organisent face à ce type de livraison. Si les chercheurs doivent trier eux-mêmes le bon grain de l'ivraie, la charge de relecture se déplace vers ceux qui ont le moins de ressources, et l'attribution devient un enjeu de crédibilité. Mon hypothèse est que les outils de vérification formelle et de traçabilité des sources vont devenir aussi importants que les modèles eux-mêmes.