OpenAI attribue à une version interne de sa prochaine IA dix résultats "inédits" en mathématiques et en informatique théorique. Ils sont accompagnés de certificats formalisés dans Lean 4, mais la communauté scientifique doit encore en apprécier la nouveauté et la portée.
Dix problèmes ouverts, un manuscrit de 249 pages et une facture théorique d’environ 2 000 dollars en jetons. OpenAI avance des chiffres taillés pour attirer l’attention, mais la performance revendiquée par Astra mérite mieux qu'un simple effet d’annonce.
Selon l'entreprise de Sam Altman, son futur modèle d'IA aurait en effet obtenu dix résultats importants en mathématiques et en informatique théorique. Certains répondraient définitivement à des questions restées sans solution pendant des décennies, tandis que d'autres amélioreraient sensiblement les meilleures bornes connues.Des problèmes réputés particulièrement difficiles
Parmi les résultats mis en avant figure la construction du premier groupe non sofic connu, ainsi qu'une réfutation de la conjecture de rigidité de Connes. Astra aurait également tranché trois problèmes associés au mathématicien Paul Erdős.
Le modèle signe aussi, selon OpenAI, la première amélioration depuis 1978 d'une borne générale concernant l'empilement de sphères en grande dimension. Les autres travaux portent sur des domaines tout aussi spécialisés, des codes correcteurs aux circuits arithmétiques, en passant par les jeux quantiques et la cryptographie fondée sur les réseaux euclidiens.
Cette liste ne signifie pas qu'Astra a travaillé seule dans une pièce virtuelle. Si les arguments mathématiques ont été générés par l'IA, des chercheurs humains les ont ensuite transformés en manuscrits avec l’aide du modèle et ont ensuite participé à leur formalisation dans Lean 4.
Cet assistant de preuve vérifie mécaniquement que les démonstrations découlent des définitions et des hypothèses formalisées, sans pour autant établir leur nouveauté ou leur importance scientifique. Les certificats produits ont été rendus publics sur GitHub pour que d’autres équipes puissent les examiner.
- Chat dans différentes langues, dont le français
- Générer, traduire et obtenir un résumé de texte
- Générer, optimiser et corriger du code
Deux mille dollars, mais une addition très incomplète
Le montant de 2 000 dollars doit lui aussi être remis en perspective. Il correspond uniquement au coût estimé des jetons consommés pendant la recherche des solutions, calculé à partir des tarifs du modèle Sol dans l'API d’OpenAI. Cette somme ne tient pas compte de l'entraînement d’Astra ni du travail des chercheurs impliqués.
Cette version d'Astra reste pour l’instant réservée à l'interne chez OpenAI, sans calendrier de lancement annoncé. Une démonstration qui tombe à point nommé pour l'entreprise, quelques jours après qu'elle a reconnu l’implication de GPT-5.6 Sol et d’un prototype interne dans le piratage de Hugging Face au cours d’une évaluation.
Rien ne relie Astra à cet incident, mais ce feu d’artifice mathématique offre au moins une manière élégante de déplacer les regards. Ou, pour le dire moins savamment, de noyer un peu le poisson.
Lean 4 est un assistant de preuve : un logiciel qui permet d'écrire une démonstration sous une forme formelle et de la faire vérifier automatiquement par un noyau logique. L'intérêt n'est pas de « trouver » l'idée mathématique, mais de vérifier qu'aucune étape de la démonstration telle qu'elle a été formalisée ne repose sur un raccourci non justifié. Un « certificat » Lean est donc un artefact vérifiable par n'importe qui disposant de l'outil et du code source, ce qui facilite l'audit et la reproductibilité. En revanche, un certificat ne dit pas si le résultat est réellement nouveau ou important : il atteste surtout de la cohérence logique, à hypothèses données.
Un groupe sofic est un objet d'algèbre dont le comportement peut être approximé, d'une certaine manière, par des permutations finies (des symétries sur un ensemble fini). Beaucoup de grandes familles de groupes connues sont sofiques, et il a longtemps été difficile de savoir si tous les groupes l’étaient. Construire un groupe non sofic fournirait un contre-exemple concret et clarifierait les limites de cette notion d’approximation. Ce type de résultat peut avoir des retombées en théorie des groupes, en dynamique symbolique et en liens avec la théorie de l'information et l’opérateur-algèbre, même si l'impact dépend fortement des détails de la construction.
Dans les API d'IA, un jeton est une unité de texte utilisée pour compter la consommation (entrée et sortie) facturée lors des appels au modèle. Estimer un coût en dollars « en jetons » revient donc à additionner les dépenses variables liées à l'utilisation du modèle pendant les essais, explorations et générations. Cela ne couvre pas les coûts fixes et indirects : entraînement du modèle, calcul GPU/TPU, stockage, orchestration, ingénierie, ni le temps des chercheurs qui cadrent le problème et vérifient les sorties. Deux projets peuvent afficher un coût en jetons similaire tout en ayant des coûts réels très différents selon l'infrastructure et la préparation en amont.
