Deux mille dollars. C'est la somme qu'OpenAI dit avoir dépensée en calcul pour faire résoudre par Astra dix problèmes mathématiques ouverts, jamais démontrés auparavant. Le chiffre surprend, tant l'IA générative a jusqu'ici été associée à des factures de calcul vertigineuses. Ici, on parle d'un montant qu'un particulier pourrait sortir de sa poche.
L'entreprise a mis en ligne sur GitHub les preuves formelles écrites en Lean, un langage de démonstration assistée par ordinateur utilisé par les mathématiciens pour vérifier rigoureusement des raisonnements. Ce choix n'est pas anodin : contrairement à une preuve rédigée en langage naturel, une preuve Lean peut être vérifiée automatiquement, ligne par ligne, sans avoir à faire confiance à l'IA qui l'a produite.
Des groupes non-sofiques et des empilements de sphères
Parmi les dix problèmes résolus figure la question de l'existence des groupes non-sofiques, un sujet de théorie des groupes resté ouvert dans la littérature mathématique. Astra se serait également attaqué à des questions liées aux empilements de sphères, un domaine qui mêle géométrie et optimisation combinatoire, connu du grand public via les travaux sur l'empilement optimal en haute dimension.
OpenAI présente ces résultats comme la première démonstration d'une découverte scientifique originale produite par une IA et vérifiable de manière indépendante. La nuance compte : il ne s'agit pas de reformuler une preuve existante ou de résoudre un exercice de manuel, mais de trancher des questions pour lesquelles aucune réponse n'était connue jusqu'ici.
Les preuves formelles en Lean permettent à n'importe quel mathématicien de vérifier le raisonnement d'Astra sans avoir à lui faire confiance sur parole.
Pourquoi le coût change la donne
Le montant de 2000 dollars intrigue autant que les résultats eux-mêmes. Jusqu'ici, les grandes démonstrations de force en IA scientifique s'accompagnaient de budgets de calcul opaques ou massifs, impliquant des clusters entiers pendant des jours. Si ce chiffre se confirme à l'échelle, il change la manière d'envisager la recherche mathématique assistée par IA : plutôt qu'un outil réservé aux laboratoires les mieux financés, on aurait affaire à une ressource accessible, capable de tourner sur un budget de département universitaire.
Cette économie de moyens intervient alors que le déploiement d'Astra commence. OpenAI n'a pas précisé le calendrier exact de disponibilité pour les chercheurs externes, ni les modalités d'accès. Mais la publication des preuves sur GitHub, en accès libre, envoie un signal : l'entreprise cherche visiblement à établir la crédibilité scientifique de son système avant toute commercialisation plus large.
La vérification, nerf de la confiance
Le recours à Lean répond à une inquiétude légitime dans le monde académique : celle de voir une IA produire des résultats impressionnants mais invérifiables, ou pire, erronés sans que personne ne s'en rende compte avant publication. En formalisant chaque étape dans un langage que des vérificateurs automatiques peuvent contrôler, OpenAI s'épargne le débat sur la fiabilité et déplace la discussion vers le fond : ces théorèmes sont-ils vraiment nouveaux, et vraiment utiles ?
Les mathématiciens spécialistes de théorie des groupes ou d'empilements de sphères devront désormais éplucher ces preuves pour juger de leur portée réelle. Une preuve formelle correcte n'est pas nécessairement une preuve élégante ou éclairante : elle peut être valide tout en restant difficile à exploiter pour la suite des recherches humaines. C'est là que se jouera la vraie évaluation d'Astra, loin des communiqués.
Reste une question que la communauté mathématique va sans doute se poser dans les mois qui viennent : combien de problèmes ouverts, jusqu'ici jugés hors de portée, pourraient tomber avec un budget de calcul comparable ?
