OpenAI retire déjà 3 de ses 722 manuscrits de maths après une erreur de signe

Trois manuscrits en moins, sur un catalogue présenté comme une démonstration de puissance mathématique à grande échelle. Après la découverte d’une erreur de signe dans l’un de ses arguments, OpenAI a retiré des travaux et rappelle qu’un texte produit par une IA ne vaut pas encore validation d’un résultat.

De 722 manuscrits à 719

Le 6 octobre, OpenAI a mis à disposition 722 manuscrits générés par un modèle interne, regroupés en 372 familles de résultats. L’ensemble couvre de nombreux domaines des mathématiques et revendique des avancées sur plusieurs problèmes ouverts ou réputés difficiles.

L’annonce était spectaculaire par son volume. Elle suggérait qu’un même système pouvait explorer, en parallèle, des centaines de pistes de recherche généralement traitées par des équipes spécialisées pendant des mois, voire des années. Mais un catalogue de textes n’est pas une collection de théorèmes certifiés.

Après la découverte d’une erreur de signe dans un argument, trois manuscrits ont été retirés. Le catalogue en compte désormais 719. OpenAI indique également avoir corrigé d’autres documents et ajouté des formalisation de preuves dans Lean, un assistant de preuve capable de vérifier automatiquement certaines étapes mathématiques.

La différence entre les trois catégories est essentielle : retirer un manuscrit signifie reconnaître qu’il ne peut plus être présenté dans sa forme initiale ; corriger un document suppose que l’erreur peut être isolée et réparée ; ajouter une formalisation vise à rendre certaines preuves contrôlables par un outil informatique. Aucun de ces mécanismes ne permet toutefois, à lui seul, de conclure que l’ensemble du corpus est fiable.

Une erreur de signe peut invalider toute une preuve

Dans un raisonnement mathématique, une erreur de signe n’est pas nécessairement une coquille sans conséquence. Elle peut modifier une inégalité, inverser une condition de convergence ou rendre fausse une identité utilisée plusieurs pages plus loin. Si l’étape fautive sert de fondation à plusieurs résultats, l’invalidité se propage dans tout le manuscrit.

La difficulté tient précisément au fait que les textes produits par les modèles de langage peuvent présenter une apparence convaincante : notation cohérente, enchaînement formel, vocabulaire spécialisé et conclusions plausibles. Cette apparence rend la vérification humaine indispensable, surtout lorsque les arguments s’appuient sur des objets abstraits ou de longues chaînes de déductions.

Le retrait de trois manuscrits ne permet donc pas d’estimer directement la proportion d’erreurs restante. Il constitue seulement le premier chiffre public d’un audit dont l’étendue n’est pas connue. Le passage de 722 à 719 mesure le volume du catalogue, pas son taux de validité.

Cette distinction est centrale pour évaluer la portée de l’initiative. Une découverte mathématique ne se résume pas à une conjecture intéressante ou à une stratégie prometteuse. Elle doit résister aux vérifications, aux contre-exemples, à la relecture de spécialistes et, lorsque c’est possible, à une formalisation indépendante.

Lean renforce la vérification, sans supprimer toutes les ambiguïtés

La présence de preuves formalisées dans Lean constitue l’élément le plus solide de la mise à jour annoncée par OpenAI. Dans cet environnement, une preuve est traduite dans un langage dont le noyau informatique vérifie que les règles appliquées respectent les définitions et les axiomes déclarés.

Cette approche peut empêcher certaines erreurs classiques : étape logique manquante, utilisation incorrecte d’un lemme ou manipulation algébrique invalide. Elle transforme une partie du débat en question vérifiable par ordinateur plutôt qu’en simple examen de prose mathématique.

Mais Lean ne répond pas à toutes les questions. Le système vérifie la preuve d’un énoncé formalisé ; il ne garantit pas que cet énoncé correspond exactement au problème décrit dans le manuscrit. Il ne juge pas non plus la pertinence des hypothèses, l’intérêt du résultat ou l’originalité de la démarche. Une formalisation peut être parfaitement correcte tout en démontrant une proposition plus faible, différente ou moins générale que celle annoncée.

La couverture compte également. OpenAI indique avoir ajouté des formalisations, mais cela ne signifie pas que les 719 manuscrits restants sont intégralement traduits dans Lean. La fiabilité du corpus dépendra donc de la part effectivement formalisée, de la qualité de cette traduction et de la capacité de chercheurs indépendants à reproduire les résultats.

Le vrai test sera la vérification indépendante

L’épisode met en lumière une tension entre deux échelles de temps. Un modèle peut générer rapidement des centaines de pistes, de conjectures et d’arguments. La validation, elle, reste contrainte par le temps des mathématiciens capables de les lire, de les tester et de les replacer dans la littérature existante.

Ce décalage est particulièrement important pour les problèmes ouverts. Dans ce domaine, une idée partiellement juste peut être précieuse même si le manuscrit qui la contient comporte une erreur. Mais il faut alors distinguer clairement une piste de recherche, un résultat corrigible et une preuve établie. Les trois manuscrits retirés montrent que cette frontière ne peut pas être laissée à la seule présentation du modèle.

L’annonce d’OpenAI doit donc être lue comme un programme d’exploration, non comme une liste de 719 avancées validées. La quantité produite peut aider à repérer des structures, proposer des lemmes ou accélérer certaines recherches. Elle accroît aussi le coût du tri : plus le modèle génère de textes, plus la vérification devient le goulot d’étranglement.

Le prochain jalon sera concret : publication d’un historique détaillé des corrections, extension des formalisations dans Lean et validation par des équipes extérieures. La mesure la plus significative ne sera pas le nombre de manuscrits déposés, mais celui des résultats qui survivront à une relecture indépendante et à une vérification formelle. Pour l’instant, 719 est un inventaire ; ce n’est pas encore un bilan scientifique.