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

Le 1er août, OpenAI a publié un rapport affirmant que son prochain modèle, nommé en interne Astra (pas encore disponible), avait produit de nouveaux résultats sur dix problèmes ouverts en mathématiques. (Non, il ne s’agit pas des problèmes du prix du millénaire, mais ils restent majeurs.)

Point notable : ces solutions ne sont pas de simples avancées incrémentales. Ce sont de véritables résolutions, vérifiées avec Lean. (Lean est un langage de programmation et un assistant de preuve qui oblige à expliciter chaque étape d’un raisonnement mathématique dans un formalisme lisible par machine.) 

C’est beaucoup d’informations d’un coup. Dans cet article, j’ai classé les problèmes par domaine et décrit à haut niveau ce qui s’est passé, ce que cela peut impliquer pour la discipline, 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 spécifique de mathématiques ou d’informatique théorique auquel il appartient.

Groupes non sofiques

Domaine : Théorie des groupes

Astra a produit une construction explicite d’un groupe qui ne peut être approché, quelle que soit la précision, par de grandes structures finies — clôturant une question ouverte depuis l’introduction du concept de groupe \"sofitique\" en 1999. La construction s’accompagne d’une preuve qu’aucune suite d’approximations finies ne peut fonctionner, formalisée dans Lean pour un contrôle mécanique de la logique.

La page Wikipedia a déjà été mise à jour :

Empilement de sphères

Domaine : Géométrie en grande dimension

La question porte sur la densité maximale d’empilement de sphères identiques non chevauchantes lorsque la dimension augmente. Astra a établi un plafond plus serré sur cette densité en haute dimension, première amélioration de cette borne particulière depuis 1978. Cela ne fournit pas une meilleure méthode d’empilement — cela resserre la limite sur ce que toute méthode future pourra atteindre.

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 puissent pas transformer l’un en l’autre. Astra a démontré des limites nettement plus serrées (amélioration 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é cette conjecture en produisant deux groupes réellement distincts donnant naissance à 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 \"permanent\", 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 à améliorer.

Répétition parallèle quantique

Domaine : Complexité quantique

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

Problème du vecteur le plus proche

Domaine : Cryptographie sur réseaux

Étant donné une grille de points répétée (un réseau) et une cible, le problème consiste à trouver le point de la grille le plus proche — un problème réputé très difficile en grande dimension, raison pour laquelle il sous-tend certains chiffrement résistants au quantique. Astra a prouvé que même l’approximation de la réponse, dans un certain facteur polynomial, reste démontrablement difficile, renforçant 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 intérieur du réseau se situe exactement au centre de masse, les mathématiciens voulaient connaître le volume maximal possible en toute dimension. Astra a déterminé ce volume maximum pour chaque dimension, tranchant la conjecture dans sa pleine 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 inévitablement par trouver trois personnes toutes liées par la même catégorie. Astra a montré que la taille minimale du groupe nécessaire croît plus vite que tout taux exponentiel fixé à mesure que 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

Cette branche des maths s’intéresse au nombre de connexions qu’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 à quel point de tels réseaux peuvent être denses avant que ces motifs ne deviennent inévitables.

Chacun de ces problèmes était ouvert 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 côté informatique théorique.

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

Qui suis-je pour émettre une réserve ici, mais je sais que c’est une question ou réaction fréquente, surtout chez celles et ceux qui connaissent un peu les 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 par oui/non sans expliquer, à lui seul, pourquoi le schéma se brise ni fournir une famille d’objets similaires à é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 disqualifie pas en bloc toute cette série de problèmes. Premièrement, le résultat sur les groupes non sofiques n’est pas une petite retouche d’un quasi-exemple existant — c’est la première construction du genre après 27 ans sans aucun exemple, 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 sur l’empilement de sphères et la difficulté du CVP, ne sont pas des contre-exemples du tout ; ce sont des améliorations directes de bornes connues. 

Ce qui reste en suspens

Quelques points à suivre au fil de l’examen par la communauté dans les prochains jours, semaines et mois :

\n
• Pas encore d’évaluation par les pairs. Les preuves sont vérifiées par Lean et ont été relues de façon informelle par des mathématiciens ayant vu les prépublications, mais aucune n’a encore été publiée dans une revue à comité de lecture. 
\n
• La paternité 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 réplication indépendante du processus (par opposition à la vérification des preuves) est difficile à réaliser pour l’instant.
\n

Ce que cela signifie pour les mathématiques

Le changement le plus immédiat concerne ce à quoi les mathématiciens vont réellement consacrer leur temps. Si un problème bien posé peut être confié à un modèle et vérifié dans Lean, le goulot d’étranglement passe de \"quelqu’un peut-il résoudre cela\" à \"avons-nous posé la bonne question et bien formalisé le problème\". Savoir poser une bonne question et choisir celles qui valent l’effort est une véritable compétence qui s’acquiert avec l’expérience. 

Se pose aussi une question de financement et de reconnaissance. Les subventions, titularisations et prix ont historiquement été construits autour de la rareté : ces problèmes étaient suffisamment difficiles pour que les résoudre dise quelque chose de la personne qui y parvient. Si les résultats assistés par l’IA deviennent courants, la discipline devra trouver de nouveaux moyens d’indiquer ce qui est réellement difficile par rapport à ce qui devient accessible avec 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. La connaissance en mathématiques n’a jamais été aussi précieuse. 

Comment les gens réagissent

Sur les réseaux sociaux, les réactions portent moins sur la validité des preuves que sur ce qu’elles révèlent.

Certaines voient dans le rythme la véritable 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 l’avenir : \"Pourra-t-on suivre le rythme de vérification de tout cela ?\"

D’autres rétorquent que cela en dit moins sur l’IA en général qu’on ne l’imagine. Les maths sont un domaine rare où le travail d’un modèle peut être vérifié automatiquement et complètement. La plupart des problèmes réels n’offrent pas une telle clé de correction automatique intégrée. Dans cette optique, l’exploit est réel, mais souligne surtout que les mathématiques se prêtent particulièrement bien à l’IA.

Troisième angle des commentaires : une preuve correcte que personne n’a encore entièrement auditée ou assimilée n’a pas vraiment été comprise, seulement vérifiée. Découvrir un théorème et en comprendre la portée sont, dans cette perspective, deux tâches différentes.

Dernières réflexions

Des mathématiciens affirment que le résultat sur les groupes non sofiques ressemble au \"vrai\": une question ouverte de longue date en théorie des groupes, close par une construction explicite que la communauté prend au sérieux. Les neuf autres résultats, pris ensemble, représentent 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 réplication du processus de recherche et l’appropriation de ces résultats par la communauté. Cette étape prend plus de temps qu’un billet de blog, et c’est elle qui dira vraiment l’ampleur de ce qui s’est passé. Nous vous tiendrons au courant.