OpenAI annonce dix avancées majeures en mathématiques et informatique théorique avec le modèle Astra

OpenAI annonce que son futur modèle Astra a résolu dix problèmes ouverts en mathématiques et informatique théorique, portant sur la géométrie de haute dimension, la théorie des codes et la cryptographie. La source est le blog officiel du laboratoire. C'est crédible, mais ça reste un communiqué. Le modèle n'est pas encore disponible et personne d'extérieur n'a pu rejouer ces trouvailles pour vérifier leur validité.

Ce que je relève d'abord, c'est la méthode. Des mathématiciens ont travaillé avec Astra pour préparer les arguments puis formaliser les preuves avec des certificats Lean. Pour ceux qui ne connaissent pas, Lean est un langage qui sert à écrire des démonstrations qu'un ordinateur peut vérifier ligne à ligne. Si les certificats sont publiés et qu'ils passent, une bonne partie du débat est tranchée. Dans ce cas précis, le modèle n'est pas en autonomie totale. Il est supervisé par un programme déterministe qui valide chaque résultat. C'est ça qui devrait être au cœur des architectures IA modernes : un harnais qui encadre le modèle et vérifie son travail.

L'ensemble aurait tourné pour environ deux mille dollars de calcul. Si le montant est exact, résoudre des problèmes ouverts depuis dix ans pour le prix d'un ordinateur portable correct en dit long sur l'intérêt de ce type d'architecture. L'annonce arrive aussi à un moment particulier, pendant que le labo est empêtré dans des affaires juridiques et un incident de sécurité récent. Le calendrier interroge, même si ça ne change rien à la validité du travail.

Il faut rappeler qu'OpenAI n'est pas seul sur ce terrain. Mistral a sorti Leanstral, un modèle open source sous licence Apache taillé pour la preuve en Lean 4. Sa version 1.5 sature le banc d'essai miniF2F et résout 587 des 672 problèmes de PutnamBench d'après l'annonce officielle. On peut le télécharger et le faire tourner soi-même, chez soi, avec une grosse machine. C'est précisément là que se joue la confiance : sur un résultat qu'on peut rejouer, pas sur un communiqué. Tant que des pairs n'ont pas relu les manuscrits et rejoué les certificats, on tient une performance prometteuse, pas encore une avancée scientifique établie.