OpenAI a chiffré dix preuves aux tarifs d'un autre

Un article de 249 pages arrivé avec un nom

Sébastien Bubeck, chercheur chez OpenAI, a passé son samedi à expliquer à l'internet que les groupes non sofiques existent. Il a présenté cet énoncé comme l'un des nombreux résultats démontrés par Astra, qu'il a qualifié de prochain grand modèle de l'entreprise, et a annoncé qu'OpenAI publiait dix preuves de ce type, assorties de certificats en Lean et d'explications du raisonnement pour chacune. À l'annonce étaient joints un manuscrit de 249 pages, un second document reprenant ces explications et un dépôt public de certificats vérifiables par machine. La couverture qui a suivi s'est vite arrêtée sur deux chiffres: dix problèmes et environ 2 000 dollars de calcul.

Le manuscrit, lui, n'emploie jamais le mot Astra. Il s'ouvre en présentant un ensemble de résultats obtenus par un modèle interne d'OpenAI, puis consacre 249 pages à l'empilement de sphères, aux algèbres de von Neumann et à la complexité des circuits sans nommer ce qui les a produits. Le nom vit dans l'annonce. La mathématique vit dans l'article. Tenir ces deux surfaces séparées, c'est tout le travail de celui qui lit en acheteur et non en spectateur.

Ce qui a été livré est réellement vérifiable

Les dix résultats ne sont pas décoratifs. Le premier détermine la force asymptotique exacte du programme de Cohn-Elkies et relève l'exposant général d'empilement de sphères en grande dimension, de la valeur classique de Kabatianskii-Levenshtein de 0,59905576 à environ 0,6044, ce que l'article présente comme la première amélioration de cette borne générale depuis 1978. Le troisième construit un groupe non sofique explicite et tranche la question de savoir si tout groupe dénombrable admet des approximations finies par permutations. Le quatrième réfute la conjecture de rigidité de Connes en construisant une infinité de groupes de propriété (T), deux à deux non isomorphes, partageant une même algèbre de von Neumann de groupe. Les autres portent sur les codes binaires et sphériques, les bornes inférieures pour le calcul de la permanente, la répétition parallèle quantique, le problème du vecteur le plus proche, la conjecture du volume d'Ehrhart, une borne inférieure superexponentielle pour les nombres de Ramsey multicolores, et des contre-exemples à deux conjectures de théorie extrémale des graphes, dont trois issus du catalogue de Paul Erdos.

Chacun s'accompagne d'une formalisation en Lean 4 dans un dépôt public, construite sur mathlib avec Lean 4.32.0 et diffusée sous licence Apache-2.0. C'est la partie de cette publication qui mérite un éloge sans réserve. Un certificat vérifiable par machine signifie qu'un inconnu muni d'un portable peut confirmer la validité de l'argument sans faire confiance à OpenAI, sans faire confiance au modèle et sans attendre l'évaluation par les pairs. La plupart des affirmations de capacité présentées cette année à un dirigeant sont arrivées sous forme de score publié par celui-là même qui vend le modèle. Celles-ci sont arrivées sous forme d'objets qui ne répondent ni à l'un ni à l'autre.

Le remerciement nomme un modèle déjà achetable

À la fin du quatrième chapitre, après les remerciements à Sorin Popa et à d'autres pour leurs commentaires et relectures, figure une phrase qu'aucune couverture n'a relevée. Pendant la préparation de ce manuscrit, écrit OpenAI, l'entreprise a eu connaissance de travaux indépendants et simultanés de Shuoxing Zhou établissant eux aussi un contre-exemple à la conjecture de rigidité de Connes, développés en partie avec l'assistance de GPT-5.6 Sol. Sol n'est pas le modèle inédit. Sol est le modèle qu'OpenAI vend aujourd'hui, avec une grille tarifaire publiée.

Lu sobrement, l'un des dix résultats phares a été atteint au même moment par quelqu'un d'extérieur au laboratoire, travaillant avec un logiciel de disponibilité générale. Cela ne diminue pas les neuf autres, et OpenAI l'a divulgué dans son propre document plutôt que de laisser la chose se découvrir, ce qui est à porter à son crédit. Mais c'est de loin la phrase la plus déterminante de toute la publication pour qui doit choisir ce qu'il va licencier, et elle se trouve dans un paragraphe de remerciements, au-delà de 200 pages d'algèbre d'opérateurs, et non dans l'annonce. Pour les entreprises françaises qui mettent en concurrence des prestations d'intelligence artificielle, c'est exactement là que se joue l'écart entre une démonstration et un engagement.

Une étiquette de prix empruntée à un autre produit

Le chiffre de 2 000 dollars a plus servi ces dernières vingt-quatre heures que tout autre nombre de la publication, et ce n'est pas un prix. C'est un volume de jetons valorisé aux tarifs d'API publiés de GPT-5.6 Sol, soit environ 1 800 euros. Astra n'a pas de tarifs publiés, parce qu'Astra n'est pas à vendre. Le chiffre répond donc à une question hypothétique, celle de savoir ce que ces jetons auraient coûté s'ils avaient été facturés comme des jetons de Sol, et on le lit comme la réponse à une tout autre question, celle du coût actuel de la recherche mathématique de pointe.

Ce que le nombre ne dit pas compte autant que ce qu'il dit. Il ne révèle ni combien de tentatives ont précédé les dix qui ont abouti, ni quelle part de direction humaine les a façonnées, ni la durée réelle de l'ensemble, ni ce que coûtera Astra le jour où il sortira. OpenAI n'a donné aucune date et le décrit seulement comme sa prochaine grande famille de modèles. Le dirigeant qui range 2 000 dollars comme le tarif en vigueur d'une conjecture résolue a noté un nombre qui ne fut jamais une facture, pour un produit qu'on ne peut pas encore acheter.

Demandez ce que fait le modèle en production

L'écart entre le modèle de la démonstration et le modèle de la grille tarifaire est la variable la plus systématiquement manipulée dans l'achat d'intelligence artificielle, et il reste d'ordinaire invisible parce que les fournisseurs ne sont pas tenus de le documenter. Cette publication est inhabituelle précisément parce que la preuve concernant le modèle en production se trouve dans le manuscrit du fournisseur lui-même. La bonne réaction n'est pas la méfiance envers la mathématique, qui est formalisée et vérifiable, mais la rigueur dans l'inférence. Une preuve vérifiée est une affirmation sur la preuve. Elle ne dit rien du modèle qui l'a produite, ni de la tentative, ni de l'aide reçue, ni du prix.

Trois questions transforment cela en pratique d'achat. Quelle version du modèle a produit le résultat que vous me montrez, et cette version est-elle aujourd'hui disponible pour tous. Si elle ne l'est pas, que fait la version disponible sur la même tâche. Et quels sont les tarifs publiés de la version que j'exploiterais réellement. Un fournisseur capable de répondre aux trois vend un produit. Un fournisseur qui ne répond qu'à la première présente un aperçu de recherche, si remarquable que soit l'objet qui l'accompagne.

À lire ensuite: Microsoft a formé ses vendeurs à dire que Claude est plus lent  |  Google a jeté un modèle d'IA presque fini