Contexte et ampleur du dépôt
OpenAI a mis en ligne près de 400 résultats générés par IA répartis dans plus de 700 manuscrits. Les travaux couvrent la combinatoire, plusieurs branches de la géométrie, la théorie des nombres, l’informatique théorique, l’algèbre, la topologie, la probabilité, la mécanique statistique et la physique mathématique. La taille du corpus a poussé OpenAI à publier un guide d’utilisation du dépôt GitHub afin d’aider les chercheurs à naviguer parmi les documents.
Les mathématiciens interrogés ont indiqué que la simple lecture du tableau des matières, d’environ 40 pages, prenait déjà plus d’une heure. Cette première impression d’encombrement reflète la difficulté d’évaluer rapidement la pertinence ou la validité de chaque contribution.
Méthodologie de formalisation et rôle de Lean
Parmi les manuscrits, une partie a été traduite en Lean, langage de preuve assistée par ordinateur. OpenAI affirme que 300 résultats majeurs sur 719 manuscrits ont été formalisés, soit environ 42 % du total. Cette proportion indique que la majorité des travaux reste à l’état de texte théorique, sans vérification mécanique.
Les formalisation en Lean permettent de confirmer la logique d’un théorème même si l’argument humain reste obscur. Cependant, la présence d’un fichier Lean ne garantit pas une correspondance parfaite avec l’énoncé du manuscrit ; les chercheurs doivent vérifier que le code prouve exactement la même proposition.
Analyse des défis de vérification et implications pour la recherche
Les mathématiciens soulignent que la qualité des formalisation varie. Certains résultats sont correctement prouvés, d’autres présentent des écarts entre le code et l’énoncé, ou sont incomplets. Kevin Buzzard, spécialiste de la théorie algébrique des nombres, n’a identifié que six théorèmes clairement pertinents parmi des dizaines dans son domaine, et peu d’entre eux sont formalisés.
Cette hétérogénéité impose un travail de validation qui peut s’étendre sur plusieurs années. Les chercheurs doivent d’abord filtrer les contributions, puis reproduire ou compléter les preuves Lean, ce qui nécessite des compétences en programmation de preuves et en mathématiques avancées. Le risque d’adopter des résultats non vérifiés est élevé, car une erreur non détectée pourrait se propager dans des travaux subséquents.
En outre, le rythme de publication d’OpenAI laisse peu de temps aux communautés académiques pour assimiler les avancées. Si l’entreprise continue à publier de nouveaux ensembles, le fossé entre production IA et validation humaine risque de s’élargir, remettant en question la manière dont les mathématiques traditionnelles intègrent les outils d’IA.
