Le fait
Le 8 octobre 2026, la revue Science publie l’article peer-reviewed d’AlphaProof Nexus, le cadre de Google DeepMind pour la recherche de preuves mathématiques formelles. Une vague de couverture technique suit dans les jours suivants, dont The Decoder le 12 octobre. Le preprint était déjà sorti en mai ; c’est la version revue par les pairs qui relance le sujet.
Ce que le système revendique
D’après le communiqué EurekAlert et The Decoder, Nexus s’appuie sur des agents qui rédigent et révisent des preuves en Lean, le compilateur validant chaque étape. Pour les sous-problèmes difficiles, un agent plus complet peut appeler AlphaProof, outil spécialisé, et coordonner des sous-agents via un algorithme évolutif.
Résultats revendiqués :
- 9 problèmes d’Erdős résolus sur 353 tentés, dont deux ouverts depuis 56 ans ;
- 44 conjectures ouvertes de l’OEIS prouvées sur 492 autoformalizées ;
- des avancées citées en géométrie algébrique, optimisation min-max et d’autres domaines.
DeepMind indique que même sans AlphaProof, l’agent de base a résolu les neuf problèmes d’Erdős. Les preuves ont été partagées en ligne avant la publication.
Le contexte du débat
La publication tombe dans un climat tendu : OpenAI a récemment publié en masse des manuscrits de preuves sur GitHub hors revue, ce qui a poussé l’Association for Human Mathematics, associée à Terence Tao, à appeler à un boycott de cette pratique. DeepMind choisit au contraire la voie du journal. Dans une Perspective liée, Jeremy Avigad et Matthew Ballard soulignent que même les tentatives échouées peuvent aider les mathématiciens à mieux comprendre les problèmes.
Lecture Neurone21
Le signal fort n’est pas seulement le score Erdős : c’est la vérification machine via Lean, qui change la nature de la confiance qu’on peut accorder à une preuve générée. Pour une équipe R&D, la leçon est concrète : exiger une formalisation vérifiable plutôt qu’un PDF généré. Les chiffres restent ceux de DeepMind et de la couverture Science ; la critique méthodologique (formalisation fidèle du problème d’origine, coût des échecs) doit être lue en parallèle.