OpenAI affirme que son prochain modèle d'IA, Astra, a résolu dix problèmes mathématiques de longue date pour environ 2 000 $.

La société a publié sur GitHub des preuves Lean 4 vérifiables par machine pour les 10 résultats, y compris la première construction explicite d'un groupe non sofi.

Par Cris Tolomia3 min de lectureMis à jour 3 août 2026

Add QZ to Google

OpenAI affirme que son prochain modèle d'IA, Astra, a résolu dix problèmes mathématiques de longue date pour environ 2 000 $.

Cheng Xin / Getty Images

OpenAI a annoncé samedi qu'Astra, son prochain modèle majeur toujours en attente de sortie publique, avait généré des solutions à 10 problèmes de longue date en mathématiques et en informatique théorique, chacun non résolu depuis dix ans ou plus. En parallèle de l'annonce, OpenAI a publié un manuscrit de 249 pages et des certificats de preuve Lean 4 sur GitHub sous une licence Apache 2.0; le nombre de « désolé » du dépôt est de zéro, indiquant que chaque étape de toutes les dix preuves formalisées est entièrement vérifiée.

Parmi les découvertes, une construction explicite d'un groupe non sofic, résolvant une question restée sans réponse depuis que Mikhail Gromov a présenté le concept de soficité en 1999. Astra a également réfuté la conjecture de rigidité de Connes sur les algèbres de von Neumann, prouvé la conjecture de volume d'Ehrhart, et résolu trois problèmes du catalogue de Paul Erdős, y compris le problème 183 sur les nombres de Ramsey multicolores, selon SiliconAngle. Les résultats supplémentaires couvrent le placement de sphères en haute dimension, les codes binaires et sphériques, la complexité des circuits arithmétiques, la répétition parallèle quantique et la difficulté du problème du vecteur le plus proche.

OpenAI a estimé le coût total de calcul pour les 10 solutions à environ 2 000 $ aux tarifs API GPT-5.6 Sol. Le chef de la recherche en mathématiques de la société, Sebastien Bubeck, a confirmé les résultats sur X $TWTR, les qualifiant de « magnifiques », selon The Next Web. Le chercheur Noam Brown a qualifié les résultats de "grande avancée pour le raisonnement scientifique" dans un post sur X. OpenAI a crédité Astra pour le raisonnement mathématique sous-jacent, tandis que des chercheurs humains ont travaillé la sortie du modèle dans des articles adaptés à la publication.

Thomas Bloom, qui gère la base de données erdosproblems.com, a décrit les dix résultats comme "grandes nouvelles" sur X, plaçant leur importance au-dessus du contre-exemple de distance unitaire qu'un modèle interne d'OpenAI a généré en mai, selon The Next Web.

Parce que le noyau de Lean accepte ou rejette une preuve de manière définitive, la vérification indépendante nécessite seulement de faire passer les certificats dans le compilateur. Cependant, aucun des 10 résultats n'a été soumis à un examen par les pairs, selon SiliconAngle.

L'annonce intervient dans un contexte de friction entre les entreprises d'IA et la communauté mathématique. L'approbation en juin par l'Union Mathématique Internationale de la Déclaration de Leiden a formalisé les préoccupations de la communauté, la déclaration accusant les entreprises d'IA d'exploiter les recherches publiées sans permission, d'éviter l'examen par les pairs, et d'éroder les normes autour de la preuve et du crédit.

OpenAI n'a pas donné de date de sortie pour Astra. OpenAI a récemment réduit les prix de deux modèles de sa famille GPT-5.6 après des améliorations d'efficacité lors du développement interne, tandis que les prix Sol — le taux utilisé pour calculer le coût informatique de 2 000 $ Astra — sont restés inchangés.

OpenAI n'a pas encore précisé si Astra portera une désignation GPT-6 ou s'intégrera dans la ligne GPT-5 existante, et le modèle devra passer l'examen de sécurité fédéral de l'IA avant de pouvoir atteindre les utilisateurs.

L'essentiel de l'actualité économique, livré chaque matin.

Rejoignez plus de 500 000 lecteurs qui commencent leur journée avec Quartz.

En vous abonnant, vous acceptez nos Conditions d'utilisation et notre Politique de confidentialité.