Les critiques jugent les prouesses mathématiques d’Astra surestimées

OpenAI a annoncé le 1er août que sa famille de modèles Astra, non encore publiée, a produit des solutions à 10 problèmes ouverts de longue date en mathématiques et en informatique théorique, publiant un manuscrit de 249 pages et des certificats de preuve entièrement vérifiés en Lean 4 sur GitHub. Les résultats couvrent des domaines tels que la géométrie de haute dimension, la théorie des codes, la théorie des groupes, la complexité quantique et la combinatoire extrémale, l'entreprise rapportant un coût de calcul total d'environ 2 000 dollars aux tarifs de l'API GPT-5.6 Sol.ndtv+2

Ce qu'Astra a résolu

Selon le blog d'OpenAI, Astra a généré des avancées dans les bornes d'empilement de sphères, les codes correcteurs d'erreurs et la construction du premier groupe non sofique explicite, une structure qui restait une question ouverte depuis 1999. Le modèle a également prouvé le théorème de répétition parallèle quantique pour les jeux généraux à deux joueurs intriqués et a fourni des résultats sur la conjecture du volume d'Ehrhart et la conjecture de rigidité de Connes. Trois problèmes supplémentaires du catalogue de Paul Erdős ont également été résolus, selon les rapports de Quartz.qz+2

OpenAI a déclaré que son IA a généré les arguments mathématiques fondamentaux, tandis que les chercheurs ont ensuite formalisé chaque preuve à l'aide de l'assistant de preuve Lean. Le nombre de "sorry" dans le dépôt GitHub, un indicateur d'étapes non vérifiées, est à zéro, ce qui signifie que chaque étape logique à travers les dix preuves est vérifiée par machine.qz

Les sceptiques répliquent

Malgré la vérification formelle, les critiques ont remis en question le fait que les résultats représentent un véritable bond en avant dans les capacités de l'IA. Gary Marcus, un chercheur en IA renommé, a écrit qu'un mathématicien d'Anthropic, Levent Alpöge, a pu reproduire partiellement la moitié des résultats d'OpenAI en 24 heures en utilisant Fable, un modèle déjà rendu public. Marcus a fait valoir que cela soulève des doutes quant à savoir si Astra est lui-même la percée ou si le progrès réside dans l'identification des problèmes susceptibles d'être résolus par des techniques de recherche et de vérification.garymarcus.substack

"OpenAI ne rapporte pas quels problèmes ils ont essayés et où ils ont échoué. Ils nous ont donné un numérateur sans dénominateur, ce qui est toujours un signe inquiétant", a écrit Marcus. Il a également noté qu'OpenAI n'a pas encore décidé s'il fallait désigner Astra comme GPT-6 ou GPT-5.7, suggérant en interne que le saut pourrait être considéré comme incrémental.garymarcus.substack

Le blog de communication de l'ACM a publié une analyse le 4 août décrivant Astra comme "incroyable, mais largement surestimé". Pendant ce temps, la Déclaration de Leiden sur l'IA en mathématiques, signée par des centaines de mathématiciens en juin 2026, a soulevé des préoccupations plus larges concernant les preuves générées par l'IA peu fiables et l'attribution.analyticsinsight+1

Et ensuite ?

OpenAI n'a pas annoncé de date de sortie pour Astra, et le modèle devra passer l'examen fédéral de sécurité de l'IA avant d'atteindre les utilisateurs. L'entreprise a reconnu le débat, déclarant qu'elle a un "profond respect et une compréhension pour ceux qui sont préoccupés par son impact" et prévoit de publier sa méthodologie. OpenAI a également lancé récemment ChatGPT pour les chercheurs universitaires, offrant à 100 000 scientifiques un accès gratuit à ses derniers modèles.analyticsinsight+1

Le mathématicien Terence Tao, dans une conférence du 26 juillet référencée par Marcus, a établi une distinction entre la résolution de problèmes ouverts isolés, où l'IA semble forte, et la construction de théories mathématiques, où aucune preuve de capacité de l'IA n'existe encore.garymarcus.substack