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 ». Ce n'était pas le cas — ces problèmes n'étaient répertoriés comme 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 localisé de la littérature déjà existante. Bloom avait qualifié le tweet de « dénaturation flagrante », le propre chercheur d'OpenAI avait reconnu l'erreur, le tweet avait été supprimé, et Demis Hassabis avait qualifié tout l'épisode d'« embarrassant ». Cet historique compte pour lire ce qu'OpenAI a publié cette semaine : dix nouveaux résultats sur des problèmes n'ayant connu aucun progrès depuis une décennie ou plus, produits par une version interne et non publiée d'un modèle appelé Astra. L'affirmation a une forme presque identique à celle qui avait explosé en octobre. La raison de prendre celle-ci plus au sérieux, c'est que c'est Thomas Bloom lui-même qui s'en porte garant.
Ce qui est réellement affirmé
Dix résultats, couvrant la géométrie en haute 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 — parmi eux, 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 uniquement déterminés par leurs algèbres de von Neumann), une nouvelle borne inférieure de formule arithmétique pour le calcul du permanent, une dureté d'approximation à facteur polynomial pour le problème du vecteur le plus proche (une question fondamentale de la cryptographie post-quantique), et une résolution du problème 183 d'Erdős — une borne inférieure superexponentielle pour les nombres de Ramsey triangulaires multicolores. Le cadrage propre d'OpenAI est précis sur la barre fixée : des problèmes sans progrès sur le résultat principal « depuis au moins une décennie, et dans la plupart des cas bien plus longtemps ».
Le processus de production mérite d'être noté en soi : une version interne d'Astra a généré les arguments mathématiques — OpenAI estime 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 préparer les arguments sous forme de manuscrits, et le modèle a formalisé chaque preuve en un certificat Lean, une vérification formelle vérifiable par machine. OpenAI publie aussi la propre narration du modèle de son processus de raisonnement pour chaque résultat.
Pourquoi l'étape Lean est la partie qui compte le plus
Une preuve en langage naturel peut être à la fois convaincante et fausse — des mathématiciens se sont déjà fait piéger par des arguments générés par IA qui se lisent avec fluidité mais contiennent une faille qu'un lecteur attentif finirait par trouver. Un certificat Lean est un type d'affirmation différent : il est vérifié par un assistant de preuve, pas par l'attention d'un lecteur. C'est le même instinct qui sous-tend le cadre ScientistOne / Chain-of-Evidence de Google, publié un jour avant cet article d'OpenAI — le problème de confiance dans la production de recherche générée par IA n'est pas « le modèle est-il assez intelligent », c'est « l'affirmation peut-elle être vérifiée indépendamment de qui la formule ». Le langage d'attribution propre d'OpenAI va dans le même sens : « revendiquer une paternité humaine pour une preuve entièrement générée par un système d'IA dénaturerait à la fois la contribution du système et la nature du véritable travail intellectuel humain. Nous avons aidé à 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. » C'est une répartition du travail plus précise que ce que la plupart des annonces IA-et-science prennent la peine de tracer.
Le précédent de mai, et le test de crédibilité cette fois-ci
Ce n'est pas la première tentative d'OpenAI sur exactement cette même forme d'affirmation. En mai, l'entreprise avait partagé une réfutation générée par IA de la conjecture de la distance unité d'Erdős, trouvée en évaluant un modèle non publié — et cette fois-là, la réaction des mathématiciens qui avaient toutes les raisons d'être sceptiques avait été fortement positive. Le lauréat de la médaille Fields Timothy Gowers 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 — la même personne qui avait détecté la surinterprétation d'octobre — les a qualifiés de « grande nouvelle », et les a même classés au-dessus de la réfutation de mai en termes de portée : « Peut-être pas plus grand qu'une preuve de la distance unité ne l'aurait été, mais en termes de constructions, c'est important. »
C'est le signal réel qui mérite l'attention ici, plus que les résultats eux-mêmes : le sceptique qui avait le plus de raisons de se méfier des affirmations mathématiques d'OpenAI, et l'antécédent précis d'en avoir démenti une, déclare publiquement trouver celle-ci crédible. Les antécédents jouent dans les deux sens.
La réserve qui ne doit pas se perdre dans le titre
Une analyse indépendante du résultat de mai avait relevé un point qui mérite d'être gardé à l'esprit aussi pour ce lot : le modèle n'a pas inventé de nouvelles techniques mathématiques à partir de rien — il a recombiné et étendu des idées existantes tirées de plusieurs sous-domaines, ce qui est une compétence réelle et difficile, mais différente de l'invention d'une nouvelle méthode de preuve. Des mathématiciens humains sont aussi intervenus pour resserrer et étendre le résultat de mai après le premier passage du modèle, et la même structure collaborative est explicite dans la publication de cette semaine — des humains ont préparé les manuscrits aux côtés du modèle, ils n'ont pas simplement publié la sortie brute du modèle. Rien de tout cela ne rend les résultats moins réels. Cela signifie que le cadrage 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 », pas « un système qui raisonne sur les mathématiques comme le ferait un humain ». L'article d'OpenAI crédite explicitement les signataires de la Déclaration de Leiden sur l'IA et les Mathématiques — la déclaration de juin 2026, soutenue par plus d'un millier de mathématiciens dont Terence Tao et Peter Scholze, et approuvée par l'Union mathématique internationale, qui met en garde précisément contre les résultats non fiables, l'attribution manquante et les affirmations exagérées — pour avoir soulevé exactement ces questions. Nommer ce document dans un article qui fait exactement le type d'affirmation contre lequel il met en garde se lit comme une tentative de maintenir cette distinction plutôt que de la brouiller pour un meilleur titre.
Où cela se situe dans le reste du vertical scientifique
C'est le même vertical à capital quasi nul et à courbe de coût vertigineuse que ce blog a suivi en mathématiques formelles via Leanstral de Mistral — sauf que celui-ci arrive d'un laboratoire généraliste de pointe plutôt que d'un modèle de mathématiques dédié, en utilisant un modèle phare non publié plutôt qu'une sortie spécialisée, et en touchant des problèmes ouverts depuis des décennies plutôt que des jeux de benchmarks. Cela arrive aussi deux jours après le lancement du programme ChatGPT for Academic Researchers d'OpenAI pour 100 000 scientifiques et mathématiciens — cet article se lit, en partie, comme la preuve de concept de ce programme, publiée avant même que la plupart des 100 000 n'aient reçu leur compte.
À surveiller ensuite
- La vérification formelle devient la barre minimale pour toute affirmation mathématique liée à l'IA, pas un plus. Après octobre, « le modèle l'a dit » ne suffit plus pour OpenAI en particulier ; un certificat Lean est la seule version de cette annonce qui survit à l'examen dès son arrivée.
- L'aval nominatif d'un mathématicien reconnu devient une partie de la stratégie de publication. Gowers sur le résultat de mai, Bloom sur celui-ci — OpenAI construit visiblement un historique consistant à faire s'exprimer publiquement les sceptiques spécifiques du domaine avant que le titre ne tombe, une leçon apprise en public.
- Surveillez quels sous-domaines recevront la prochaine vague. Dix résultats sur huit domaines en une seule annonce suggère que la capacité mathématique d'Astra n'est pas étroite — la question intéressante est de savoir si les dix prochains ressembleront encore à de la recombinaison à grande échelle ou commenceront à inclure une technique authentiquement nouvelle.
Références : OpenAI — "Ten advances in mathematics and theoretical computer science" · the-decoder.com — les dix solutions mathématiques d'Astra · Scientific American — la réfutation de mai de la distance unité d'Erdős · TechCrunch — la rétractation « embarrassante » d'octobre 2025 · Déclaration de Leiden sur l'Intelligence Artificielle et les Mathématiques · couverture liée sur ce blog : ScientistOne / Chain-of-Evidence · Le vertical scientifique