Le prochain modèle d’OpenAI, Astra, vient de résoudre dix problèmes ouverts de mathématiques vieux de plusieurs décennies

Le 1er août, OpenAI a publié un rapport affirmant que son prochain modèle, appelé en interne Astra, avait obtenu de nouveaux résultats sur dix problèmes ouverts distincts en mathématiques. (Non, il ne s’agit pas des problèmes du prix du millénaire, mais ils sont tout de même significatifs.)

À noter : ces solutions ne sont pas de simples avancées progressives. Ce sont de véritables résolutions, vérifiées avec Lean. (Lean est un langage et un assistant de preuve qui impose d’expliciter chaque étape d’un raisonnement mathématique de manière lisible par machine.) 

C’est beaucoup à digérer d’un coup. Dans cet article, j’ai regroupé les problèmes par domaine et j’explique, à haut niveau, ce qui s’est passé, ce que cela peut impliquer pour les mathématiques, et ce que l’on peut en déduire sur Astra.

Quels sont les dix problèmes ?

Voici chaque résultat, en termes simples, avec le domaine précis des mathématiques ou de l’informatique théorique auquel il se rattache.

Groupes non sofiques

Domaine : théorie des groupes

Astra a produit une construction explicite d’un groupe qui ne peut en aucun cas être approché, même de très près, par de grandes structures finies — clôturant une question ouverte depuis l’introduction du concept de groupe «\u00a0sofique\u00a0» en 1999. La construction s’accompagne d’une preuve qu’aucune suite d’approximations finies ne peut fonctionner, formalisée dans Lean afin que la logique soit vérifiable automatiquement.

Wikipédia a déjà été mis à jour\u00a0:

Empilement de sphères

Domaine : géométrie en grande dimension

La question est de savoir à quelle densité on peut empaqueter des sphères identiques et non superposées lorsque le nombre de dimensions augmente. Astra a établi un plafond plus strict sur cette densité en haute dimension, première amélioration de cette borne particulière depuis 1978. Il ne fournit pas une meilleure méthode d’empaquetage — il resserre la limite de ce que toute méthode future pourrait atteindre au mieux.

Codes binaires et sphériques

Domaine : théorie du codage

Les codes correcteurs d’erreurs fonctionnent en espaçant suffisamment les messages valides pour que de petites erreurs ne transforment pas l’un en l’autre. Astra a établi des limites nettement plus serrées (améliorées de façon exponentielle) sur le nombre de messages possibles pour une distance minimale donnée, avec un résultat analogue pour des points répartis sur une sphère de grande dimension.

Conjecture de rigidité de Connes

Domaine : algèbres d’opérateurs

Alain Connes a conjecturé que certains groupes pouvaient toujours être reconstruits de manière unique à partir d’une structure algébrique, appelée algèbre de von Neumann, construite à partir d’eux. Astra a réfuté cela en produisant deux groupes réellement différents donnant lieu à la même algèbre, montrant que la reconstruction n’est pas toujours bijective.

Complexité des circuits arithmétiques

Domaine : théorie de la complexité

Le «\u00a0permanent\u00a0», un nombre calculé à partir d’une grille de nombres, est coûteux à évaluer, et les théoriciens de la complexité cherchent le nombre minimal d’opérations arithmétiques qu’une méthode pourrait nécessiter. Astra a établi une nouvelle borne inférieure, plus forte, sur ce minimum — un type de résultat notoirement difficile à faire progresser.

Répétition parallèle quantique

Domaine : théorie de la complexité quantique

La théorie classique dit que forcer deux joueurs non communicants à répéter en parallèle un jeu difficile rend la triche exponentiellement moins susceptible de réussir. Astra a démontré que cette garantie tient même lorsque les joueurs partagent un état d’intrication quantique, prolongeant un principe classique fondamental au cadre quantique.

Problème du vecteur le plus proche

Domaine : cryptographie sur réseaux

Étant donné un réseau (une grille de points) et une cible, le problème consiste à trouver le point du réseau le plus proche — un problème réputé très difficile en grande dimension, raison pour laquelle il sous-tend certains schémas de chiffrement résistants au quantique. Astra a prouvé que même approximer la réponse, à un certain facteur polynomial près, reste démontrablement difficile, consolidant la cryptographie qui s’appuie dessus.

Conjecture de volume d’Ehrhart

Domaine : géométrie discrète et convexe

Pour une forme convexe dont l’unique point de réseau intérieur se situe exactement au centre de gravité, les mathématiciens voulaient connaître le plus grand volume possible en toute dimension. Astra a déterminé ce volume maximal pour chaque dimension, résolvant la conjecture dans toute sa généralité.

Nombres de Ramsey multicolores

Domaine : théorie de Ramsey / combinatoire

Avec suffisamment de personnes et de catégories de relation entre elles, on finit forcément par trouver trois personnes toutes reliées par la même catégorie. Astra a démontré que la taille minimale du groupe nécessaire croît plus vite que toute vitesse exponentielle fixe lorsque le nombre de catégories augmente, résolvant le problème 183 d’Erdős.

Conjectures en théorie extrémale des graphes

Domaine : théorie extrémale des graphes

Ce domaine étudie combien de connexions un réseau peut avoir tout en évitant certains petits motifs interdits. Astra a résolu deux conjectures liées, correspondant aux problèmes 146 et 180 d’Erdős, en précisant jusqu’à quelle densité ces réseaux peuvent aller avant que ces motifs ne deviennent inévitables.

Chacune de ces questions était ouverte depuis au moins dix ans ; plusieurs tenaient depuis trente ans ou plus, y compris des problèmes travaillés par des lauréats du prix Turing du côté informatique théorique.

Un contre-exemple, est-ce la \"voie facile\" pour prouver ?

Qui suis-je pour émettre une réserve ici, mais je sais que c’est une question fréquente, notamment chez celles et ceux qui ont quelques bases en maths.

La remarque la plus courante, en guise de critique : plusieurs de ces résultats sont des contre-exemples plutôt qu’une nouvelle théorie générale. C’est important, car un contre-exemple répond à une question oui/non sans, à lui seul, expliquer pourquoi le schéma se brise ni fournir d’emblée une famille d’objets analogues à étudier, alors qu’un théorème de classification ou une nouvelle technique ouvrent davantage de portes.

Je dirais que cette critique tient en général, mais elle ne permet pas d’écarter en bloc toute cette série de résultats. Premièrement, le résultat sur les groupes non sofiques n’est pas une petite retouche d’une quasi-réussite existante — c’est la première construction de ce type après 27 ans sans aucune, et la technique employée devrait se généraliser pour en trouver d’autres.

Deuxièmement, plusieurs des neuf autres résultats, dont la borne d’empaquetage de sphères et la dureté du CVP, ne sont pas des contre-exemples du tout ; ce sont des améliorations directes de bornes connues. 

Ce qui reste en suspens

Plusieurs points seront à suivre à mesure que la communauté passera ces travaux au crible dans les prochains jours, semaines et mois\u00a0:

\n
• Pas encore d’évaluation par les pairs. Les preuves sont vérifiées par Lean et ont été relues de manière informelle par des mathématiciens ayant vu les prépublications, mais aucune n’a encore suivi un processus de revue par un journal à comité de lecture. 
\n
• La question de l’attribution est encore en discussion. OpenAI dit assumer la responsabilité des manuscrits et des formalisations Lean, tout en attribuant les arguments mathématiques eux-mêmes au modèle. La reproduction indépendante du processus (par opposition à la vérification des preuves) est difficile à mener pour l’instant.
\n

Ce que cela signifie pour les mathématiques

Le changement le plus immédiat concerne ce à quoi les mathématiciens consacreront réellement leur temps. Si l’on peut confier un problème ouvert bien posé à un modèle et le faire vérifier dans Lean, le goulot d’étranglement passe de «\u00a0quelqu’un peut-il le résoudre\u00a0» à «\u00a0avons-nous posé la bonne question et l’avons-nous correctement formalisée\u00a0». Savoir formuler une bonne question et choisir celles qui valent la peine d’être attaquées est une vraie compétence, acquise par l’expérience. 

Il y a aussi une question de financement et de reconnaissance. Les subventions de recherche, les titularisations et les prix se sont historiquement fondés sur la rareté : ces problèmes étaient assez difficiles pour que les résoudre en dise long sur la personne qui y parvenait. Si les résultats assistés par l’IA deviennent routiniers, la discipline devra trouver de nouveaux moyens d’indiquer ce qui est réellement ardu par rapport à ce qui devient accessible pour quelques milliers de dollars d’inférence. Bien sûr, le grand public ne comprend pas pleinement ces problèmes. Les personnes formées, elles, comprennent — et cela ne change pas. Le savoir mathématique n’en devient que plus précieux. 

Comment les gens réagissent

Sur les réseaux sociaux, le débat porte moins sur la validité des preuves que sur ce qu’elles indiquent réellement.

Certaines personnes voient dans le rythme la vraie histoire : dix problèmes anciens résolus d’un coup, dans des domaines sans lien, plus vite que les experts ne peuvent les relire. Une question pour la suite\u00a0: «\u00a0Parviendrons-nous à suivre pour tout vérifier\u00a0?\u00a0»

D’autres rétorquent que cela en dit moins sur l’IA en général qu’on pourrait le croire. Les maths sont un domaine rare où le travail d’un modèle peut être vérifié automatiquement et de manière exhaustive. La plupart des problèmes du monde réel n’offrent pas une telle «\u00a0grille de correction\u00a0» intégrée. Sous cet angle, la performance est bien réelle, mais elle dirait surtout que les maths se prêtent particulièrement bien à l’IA.

Troisième angle de commentaire : une preuve correcte que personne n’a encore entièrement audité ou assimilé n’a pas vraiment été comprise, seulement vérifiée. Découvrir un théorème et comprendre ce qu’il signifie sont, dans cette optique, deux métiers différents.

Dernières réflexions

Les mathématiciens estiment que le résultat sur les groupes non sofiques est du solide : une véritable question ouverte de longue date en théorie des groupes, close par une construction explicite que les spécialistes prennent au sérieux. Les neuf autres résultats, pris ensemble, constituent un ensemble large et techniquement substantiel de progrès en mathématiques pures.

Ce qui n’a pas encore eu lieu, c’est la partie plus lente : l’évaluation par les pairs, la reproduction du processus de recherche et l’appropriation de ces résultats par la communauté. Cela prend plus de temps qu’un article de blog, et c’est ce qui nous dira réellement l’ampleur de cette avancée. Nous vous tiendrons au courant.