OpenAI a publié le 1er août dix résultats sur des problèmes ouverts de mathématiques et d'informatique théorique, générés par une version interne de son prochain modèle, baptisé Astra. Chaque preuve est accompagnée d'un certificat Lean 4 vérifiable par machine et d'un compte rendu du raisonnement du modèle. La nouveauté par rapport aux annonces passées tient à cette vérification formelle, qui coupe court à une partie du scepticisme. Mais aucun de ces travaux n'a encore franchi l'étape d'une revue par les pairs, et le partage exact du travail entre l'IA et les chercheurs humains reste flou.

Ce qui est annoncé

Les dix avancées couvrent des domaines très différents des mathématiques et de l'informatique théorique : géométrie en haute dimension, théorie des codes, complexité des circuits arithmétiques, théorie des groupes, algèbres d'opérateurs, complexité quantique, cryptographie sur les réseaux euclidiens et combinatoire extrémale. Parmi les résultats mis en avant :

  • Un empilement de sphères en haute dimension : le modèle détermine la force asymptotique du programme linéaire de Cohn–Elkies et améliore la borne générale sur la densité d'empilement en grande dimension — un terrain où la meilleure borne connue remontait, pour l'essentiel, à la fin des années 1970.
  • La construction d'un groupe non sofique explicite, qui tranche une question restée ouverte depuis que Mikhaïl Gromov a introduit la notion de soficité à la fin des années 1990 : tous les groupes ne peuvent pas être approchés par des structures finies.
  • Un contre-exemple à une conjecture de rigidité de Connes en théorie des algèbres de von Neumann.
  • Des améliorations, par des facteurs exponentiels, des bornes classiques sur les codes binaires et sphériques.

S'ajoutent des résultats en complexité des circuits (autour du calcul du permanent), en répétition parallèle quantique, sur l'approximation du problème du vecteur le plus proche, sur la conjecture de volume d'Ehrhart, sur des nombres de Ramsey multicolores et sur des conjectures de nombres extrémaux. OpenAI affirme avoir dépensé moins de 2 000 dollars de calcul par problème, aux tarifs en jetons de son modèle GPT-5.6.

Pourquoi la vérification Lean change la donne

Les démonstrations d'IA en mathématiques traînent depuis des années un soupçon tenace : un texte qui ressemble à une preuve n'est pas une preuve tant qu'on ne l'a pas contrôlé pas à pas. Un modèle de langage peut produire un enchaînement d'apparence rigoureuse en recopiant des schémas vus à l'entraînement, sans qu'aucune logique correcte ne le sous-tende.

C'est ce point que la publication cherche à désamorcer. Chaque résultat est fourni avec une formalisation en Lean 4, un assistant de preuve dont le noyau vérifie mécaniquement que chaque étape découle des précédentes. Si le fichier « type-checke », la chaîne logique est correcte — indépendamment de la confiance qu'on accorde ou non au modèle qui l'a produite. C'est une garantie réelle, et rare pour ce genre d'annonce.

Signe que le résultat est pris au sérieux : Thomas Bloom, le mathématicien de l'université de Manchester qui tient le catalogue des problèmes d'Erdős — et qui avait publiquement démonté une revendication erronée d'OpenAI à l'automne 2025 — a qualifié ces travaux de « grande nouvelle », les jugeant plus significatifs qu'un précédent contre-exemple publié quelques mois plus tôt.

Ce que la vérification formelle ne dit pas

La prudence reste de mise, pour au moins trois raisons.

D'abord, Lean vérifie la correction logique, pas l'intérêt mathématique. Un fichier valide garantit qu'il n'y a pas de trou dans le raisonnement ; il ne dit pas si le résultat est profond, nouveau, ou obtenu par une idée neuve plutôt que par un assemblage habile d'outils déjà connus. Sur les forums spécialisés, plusieurs mathématiciens s'interrogent : s'agit-il de percées méthodologiques, ou de résultats incrémentaux tirés d'une exploration systématique de la littérature pour combiner les bons théorèmes existants ? Il faudra des mois de lecture par des spécialistes pour trancher, problème par problème.

Ensuite, la responsabilité couverte par Lean s'arrête à la traduction. OpenAI précise que sa garantie porte sur la fidélité entre l'énoncé en langage humain et sa version formalisée, pas sur le noyau de Lean lui-même. Or des cas récents ont montré qu'un modèle pouvait exploiter un bug du vérificateur pour faire passer un faux résultat. Autrement dit : la formalisation déplace la confiance, elle ne la supprime pas.

Enfin, et c'est peut-être le plus important, on ignore le dénominateur. Combien de problèmes ont été tentés au total ? Avec quel taux d'échec ? OpenAI reconnaît avoir échoué sur d'autres grands problèmes sans en préciser le nombre. Des commentateurs y voient un risque de sélection : présenter dix succès sans dire combien de tentatives les ont précédés revient à ne montrer que le haut de la distribution. Le chiffre des « moins de 2 000 dollars par problème » relève de la même prudence — il ne compte ni les échecs, ni le temps des chercheurs, ni l'infrastructure. À titre de comparaison, un laboratoire concurrent a récemment évoqué une facture bien plus lourde en jetons pour un seul travail de recherche cryptographique.

L'IA outille la recherche, elle ne signe pas la preuve seule

Le point de friction central est le partage du travail. La communication d'OpenAI ne détaille pas précisément ce qu'Astra a apporté et ce que l'équipe de recherche a fait : des humains ont dirigé la formalisation, mis en forme les résultats pour la publication et jugé lesquels valaient d'être publiés. On est donc loin d'une IA qui résout seule, de bout en bout, un problème ouvert et signe sa démonstration.

C'est aussi ainsi que des mathématiciens comme Terence Tao décrivent l'horizon crédible de ces outils : une « grande mathématique » où les humains gardent la part créative — poser les bonnes questions, choisir les stratégies — tandis que la machine prend en charge le travail technique de vérification et d'exploration. Dans cette lecture, ces dix résultats ne sont pas la fin des mathématiciens, mais un nouvel instrument, puissant et à manier avec méthode.

La question de fond, largement partagée dans la communauté, rejoint celle qui traverse déjà l'édition scientifique face à l'IA : un outil qui accélère la production de résultats ne garantit pas, à lui seul, leur qualité ni leur fiabilité — c'est la vérification, humaine et formelle, qui reste le juge. OpenAI n'est du reste pas seul sur ce créneau : d'autres laboratoires, dont DeepMind, poussent depuis plusieurs années l'IA appliquée à la démonstration mathématique et aux sciences ; quelques semaines plus tard, un modèle d'Anthropic a même réfuté la conjecture jacobienne, un problème de géométrie algébrique resté ouvert depuis 1939.

Reste que cette publication marque une inflexion réelle. En livrant des certificats machine-vérifiables plutôt que de simples affirmations, OpenAI répond à la critique la plus solide qu'on adressait à ce type d'annonce. Le verdict définitif, lui, viendra plus lentement : de la lecture attentive des spécialistes et du passage par la revue par les pairs, qui diront si ces dix résultats sont aussi neufs et importants que le communiqué le suggère.