OpenAI a une fois de plus mis l'intelligence artificielle sous les projecteurs avec une annonce qui a bouleversé la communauté mathématique. Son dernier modèle, Astra, a résolu dix problèmes ouverts restés irrésolus pendant des décennies, grâce à une méthode permettant la vérification automatique de chaque étape. Il s'agit d'un véritable exploit : des questions qui ont résisté aux efforts des meilleurs spécialistes pendant des années, et qui ont désormais été résolues grâce à un système entraîné à raisonner de manière autonome.
L'entreprise a publié ses résultats dans un recueil de manuscrits comprenant 249 pages d'arguments et de certificats formels générés avec Lean, un logiciel qui vérifie la validité des démonstrations étape par étape. De plus, le coût de calcul de ces résultats s'est avéré étonnamment bas : moins de 2 000 $ en jetons API. Mais que signifie réellement cette avancée ? Assistons-nous à un tournant dans la recherche mathématique, ou devons-nous l'aborder avec prudence ?
Dix problèmes mathématiques vieux de plusieurs décennies résolus
Les résultats couvrent des domaines aussi variés que la géométrie de grande dimension, la théorie du codage, la complexité des circuits arithmétiques, la théorie des groupes, la complexité quantique, la cryptographie sur réseau et la combinatoire extrémale. Parmi les avancées les plus significatives figurent la réfutation de la conjecture de rigidité de Connes , un problème de longue date en algèbre d'opérateurs, et la construction de groupes non sophiques, une question qui préoccupait les spécialistes depuis des années. La borne supérieure de la densité de remplissage des sphères en grande dimension, une limite restée inchangée depuis 1978, a également été améliorée.
De plus, Astra a résolu trois problèmes du catalogue de Paul Erdős, dont le célèbre problème 21 , que le mathématicien Thomas Bloom a qualifié de « plus surprenant de toute la liste ». Au total, ce sont dix problèmes qui étaient restés irrésolus pendant au moins une décennie, et dans la plupart des cas, bien plus longtemps. La communauté mathématique a accueilli la nouvelle avec un mélange d'étonnement et de scepticisme, comme on pouvait s'y attendre.
Vérification automatique avec Lean
Ce qui distingue cette annonce des autres, c'est son processus de vérification. Chaque démonstration a été formalisée dans Lean , un assistant qui vérifie automatiquement chaque étape logique. Les certificats sont disponibles publiquement sur GitHub ; chacun peut les télécharger et exécuter le vérificateur. Si une seule étape est mal interprétée, le logiciel la rejette. Ainsi, il n'est plus nécessaire de se fier à la parole d'OpenAI : la validité des résultats peut être vérifiée indépendamment.
Cette méthode contraste avec la méthode traditionnelle de validation des démonstrations mathématiques, qui exige un processus d'évaluation par les pairs pouvant durer des mois. Avec Lean, la vérification est réduite à quelques minutes. Les chercheurs ont souligné qu'il s'agit de la première fois qu'un système d'IA présente des résultats avec un tel niveau de transparence. Cependant, certains experts, comme Bharath Ramsundar, mettent en garde : « Nous accumulons rapidement une multitude de résultats d'IA potentiellement vrais », et appellent à ce que des mathématiciens examinent ces résultats avant de les intégrer au corpus de connaissances établi.
Le coût et la sélection des problèmes
Un autre détail frappant est le coût. OpenAI affirme que le nombre total de jetons nécessaires pour trouver des solutions à ces problèmes coûterait environ 2 000 $, selon ses frais d'API. Mais ce chiffre ne tient compte que des exécutions réussies, et non des tentatives infructueuses. Comme le souligne un expert : « C'est comme gagner au loto et dire que j'ai dépensé 20 € pour un billet et gagné 20 000 €, sans compter les 5 000 € dépensés en billets précédents. » Le coût réel du processus de découverte est bien plus élevé.
De plus, OpenAI a soigneusement sélectionné les problèmes qu'elle a choisi de publier. On ignore combien de problèmes Astra a tenté de résoudre sans succès. Si elle a retenu 10 réussites sur 1 000 tentatives, l'interprétation est très différente de celle obtenue avec 10 réussites sur 12. Tant que le dénominateur reste inconnu , le « moment Deep Blue des mathématiques » relève davantage du titre que de la conclusion. Malgré tout, les résultats sont vérifiables, ce qui représente une nette amélioration par rapport aux annonces précédentes.
Réactions de la communauté mathématique
Tim Gowers, lauréat de la médaille Fields, a déclaré qu'il aurait vivement recommandé la publication de la démonstration dans une revue mathématique de premier plan. Une équipe de neuf mathématiciens, dont Gowers et Noga Alon, a publié un article complémentaire expliquant la démonstration de manière plus accessible. Thomas Bloom, responsable du catalogue des problèmes d'Erdős, a qualifié ces résultats de « découverte majeure » et a affirmé qu'ils étaient encore plus importants que la solution apportée par Astra à la conjecture de la distance unitaire en mai.
Mais des voix critiques se font également entendre. Gary Marcus , un sceptique notoire en matière d'IA, a qualifié l'annonce d'« incroyable », tout en estimant que son ampleur a été exagérée. Certains experts pensent que seules quelques-unes des dix démonstrations seront véritablement stupéfiantes, tandis que les autres abordent des problèmes que la communauté aurait pu résoudre, même si personne ne s'en était soucié. Malgré ces critiques, la vérifiabilité automatique des résultats constitue une différence fondamentale par rapport aux autres annonces concernant l'IA.
En résumé, l'annonce d'OpenAI concernant Astra marque une étape importante dans l'application de l'intelligence artificielle à la recherche mathématique. Pour la première fois, un système d'IA a résolu des problèmes ouverts de longue date et fourni des preuves vérifiables par machine. Bien que des questions subsistent quant au choix des problèmes et au coût réel, la transparence du processus et la possibilité de vérifier chaque étape ouvrent la voie à une nouvelle ère où l'IA collaborera avec les mathématiciens. La communauté scientifique devra s'adapter à cette nouvelle réalité, mais une chose est sûre : la frontière de la connaissance a bougé, et Astra est l'outil qui a rendu cela possible.
