Il n’est ni disponible dans ChatGPT ni documenté comme un produit que les chercheurs pourraient tester. Pourtant, ce modèle interne d’OpenAI aurait déjà produit ce que l’entreprise présente comme dix avancées en mathématiques et en informatique théorique, sur des problèmes restés sans progrès décisif pendant au moins dix ans.
Son nom est Astra. OpenAI le décrit comme une version interne de son « prochain grand modèle ». Le 1er août 2026, l’entreprise a publié un ensemble inhabituel : un rapport de 249 pages, dix démonstrations, leurs traductions dans l’assistant de preuve Lean et des récits expliquant comment les idées seraient apparues. Les résultats vont de l’empilement de sphères à la cryptographie post-quantique, en passant par la théorie des groupes et les jeux quantiques.
L’annonce est spectaculaire. Elle demande aussi une lecture précise : certains problèmes sont résolus, d’autres réfutés, et plusieurs résultats améliorent fortement les meilleures bornes connues sans fermer définitivement leur domaine. Surtout, les documents sont publiés par OpenAI elle-même. Ils constituent une matière scientifique examinable, pas encore un consensus indépendant.
Astra, le modèle que personne ne peut encore essayer
OpenAI présente Astra comme un système généraliste, et non comme un logiciel spécialisé dans le calcul symbolique. L’entreprise ne fournit toutefois presque aucun détail sur son architecture, sa taille, ses données d’entraînement ou sa date de mise à disposition. Le modèle reste donc, pour le public, une boîte noire entourée de preuves que chacun peut tenter de vérifier.
Cette distinction compte. Un benchmark mesure généralement la capacité d’un modèle sur des exercices dont la réponse est connue. Ici, OpenAI affirme qu’Astra a travaillé sur des questions de recherche ouvertes, choisies parce que leur résultat principal n’avait pas progressé depuis une décennie au minimum, souvent beaucoup plus. Le modèle ne devait pas seulement retrouver une solution : il devait proposer un argument nouveau, suffisamment cohérent pour être transformé en manuscrit mathématique puis formalisé.
Le nom Astra apparaît ainsi moins comme une annonce de produit que comme un aperçu des capacités qu’OpenAI souhaite attribuer à sa prochaine génération de modèles. Tant que l’accès au système et son protocole complet d’évaluation ne sont pas publics, il reste impossible de mesurer sa reproductibilité sur un échantillon de problèmes choisi hors de l’entreprise.
Dix résultats, mais pas dix fois la même prouesse
Les dix travaux ne relèvent pas d’une technique unique. Ils traversent plusieurs branches des mathématiques et de l’informatique théorique. C’est précisément cette diversité qui donne du poids à la série — et qui interdit de la résumer par « l’IA a résolu dix conjectures ».
Des sphères et des codes mieux serrés
Le premier résultat concerne l’empilement de sphères en grande dimension. Imaginez des oranges rangées dans une caisse, puis transposez la question à des espaces comportant des centaines de dimensions. Les mathématiciens cherchent la densité maximale possible. Le rapport attribué à Astra améliore l’exposant de la meilleure borne supérieure générale, une première depuis 1978 selon le manuscrit, jusqu’au seuil associé à la méthode de Cohn et Elkies.
Un travail voisin porte sur les codes binaires et sphériques. Un code correcteur doit séparer suffisamment ses mots pour que les erreurs de transmission puissent être détectées ou corrigées. Astra aurait obtenu des bornes exponentiellement meilleures sur le nombre maximal de mots pouvant coexister à une distance minimale donnée. Derrière la géométrie abstraite se trouve donc une question centrale pour la fiabilité des communications et du stockage.
Une existence démontrée, une rigidité brisée
En théorie des groupes, le modèle aurait construit un exemple explicite de groupe non sofic. La notion de soficité décrit, très grossièrement, la possibilité d’approcher la structure d’un groupe infini par des objets finis. L’existence de groupes échappant à cette approximation était une question centrale et ancienne. Le résultat annoncé ne se contente pas d’un argument abstrait : il propose une construction explicite.
Un autre manuscrit réfute une conjecture de rigidité attribuée à Alain Connes. Celle-ci suggérait que certaines algèbres d’opérateurs conservaient assez d’information pour identifier le groupe dont elles provenaient. Les contre-exemples d’Astra indiqueraient que des groupes différents peuvent donner naissance à la même algèbre de von Neumann. Ici, « résoudre » signifie donc montrer qu’une intuition durable était fausse.
Des circuits, des jeux quantiques et un problème de réseau
En complexité algébrique, Astra aurait renforcé les bornes inférieures pour le calcul du permanent, un cousin du déterminant notoirement difficile à calculer. Le rapport annonce notamment une borne de l’ordre de (n^4 / \log n) pour les formules arithmétiques et de (n^2 \log\log n) pour certains circuits. Une borne inférieure ne donne pas un algorithme plus rapide : elle prouve qu’une famille de méthodes ne peut pas descendre sous un certain coût.
En informatique quantique, le modèle propose un théorème de répétition parallèle exponentielle pour des jeux quantiques généraux à deux joueurs. Répéter un test plusieurs fois doit normalement rendre la triche ou la réussite fortuite de plus en plus improbable. Dans le monde quantique, l’intrication rend cette intuition difficile à formaliser. Le résultat annoncé donne une décroissance exponentielle dans un cadre beaucoup plus général.
Le travail sur le problème du vecteur le plus proche améliore, lui, une borne de difficulté d’approximation dans les réseaux euclidiens, avec un facteur (n^{1/400}). Ce problème consiste à trouver, dans une grille de points de très grande dimension, celui qui se rapproche le plus d’une cible. Il est étroitement lié à la cryptographie fondée sur les réseaux, l’une des grandes familles envisagées pour résister aux futurs ordinateurs quantiques. Le résultat ne casse pas ces systèmes, mais affine la carte théorique de leur difficulté.
Volumes, triangles colorés et graphes extrêmes
Astra aurait également démontré une borne optimale liée à une conjecture d’Ehrhart : pour certains corps convexes contenant un unique point du réseau à l’intérieur, le volume normalisé ne dépasse pas ((n+1)^n/n!). Ce problème relie géométrie continue et arithmétique discrète.
En combinatoire, le modèle obtient une nouvelle borne inférieure superexponentielle pour des nombres de Ramsey multicolores. La question peut se raconter comme un jeu de coloriage : combien de sommets faut-il avant qu’un triangle d’une seule couleur devienne inévitable ? Le résultat résout le problème 183 de la liste d’Erdős, d’après OpenAI.
Enfin, deux questions de théorie extrémale des graphes, répertoriées comme les problèmes 146 et 180 d’Erdős, reçoivent des réponses portant sur la compacité et la dégénérescence. Cette dernière mesure à quel point un graphe peut être simplifié en retirant successivement des sommets peu connectés. Ces travaux montrent bien la variété du lot : Astra n’aurait pas seulement appliqué la même recette à dix variantes d’un exercice.
De l’intuition au certificat Lean
OpenAI décrit une chaîne de production en trois étages. Astra aurait d’abord généré les idées et les arguments mathématiques. Des humains, assistés par le même modèle, les auraient ensuite organisés en manuscrits lisibles. Enfin, chaque démonstration aurait été traduite dans Lean, un langage et assistant de preuve capable de vérifier mécaniquement chaque étape à partir de règles logiques explicites.
Le dépôt public contient dix dossiers de formalisation, correspondant aux dix résultats, ainsi que des défis de comparaison où la preuve doit compiler seule. C’est beaucoup plus solide qu’une réponse convaincante en langage naturel : une formule oubliée, une implication invalide ou un cas non traité empêche normalement Lean d’accepter le certificat.
OpenAI publie aussi des « parcours de raisonnement » qui racontent les impasses, changements de perspective et intuitions décisives. Il faut les lire pour ce qu’ils sont : des reconstructions narratives produites à partir des traces de travail et des manuscrits, pas l’accès brut et intégral à un monologue intérieur du modèle. Elles restent néanmoins utiles pour comprendre comment une recherche a pu passer d’une piste fragile à un argument formalisable.
Lean n’est pas un tampon magique
Une preuve acceptée par Lean apporte une garantie forte sur une proposition précisément encodée et sur les dépendances autorisées. Elle ne tranche pas, à elle seule, toutes les questions scientifiques.
Il faut encore vérifier que l’énoncé formel correspond exactement à la revendication formulée en langage humain, que les hypothèses n’ont pas été subtilement renforcées et que les bibliothèques utilisées ne masquent pas une dépendance problématique. La formalisation ne mesure pas non plus l’importance d’un résultat, son originalité historique ou la qualité de son attribution. Ces dimensions exigent toujours le regard de spécialistes du domaine.
Le choix de publier le code Lean est donc essentiel, mais il ne remplace pas l’examen indépendant. Au moment de l’annonce, les principaux éléments disponibles — article de synthèse, manuscrits, formalisation et récits de raisonnement — proviennent d’OpenAI. La prochaine étape sera la reproduction des vérifications, puis la lecture critique des preuves informelles par les communautés concernées.
Les 2 000 dollars qui peuvent tromper
OpenAI estime que les jetons consommés pour trouver les dix solutions auraient coûté environ 2 000 dollars aux tarifs de son API Sol. Le chiffre frappe : il suggère qu’une production mathématique de haut niveau pourrait devenir extrêmement peu coûteuse.
Mais cette comparaison ne représente pas le coût total de l’expérience. Elle ne couvre pas l’entraînement du modèle, l’infrastructure ayant permis de le développer, la sélection des problèmes, les tentatives infructueuses hors du lot publié, le travail humain de préparation ni la construction de l’environnement de vérification. Il s’agit d’un équivalent de coût d’inférence sur les exécutions retenues, pas du prix réel de dix découvertes livrées de bout en bout.
Cette nuance n’annule pas l’intérêt économique. Si un modèle généraliste peut effectivement proposer des preuves nouvelles pour quelques centaines de dollars d’inférence, le coût marginal de l’exploration scientifique pourrait chuter. Mais sans protocole complet, taux d’échec et échantillon non sélectionné, le ratio entre calcul dépensé et découverte utile reste inconnu.
Une question d’attribution autant que de performance
OpenAI signe le rapport au nom de l’organisation et affirme prendre la responsabilité de l’exactitude des résultats, tout en indiquant que les arguments mathématiques viennent du modèle. Cette formulation touche un débat déjà vif : qui doit recevoir le crédit lorsqu’une IA produit l’idée, que des humains choisissent le problème et éditent le texte, puis qu’un assistant de preuve contrôle la logique ?
La Déclaration de Leiden sur l’IA et les mathématiques, publiée par des chercheurs et institutions du domaine, appelle à une attribution transparente, à l’accès aux outils et à une évaluation par des experts plutôt qu’à la seule communication des entreprises. Elle rappelle aussi que les mathématiques occupent une place particulière : la correction formelle peut être automatisée, ce qui offre aux modèles un signal de retour extraordinairement précis.
L’enjeu dépasse donc la paternité d’un article. Si les meilleurs systèmes restent internes à quelques laboratoires, ils pourraient accélérer certaines équipes bien avant que l’ensemble de la communauté dispose des mêmes instruments. La découverte se déplacerait alors en partie vers ceux qui contrôlent le calcul, les modèles et la capacité de sélectionner des milliers de problèmes prometteurs.
Le vrai mystère n’est plus seulement ce qu’Astra sait résoudre
Les dix manuscrits déplacent la conversation. La question n’est plus uniquement de savoir si un modèle peut réussir une olympiade ou compléter une démonstration connue. Elle devient : peut-il ouvrir plusieurs chemins réellement nouveaux, dans des domaines éloignés, avec un taux de réussite prévisible et des preuves que d’autres peuvent vérifier ?
OpenAI a fourni assez de matière pour que les mathématiciens puissent commencer ce travail de contrôle. Elle n’a pas encore fourni assez d’accès pour que l’on mesure Astra comme un outil scientifique reproductible. Si les résultats résistent à l’examen, la série marquera un cap : non pas la fin des mathématiciens, mais l’arrivée d’un partenaire capable de chercher à une échelle inhabituelle.
Le mystère le plus intéressant tient donc moins aux dix réponses déjà publiées qu’à tout ce qui manque encore : combien de problèmes ont échoué, quelles interventions humaines ont été décisives, et que trouverait Astra face à une liste préparée par des chercheurs indépendants ? C’est là que se jouera la différence entre une démonstration impressionnante et une nouvelle méthode de découverte.
Références
- OpenAI — Ten advances in mathematics and theoretical computer science
- Rapport complet — Ten proofs (PDF)
- OpenAI — Reasoning walkthroughs (PDF)
- Dépôt Lean public — openai/ten-proofs
- Déclaration de Leiden sur l’IA et les mathématiques
- Nature Machine Intelligence — AI and mathematics
