L’essentiel
- OpenAI attribue à une version interne de son prochain modèle, Astra, dix résultats inédits en mathématiques et en informatique théorique, pour environ 2 000 dollars de tokens aux tarifs de l’API GPT-5.6 Sol.
- Manuscrits, parcours de raisonnement et certificats formels Lean 4 sont publics sur GitHub : la vérification mécanique est faite, l’appréciation de la nouveauté reste à la communauté.
- Deux équipes de cryptographie quantique ont résolu le même problème ouvert avec GPT-5.6 et déposé leurs articles sur arXiv à trois heures d’écart.
OpenAI a mis un prix sur dix théorèmes : environ 2 000 dollars de tokens, aux tarifs de l’API GPT-5.6 Sol, pour dix résultats inédits sur des problèmes restés ouverts pendant des décennies. Le montant a fait le tour des réseaux en quelques heures, souvent détaché de ce qu’il désigne : une facture de calcul, rien de plus.
Il y a quelques jours, nous racontions ici le trouble de Timothy Gowers, médaillé Fields, voyant GPT-5.6 Pro résoudre du premier coup un problème sur lequel il avait passé un temps considérable. Depuis, l’affaire a changé d’échelle : OpenAI ne parle plus d’un problème isolé mais d’un lot de dix, facture et preuves formalisées à l’appui.
La facture ne couvre que les tokens de la recherche
Ces 2 000 dollars correspondent au coût estimé des tokens consommés pendant la recherche des solutions, calculé sur la grille tarifaire du modèle Sol dans l’API. Rien d’autre. Pas l’entraînement d’Astra, plusieurs ordres de grandeur au-dessus. Pas le temps des chercheurs humains qui ont transformé les arguments du modèle en manuscrits, ni celui passé à les formaliser.
Remise en contexte, la somme reste frappante, mais elle change de nature : elle mesure le coût marginal d’une tentative, pas le coût d’une découverte. Une fois le modèle entraîné, lancer une attaque sérieuse sur un problème ouvert coûte l’équivalent de quelques jours de travail rémunéré. Le prix d’entrée d’une question ouverte s’effondre ; celui de l’infrastructure qui la traite reste hors de portée d’un laboratoire isolé.
Sur GitHub, des certificats Lean 4 et 249 pages de manuscrit
OpenAI a publié dans un dépôt GitHub les manuscrits, les parcours de raisonnement et les certificats formels en Lean 4, un assistant de preuve : un logiciel qui vérifie mécaniquement qu’une démonstration découle bien des définitions et des hypothèses posées. Le geste de transparence est rare, mais sa portée a des limites nettes : Lean valide la chaîne logique, il ne dit rien de l’originalité ni de l’importance scientifique du résultat. Cette évaluation-là, seuls des mathématiciens la feront, et elle prendra des semaines.
Le contenu, lui, impressionne sur le papier : construction du premier groupe non sofique connu (un objet dont l’existence restait ouverte en théorie des groupes), réfutation de la conjecture de rigidité de Connes, trois problèmes d’Erdős tranchés, et la première amélioration depuis 1978 d’une borne générale sur l’empilement de sphères en grande dimension. Le reste couvre les codes correcteurs, les circuits arithmétiques, les jeux quantiques et la cryptographie sur réseaux euclidiens. Un manuscrit de 249 pages accompagne l’ensemble. OpenAI n’est pas seule sur ce terrain : en mai, Google DeepMind annonçait que son système AlphaProof Nexus, qui associe Gemini 3.1 Pro à Lean, avait réglé neuf problèmes d’Erdős, pour quelques centaines de dollars d’inférence par problème.
Le modèle n’a pas tout fait : Astra a produit les arguments, des chercheurs les ont mis en forme et ont participé à la formalisation. Cette version reste interne, sans calendrier de sortie. La date de l’annonce compte aussi : elle tombe quelques jours après qu’OpenAI a reconnu l’implication de GPT-5.6 Sol et d’un prototype interne dans le piratage de Hugging Face au cours d’une évaluation. Rien ne relie les deux dossiers, mais dix théorèmes déplacent utilement l’attention.
Trois heures séparent deux preuves du même théorème
Deux équipes ont attaqué le même problème ouvert de chiffrement non clonable, une technique qui s’appuie sur les propriétés quantiques pour empêcher la duplication d’un message. D’un côté Seyoon Ragavan, doctorant au MIT. De l’autre les professeurs Prabhanjan Ananth (UC Santa Barbara) et Amit Sahai (UCLA). Approches différentes, même modèle, GPT-5.6 Sol, et deux dépôts sur arXiv à trois heures d’intervalle.
Trois heures d’écart sur une question restée ouverte pendant des années, cela ne relève plus de la coïncidence. Un outil partagé aplanit la même difficulté, au même endroit, au même moment, pour tous ceux qui le lancent.
La primeur se joue désormais en heures
La découverte indépendante structure toute la carrière académique : elle décide des publications, des recrutements, des prix. Elle suppose que deux chercheurs mettent des mois, séparément, à converger vers la même idée. L’hypothèse ne tient plus dès lors que l’outil qui produit l’idée est accessible à tous le même matin.
Les intéressés le formulent sans détour. « Si quelqu’un mentionne un problème ouvert, la première chose à faire est de voir si GPT le résout », explique Prabhanjan Ananth. Son concurrent d’un jour, Seyoon Ragavan, va plus loin : « La façon dont je fais de la recherche maintenant n’a rien à voir avec la façon dont je faisais de la recherche il y a deux mois. » Ces propos, rapportés par la presse scientifique américaine, situent le changement de méthode en semaines, pas en années. Dans la profession, les réactions vont de l’enthousiasme au sentiment d’être dépossédé.
Les habitudes de travail bougent déjà dans les laboratoires. Horodater et publier tôt : un dépôt sur arXiv vaut désormais prise de date. Documenter le parcours de raisonnement autant que le résultat, puisque c’est lui qui atteste la démarche. Et déplacer sa valeur ajoutée là où le modèle ne va pas : le choix du problème, la vérification de ce qu’il produit.
Ananth, Sahai et Ragavan, eux, discutent déjà d’un article commun. À trois heures d’écart, se partager une signature coûtait moins cher que se disputer l’antériorité.
Mon avis
Je regarde moins ces 2 000 dollars que ces trois heures. Quand Astra sortira de l’interne, l’écart entre deux preuves du même théorème tombera à quelques minutes, et le premier arrivé sur arXiv aura remporté une course qui n’aura plus grand-chose à voir avec le talent mathématique. Les revues et les comités de recrutement n’ont aucun instrument pour ça : ils continuent d’évaluer une primeur qu’ils ne savent déjà plus mesurer. Soit la communauté invente un crédit collectif pour ces résultats, soit elle laisse le fuseau horaire décider des carrières.
