Astra d'OpenAI résout dix problèmes mathématiques ouverts : ce que l'IA vérifiable signifie pour votre entreprise

Astra d'OpenAI résout dix problèmes mathématiques ouverts, et la vraie histoire n'est pas les mathématiques

En bref : le 1er août 2026, OpenAI a annoncé qu'une version interne de son prochain modèle, Astra, avait produit de nouveaux résultats sur dix problèmes ouverts de mathématiques et d'informatique théorique, chacun non résolu depuis au moins dix ans. Plus important que les résultats eux-mêmes : la façon dont ils ont été livrés. Chacun est accompagné d'un certificat de preuve Lean 4 vérifiable par machine sur GitHub, avec un manuscrit de 249 pages, pour un coût de calcul total d'environ 2 000 $. La leçon pour un dirigeant ne porte ni sur la théorie des groupes ni sur l'empilement de sphères. Elle tient en un principe : une IA qui vous remet un résultat vérifiable par machine est fondamentalement différente d'une IA qui vous remet une prose convaincante.

Qu'a-t-on annoncé exactement ?

Le résultat phare est la première construction explicite d'un groupe dit non sofique, une question ouverte depuis que Mikhaïl Gromov a introduit la notion de soficité en 1999. À ses côtés : une réfutation de la conjecture de rigidité de Connes sur les algèbres de von Neumann, une preuve de la conjecture du volume d'Ehrhart, la résolution de trois problèmes du catalogue de Paul Erdős, dont le problème 183 sur les nombres de Ramsey multicolores, et une amélioration de la borne supérieure de la densité d'empilement de sphères en grande dimension, apparemment la première amélioration depuis 1978.

Ce qui distingue cette annonce des vagues précédentes de « l'IA a résolu un problème », c'est la livraison. Au lieu d'une affirmation à laquelle on vous demande de croire, OpenAI a publié des certificats Lean 4 pour chaque résultat, avec un nombre de « sorry » égal à zéro, le marqueur technique qui signifie qu'aucune étape des fichiers publiés n'est laissée sans preuve. N'importe qui disposant d'un ordinateur peut cloner le dépôt, lancer le vérificateur et obtenir un verdict définitif en quelques minutes, au lieu d'attendre des mois une relecture manuelle.

La valeur n'est pas que le modèle ait revendiqué un résultat. C'est qu'il ait livré une machine qui vérifie la revendication à votre place.

L'autre face : des critiques sérieuses qu'il faut mentionner

Le tableau n'est pas uniformément brillant, et il n'est qu'honnête de le dire. Des mathématiciens spécialistes ont soulevé des objections de fond. D'abord, aucun des dix résultats n'a été relu par les pairs, et l'annonce est passée par un billet de blog d'entreprise plutôt que par une revue, ce que certains jugent contraire à l'esprit de la Déclaration de Leyde publiée en juin 2026. Ensuite, des accusations d'attribution manquante à des travaux antérieurs : des chercheurs ont relevé que l'argument sur l'empilement de sphères reprenait un raisonnement déjà publié sans le citer, et le même schéma a été signalé dans le résultat sur les groupes non sofiques.

Il y a aussi une réserve technique importante. Lean élimine une large classe d'erreurs logiques locales, mais il ne transforme pas les définitions, ni la traduction d'une question mathématique informelle en énoncé formel, en faits mécaniques. Autrement dit : une preuve peut être entièrement correcte alors que l'énoncé prouvé ne correspond pas à la question que l'on croit avoir résolue. Le dépôt lui-même décrit le travail comme « relu par des agents » plutôt que relu de façon indépendante par des humains.

La traduction pratique pour une entreprise saoudienne

La distance entre une question de théorie des groupes et votre boutique, votre usine ou votre société de services peut sembler énorme. Mais l'idée centrale se transpose directement, car les résultats de l'IA se rangent en deux catégories qui exigent une gestion des risques totalement différente :

• Les résultats vérifiables par machine : du code qui passe des tests, une écriture comptable équilibrée, une facture que la plateforme de facturation électronique accepte, une requête en base de données dont vous pouvez rapprocher le résultat d'une source de référence. Ici, vous pouvez laisser le modèle aller vite, car il existe un juge final qui ne flatte pas.
• Les résultats non vérifiables : un compte rendu de réunion, une réponse à un client, une analyse de marché, une recommandation de recrutement. Aucun vérificateur ne renvoie « réussi » ou « échoué » : il vous faut une relecture humaine, des sources visibles et des limites claires sur ce que le modèle a le droit d'affirmer.

Les projets d'IA qui échouent le plus lourdement dans les entreprises sont ceux qui traitent la seconde catégorie comme si c'était la première. L'inverse est vrai aussi : beaucoup d'opportunités gagnantes sont manquées parce que personne n'a remarqué qu'un processus donné admet en réalité une vérification automatique s'il est bien conçu.

Comment construire une couche de vérification dans votre entreprise

La première étape consiste à demander, pour chaque processus que vous envisagez d'automatiser : quel test prouve que le résultat est correct sans qu'un humain le lise ? S'il existe une réponse, vous avez un excellent candidat à l'automatisation. S'il n'y en a pas, soit vous concevez un tel test, soit vous gardez un humain dans la boucle.

Dans les systèmes de gestion, cela signifie des choses concrètes : des règles de validation appliquées au niveau de la base de données et pas seulement dans l'interface ; un rapprochement automatique à trois voies entre commande, facture et stock ; la confrontation des résultats du modèle à une source de vérité unique avant de s'y fier ; des tests automatisés exécutés à chaque modification du code ; et une piste d'audit qui montre qui a produit quoi, quand et à partir de quelles données. Ce n'est pas un luxe d'ingénierie : c'est ce qui rend l'usage de l'IA dans des opérations sensibles défendable devant votre auditeur, votre client et votre régulateur.

Ne négligez pas non plus la dimension réglementaire. Tout traitement de données personnelles dans le Royaume relève de la loi sur la protection des données personnelles, et ses principes de limitation des finalités, de minimisation des données et de responsabilité signifient en pratique qu'il vous faut un registre documenté de ce qu'a fait le modèle, et pas seulement une confiance dans sa qualité.

Trois enseignements à retenir

Premièrement, les capacités de raisonnement approfondi progressent plus vite que ne le supposent beaucoup de feuilles de route d'entreprise, pour un coût d'exploitation qui baisse rapidement : 2 000 $ pour dix résultats de niveau recherche est un chiffre qui mérite qu'on s'y arrête. Deuxièmement, c'est la vérification, et non la confiance, qui transforme la capacité d'un modèle en valeur opérationnelle sur laquelle on peut compter. Troisièmement, la transparence sur les sources et l'attribution fait désormais partie de la qualité du résultat lui-même, ce n'est pas un ajout cosmétique, et c'est précisément là que les critiques de cette semaine ont porté.

Comment nous le construisons chez Origami

Nous sommes une société technologique, et notre travail en IA part de la même question : où le résultat peut-il être vérifié automatiquement, et où ne le peut-il pas ? Nous concevons des systèmes où le modèle opère dans des limites claires, où ses résultats passent par des règles de validation et des sources de vérité au sein de vos propres systèmes, et où chaque étape laisse une trace. L'objectif n'est pas un modèle plus intelligent, c'est un processus auquel vous pouvez faire confiance parce que vous pouvez l'inspecter.

Sources

• Annonce officielle d'OpenAI : openai.com
• Couverture de The Next Web, avec le détail sur les groupes non sofiques : thenextweb.com
• SiliconANGLE sur les résultats et les preuves publiées : siliconangle.com
• Autorité saoudienne des données et de l'intelligence artificielle, loi sur la protection des données personnelles : sdaia.gov.sa