AlphaProof Nexus : l'IA de DeepMind face à Erdős

AlphaProof Nexus, le système de Google DeepMind, a résolu 9 des 353 problèmes d'Erdős encore ouverts auxquels il s'est attaqué. Ces travaux, d'abord diffusés en prépublication sur arXiv en mai 2026, ont été publiés le 8 octobre dans la revue Science. Leur particularité : chaque preuve est vérifiée par une machine, grâce au langage de preuve formelle Lean, plutôt que de reposer sur le seul raisonnement d'un modèle de langage.

Un modèle de langage sous contrôle d'un vérificateur

Le point de départ des auteurs est connu : les grands modèles de langage raisonnent de mieux en mieux en mathématiques, mais restent peu fiables. Ils peuvent produire une démonstration convaincante et pourtant fausse (voir notre article pour comprendre les grands modèles de langage).

AlphaProof Nexus contourne le problème en faisant écrire au modèle des preuves en Lean. Le compilateur de Lean vérifie chaque étape ; en cas d'erreur, son message est renvoyé au modèle, qui corrige sa tentative. Selon le Science Media Centre espagnol, le modèle de base utilisé est Gemini 3.1 Pro.

L'équipe a comparé plusieurs agents : une simple boucle génération-vérification, une version qui s'appuie aussi sur le prouveur AlphaProof entraîné par apprentissage par renforcement, et une variante plus complexe ajoutant un algorithme évolutionnaire.

Erdős, OEIS et recherche appliquée

Sur 353 problèmes d'Erdős ouverts, l'agent le plus abouti en a résolu 9. Il a également démontré 44 des 492 conjectures ouvertes tirées de l'OEIS, l'encyclopédie en ligne des suites d'entiers. Les auteurs indiquent un coût de quelques centaines de dollars par problème.

Résultat notable : l'agent le plus simple, qui alterne génération par le modèle et vérification par Lean, a résolu les mêmes problèmes d'Erdős, avec toutefois un coût plus élevé sur les plus difficiles. Pour les auteurs, la recherche de preuves formelles assistée par IA est puissante, et la conception de l'agent compte.

DeepMind a publié les preuves Lean sur GitHub, accompagnées de démonstrations rédigées en langage naturel. Le dépôt contient aussi des résultats issus de collaborations avec des chercheurs en combinatoire additive, géométrie algébrique, théorie des graphes, optimisation et optique quantique.

Les réserves des mathématiciens

Les experts interrogés par le Science Media Centre espagnol saluent la méthode mais en soulignent les limites. Josep Curto, de l'Université ouverte de Catalogne, rappelle que Lean ne garantit la validité d'une preuve que par rapport à l'énoncé formalisé : rien ne prouve que cet énoncé traduise fidèlement le problème d'origine, et l'article rapporte des erreurs de formalisation commises par les agents. Une supervision humaine experte reste donc nécessaire. Il note aussi que l'analyse des coûts ne porte que sur les exécutions réussies.

Javier Aramayona, directeur de l'Institut des sciences mathématiques (ICMAT) à Madrid, s'inquiète de l'émergence de nombreux résultats dont on sait qu'ils sont vrais mais que personne ne comprend pleinement. Teodoro Calonge, de l'Université de Valladolid, rappelle que l'approche a échoué sur beaucoup d'autres problèmes et qu'il reste une large marge de progression.

Ce qu'il faut retenir

AlphaProof Nexus ne remplace pas les mathématiciens. Mais il montre qu'associer un modèle de langage à un vérificateur formel permet d'obtenir des résultats nouveaux et contrôlables, à un coût modeste. Le passage par Science donne à ces travaux une validation par les pairs que la prépublication n'avait pas encore.