Le système de démonstration mathématique AlphaProof Nexus de Google DeepMind est officiellement paru dans Science. Le premier auteur de l'article est Tsoukalas, et toute l'équipe de recherche appartient à DeepMind. Le travail avait déjà été rendu public en preprint fin mai ; il s'agit cette fois de la version publiée en revue, après évaluation par les pairs.
Le bilan reste le même : le système s'est attaqué à 353 problèmes d'Erdős non résolus et en a résolu 9, dont 2 ouverts depuis 56 ans ; sur les 492 conjectures ouvertes de l'OEIS, la base de données des suites d'entiers, il en a prouvé 44. Il a aussi répondu à une question de géométrie algébrique sur la fonction de Hilbert, en suspens depuis environ 15 ans, et amélioré une borne connue en optimisation min-max.
Un Gemini, un compilateur Lean
Le socle du système est Gemini 3.1 Pro. Le modèle rédige des preuves dans le langage formel Lean ; le compilateur Lean les vérifie à chaque modification, et les messages d'erreur sont renvoyés directement à la tentative suivante. Tout au long du processus, l'humain ne regarde que le résultat final.
L'article distingue quatre versions :
- Version A : la boucle « génération puis vérification » la plus simple, où le grand modèle écrit et le compilateur juge ;
- Version B : sur la base de A, intègre AlphaProof, le prouveur antérieur de DeepMind, chargé de combler les fragments manquants de la preuve ;
- Version C : ajoute un mécanisme évolutif, dans lequel plusieurs sous-agents partagent un réservoir de brouillons de preuves classés par score Elo ;
- Version D : tout ce qui précède, combiné, utilisé pour s'attaquer aux problèmes d'Erdős.
Le point le plus intrigant du résultat est que la version A a elle aussi prouvé, indépendamment, les 9 problèmes d'Erdős ; simplement, elle a dépensé davantage sur les plus difficiles. Le coût d'inférence cité par The Decoder est de quelques centaines de dollars par problème. Les auteurs écrivent dans l'article :
"power of compiler feedback in grounding LLM reasoning"
(Le retour du compilateur ancre dans le réel le raisonnement des grands modèles de langage.)
Les réserves de plusieurs universitaires espagnols
Le jour de la mise en ligne de l'article, le Science Media Centre espagnol a recueilli l'avis de plusieurs chercheurs du pays, et les opinions se sont partagées.
Pablo Haya Coll, chercheur à l'UAM, estime que cette méthode peut produire de manière systématique des découvertes mathématiques de poids. Josep Curto, de l'UOC, y voit "a dazzling display of technical capability marred by significant methodological inconsistencies", c'est-à-dire une démonstration techniquement éblouissante mais entachée d'incohérences méthodologiques nettes. Il avance trois points : le fait que A et D résolvent les mêmes problèmes montre que la complexité du cadre ne détermine pas forcément la capacité de découverte ; le coût ne tient compte que des exécutions réussies, et les comptes de B et D n'incluent pas non plus les dépenses d'inférence d'AlphaProof lui-même ; enfin, Lean garantit seulement que la preuve vaut pour « l'énoncé tel qu'il a été écrit » ; savoir si cet énoncé traduit fidèlement le problème d'origine exige toujours une vérification manuelle par des mathématiciens, et l'article reconnaît que des erreurs de formalisation se sont produites.
Le directeur de l'ICMAT, Javier Aramayona, s'inquiète d'autre chose : l'apparition d'un grand nombre de résultats « connus pour être vrais, mais que personne ne comprend entièrement », qui pourrait affaiblir le maillon de la compréhension dans la recherche mathématique et la formation des jeunes chercheurs. Teodoro Calonge, de l'université de Valladolid, est plus direct : le domaine a encore une marge d'amélioration considérable.
Les auteurs précisent eux-mêmes la portée : le taux de réussite global de l'IA sur les problèmes d'Erdős est d'environ 1 % à 2 %, les problèmes résolus sont pour la plupart relativement faciles et concentrés en combinatoire, en optimisation convexe et en théorie des nombres, des domaines où la bibliothèque Mathlib est la plus fournie et où les problèmes se décomposent bien en sous-objectifs. Les problèmes qui demandent d'inventer beaucoup de théorie nouvelle restent presque hors de portée du système.
Relier les événements de cette année
En mai, nous avons rapporté qu'un modèle d'OpenAI avait résolu une conjecture d'Erdős vieille de 80 ans ; en septembre, une querelle d'attribution a opposé des mathématiciens et OpenAI ; le 6 octobre, OpenAI a publié d'un seul coup 722 manuscrits mathématiques générés par IA sur GitHub, dans un dépôt open source sous licence Apache 2.0, sans passer par une revue. D'après The Decoder, un groupe de mathématiciens mené par Terence Tao a ensuite appelé à boycotter cette pratique.
La différence entre les deux entreprises apparaît nettement. OpenAI choisit le volume et l'ouverture, en laissant la communauté faire le tri ; DeepMind choisit un nombre de résultats bien plus faible, mais chacun est passé par le compilateur Lean puis par l'évaluation d'une revue. Quant au rôle de Lean, DeepMind reste très mesurée dans l'article ; la formule d'origine est que la vérification formelle "can serve as a filter for determining which proofs merit human review", c'est-à-dire qu'elle sert à décider quelles preuves méritent d'être lues par un humain.
Un calcul approximatif : à quelques centaines de dollars par problème, le coût d'inférence des 9 problèmes d'Erdős reste bien inférieur au salaire mensuel d'un postdoctorant ; mais de combien la facture augmenterait selon le périmètre signalé par Curto, en ajoutant les exécutions échouées et les appels à AlphaProof, l'article ne le chiffre pas pour l'instant. DeepMind a déposé les preuves et une partie des explications dans le dépôt GitHub alphaproof-nexus-results, afin que des mathématiciens extérieurs puissent les vérifier une à une.
Sources : article de la revue Science, The Decoder, CocoLoop, avis d'experts du Science Media Centre espagnol ; le texte de l'article a été vérifié pour les 9 problèmes résolus sur 353 problèmes d'Erdős, les 44 conjectures prouvées sur 492 de l'OEIS et la répartition des rôles entre les quatre versions d'agents.