Dix résultats qui auraient mobilisé des carrières entières, condensés dans un manuscrit de 249 pages et formalisés par machine. OpenAI affirme que son futur modèle Astra a attaqué dix problèmes majeurs de mathématiques et d’informatique théorique pour environ 2 000 dollars de jetons. Le chiffre est explosif. La validation scientifique, elle, ne fait que commencer.
Astra attaque dix forteresses mathématiques d’un seul coup
Le 1er août 2026, OpenAI a publié dix résultats produits par une version interne d’Astra, présenté comme son prochain grand modèle. La liste traverse la géométrie en haute dimension, la théorie des groupes, la cryptographie sur réseaux, la complexité quantique et la combinatoire. Ce n’est plus un chatbot qui termine un exercice : c’est une IA qui entre dans plusieurs laboratoires en même temps.
Certains résultats ferment réellement des dossiers anciens. Astra aurait construit le premier groupe non sofique explicite, réfuté la conjecture de rigidité de Connes, prouvé la conjecture de volume d’Ehrhart et résolu trois problèmes d’Erdős. Sur l’empilement de sphères, le modèle annonce aussi la première amélioration générale depuis 1978. Deux mois après la réfutation d’une conjecture d’Erdős vieille de 80 ans, l’accélération ressemble à un changement de régime.
Sébastien Bubeck, chercheur chez OpenAI, a mis en avant le résultat sur les groupes non sofiques. Son message révèle l’ambition réelle : Astra n’est plus présenté comme un assistant, mais comme l’auteur intellectuel des arguments.
2 000 dollars pour faire trembler des décennies de recherche
OpenAI estime que les jetons nécessaires pour trouver les dix solutions auraient coûté environ 2 000 dollars aux tarifs de son API Sol. Une partie de la recherche mathématique de très haut niveau commence donc à afficher un prix comparable à celui d’un ordinateur, pas d’un programme pluriannuel. Le coût marginal de la découverte pourrait s’effondrer.
Mais ce montant ne couvre ni l’entraînement d’Astra, ni l’infrastructure, ni le travail humain sur les manuscrits. La publication ne précise pas combien de problèmes ont échoué avant la sélection finale. Il s’agit d’un coût marginal annoncé par OpenAI, pas de la facture complète. Même avec cette astérisque, le signal envoyé aux universités est brutal. Cette limite a également été relevée par l’analyste Simon Willison.
Avec Lean, les hallucinations ne passent plus
Pour éviter le classique « faites-nous confiance », OpenAI a publié dix certificats dans Lean 4, un assistant qui vérifie mécaniquement chaque étape formalisée. Le dépôt GitHub contient un fichier par résultat et permet de reconstruire l’ensemble avec Lean 4.32.0 et Mathlib. Une hallucination bien rédigée ne suffit plus : le système doit compiler.
Cette vérification n’élimine pas le jugement humain. Lean confirme qu’une conclusion suit des hypothèses encodées, mais des spécialistes doivent vérifier que l’énoncé correspond au problème historique et que la démonstration apporte une compréhension utile. La machine verrouille la logique ; elle ne décide pas seule de la portée scientifique.
Cette présentation de l’École polytechnique montre comment Lean et Mathlib transforment une démonstration en objet vérifiable. Elle explique pourquoi les certificats comptent presque autant que les 249 pages du manuscrit.
Les mathématiciens refusent de laisser OpenAI se corriger seul
La Déclaration de Leiden sur l’IA et les mathématiques, soutenue par l’Union mathématique internationale, exige des publications évaluées par les pairs, des descriptions humaines et une vérification formelle lorsque c’est pertinent. Elle avertit aussi contre l’intérêt commercial des entreprises à gonfler leurs performances. Le communiqué de presse ne peut pas devenir le nouveau comité de lecture.
OpenAI a reconnu cette fracture. L’entreprise affirme qu’attribuer à des humains des arguments entièrement générés par une IA serait trompeur, tout en assumant la préparation des manuscrits. Qui signe alors un théorème lorsque la découverte vient du modèle, la rédaction d’une équipe et la validation d’un compilateur ?
Le mathématicien Thomas Bloom, spécialiste des problèmes d’Erdős, a estimé que certains résultats dépassaient la précédente percée sur les distances unitaires. Son enthousiasme ne remplace pas l’examen indépendant, mais il interdit déjà de balayer l’annonce comme une simple démonstration marketing.
L’IA écrit déjà plus vite que les chercheurs ne peuvent relire
OpenAI prévoit parallèlement d’offrir ses meilleurs modèles à 100 000 scientifiques et mathématiciens. Après les IA médaillées aux Olympiades et les travaux où les LLM produisaient des idées jugées plus novatrices que celles de chercheurs, Astra pousse la logique jusqu’au laboratoire semi-autonome : lire, tenter, formaliser, recommencer.
La conséquence n’est pas la disparition immédiate des mathématiciens. C’est une avalanche potentielle de résultats que trop peu d’experts auront le temps de relire, contextualiser et transmettre. Si Astra tient ses promesses, le problème ne sera bientôt plus de trouver une preuve. Ce sera de décider lesquelles méritent encore l’attention humaine.
- Partager l'article :
