Présentation des travaux
OpenAI Group PBC a mis en ligne 722 articles de recherche mathématique produits par un modèle d’intelligence artificielle non publié. Les documents, déposés sur GitHub, couvrent environ vingt sous‑domaines des mathématiques, allant de la théorie des nombres à la physique appliquée. Chaque article inclut des fichiers Lean, un langage de preuve assistée par ordinateur, permettant de vérifier automatiquement les démonstrations.
Principaux résultats scientifiques
Parmi les contributions, l’une des plus médiatisées porte sur la hypothèse de Riemann. Le modèle n’a pas résolu la conjecture complète, mais il a démontré le quasi‑Riemann hypothesis, un sous‑ensemble qui affine la compréhension du comportement de la fonction zêta de Riemann. En théorie informatique, plus de 80 papiers ont été générés, dont trois analysent la multiplication de matrices, un opérateur central dans les réseaux de neurones. L’IA a proposé une définition plus précise de la limite théorique de vitesse d’exécution de ces multiplications, suggérant que les gains futurs seront limités par des contraintes matérielles fondamentales.
Un autre article introduit un algorithme inédit de multiplication d’entiers, visant à réduire la complexité asymptotique de l’opération. Bien que le texte ne fournisse pas de borne exacte, il décrit une approche qui combine la décomposition en blocs et l’utilisation de transformations de Fourier discrètes, rappelant les méthodes de Schönhage‑Strassen mais avec une structure de données différente.
Dans le domaine des équations aux dérivées partielles, OpenAI a publié plus d’une dizaine de preuves liées aux PDE. Parmi elles, une version de la conjecture de De Giorgi, pertinente pour la modélisation des alliages métalliques, et plusieurs clarifications concernant les équations de Navier‑Stokes, notamment une preuve partielle d’existence de solutions régulières dans des configurations spécifiques. Ces résultats s’appuient sur des constructions Lean qui permettent de reproduire chaque étape de la démonstration.
Analyse technique et limites
Le recours à Lean garantit une vérifiabilité formelle, mais la lisibilité humaine reste limitée ; les preuves sont souvent plus longues que leurs équivalents traditionnels. De plus, le modèle reste « unreleased », ce qui empêche l’évaluation indépendante de son architecture, de ses données d’entraînement et de ses biais potentiels. Aucun chiffre de performance (temps de génération, consommation GPU) n’est communiqué, ce qui complique l’estimation de la scalabilité du procédé.
Sur le plan algorithmique, la définition de la limite de vitesse pour la multiplication de matrices repose sur des hypothèses de modèle de calcul idéalisé (mémoire infinie, accès constant). En pratique, les architectures modernes (GPU, TPU) introduisent des goulots d’étranglement différents, rendant la transposition directe des résultats incertaine. De même, l’algorithme d’entier proposé n’a pas été comparé à des implémentations existantes telles que l’algorithme de Fürer, ce qui empêche de mesurer son avantage réel.
Perspectives et implications
OpenAI prévoit de publier davantage de fichiers Lean et de financer des événements de revue par les pairs, afin de valider ces découvertes. Si les preuves formelles sont acceptées, elles pourraient accélérer la validation de conjectures complexes et réduire le temps de recherche pure. Toutefois, la dépendance à un modèle propriétaire soulève des questions de reproductibilité et de contrôle de la qualité scientifique. L’équilibre entre automatisation de la preuve et rigueur humaine restera le principal défi à relever.
