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 qui offre à 100 000 scientifiques et mathématiciens un accès gratuit à nos meilleurs modèles ChatGPT. Nous continuons également d’évaluer nos modèles sur des problèmes de recherche ouverts pendant leur développement.

En mai, nous avons présenté une réfutation produite par l’IA⁠ de la conjecture d’Erdős sur les distances unitaires, découverte lors de l’évaluation d’un modèle inédit. Ces travaux ont déjà inspiré d’autres 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 réaliser des progrès considérables. Ces problèmes couvrent la géométrie en grande dimension, la théorie des codes, la complexité des circuits arithmétiques, la théorie des groupes, les algèbres d’opérateurs, la complexité quantique, la cryptographie sur réseaux euclidiens et la combinatoire extrémale. Tous ces problèmes présentent un intérêt considérable pour leurs communautés mathématiques respectives, et plusieurs intéressent l’ensemble du domaine 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 tokens nécessaires pour trouver des solutions à ces problèmes coûterait environ 2 000 $ aux tarifs de l’API Sol. Ces arguments ont ensuite été transformés en articles par des humains à l’aide du même modèle. Le modèle a ensuite formalisé chaque argument dans un certificat Lean⁠(s'ouvre dans une nouvelle fenêtre). Nous publions également, pour chaque solution, le récit par un modèle de son processus de réflexion.

1. Empilement de sphères en grande dimension. Nouvelles bornes supérieures de la densité d’empilement de sphères jusqu’au seuil de Cohn–Elkies.
2. Codes binaires et sphériques : bornes améliorées de façon exponentielle 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 de longue date selon laquelle certains groupes sont uniquement déterminés par leurs algèbres de von Neumann.
5. Complexité des circuits arithmétiques. Nouvelles bornes inférieures pour le calcul du permanent à l’aide de circuits et de formules arithmétiques, dont 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 à facteur polynomial pour le problème du vecteur le plus proche, une question fondamentale sur les réseaux euclidiens 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 son seul 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 opinions sur le rôle de l’IA en mathématiques sont nombreuses, 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⁠(s'ouvre dans une nouvelle fenêtre). Nous croyons que l’attribution doit refléter honnêtement la façon 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 étudiera ces résultats en profondeur, les situera 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 évoluent pour devenir des collaborateurs de recherche plus évolués, assurer un accès généralisé est essentiel pour soutenir les scientifiques et les mathématiciens tandis qu’ils explorent et définissent l’avenir de leurs disciplines durant cette ère transformatrice.