OpenAI publie sur GitHub 722 travaux de mathématiques rédigés par un modèle non publié

Il y a quelques jours, OpenAI a publié sur GitHub 722 travaux mathématiques générés par un modèle frontier interne, pas encore sorti. Les sujets : théorie des nombres, géométrie algébrique, analyse, combinatoire. Une partie des résultats s'accompagne de preuves formelles en Lean. Le média chinois Jiqizhixin en tire une conclusion tranchée : l'IA a commencé à produire de nouvelles mathématiques plus vite que les mathématiciens ne peuvent les comprendre, et la communauté aura besoin de plusieurs années pour digérer le tout.

Ce qui a été publié exactement

C'est l'ampleur qui frappe. Plus de sept cents travaux d'un seul coup, dans plusieurs branches des mathématiques à la fois. Un tel volume s'accumule d'ordinaire sur des années, avec des dizaines d'auteurs.

Le fragment de matériel disponible s'interrompt à la description du dépôt. Plusieurs détails importants restent donc inconnus : l'organisation des fichiers, la licence des textes, le nombre de personnes ayant participé à la sélection, la relecture ou non des travaux par des pairs. OpenAI n'a pas publié le modèle lui-même, et il est impossible de reproduire le résultat de l'extérieur.

• 722 travaux dans un dépôt public sur GitHub
• Source : un modèle interne d'OpenAI, non publié
• Domaines : théorie des nombres, géométrie algébrique, analyse, combinatoire
• Une partie des travaux bénéficie d'une vérification formelle en Lean
• Statut de l'expertise indépendante : non précisé dans le matériel disponible

Le goulot d'étranglement s'est déplacé vers la vérification

Lean joue ici le rôle de garde-fou. Dans ce système de preuve, un compilateur vérifie chaque étape. Si la preuve compile, elle ne contient aucune faille logique. Mais certaines questions restent hors de portée de la machine. L'énoncé formalisé est-il bien celui que revendique l'article ? Le résultat est-il intéressant, ou simplement un corollaire secondaire d'un résultat connu ? S'inscrit-il dans une ligne de recherche active ?

Pour les travaux sans formalisation, la situation est pire. Un humain doit les lire, et la relecture d'un seul article complexe prend des semaines, parfois des mois. Avec 722 textes, cette file d'attente devient un problème qu'on ne règle pas en embauchant deux ou trois relecteurs de plus.

La seconde moitié du titre de Jiqizhixin affirme que les mathématiciens ont « perdu leurs projets de recherche ». Le mécanisme est simple. Si le modèle résout un problème sur lequel un doctorant comptait travailler pendant un an et demi, le sujet perd sa valeur avant même la soutenance. C'est l'appréciation du média, pas un fait confirmé sur des personnes précises, mais la logique se tient. Les plus exposés sont ceux qui travaillent sur des problèmes techniques et facilement formalisables.

Comment s'y adapter

Les mathématiciens ont intérêt à comparer leurs sujets en cours avec le dépôt. Mieux vaut repérer les recoupements maintenant qu'après l'envoi d'un preprint. Il est aussi utile d'apprendre Lean, ne serait-ce qu'à un niveau de lecture : savoir vérifier rapidement la formalisation d'un tiers devient une compétence de travail.

Les revues et les plateformes de type arXiv devront définir une politique. Faut-il accepter les textes écrits par un modèle ? Faut-il exiger une preuve formelle comme condition d'examen ? Sans règle, le flux de travaux machine saturera simplement la file d'attente.

Pour les ingénieurs et les responsables d'équipe, une leçon plus large s'impose. La vérification formelle sort de sa niche académique et devient un moyen d'accepter les résultats d'une IA sans leur faire confiance sur parole. Le même principe s'applique au code et aux systèmes critiques.

Enfin, tant qu'aucune analyse indépendante n'existe, mieux vaut s'abstenir de conclusions tapageuses. L'indicateur clé des prochains mois : quelle part des 722 travaux résistera à la vérification, et combien se révéleront substantiels, et pas seulement corrects.