Dix avancées en mathématiques et en informatique théorique

Nous voulons donner aux scientifiques et aux mathématiciens des outils qui accélèrent les découvertes. C’est pourquoi nous avons récemment annoncé ChatGPT pour les chercheurs universitaires⁠, une initiative offrant à 100 000 scientifiques et mathématiciens un accès gratuit à nos meilleurs modèles ChatGPT. Nous continuons également à évaluer nos modèles sur des problèmes de recherche ouverts pendant leur développement.

En mai, nous avons présenté une réfutation générée par l’IA⁠ de la conjecture d’Erdős sur les distances unitaires, découverte lors de l’évaluation d’un modèle non publié. Ces travaux ont déjà inspiré de nouvelles avancées en mathématiques et en informatique théorique¹. Aujourd’hui, nous présentons une sélection de dix résultats, dont chacun résout un problème ouvert de longue date ou permet d’y accomplir des progrès substantiels. Ces problèmes relèvent de la géométrie en grande dimension, de la théorie des codes, de la complexité des circuits arithmétiques, de la théorie des groupes, des algèbres d’opérateurs, de la complexité quantique, de la cryptographie sur réseaux et de la combinatoire extrémale. Tous ces problèmes présentent un intérêt majeur pour leurs communautés mathématiques respectives, et plusieurs intéressent largement l’ensemble des mathématiques.

Nous présentons de nouveaux résultats pour les problèmes suivants. Les résultats ont été obtenus par une version interne d’Astra, notre prochain modèle majeur. Le nombre total de jetons nécessaires pour trouver les solutions à ces problèmes coûterait environ 2 000 $ aux tarifs de l’API Sol. Ces arguments ont ensuite été mis en forme sous forme de manuscrits par des humains à l’aide du même modèle. Le modèle a ensuite formalisé chaque argument dans un certificat Lean⁠(ouverture dans une nouvelle fenêtre). Nous publions également, pour chaque solution, un récit par le modèle de son processus de réflexion.

1. Empilement de sphères en grande dimension. Nouvelles bornes supérieures sur la densité d’empilement de sphères jusqu’au seuil de Cohn–Elkies.
2. Codes binaires et sphériques : bornes améliorées exponentiellement sur la taille maximale des codes binaires pour toute distance minimale prescrite, avec des résultats analogues pour les codes sphériques en grande dimension.
3. Groupes non sofiques. Une construction établissant l’existence de groupes non sofiques et répondant à une question ouverte centrale de la théorie des groupes.
4. Conjecture de rigidité de Connes. Réfutation d’une conjecture ancienne selon laquelle certains groupes sont déterminés de manière unique par leurs algèbres de von Neumann.
5. Complexité des circuits arithmétiques. Nouvelles bornes inférieures pour le calcul du permanent au moyen de circuits et de formules arithmétiques, notamment une borne inférieure d’ordre n⁴/log n pour les formules arithmétiques.
6. Répétition parallèle quantique. Un théorème de répétition parallèle exponentielle pour les jeux quantiques généraux à deux joueurs, qui étend un principe fondamental de la théorie classique de la complexité.
7. Problème du vecteur le plus proche. Difficulté d’approximation à un facteur polynomial pour le problème du vecteur le plus proche, une question fondamentale sur les réseaux liée à la cryptographie postquantique.
8. Conjecture d’Ehrhart sur le volume. Détermination, dans chaque dimension, du volume maximal possible d’un corps convexe dont le centroïde est l’unique point intérieur du réseau.
9. Nombres de Ramsey multicolores. Une borne inférieure superexponentielle pour les nombres de Ramsey multicolores des triangles, résolvant le problème 183 d’Erdős.
10. Conjectures sur les nombres extrémaux. Résultats sur les conjectures de compacité et de dégénérescence en théorie extrémale des graphes, résolvant les problèmes 146 et 180 d’Erdős.

L’émergence de systèmes capables de contribuer à la recherche mathématique soulève des questions auxquelles une entreprise technologique ne peut répondre seule. Les avis sur le rôle de l’IA en mathématiques sont nombreux, et nous respectons et comprenons profondément les personnes préoccupées par ses répercussions, notamment les signataires de la Déclaration de Leiden sur l’IA et les mathématiques⁠(ouverture dans une nouvelle fenêtre). Nous estimons que l’attribution doit refléter honnêtement la manière dont un résultat a été produit : revendiquer la paternité humaine d’une preuve entièrement générée par un système d’IA dénaturerait à la fois la contribution du système et la nature du véritable travail intellectuel humain. Nous avons contribué à préparer les manuscrits et à formaliser les preuves dans Lean, et nous assumons la responsabilité de leur exactitude, tandis que les arguments mathématiques eux-mêmes ont été générés par notre système. Nous espérons que la communauté mathématique examinera ces résultats en profondeur, les replacera dans leur contexte et donnera vie aux idées qui les sous-tendent grâce à de nouvelles recherches et découvertes.

À mesure que les systèmes d’IA deviennent des collaborateurs de recherche plus sophistiqués, garantir un large accès est essentiel pour soutenir les scientifiques et les mathématiciens tandis qu’ils explorent et définissent l’avenir de leurs disciplines en cette période de transformation.