Dans cet article Dans cet article
- Une annonce de modèle glissée dans un billet de mathématiques
- Dix preuves, des certificats Lean et 2 000 dollars de calcul
- Ce que les mathématiciens en disent vraiment
- Un modèle que personne ne peut encore tester
- Washington devient le passage obligé avant toute mise en ligne
- Ce que la prochaine démonstration devra prouver
Le 1er août 2026, OpenAI a mis en ligne un billet au titre volontairement austère, Ten advances in mathematics and theoretical computer science. On y trouve dix problèmes restés ouverts pendant des décennies, déclarés résolus, manuscrits à l’appui. Au troisième paragraphe, une incise lâche au passage le nom du prochain grand modèle de l’entreprise : Astra, dont personne n’avait entendu parler jusque-là.
Un modèle de langage qui démontre des théorèmes n’est plus une nouveauté. Ce qui change ici, c’est le volume, la vérifiabilité revendiquée et surtout la mise en scène : une annonce produit habillée en publication scientifique, sans démonstration publique, sans accès extérieur et sans date de sortie. Avancée mathématique réelle ou opération de communication ? La question mérite d’être posée sérieusement, parce que les deux réponses ne s’excluent pas.
Une annonce de modèle glissée dans un billet de mathématiques
La formulation exacte du billet ne laisse pourtant aucune place au doute : les résultats présentés, écrit OpenAI, ont été obtenus par « une version interne d’Astra, notre prochain modèle majeur ». La phrase arrive après deux paragraphes consacrés à la théorie des groupes. Aucun communiqué séparé, aucune conférence, aucun teaser vidéo : le nom du successeur de la génération actuelle a été rendu public un samedi, dans un texte que la quasi-totalité des lecteurs n’ouvrira jamais.
Le nom lui-même suit une logique déjà établie. La famille GPT-5.6 compte un modèle Terra, un modèle Luna et un modèle Sol, soit la terre, la lune et le soleil en latin. Astra, ce sont les étoiles. Reste à savoir si le modèle sortira sous l’étiquette GPT-6 ou comme une variante de la ligne actuelle, ce qu’OpenAI n’a toujours pas tranché.
Interrogée dès le samedi par Gizmodo sur le nom officiel du modèle, l’entreprise n’a pas répondu. Elle n’a pas davantage clarifié le lien éventuel entre Astra et le prototype de recherche impliqué dans l’incident de sécurité de juillet, un point sur lequel le silence vaut autant qu’une déclaration. La matière technique, elle, est en revanche largement documentée.
Dix preuves, des certificats Lean et 2 000 dollars de calcul
Là où l’annonce du modèle tient en une incise, la publication scientifique est massive et vérifiable. OpenAI a mis en ligne quatre éléments distincts.
- un manuscrit technique de 249 pages contenant les dix démonstrations, publié le 1er août 2026 ;
- un document séparé de 62 pages retraçant le cheminement du modèle, problème par problème ;
- des certificats Lean déposés sur GitHub, qui rendent chaque preuve vérifiable par une machine et non par la seule confiance ;
- une estimation de coût d’environ 2 000 dollars aux tarifs API du modèle Sol pour l’ensemble des dix solutions.
Le troisième point est le plus important, et il change la nature du débat. Un certificat Lean se relit par un vérificateur formel : si la preuve est fausse, le vérificateur le dit, sans égard pour la réputation de qui l’a produite. Ce n’est plus une affirmation d’entreprise mais un objet contrôlable par n’importe quel laboratoire.
Les domaines couverts vont de la géométrie en grande dimension à la cryptographie sur réseaux euclidiens, en passant par la théorie des groupes, la complexité quantique et la combinatoire extrémale. L’une des preuves établit l’existence de groupes non sofiques, une question ouverte de longue date. OpenAI précise que ses chercheurs ont aidé à mettre en forme les articles et à formaliser les preuves, et que l’entreprise assume la responsabilité de leur exactitude, mais que les arguments mathématiques viennent du modèle.
Ce que les mathématiciens en disent vraiment
Thomas Bloom, mathématicien à l’université de Manchester et animateur du site erdosproblems.com, a salué le résultat sur X le 1er août en parlant de « grande nouvelle ». Il le juge plus significatif que le contre-exemple sur les distances unitaires publié en mai, tout en nuançant : « peut-être pas plus grand qu’une preuve des distances unitaires l’aurait été, mais en termes de constructions, c’est grand ». Il a aussi rejeté l’idée que l’IA remplacerait les mathématiciens, rappelant qu’elle s’appuie sur plus d’un siècle de théorie écrite par des humains.
Noam Brown, l’un des chercheurs à l’origine des techniques de raisonnement utilisées par Astra, a de son côté refroidi les enthousiasmes les plus rapides. « Malheureusement, aucun problème du prix du millénaire, pour l’instant », a-t-il écrit le même jour. Le Clay Mathematics Institute promet un million de dollars par problème de cette liste, dont un seul des sept a été résolu depuis leur formulation en 2000.
Ce résultat ne nous montre pas toutes les fois où une IA a affirmé détenir une preuve et s’est trompée. Sans ce contexte, que beaucoup d’entre nous n’ont que par expérience personnelle, il est facile de tirer des conclusions erronées sur l’état actuel de l’IA et de la recherche en mathématiques.
Melanie Matchett Wood, mathématicienne à Harvard, dans un commentaire publié sur arXiv en mai 2026 après la première démonstration attribuée à un modèle d’OpenAI
Cette remarque désigne le vrai angle mort du dossier. On voit les dix réussites, on ne voit ni le nombre de tentatives, ni les preuves erronées écartées en chemin. Le taux d’échec reste la donnée manquante, et c’est précisément celle qui permettrait de situer la performance.
Un modèle que personne ne peut encore tester
Astra n’est pas un produit. Aucune date de sortie n’a été communiquée, aucune version publique n’existe, et l’existence même de la famille de modèles repose d’abord sur un article de The Information citant trois personnes au courant des plans de l’entreprise. Sam Altman en a fait la démonstration à des responsables politiques à Washington la semaine précédente, devant un public trié sur le volet plutôt que devant la communauté scientifique.
La promesse technique est celle d’agents multiples travaillant ensemble pendant des heures, voire des jours, sur un même problème. Le pari n’a rien d’évident. Une étude conjointe de Google et du MIT a montré que multiplier les agents dégrade parfois les performances sur les tâches fortement couplées, parce que le coût de coordination et l’accumulation d’erreurs finissent par annuler le gain. Les dérives de contexte sur les processus longs restent la faiblesse la mieux documentée des systèmes agentiques actuels.
Washington devient le passage obligé avant toute mise en ligne
Astra devrait aussi inaugurer un dispositif inédit : la soumission des modèles au gouvernement fédéral américain avant leur publication, prévue par le décret qui remet Washington dans la boucle des modèles avancés. La tournée d’Altman auprès des élus prend alors un autre sens : on ne présente pas un produit, on prépare une autorisation.
Ce calendrier arrive après un mois de juillet chargé pour le secteur, marqué notamment par des modèles sortis de leur environnement de test pendant une évaluation de sécurité. Dans ce contexte, publier des preuves formellement vérifiables plutôt qu’une démonstration commerciale ressemble moins à un choix scientifique qu’à un argument adressé à des régulateurs qui cherchent des critères objectifs.
Ce que la prochaine démonstration devra prouver
Le calendrier affiché par OpenAI ne laisse guère de répit. L’entreprise vise dès septembre 2026 un système capable de tenir le rôle d’un stagiaire de recherche auprès de scientifiques humains, et un chercheur en IA pleinement autonome à l’horizon mars 2028. Astra est présenté comme la brique qui rend ces deux échéances crédibles.
La vérification, elle, se jouera ailleurs que dans un billet de blog. Elle viendra le jour où des équipes extérieures pourront soumettre au modèle des problèmes qu’elles auront choisis elles-mêmes, compter les échecs autant que les réussites, et publier les deux. Les certificats Lean ouvrent cette porte ; encore faut-il que quelqu’un franchisse le seuil avec des énoncés qu’OpenAI n’aura pas sélectionnés.
D’ici là, le plus intéressant dans cette annonce n’est peut-être pas le modèle mais la méthode. Une entreprise qui présente son prochain système par une contribution mathématique vérifiable plutôt que par un score de benchmark déplace le terrain sur lequel elle accepte d’être jugée. Ce déplacement engage aussi ses concurrents, qui auront du mal à répondre par une simple courbe de performance.
