OpenAI a publié, le 6 octobre 2026, une collection de résultats mathématiques produits par un modèle interne. L’annonce met l’accent sur la diffusion des manuscrits et de leurs matériaux de preuve, plutôt que sur le lancement d’un nouvel outil accessible au public.
Des manuscrits et des formalismes ouverts à l’examen
L’entreprise indique partager de nombreuses formalisations dans Lean, un langage permettant de vérifier des preuves par ordinateur. Elle prévoit de compléter ce travail. Des informations sur la méthode et des résumés du raisonnement du modèle accompagnent aussi la publication.
OpenAI explique avoir consulté un groupe indépendant de l’Institute for Advanced Study sur les bonnes pratiques de diffusion. Cette consultation ne constitue pas une validation générale de chaque résultat. Le modèle à l’origine du travail reste interne ; l’annonce d’une démarche pour le diffuser ne signifie pas qu’il soit déjà disponible dans ChatGPT.
La collection affiche explicitement ses limites
Au moment de la consultation, le dépôt officiel openai/math présente 722 manuscrits organisés en 372 familles. Son README précise que les résultats se trouvent à différents stades de vérification et ne disposent pas tous d’une formalisation Lean. Les résultats non formalisés peuvent comporter des problèmes.
Le dépôt rassemble notamment les prépublications, les fichiers Lean et des résumés de raisonnement. Les corrections doivent être enregistrées sous forme de nouvelles versions, en conservant l’accès aux versions antérieures.
L’intérêt de cette actualité est donc l’ouverture de matériaux à l’examen, avec leurs réserves, pas la preuve que tous les problèmes abordés sont définitivement résolus. La lecture de l’annonce et du README ne remplace ni l’analyse des manuscrits par des spécialistes ni l’exécution des vérifications formelles. Aucun contrôle de ces preuves n’a été réalisé pour cet article.
