Le 7 octobre 2026, OpenAI a consigné le retrait de trois manuscrits mathématiques après une erreur de signe qui invalidait un argument dont dépendaient ces textes. Le dépôt en compte désormais 719, contre 722 au lancement, le 6 octobre. L’historique fait aussi état de réparations de preuve et de mises à jour dans d’autres manuscrits.

Trois retraits et deux autres types de révision

OpenAI attribue les trois retraits à une erreur de signe dans un argument d’annulation de trace de stabilisation, qui invalidait aussi les constructions dépendantes. Dans deux catégories distinctes, 14 autres manuscrits ont reçu des réparations de preuve et 13 autres des mises à jour de références ou de versions.

Le décompte actuel reflète donc à la fois les retraits et les révisions consignées par OpenAI. La distinction entre ces opérations compte : les trois manuscrits retirés ne sont pas les 14 textes dont les preuves ont été réparées, ni les 13 dont les références ou les versions ont été mises à jour.

Du catalogue initial de 722 manuscrits à la liste de 719

OpenAI avait annoncé sa collection le 6 octobre 2026 avec 722 manuscrits répartis en 372 familles. Après les trois retraits, le dépôt en répertorie 719, toujours dans 372 familles.

Une famille peut regrouper un résultat principal et des documents apparentés, comme des arguments complémentaires, des conséquences ou des preuves alternatives. Le nombre de manuscrits n’équivaut donc pas au nombre de problèmes distincts résolus. OpenAI indique par ailleurs qu’environ 4 000 problèmes ont été soumis au modèle pendant l’évaluation ; ce chiffre ne constitue pas un taux de résolution pour le catalogue publié.

OpenAI avait également publié une annonce mathématique distincte sur Navier–Stokes, évoquée dans notre précédent article.

Ce que signifie le décompte Lean

OpenAI rapporte que 300 des 719 résultats principaux sont formalisés en Lean, un langage de programmation et assistant de preuve qui permet de vérifier une démonstration encodée à partir d’un énoncé et d’hypothèses formalisés. Cela représente environ 42 % des résultats principaux recensés.

Ce chiffre mesure la formalisation, pas le nombre de résultats examinés ou acceptés par des mathématiciens indépendants. Une vérification dans Lean porte sur la preuve telle qu’elle a été encodée et sur les hypothèses qui y figurent ; elle ne remplace pas l’examen de la portée du résultat dans le manuscrit.

Des étapes de vérification différentes

OpenAI indique que les résultats de la collection se trouvent à des stades de vérification différents et que certains travaux sans formalisation Lean pourraient comporter des problèmes. Le décompte des formalisation ne résume donc pas l’état de vérification de l’ensemble des manuscrits : le dépôt distingue les résultats formalisés des autres travaux, et signale que la vérification n’est pas uniforme.