OpenAI retire 3 de ses 722 articles de maths écrits par IA après une erreur de signe

OpenAI a publié 722 manuscrits de mathématiques rédigés par un modèle d'IA non publié le 6 octobre 2026, puis en a retiré trois le lendemain. Selon l'historique des révisions d'OpenAI sur GitHub, une erreur de signe a cassé une étape clé d'une preuve. Deux autres articles dépendaient de cette preuve. L'épisode montre combien il est difficile de vérifier à grande échelle une recherche écrite par IA. Il explique aussi pourquoi les mathématiciens se disputent à propos de cette publication.

Ce qu'OpenAI a publié

Les fichiers se trouvent dans un dépôt GitHub public, openai/math. Implicator.ai compte 372 « familles de résultats » et 722 manuscrits. Fortune décrit la publication comme des solutions complètes ou partielles, produites par l'IA, à plus de 370 problèmes ouverts. Ce chiffre compte autre chose, il ne faut donc pas mélanger les deux nombres.

Implicator.ai et Yahoo Tech disent tous deux que le travail vient d'un modèle interne qu'OpenAI n'a pas publié. Implicator.ai indique qu'OpenAI a posé environ 4 000 problèmes pendant l'évaluation. Elle précise que chaque résultat a coûté en moyenne environ trois heures de calcul ChatGPT Pro. Un porte-parole a déclaré que presque chaque résultat venait d'une seule requête adressée à un seul agent d'IA.

Fortune rapporte qu'OpenAI revendique aussi des avancées sur trois autres des sept problèmes du prix du Millénaire (Millennium Prize). Ce sont des problèmes ouverts célèbres, dotés de prix de 1 million de dollars. Aucun n'a de solution complète. OpenAI avait déjà revendiqué une solution du problème de Navier-Stokes quelques semaines plus tôt. Cette revendication, des mathématiciens l'ont contestée.

Les trois retraits

L'historique des révisions, daté du 7 octobre, liste les articles retirés :

Article	Rôle
Algebraicity of Weil classes on split abelian eightfolds	Contenait l'erreur
Algebraicity of Kuga-Satake Correspondences for K3 Surfaces	En dépendait
The rational Hodge conjecture for products of K3 surfaces	En dépendait

La raison indiquée est la suivante : « une erreur de signe invalide un argument d'annulation de trace de stabilisation ». L'historique précise aussi qu'OpenAI a corrigé 14 autres manuscrits. Elle en a mis à jour 13 pour qu'ils citent des articles compagnons révisés. Les versions retirées restent en ligne avec des avis, rapporte Implicator.ai.

Aucune source ne dit qui a trouvé l'erreur. La page d'OpenAI ne le dit pas non plus.

Quelle part est vérifiée

Lean est un langage de programmation qui permet à un ordinateur de vérifier chaque étape logique d'une preuve. Selon Implicator.ai et l'historique des révisions, 300 des 719 résultats principaux restants ont une formalisation en Lean, soit environ 42 %. Fortune dit seulement que « certains » problèmes ont des vérifications formelles. Une vérification Lean confirme la logique. Elle ne dit pas si un résultat est nouveau ou important, note Yahoo Tech.

Les personnes extérieures ne peuvent pas relancer le modèle, car il n'est pas disponible. Implicator.ai dit qu'OpenAI n'a publié aucune requête, seulement des chiffres moyens de calcul. Un groupe consultatif de l'Institute for Advanced Study avait recommandé plus de transparence le 29 septembre. Fortune dit qu'OpenAI n'a suivi ce conseil qu'en partie.

Ce que disent les mathématiciens

Les réactions sont partagées, selon Fortune et Implicator.ai.

• Daniel Litt, de l'University of Toronto, a jugé la publication « excellente pour les mathématiques ». Il dit ne voir aucune raison de garder les articles secrets.
• Tristan Buckmaster, de la New York University, a mis en doute la diligence raisonnable, cité via le New York Times.
• Andrew Sutherland, du MIT, a dit de « traiter comme non vérifiée toute affirmation sur la résolution de problèmes en un seul essai par un seul agent ».
• Le groupe consultatif de l'IAS a déclaré : « Cette publication est le début, et non l'achèvement, du processus de compréhension humaine. »

Implicator.ai relève aussi une contradiction. La description du porte-parole, « une requête, un agent », est en conflit avec les 10 000 agents qu'OpenAI dit avoir utilisés pour le résultat sur Navier-Stokes.

Ce que cela signifie pour les développeurs

Quiconque utilise l'IA pour écrire du code, des preuves ou de la recherche fait face au même problème de vérification.

• Séparez la génération de la vérification. Les vérifications Lean ont repéré ce que la lecture n'avait pas vu. Si votre sortie d'IA a une forme vérifiable par machine, comme des tests, des types ou des preuves, exécutez-la avant que quiconque lui fasse confiance.
• Suivez les dépendances entre les sorties d'IA. Un article défectueux en a entraîné deux autres. Notez quels artefacts générés reposent sur quels autres.
• Exigez les entrées. Sans les requêtes et l'accès au modèle, personne ne peut distinguer une méthode fiable d'un coup de chance, note Yahoo Tech. Demandez les requêtes, les réglages et les journaux derrière toute affirmation d'IA sur laquelle vous vous appuyez.
• Traitez un retrait comme un événement normal. Trois sur 722 en deux jours n'a rien d'alarmant. Publier un historique de révisions clair est la partie à copier.

Le chiffre à surveiller est la part des résultats avec des preuves formelles. À 42 % aujourd'hui, il montre ce qu'un mathématicien doit encore lire à la main dans cette publication.