OpenAI a publié un ensemble de résultats obtenus par un modèle de recherche interne, non disponible publiquement, portant sur des problèmes mathématiques ouverts. L'entreprise affirme que ce modèle a contribué à faire progresser la compréhension de certaines questions non résolues, sans toutefois préciser leur nature exacte ni leur portée dans l'annonce elle-même. Le point notable de cette publication réside dans la méthode de vérification choisie : les preuves produites ont été formalisées dans l'assistant de preuve Lean, un langage permettant de vérifier mécaniquement la validité logique d'un raisonnement mathématique.
Cette approche de formalisation répond à une critique récurrente adressée aux modèles de langage en mathématiques : leur tendance à produire des raisonnements plausibles mais erronés, difficiles à vérifier pour un non-spécialiste. En s'appuyant sur Lean, OpenAI cherche à apporter une garantie de rigueur que le langage naturel seul ne peut offrir, un choix qui rapproche cette initiative des travaux menés par DeepMind avec AlphaProof et AlphaGeometry, ou encore des efforts de la communauté Mathlib.
L'entreprise a mis à disposition sur GitHub le détail des formalisations ainsi que des éléments de méthodologie, une démarche de transparence partielle puisque le modèle à l'origine de ces résultats reste, lui, propriétaire et non accessible. Cette dissociation entre ouverture des preuves et fermeture du modèle illustre une tension classique chez les grands laboratoires : partager des résultats scientifiques vérifiables tout en conservant un avantage compétitif sur la technologie sous-jacente.
Sur le fond, ces travaux s'inscrivent dans une compétition plus large entre laboratoires d'IA pour démontrer des capacités de raisonnement mathématique avancées, un domaine considéré comme un indicateur fort des progrès vers des systèmes capables de raisonnement scientifique autonome. Reste que l'annonce, assez sobre dans sa formulation, ne permet pas encore de mesurer précisément l'ampleur des problèmes traités ni leur importance au sein de la discipline mathématique.