OpenAI dévoile Astra, un modèle qui résout dix problèmes mathématiques irrésolus depuis plus d'une décennie — chaque preuve coûte 2 000 dollars en tokens
Le 2 août 2026, OpenAI a révélé Astra, une nouvelle famille de modèles conçue pour les tâches longues et complexes. Une version interne vient de produire dix avancées majeures en mathématiques et en informatique théorique, dont la résolution de la conjecture de rigidité de Connes. Le coût total en tokens pour trouver ces solutions s'élève à 2 000 dollars.
2 août 2026. OpenAI publie un article de recherche qui change la définition de ce qu’un LLM peut accomplir. Dix problèmes mathématiques — dont certains n’avaient connu aucune avancée sur leur résultat central depuis plus de dix ans — viennent d’être résolus par Astra, un modèle encore non déployé que l’entreprise décrit comme « notre prochain modèle majeur ». Le coût total de la recherche : 2 000 dollars en tokens via l’API Sol.
Ce n’est pas une démonstration de force brute. Chaque preuve a été formalisée en Lean, le vérificateur de preuves mathématiques, ce qui rend chaque résultat vérifiable mécaniquement. Astra n’a pas « halluciné » dix théorèmes — il a produit dix certificats Lean que la communauté mathématique peut inspecter ligne par ligne.
Ce qu’Astra a réellement résolu
OpenAI a ciblé des problèmes répartis dans sept domaines distincts : géométrie en haute dimension, théorie des codes, complexité des circuits arithmétiques, théorie des groupes, complexité quantique, cryptographie sur réseaux et combinatoire extrémale. Aucun de ces problèmes n’avait vu son résultat central progresser depuis au moins dix ans.
Parmi les résultats annoncés :
- L’existence de groupes non-sofiques, une question ouverte en théorie des groupes depuis les travaux de Gromov en 1999.
- La réfutation de la conjecture de rigidité de Connes, un pilier de la géométrie non commutative formulé par Alain Connes en 1976.
- De nouvelles bornes pour l’empilement de sphères en haute dimension, un problème classique de la géométrie combinatoire popularisé par Paul Erdős.
- Plusieurs résultats résolvant des conjectures explicitement posées par Erdős lui-même.
The Information a confirmé indépendamment qu’OpenAI travaille bien sur Astra, une famille de modèles conçue pour les charges de travail longues — des tâches qui nécessitent des heures, voire des jours de calcul continu. Selon OpenAI, Astra permet à plusieurs agents IA de collaborer sur différentes parties d’un même problème, chaque agent traitant un sous-ensemble avant qu’un orchestrateur ne consolide les résultats.
BleepingComputer rapporte qu’OpenAI n’a pas encore décidé si le modèle sera commercialisé sous le nom de GPT-5.7, GPT-6 ou sous une marque entièrement nouvelle.
Pourquoi c’est différent de tout ce qui précède
Depuis GPT-4, chaque nouveau modèle OpenAI a principalement amélioré trois axes : la latence, le coût par token et la longueur de contexte. GPT-5 a apporté le tool use natif et le streaming. GPT-5.6 a baissé les coûts et amélioré l’efficacité. Mais aucun de ces modèles n’avait démontré une capacité de raisonnement long comparable à celle d’un mathématicien professionnel — c’est-à-dire la capacité de poursuivre une ligne de pensée sur des centaines de milliers de tokens sans dériver.
Le coût annoncé — 2 000 dollars pour résoudre dix problèmes de niveau recherche — est une métrique qui va obséder les laboratoires. À titre de comparaison, un post-doc en mathématiques coûte entre 60 000 et 100 000 dollars par an à un laboratoire universitaire. Même en supposant qu’un chercheur humain aurait résolu ces dix problèmes en trois ans (une hypothèse extrêmement optimiste), le rapport de coût est de 1 pour 100 en faveur du modèle.
Le fait que chaque preuve soit formalisée en Lean change la nature du débat. Il ne s’agit plus de « faire confiance à la sortie d’un LLM », mais de vérifier mécaniquement chaque étape du raisonnement. C’est ce couplage — IA générative + vérification formelle — qui fait d’Astra un objet fondamentalement différent des chatbots généralistes.
Le spectre d’une sortie différenciée
BleepingComputer rapporte qu’OpenAI envisagerait une politique de sortie à deux vitesses, similaire à celle d’Anthropic avec Claude : une version « grand public » aux capacités plafonnées, et une version « recherche » soumise à une approbation spéciale pour les clients institutionnels.
Cette approche serait inédite pour OpenAI, qui a toujours commercialisé un modèle unique par génération. Si elle se confirme, elle acterait une segmentation du marché de l’IA entre :
- Les modèles conversationnels (GPT-5, Claude) destinés au grand public et aux entreprises.
- Les modèles de raisonnement long (Astra, potentiellement Gemini Deep Research) réservés à la recherche scientifique, à la découverte de vulnérabilités et à la cryptanalyse.
Cette segmentation pose une question de fond : si Astra peut résoudre des conjectures mathématiques vieilles de cinquante ans, peut-il aussi casser des primitives cryptographiques conçues à une époque où ce type de calcul n’existait pas ? OpenAI n’a pas communiqué sur ce point.
Ce que cela signifie pour les RSSI et les équipes DevSecOps
Le timeline d’OpenAI suggère qu’Astra n’est pas un prototype de laboratoire mais un produit en phase avancée de développement. Les implications pour la sécurité sont directes :
- Automates de preuve et audit de code. Un modèle capable de formaliser des preuves en Lean peut, avec les mêmes mécanismes, prouver formellement des propriétés de sécurité sur du code critique. Les implémentations cryptographiques, les kernels et les protocoles d’authentification pourraient être vérifiés automatiquement.
- Découverte de vulnérabilités. Si Astra peut explorer un espace de recherche mathématique de manière autonome, la transposition à la recherche de vulnérabilités dans du code binaire ou source est directe. Un fuzzer augmenté par un raisonneur de ce calibre change le rapport de force entre attaquants et défenseurs.
- Vérification de la supply chain logicielle. La formalisation en Lean des dépendances critiques devient économiquement viable à 2 000 dollars par cible. Pour une dépendance comme OpenSSL, c’est un investissement négligeable.
Verdict
Astra n’est pas un GPT plus rapide. C’est une nouvelle catégorie de modèle IA — le raisonneur automatique à long terme. Si OpenAI tient ses promesses de coût et de vérifiabilité, chaque laboratoire de recherche, chaque agence de cybersécurité et chaque éditeur de logiciel critique va devoir intégrer ce type d’outil dans son pipeline d’analyse avant 2027.
Pour les RSSI : commencez dès maintenant à identifier les composants logiciels de votre infrastructure dont une preuve formelle de sécurité aurait le plus d’impact. La question n’est plus de savoir si ces modèles arrivent, mais qui les utilisera en premier — vos équipes ou vos adversaires.