Il y a neuf mois, un vice-président d'OpenAI affirmait sur X que GPT-5 avait « trouvé des solutions à 10 (!) problèmes d'Erdős jusqu'alors non résolus ». C'était faux : ces problèmes n'étaient réputés ouverts qu'au sens où le mathématicien Thomas Bloom, qui tient le site de suivi erdosproblems.com, ignorait personnellement l'existence d'une solution publiée. Le modèle avait surtout retrouvé de la littérature existante. Bloom avait parlé d'une « déformation flagrante », le chercheur d'OpenAI concerné avait reconnu l'erreur, le tweet avait été supprimé, et Demis Hassabis avait jugé l'épisode « embarrassant ». Il faut garder cet antécédent en tête pour lire ce qu'OpenAI a publié cette semaine : dix résultats inédits sur des problèmes n'ayant connu aucun progrès depuis dix ans ou davantage, produits par une version interne, non publiée, d'un modèle nommé Astra. L'annonce a presque la même forme que celle qui avait explosé en vol en octobre. Si l'on peut la prendre plus au sérieux, c'est que Thomas Bloom en personne s'en porte garant.
Ce qui est annoncé
Dix résultats, couvrant la géométrie en grande dimension, la théorie des codes, la complexité des circuits arithmétiques, la théorie des groupes, les algèbres d'opérateurs, la complexité quantique, la cryptographie sur réseaux et la combinatoire extrémale. On y trouve notamment de nouvelles bornes supérieures sur la densité d'empilement de sphères jusqu'au seuil de Cohn-Elkies, une réfutation de la conjecture de rigidité de Connes — selon laquelle certains groupes seraient entièrement déterminés par leurs algèbres de von Neumann —, une nouvelle borne inférieure de formule arithmétique pour le calcul du permanent, un résultat de difficulté d'approximation à facteur polynomial pour le problème du vecteur le plus proche (une question centrale de la cryptographie post-quantique), et la résolution du problème 183 d'Erdős, avec une borne inférieure superexponentielle pour les nombres de Ramsey triangulaires multicolores. OpenAI est précis sur le critère retenu : des problèmes dont le résultat principal n'a pas bougé « depuis au moins une décennie, et le plus souvent bien davantage ».
Le mode de production mérite lui aussi d'être noté. Une version interne d'Astra a produit les arguments mathématiques — OpenAI évalue le coût total en tokens à environ 2 000 $ aux tarifs de l'API Sol pour les dix résultats. Des humains ont ensuite travaillé avec le même modèle pour mettre ces arguments en forme de manuscrits, et le modèle a formalisé chaque démonstration en un certificat Lean, vérifiable par machine. OpenAI publie également le récit que le modèle fait lui-même de son raisonnement pour chaque résultat.
L'étape Lean est ce qui compte le plus
Une démonstration en langage naturel peut être à la fois convaincante et fausse : des mathématiciens se sont déjà laissé piéger par des arguments générés par IA qui se lisent parfaitement mais recèlent une faille qu'un lecteur attentif finit par trouver. Un certificat Lean est d'une tout autre nature : il est validé par un assistant de preuve, non par la vigilance d'un lecteur. C'est la même intuition qui fonde le cadre ScientistOne / Chain-of-Evidence de Google, publié la veille. Le problème de confiance, dans la recherche générée par IA, n'est pas de savoir si le modèle est assez intelligent, mais si l'affirmation peut être vérifiée indépendamment de celui qui la formule. La façon dont OpenAI attribue le travail va dans le même sens : « Revendiquer une paternité humaine pour une preuve entièrement produite par un système d'IA travestirait à la fois la contribution du système et la nature du véritable travail intellectuel humain. Nous avons contribué à préparer les manuscrits et à formaliser les preuves en Lean, et nous assumons la responsabilité de leur exactitude, tandis que les arguments mathématiques eux-mêmes ont été générés par notre système. » Le partage des rôles est plus net que dans la plupart des annonces mêlant IA et science.
Le précédent de mai, et l'épreuve de crédibilité
Ce n'est pas la première tentative d'OpenAI dans ce registre. En mai, l'entreprise avait diffusé une réfutation, générée par IA, de la conjecture de la distance unité d'Erdős, trouvée au cours de l'évaluation d'un modèle non publié. Or, cette fois-là, les mathématiciens qui avaient toutes les raisons d'être sceptiques avaient réagi très favorablement. Timothy Gowers, médaille Fields, avait déclaré que si un chercheur humain avait soumis cet article aux Annals of Mathematics, il en aurait recommandé la publication « sans la moindre hésitation ». Sur les dix résultats de cette semaine, Bloom — celui-là même qui avait repéré l'exagération d'octobre — parle d'une « grande nouvelle » et les place même au-dessus de la réfutation de mai quant à la portée : « Peut-être pas plus important qu'une preuve de la distance unité ne l'aurait été, mais du point de vue des constructions, c'est considérable. »
Voilà le véritable signal, plus encore que les résultats eux-mêmes : le sceptique qui avait le plus de raisons de se méfier des annonces mathématiques d'OpenAI, et qui en avait déjà démenti une, déclare publiquement trouver celle-ci crédible. Les antécédents jouent dans les deux sens.
La réserve à ne pas laisser filer
Une analyse indépendante du résultat de mai relevait un point qu'il faut garder à l'esprit ici aussi : le modèle n'a pas inventé de techniques mathématiques nouvelles à partir de rien. Il a recombiné et prolongé des idées existantes puisées dans plusieurs sous-domaines — ce qui reste une compétence réelle et difficile, mais différente de l'invention d'une méthode de preuve inédite. Des mathématiciens humains étaient également intervenus pour resserrer et étendre le résultat de mai après le premier passage du modèle, et la même organisation collaborative est assumée cette semaine : des humains ont préparé les manuscrits aux côtés du modèle, ils n'ont pas simplement publié une sortie brute. Rien de tout cela ne diminue les résultats. Cela signifie simplement que la formulation honnête est « un système capable d'explorer un espace immense de techniques mathématiques existantes plus vite et plus largement qu'un humain », et non « un système qui raisonne en mathématiques comme le ferait un humain ». L'article d'OpenAI cite d'ailleurs explicitement les signataires de la Déclaration de Leyde sur l'IA et les mathématiques pour avoir soulevé précisément ces questions. Ce texte de juin 2026 — soutenu par plus d'un millier de mathématiciens dont Terence Tao et Peter Scholze, et approuvé par l'Union mathématique internationale — met en garde contre les résultats non fiables, les attributions manquantes et les annonces exagérées. Nommer ce document dans un article qui produit exactement le type d'affirmation qu'il vise ressemble à une volonté de tenir la distinction plutôt que de la brouiller pour un meilleur titre.
Où cela se situe dans la verticale scientifique
C'est la même verticale à capital quasi nul et à courbe de coût vertigineuse que ce blog suivait en mathématiques formelles avec Leanstral, de Mistral. Les différences : le résultat vient cette fois d'un laboratoire généraliste de pointe et non d'un modèle mathématique dédié, il mobilise un modèle phare non publié plutôt qu'une version spécialisée, et il porte sur des problèmes ouverts depuis des décennies plutôt que sur des jeux de benchmarks. L'annonce tombe par ailleurs deux jours après le lancement du programme ChatGPT for Academic Researchers, destiné à 100 000 scientifiques et mathématiciens. Cet article se lit en partie comme la démonstration de faisabilité de ce programme, publiée avant même que la plupart des 100 000 n'aient reçu leurs accès.
À surveiller
- La vérification formelle devient le minimum exigible pour toute annonce mathématique liée à l'IA, et non plus un bonus. Après octobre, « le modèle l'a dit » ne suffit plus, en particulier pour OpenAI ; le certificat Lean est la seule version de cette annonce qui résiste dès sa parution.
- La caution nominative d'un mathématicien reconnu fait désormais partie de la stratégie de publication. Gowers pour le résultat de mai, Bloom pour celui-ci : OpenAI prend visiblement l'habitude de faire parler les sceptiques du domaine avant que le titre ne tombe. Leçon apprise en public.
- Les sous-domaines de la prochaine vague. Dix résultats répartis sur huit domaines dans une seule annonce indiquent que la compétence mathématique d'Astra n'a rien d'étroit. La vraie question est de savoir si les dix suivants relèveront encore de la recombinaison à grande échelle ou s'ils commenceront à comporter une technique authentiquement nouvelle.