Le 1er août 2026, OpenAI a levé le voile sur Astra, ce que l’entreprise décrit comme sa prochaine grande famille de modèles. Mais l’annonce n’a pas pris la forme habituelle d’une démonstration de chatbot ou d’un tableau de scores sur des tests standardisés. Elle est arrivée sous la forme d’un manuscrit de 249 pages et d’un dépôt de code sur GitHub.
Le contenu : dix problèmes ouverts en mathématiques et en informatique théorique, résolus par une version interne d’Astra. Selon OpenAI, aucun de ces problèmes n’avait connu de progrès de la part des mathématiciens depuis au moins une décennie — et bien davantage pour la plupart d’entre eux. Le résultat le plus commenté est la première construction explicite d’un groupe non sofique, une question restée sans réponse depuis que le mathématicien Mikhaïl Gromov a introduit la notion de soficité en 1999.
Ce qui distingue cette annonce des précédentes tient en un mot : vérifiabilité. Chaque démonstration a été formalisée dans l’assistant de preuve Lean, produisant des certificats que n’importe quel chercheur peut recompiler sur sa propre machine. Pas besoin de croire OpenAI sur parole.
Ce qu’Astra a réellement démontré
Les dix résultats couvrent un spectre inhabituellement large de disciplines : géométrie en grande dimension, théorie des codes, théorie des groupes, complexité quantique, cryptographie à base de réseaux euclidiens et combinatoire extrémale. Il ne s’agit donc pas d’une spécialisation étroite sur un type de problème, mais d’une capacité transversale à attaquer des questions techniques très différentes les unes des autres.
Le cas du groupe non sofique mérite qu’on s’y arrête. La soficité est une propriété qui décrit, en gros, la possibilité d’approcher un groupe algébrique par des objets finis. Depuis 1999, personne ne savait si tout groupe dénombrable discret devait être sofique. Vingt-sept ans de recherche humaine n’avaient produit ni preuve ni contre-exemple. Astra a fourni une construction explicite.
OpenAI a été explicite sur la répartition du travail : les arguments mathématiques viennent du modèle, mais des chercheurs humains ont participé à la mise en forme des articles et à la formalisation des preuves, et l’entreprise assume la responsabilité de leur exactitude. Elle justifie ce choix de crédit en s’appuyant sur la Déclaration de Leyde sur l’IA et les mathématiques, un texte de référence sur l’attribution dans la recherche assistée par IA.
Pourquoi la vérification par Lean change la donne
En mai 2026, OpenAI avait déjà publié un contre-exemple à la conjecture des distances unités d’Erdős. Ce résultat avait nécessité la lecture et la contresignature de neuf mathématiciens extérieurs. C’est une validation solide, mais elle est sociale : elle dépend de la disponibilité de spécialistes compétents et ne peut pas être reproduite sans eux.
Lean fonctionne autrement. Son noyau de vérification rend un verdict binaire : la preuve compile, ou elle ne compile pas. Aucun doctorat requis, aucune file d’attente d’évaluation par les pairs. Les fichiers ont été publiés sur GitHub sous licence Apache 2.0, accompagnés d’un document détaillant le cheminement de raisonnement du modèle pour chaque solution.
C’est probablement là que se joue le vrai basculement. Tant que les productions mathématiques d’une IA devaient être relues à la main, le goulot d’étranglement restait humain. Avec une formalisation systématique, la vérification devient une opération machine, quasi instantanée et reproductible par n’importe qui.
2 000 dollars, mais uniquement pour les réussites
Le chiffre qui a circulé le plus vite est celui du coût. OpenAI indique que les jetons consommés pour générer les dix solutions auraient coûté environ 2 000 dollars aux tarifs de son API Sol. Rapporté à des questions restées ouvertes pendant des décennies, le montant a de quoi frapper.
Il faut cependant le lire pour ce qu’il est. Ce montant correspond aux tentatives qui ont abouti. Noam Brown, l’un des chercheurs à l’origine des techniques de raisonnement au moment de l’inférence utilisées par Astra, a reconnu publiquement que d’autres grands problèmes avaient été attaqués sans succès. « Malheureusement, aucun problème du prix du millénaire, pas encore », a-t-il écrit. L’Institut de mathématiques Clay offre un million de dollars pour chacun des sept problèmes du millénaire, et un seul a été résolu depuis leur annonce en 2000.
Brown a aussi souligné que peu de ressources avaient été investies par problème et qu’il restait possible de pousser beaucoup plus loin le calcul au moment de l’inférence. Autrement dit : le coût affiché mesure moins l’efficacité du système que la marge de progression encore disponible.
Les mathématiciens entre enthousiasme et vigilance
Thomas Bloom, mathématicien à l’université de Manchester et animateur du site erdosproblems.com, a qualifié les résultats de « grande nouvelle », les jugeant plus significatifs que le contre-exemple de mai en matière de constructions. Il a toutefois rejeté fermement l’idée que l’IA remplacerait les mathématiciens : le modèle s’appuie sur plus d’un siècle de théorie mathématique, a été construit par des mathématiciens et entraîné sur tout ce que les mathématiciens ont écrit.
Terence Tao, de son côté, a plutôt formulé une vision de collaboration à grande échelle entre humains et machines, où la direction créative reste humaine tandis que l’IA prend en charge une part importante du travail de dérivation. Une position qui n’exclut ni l’enthousiasme ni la prudence : la Déclaration de Leyde, publiée en juin 2026 et soutenue par l’Union mathématique internationale, identifie explicitement plusieurs risques liés à l’usage de l’IA dans la discipline.
Et maintenant ?
Astra n’est pas un produit. Selon les informations rapportées, la famille viendrait s’ajouter aux modèles Sol, Terra et Luna d’OpenAI, sans qu’il soit encore décidé si elle sortira sous le nom de GPT-6 ou comme variante de la ligne GPT-5. Aucune date de disponibilité n’a été annoncée, et Sam Altman en a fait la démonstration à des responsables politiques à Washington avant toute présentation publique.
L’architecture visée est celle de plusieurs agents coordonnés travaillant sur un même problème pendant des heures, voire des jours. C’est aussi la principale inconnue technique : les systèmes agentiques actuels peinent à ne pas accumuler d’erreurs sur de longues durées, et des travaux récents montrent que multiplier les agents peut dégrader les performances sur des tâches fortement couplées.
Reste que la démonstration est difficile à relativiser. Dix questions ouvertes depuis longtemps, des preuves vérifiables par machine, un coût dérisoire au regard des enjeux. Ce n’est pas la fin des mathématiques humaines — c’est plutôt le moment où l’outil devient assez bon pour qu’il faille redéfinir ce que signifie faire des mathématiques avec lui.
Sources
- The Decoder — OpenAI announces its « next major model » Astra by dropping ten previously unsolved math solutions
- Forbes — OpenAI’s Astra Solved Decades-Old Math Problems For $2,000
- Tech Times — OpenAI’s Astra Solves Ten Decade-Old Math Problems With Machine-Checkable Lean Proofs
- GitHub / OpenAI — ten-proofs (preuves formalisées en Lean)
- OpenAI — Ten proofs (manuscrit complet, PDF)
Laisser un commentaire