Une étude de Google DeepMind publiée le 8 octobre 2026 dans Science rapporte qu’AlphaProof Nexus a résolu 9 problèmes d’Erdős parmi 353 énoncés formalisés et démontré 44 conjectures sélectionnées dans l’Online Encyclopedia of Integer Sequences (OEIS), parmi 492 évaluées. Le système associe des modèles de langage à Lean, un assistant qui vérifie mécaniquement les preuves formelles.
Ce que fait AlphaProof Nexus
AlphaProof Nexus est un cadre de recherche de preuves mathématiques formelles. Le système reçoit un théorème exprimé en Lean et une esquisse de preuve ; il ne commence donc pas par une question mathématique ordinaire laissée à formaliser. Les agents proposent des modifications du code de preuve, puis Lean vérifie si elles compilent.
Cette boucle donne un retour concret : une preuve est acceptée lorsqu’elle passe les vérifications de Lean pour l’énoncé formel fourni. La configuration complète ajoute une recherche évolutionnaire, qui sélectionne et fait évoluer plusieurs esquisses, et peut appeler AlphaProof pour travailler sur des sous-objectifs.
Ce que mesurent les résultats
Les deux résultats portent sur des ensembles distincts, avec leurs propres critères et dénominateurs.
| Ensemble évalué | Problèmes ou conjectures démontrés | Éléments évalués | Périmètre |
| Problèmes d’Erdős | 9 | 353 | Énoncés formalisés disponibles dans le dépôt Formal Conjectures au moment de l’évaluation |
| Conjectures de l’OEIS | 44 | 492 | Conjectures ouvertes sélectionnées pour l’étude |
Deux des neuf problèmes d’Erdős résolus étaient ouverts depuis 56 ans. Les 353 énoncés formaient un sous-ensemble formalisé du catalogue plus vaste des problèmes d’Erdős ; ils ne représentaient pas l’ensemble de ce catalogue.
Comment fonctionne la recherche de preuves
Dans la configuration de base, des agents fondés sur des modèles de langage révisent des esquisses de preuve par modifications successives. Lean compile les propositions et fournit le retour qui oriente les tentatives suivantes. La configuration complète organise en plus un ensemble partagé d’esquisses, les classe pour en sélectionner certaines et peut solliciter AlphaProof sur des sous-problèmes.
Cette architecture associe la génération de pistes, qui peut produire des erreurs, à un vérificateur formel qui contrôle les preuves soumises. C’est ce contrôle mécanique qui donne aux résultats leur portée précise : il porte sur un énoncé écrit en Lean.
Ce que les résultats montrent
Lean vérifie qu’une preuve établit l’énoncé formalisé. Cette vérification ne suffit pas à elle seule à garantir que l’énoncé traduit fidèlement la question mathématique informelle d’origine. Pour les problèmes d’Erdős, les auteurs de l’étude rapportent une validation experte des formalisation utilisées.
Les auteurs indiquent aussi que la plupart des problèmes d’Erdős évalués restent irrésolus et que les réussites se concentrent dans des domaines où les bibliothèques mathématiques de Lean sont mûres, notamment la combinatoire, l’optimisation convexe et la théorie des nombres.
