Un catalogue de 722 manuscrits issu d’environ 4 000 problèmes
OpenAI a publié le 6 octobre un ensemble de 722 manuscrits mathématiques produits par un modèle interne qui n’est pas encore offert au public. Le catalogue regroupe ces textes dans 372 familles de résultats. Une famille peut réunir une démonstration principale, des conséquences, des arguments complémentaires ou d’autres preuves. L’entreprise affirme avoir soumis environ 4 000 problèmes au modèle, puis retenu et organisé les sorties jugées assez importantes pour le catalogue. Selon OpenAI, la vaste majorité des résultats a été obtenue avec une procédure commune et chaque résultat conservé a utilisé en moyenne l’équivalent d’environ trois heures de réflexion avec ChatGPT Pro. Le dépôt comprend des prépublications, une carte des manuscrits, dix résumés abrégés du raisonnement du modèle et des fichiers destinés à vérifier certaines preuves par ordinateur. Ces chiffres décrivent l’ampleur de la publication et son processus annoncé. Ils ne signifient pas que 722 théorèmes ont déjà été confirmés par la communauté scientifique.
Une preuve formalisée peut être vérifiée par une machine
Une partie du travail est accompagnée de formalisations dans Lean. Ce langage permet de représenter une démonstration sous une forme qu’un logiciel peut contrôler étape par étape à partir de règles précises. Lorsqu’un fichier Lean est accepté dans un environnement bien défini, il offre une assurance beaucoup plus forte qu’un texte qui semble simplement convaincant. Cette méthode est particulièrement utile avec les modèles génératifs, capables de produire un argument fluide contenant une lacune discrète. Le dépôt précise toutefois que plusieurs manuscrits n’ont pas encore de formalisation et que certains résultats non formalisés pourraient comporter des problèmes. OpenAI promet d’ajouter des fichiers et de conserver l’historique des corrections. Même une preuve validée dans Lean ne règle pas tout : des spécialistes doivent encore confirmer que l’énoncé correspond bien à la question annoncée, que les hypothèses sont pertinentes, que le travail est réellement nouveau et que les références rendent justice aux contributions antérieures. Le contrôle informatique vérifie une chaîne logique; il ne remplace pas toute l’évaluation scientifique.
Le groupe consulté parle d’un début, pas d’une conclusion
OpenAI dit avoir préparé cette publication en consultant l’Advisory Group on Mathematics and Artificial Intelligence, ou AGMAI, un groupe indépendant lié à l’Institute for Advanced Study. Ce groupe réunit des mathématiciens de plusieurs universités et affirme ne recevoir aucun paiement des entreprises qu’il conseille. Dans sa réaction du 6 octobre, il qualifie la publication d’événement important pour les mathématiques, tout en précisant que son rôle consultatif ne constitue ni une approbation du processus ni un jugement sur l’impact des résultats. AGMAI résume la limite centrale avec une idée simple : rendre le travail public est la première étape. La communauté mathématique doit maintenant évaluer les textes, les comprendre et décider lesquels peuvent entrer dans le savoir établi. Le groupe avait déjà recommandé que les laboratoires publient rapidement les résultats importants, indiquent le modèle, les consignes, le calcul utilisé et les échecs comparables, puis financent le travail nécessaire à leur compréhension. Il demande aussi que la recherche ne soit pas réduite à une démonstration commerciale des capacités d’un modèle.
Le dépôt public améliore l’inspection sans offrir la reproduction complète
Le choix d’un dépôt GitHub rend les manuscrits, les versions et les artefacts de preuve accessibles au même endroit. Les spécialistes peuvent télécharger un texte, examiner une formalisation, signaler une erreur et suivre une correction. OpenAI indique vouloir aussi explorer des dépôts gérés par la communauté scientifique. Cette ouverture répond en partie à une critique formulée après de précédentes annonces : un résultat spectaculaire ne peut pas être évalué si le détail de la démonstration demeure fermé. La reproduction complète reste néanmoins impossible pour l’instant. Le modèle utilisé n’est pas nommé publiquement ni accessible, et seules dix familles disposent d’un résumé du raisonnement partagé. Les mathématiciens ne peuvent donc pas relancer la même expérience dans les mêmes conditions. The Verge souligne aussi que l’arrivée rapide de résultats produits par des laboratoires privés alimente un débat sur l’éthique de la recherche, le crédit accordé aux travaux humains et l’accès inégal aux outils les plus puissants. Publier les sorties facilite le contrôle; ouvrir la méthode et l’instrument demeure une question distincte.
Le prochain goulot d’étranglement sera la vérification et la compréhension
Si une fraction importante du catalogue résiste à l’examen, la conséquence dépassera un classement de modèles. Des centaines de textes devront être attribués à des experts capables de vérifier les preuves, de les comparer à la littérature et d’expliquer les idées utiles. Une université ne peut pas traiter cette charge comme une simple pile de documents à résumer. Il faut du temps de recherche, des séminaires, des reproductions indépendantes et une façon durable de consigner les erreurs. OpenAI annonce vouloir financer des ateliers, des conférences et des programmes consacrés à la compréhension des résultats. Pour le public, la formulation prudente est donc essentielle. On peut dire qu’OpenAI a publié 722 manuscrits et que son dépôt rapporte des solutions à des problèmes ouverts. On ne devrait pas présenter chaque texte comme un théorème confirmé. La portée réelle apparaîtra à mesure que les spécialistes valideront, corrigeront ou rejetteront les résultats. Cette publication montre déjà une capacité nouvelle : produire des candidats à la recherche à grande échelle. Elle déplace aussi la responsabilité vers une étape moins spectaculaire, mais décisive, celle de transformer une sortie de modèle en connaissance comprise, vérifiée et partagée.
