Astra d'OpenAI dit avoir résolu 10 problèmes ouverts : ce qu'en disent les mathématiciens

Le 1er août 2026, OpenAI a publié un billet intitulé « Ten advances in mathematics and theoretical computer science ». L'entreprise y présente dix résultats obtenus par une version interne d'Astra, présentée comme sa prochaine grande famille de modèles. Empilement de sphères, théorie des codes, complexité des circuits arithmétiques, théorie des groupes, algèbres d'opérateurs, complexité quantique, cryptographie sur réseaux, combinatoire extrémale : le spectre est large, et plusieurs de ces questions étaient ouvertes depuis des décennies.

Le même jour, Noam Brown, chercheur chez OpenAI, résume l'affaire en une phrase sur X. Sa formulation et celle du billet ne disent pourtant pas tout à fait la même chose, et c'est de cet écart qu'est né tout le débat des soixante-douze heures suivantes.

Ce qu'OpenAI revendique, exactement

Le billet officiel est daté du 1er août 2026 et signé OpenAI, sans auteur individuel. Il annonce dix résultats, chacun accompagné d'un manuscrit, d'un certificat de preuve en Lean 4 et d'un document décrivant le cheminement du modèle.

Trois précisions comptent, et elles figurent noir sur blanc dans le billet. Les arguments mathématiques ont été produits par le modèle. La mise en forme des manuscrits et la formalisation en Lean ont été faites par des humains de chez OpenAI avec ce même modèle. Et l'entreprise déclare assumer la responsabilité de la correction des preuves, tout en refusant d'en revendiquer la paternité intellectuelle.

Le mot « résolu » n'a pas le même sens dans le billet et dans le post

Le billet écrit que chacun des dix résultats « résout ou fait progresser substantiellement » un problème ouvert de longue date. Le post de Noam Brown, lui, dit que le modèle « a résolu 10 problèmes ouverts majeurs ». C'est la formulation qui a fait 11 millions de vues, et c'est elle qui a circulé.

L'écart n'est pas anodin. Sur les dix entrées, certaines sont des contre-exemples qui referment définitivement une question (Connes, les problèmes d'Erdős 146, 180 et 183), d'autres sont des bornes améliorées qui font avancer un front sans le clore (les codes binaires, le permanent, l'empilement de sphères).

Ce que le certificat Lean prouve, et ce qu'il ne prouve pas

C'est le point technique le plus mal compris de l'affaire. Le dépôt `openai/ten-proofs` est public depuis le 1er août. Il contient dix fichiers Lean, dont un de 1,4 million de caractères pour la conjecture de Connes. Son fichier de suivi indique zéro `sorry`, c'est-à-dire aucune étape laissée en blanc, et seulement les trois axiomes standards de Lean.

Deux mentions de ce même fichier méritent d'être lues attentivement. La première dit que la production a été faite par un agent, avec le harnais Codex, sur une semaine. La seconde tient en deux mots : `review: agent-reviewed`. La relecture a été confiée à un agent, pas à un comité humain.

Surtout, un noyau Lean certifie qu'une preuve correspond bien à l'énoncé tel qu'il a été écrit en Lean. Il ne certifie pas que cet énoncé traduit fidèlement la question mathématique d'origine. Si la formalisation dit autre chose que le théorème visé, la machine valide quand même.

Ce que disent les mathématiciens qui ont lu les preuves

Ils sont peu nombreux à s'être exprimés, mais ceux qui l'ont fait sont précisément les spécialistes des questions concernées. Henry Yuen est l'auteur du théorème de 2016 sur lequel s'appuie le résultat de répétition parallèle quantique. Il se dit impressionné, présume la preuve correcte, et critique sévèrement la rédaction : selon lui le manuscrit s'étend longuement sur les préliminaires puis introduit le cœur technique du résultat sans le signaler, ce qui est caractéristique des preuves écrites par ChatGPT.

Chris Peikert, spécialiste des réseaux euclidiens à l'université du Michigan, a passé plusieurs heures sur le résultat concernant le problème du vecteur le plus proche. Son jugement est nettement plus favorable.

Il ajoute deux choses qui donnent la mesure exacte du résultat. D'abord, il a d'abord trouvé l'article mal écrit, puis a changé d'avis après une heure passée sur le résumé de preuve. Ensuite, Astra n'a pas optimisé son propre facteur d'approximation : une minute avec GPT-5.6 suffit, dit-il, à améliorer le résultat en resserrant la comptabilité.

Huck Bennett, de l'université du Colorado, replace la semaine dans son contexte, et son verdict rejoint une actualité que nous avions couverte quatre jours plus tôt.

En pratique, précise-t-il, c'est l'attaque de Claude contre le schéma de signature HAWK qui a eu des conséquences immédiates, puisqu'elle a sorti un candidat du processus de standardisation du NIST. Un résultat d'OpenAI sur la difficulté d'approximation ne change, lui, rien à ce qui tourne aujourd'hui.

La contestation qui n'a pas tenu, et celle qui tient

Le 2 août, un manuscrit déposé sur PhilArchive par Jenny Lorraine Nielsen a beaucoup circulé, jusqu'en une de Hacker News. Il annonce deux choses : que le contre-exemple d'OpenAI à la conjecture de Connes est invalide, et que la conjecture est en réalité vraie.

L'objection technique se résume ainsi. Le contre-exemple construit des groupes par extension par cocycle, un assemblage où la conjugaison fait apparaître des termes supplémentaires. Or, selon le manuscrit, la formalisation vérifie la propriété requise (des classes de conjugaison toutes infinies) avec des arguments qui ne valent que pour un produit direct, cas beaucoup plus simple où ces termes n'existent pas. Autrement dit, l'objection porte exactement sur le point signalé plus haut : Lean validerait un énoncé qui n'est pas celui qu'on croit.

L'accueil a été sévère. Un étudiant en mathématiques de Cambridge qui travaille sur le raisonnement mathématique chez OpenAI a répondu publiquement sur X dès le 1er août au soir que le texte relevait de la désinformation. Sur Hacker News, un commentateur relève que l'affirmation centrale sur le centre d'un produit semi-direct est simplement fausse, et le compte qui défendait le manuscrit dans le fil a été banni par la modération pour publication de texte généré par IA. Celui qui avait soumis le lien a fini par écrire qu'il regrettait de l'avoir partagé. Le manuscrit n'est pas relu par les pairs, et il revendique dans le même document la démonstration complète d'une conjecture ouverte depuis un demi-siècle.

« Une objection sérieuse existe bel et bien, mais elle ne porte pas sur les preuves. Elle porte sur ce qu'OpenAI n'a pas publié. »

Dans son analyse publiée le 2 août, Gary Marcus juge le résultat impressionnant mais largement survendu, et reprend deux questions que lui adresse le chercheur Ernie Davis. Combien de conjectures ont été tentées au total ? Si dix ont été tirées au sort parmi toutes les questions ouvertes, le résultat est stupéfiant ; si dix ont abouti sur cinquante soigneusement choisies, il reste remarquable mais change de nature ; et les échecs renseigneraient autant que les succès. Combien a coûté le travail des mathématiciens salariés qui ont préparé les manuscrits ? Le chiffre de 2 000 $ ne couvre que les jetons.

Aucune de ces informations ne figure dans le dossier. C'est la seule critique que personne n'a réfutée.

Reste le sujet dont la communauté parle le plus entre elle. Sur MathOverflow, une question posée le 1er août par un mathématicien qui n'exerce pas dans un grand centre de recherche a recueilli plus de 80 votes : OpenAI ouvre l'accès gratuit à ses meilleurs modèles à 100 000 scientifiques, mais seulement dans des institutions éligibles. Le débat n'est déjà plus de savoir si les modèles font des mathématiques. Il est de savoir qui aura le droit de s'en servir.