OpenAI publie 722 textes de maths écrits par une IA, à vérifier

Ce qu’OpenAI a publié, et comment

Mardi 6 octobre, OpenAI a publié d’un coup 722 textes de mathématiques de recherche, regroupés en 372 familles de résultats. Ils sont écrits presque entièrement par un modèle interne non public. Tout est déposé dans un dépôt public sur GitHub, sous licence libre Apache-2.0.

Le dépôt contient les textes en PDF, des preuves écrites en Lean et des résumés du raisonnement du modèle pour 10 familles. OpenAI présente l’ensemble comme une évaluation : ses tests de maths habituels étant saturés, il est passé à de vrais problèmes de recherche encore ouverts.

D’après le dépôt, environ 4 000 problèmes ont été posés au modèle, avec pour chaque résultat, en moyenne, l’équivalent de 3 h de réflexion de ChatGPT Pro. Selon un porte-parole d’OpenAI cité par Scientific American, presque tout est sorti d’une seule consigne donnée à un seul agent ; certains résultats ont demandé plusieurs essais.

Ce qui est prouvé, et ce qui reste à vérifier

Selon Scientific American, OpenAI met en avant une solution de la conjecture de Kakeya en dimension 4, des améliorations d’algorithmes informatiques importants et des progrès vers l’hypothèse de Riemann. Ce sont des affirmations d’OpenAI, pas encore vérifiées par la communauté. Et 722 textes ne font pas 722 grands problèmes résolus.

Le point clé, c’est Lean, un langage qui vérifie la logique d’une preuve, comme le rappelle Scientific American. Tous les textes ne sont pas passés par là. Le README du dépôt le dit lui-même : certains résultats non formalisés peuvent contenir des erreurs.

Le lendemain, mercredi 7 octobre, le journal du dépôt a enregistré trois retraits. Une erreur de signe dans un texte sur les « classes de Weil » invalidait un argument clé, et deux autres textes reposaient dessus. Quatorze autres ont été corrigés.

Dave Goldblatt a relancé de son côté la vérification Lean d’un résultat sur la fonction zêta de Riemann, avec deux vérificateurs indépendants : les deux acceptent la preuve. Il en donne les limites : une seule vérification, menée par l’agent Claude Code sur une seule machine, pas encore refaite par d’autres, et seule la preuve Lean a été contrôlée, pas le texte.

Les mathématiciens divisés sur la méthode

Le 29 septembre, le groupe consultatif sur les mathématiques et l’IA (AGMAI) avait publié ses recommandations, après plus de 600 réponses de la communauté mathématique. Il demande aux labos d’arrêter de tester des problèmes avancés sur des modèles fermés, et de publier modèle, consignes, temps, coût et échecs. Selon Scientific American, OpenAI ne publie que le temps de calcul moyen et quelques statistiques, et n’est pas tenu par ces recommandations.

Le 6 octobre, le même groupe a jugé la publication importante pour les mathématiques, sans approuver pour autant la méthode d’OpenAI. Andrew Sutherland (MIT) veut voir le modèle publié et les résultats reproduits avant d’y croire. Daniel Litt (Université de Toronto), lui, ne voit pas pourquoi on demanderait à l’entreprise de garder ces résultats secrets. L’Association for Human Mathematics y voit une démonstration de pouvoir plutôt que de travail savant, et appelle les mathématiciens à cesser de travailler avec OpenAI.

Rénald Vie y consacre sa vidéo du samedi 10 octobre, « Ce que cette IA vient d’écrire va changer la science ».

Ce que ça change pour toi

Ce dossier dit deux choses utiles. D’abord, OpenAI mesure désormais les progrès de ses modèles sur des problèmes de recherche encore ouverts : selon Scientific American, l’entreprise y voit un test clé pour savoir si son IA s’améliore.

Ensuite, c’est une leçon pour ton propre usage. Trois textes ont pourtant été retirés dès le lendemain, à cause d’une seule erreur de signe. Dans ton travail aussi, une analyse produite par l’IA vaut ce que vaut ta vérification.

La nuance à garder

La production ne se refait pas de l’extérieur. Le modèle n’est pas public et les consignes non plus : seules les preuves Lean se contrôlent de l’extérieur. Au 7 octobre, environ 42 % des résultats principaux étaient formalisés ; pour les autres, rien n’est vérifié par Lean.

Le chiffre de 722 ne mesure pas l’importance. Juger ce qui est vraiment nouveau prendra des mois, selon Scientific American.

Les chiffres bougent. Le dépôt évolue : ceux de cet article datent de sa mise à jour du 7 octobre.