OpenAI revendique dix avancées mathématiques : ce que les preuves Lean changent vraiment

OpenAI affirme qu’une version interne de son prochain modèle, appelée Astra, a résolu ou fait progresser dix problèmes ouverts en mathématiques et en informatique théorique. Les sujets vont de l’empilement de sphères à la cryptographie sur réseaux, en passant par la théorie des groupes, les jeux quantiques et les nombres de Ramsey. L’entreprise publie un manuscrit de 253 pages, des déroulés de raisonnement et des certificats formalisés avec l’assistant de preuve Lean.

L’annonce est importante, mais elle ne doit pas être résumée par « une IA a prouvé dix théorèmes ». Une démonstration peut être logiquement correcte tout en reposant sur une formulation incomplète, une hypothèse mal transcrite ou un résultat dont la portée a été surévaluée. Lean renforce considérablement la vérification mécanique ; il ne remplace ni la lecture des spécialistes, ni la comparaison avec la littérature, ni le temps nécessaire au consensus scientifique.

La réponse rapide

Dix problèmes, pas un unique test de calcul

La sélection ne se limite pas à des exercices difficiles dont la réponse était déjà connue. OpenAI présente de nouvelles bornes pour l’empilement de sphères en grande dimension et pour les codes binaires et sphériques. Le manuscrit propose aussi une construction de groupes non sofiques, sujet central en théorie des groupes, ainsi qu’une réfutation d’une conjecture de rigidité liée aux algèbres de von Neumann.

En complexité, les auteurs annoncent de nouvelles bornes inférieures pour le calcul du permanent par des circuits arithmétiques. Un autre résultat porte sur la répétition parallèle de jeux quantiques à deux joueurs. La liste inclut encore une dureté d’approximation du problème du vecteur le plus proche, directement pertinent pour la compréhension des réseaux utilisés en cryptographie post-quantique.

Les trois derniers ensembles concernent la conjecture de volume d’Ehrhart, les nombres de Ramsey multicolores et plusieurs problèmes d’Erdős en théorie extrémale des graphes. Cette diversité compte : elle cherche à montrer une capacité à naviguer entre des vocabulaires et des méthodes différents, plutôt qu’une optimisation sur un benchmark homogène.

Comment Astra aurait travaillé

Selon OpenAI, Astra a exploré les problèmes avec un grand volume de calcul, puis des humains ont préparé les arguments en manuscrits avec l’aide du même modèle. Le processus ne ressemble donc pas à une feuille de papier sortie intacte d’une boîte noire. Il combine recherche automatisée, sélection, reformulation humaine et formalisation.

OpenAI estime que les jetons nécessaires à la découverte des solutions auraient coûté environ 2 000 dollars au tarif de son API Sol. Ce chiffre est frappant, mais il ne représente pas le coût complet. Il exclut vraisemblablement l’entraînement du modèle, l’infrastructure expérimentale, le temps des chercheurs, les essais non retenus et la formalisation finale. Il mesure un coût marginal de génération, pas le budget scientifique total.

Le modèle utilisé n’est par ailleurs pas disponible publiquement au moment de l’annonce. Une équipe extérieure ne peut donc pas reproduire le protocole complet en lançant les mêmes expériences. Elle peut en revanche examiner les manuscrits et les certificats fournis, ce qui constitue la partie la plus utile pour l’évaluation immédiate.

Ce qu’un certificat Lean vérifie

Lean est un assistant de preuve : une démonstration y est traduite en objets formels que le noyau du logiciel vérifie étape par étape. Si le certificat est accepté, il devient très difficile de dissimuler un saut logique, un cas oublié ou une manipulation algébrique invalide à l’intérieur de la partie formalisée.

Cette garantie est plus forte qu’une relecture superficielle d’un texte de plusieurs centaines de pages. Le dépôt public permet aussi à d’autres chercheurs de compiler les preuves, d’inspecter les dépendances et de chercher les axiomes utilisés. La petite taille du noyau de confiance est précisément l’un des intérêts de ce type d’outil.

Mais Lean répond à une question limitée : « ce terme constitue-t-il une preuve du théorème tel qu’il a été encodé, avec ces définitions et ces axiomes ? » Il ne décide pas si le théorème formel correspond exactement au problème que la communauté avait en tête. Une erreur dans la traduction de l’énoncé, une hypothèse trop forte ou une définition légèrement déplacée peuvent produire une preuve valide d’un résultat moins intéressant.

Pourquoi la relecture humaine reste indispensable

Les spécialistes doivent d’abord comparer chaque énoncé à la littérature. Une idée peut être nouvelle, redécouvrir un résultat dispersé, ou n’améliorer qu’un cas déjà connu. Cette évaluation exige une connaissance historique et des échanges avec les communautés concernées.

Ils doivent ensuite juger la valeur explicative. Une preuve formelle peut être correcte mais difficile à comprendre, fragile à généraliser ou peu éclairante sur la structure du problème. Les mathématiques ne servent pas uniquement à certifier une proposition ; elles construisent aussi des méthodes que d’autres pourront réutiliser.

Enfin, la paternité et la responsabilité doivent être claires. Le manuscrit a été produit dans un dispositif mêlant modèle et chercheurs humains. Citer les contributions, documenter les choix et permettre la critique est nécessaire pour éviter qu’une communication d’entreprise ne devienne le seul récit disponible.

Ce que l’on peut vérifier dès maintenant

La première étape consiste à cloner le dépôt openai/ten-proofs, relever la version de Lean et compiler les certificats dans l’environnement indiqué. Une compilation réussie confirme l’intégrité technique du paquet reçu ; elle ne constitue pas encore une expertise mathématique.

La deuxième est de relier chaque théorème formel à sa formulation lisible dans le manuscrit. Les définitions, conditions de dimension, constantes et quantificateurs méritent une attention particulière. Une différence minuscule peut transformer la portée d’un résultat.

La troisième est de suivre les commentaires des chercheurs des domaines concernés, les éventuelles corrections du dépôt et la soumission des manuscrits à des revues ou conférences. La solidité de l’annonce se mesurera dans la durée, lorsque les arguments auront survécu à des lectures hostiles et indépendantes.

Un changement de méthode plus important qu’un classement

Même si certains résultats étaient révisés, le processus présenté resterait significatif. Un modèle peut proposer des pistes, un humain peut choisir celles qui méritent d’être développées, puis un assistant de preuve peut fermer une partie de la boucle de vérification. Cette chaîne est plus crédible qu’un chatbot qui affirme avoir démontré quelque chose sans artefact contrôlable.

Elle change aussi le travail des chercheurs. Le goulot d’étranglement peut se déplacer de la production d’idées vers la formulation des bons problèmes, l’audit des hypothèses et l’organisation de milliers de candidats. Les outils formels deviennent alors une infrastructure de confiance, pas un simple supplément pédagogique.

La déclaration de Leiden rappelle toutefois que l’adoption de l’IA en mathématiques touche à l’attribution, à l’accès aux outils, à la concentration des ressources et à la façon dont les jeunes chercheurs apprennent. Publier les preuves aide, mais ne répond pas à toutes ces questions.

Ce qu’il faut retenir

OpenAI fournit davantage qu’une série de résultats annoncés dans un billet : les manuscrits et certificats Lean donnent une matière concrète à auditer. C’est la bonne direction pour une revendication scientifique produite avec une IA.

La formulation prudente reste néanmoins essentielle. Une preuve formellement vérifiée est un jalon puissant, pas un raccourci vers le consensus. Si les dix contributions sont confirmées par les communautés concernées, l’événement marquera surtout l’arrivée d’un nouveau flux de recherche où génération automatique, expertise humaine et vérification formelle travaillent ensemble.