// CLUBIC — INTELLIGENZA ARTIFICIALE
Cette IA aurait signé 10 avancées mathématiques : exploit ou coup de com’ d’OpenAI ?
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.
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.
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.