Neuf preuves de DeepMind, nouveauté à vérifier

L’agent AlphaProof Nexus de Google DeepMind a produit des preuves pour neuf problèmes d’Erdős et 44 conjectures, toutes vérifiées par Lean. Mais établir la validité d’une démonstration ne suffit pas à savoir si elle apporte quelque chose de nouveau.

Une démonstration peut être élégante tout en dissimulant une faille que personne ne repère pendant des années. L’agent d’IA AlphaProof Nexus a produit des preuves pour neuf problèmes posés par Paul Erdős, et un logiciel en a vérifié chaque étape. Présenté dans une prépublication en mai (arXiv), le travail a été publié après évaluation par les pairs dans Science, le 8 octobre (Science). Le logiciel pouvait confirmer la logique ; aux mathématiciens revenait de déterminer si elle apportait du neuf.

Un arbitre que l’éloquence ne convainc pas

Les agents conversationnels savent produire des raisonnements mathématiques qui semblent justes. Une formulation assurée peut masquer une étape manquante, que seul un lecteur attentif repérera. AlphaProof Nexus réduit ce risque en travaillant avec Lean, un langage de programmation qui permet de formuler définitions, énoncés et démonstrations avec assez de précision pour qu’un ordinateur les vérifie.

On peut voir Lean comme un arbitre qui examine chaque ligne d’une démonstration achevée et applique des règles fixes. Le style ne compte pas : si une étape ne découle pas des précédentes, la preuve échoue, même si tout le reste est élégant.

L’équipe décrit l’agent comme un système qui cherche des démonstrations écrites en Lean. Les chercheurs lui ont aussi donné accès à AlphaProof, un système antérieur de DeepMind conçu spécialement pour les preuves. Or, dans leurs essais, une configuration plus simple a obtenu les mêmes résultats : un modèle de langage associé à Lean, sans AlphaProof, a lui aussi trouvé les neuf preuves d’Erdős (The Decoder). Pour ces problèmes, le composant spécialisé n’était donc pas nécessaire.

L’article fait état de preuves acceptées pour les neuf énoncés d’Erdős et pour 44 conjectures — des affirmations tenues pour vraies mais pas encore démontrées — tirées de l’Online Encyclopedia of Integer Sequences, un vaste catalogue de suites de nombres (Science). Parmi les résultats d’Erdős figure une question en deux parties sur les nombres entiers, posée en 1970 par Erdős et András Sárközy. Elle est restée considérée comme ouverte pendant plus d’un demi-siècle (ABC).

Ce que l’arbitre ne peut pas voir

La garantie de Lean a une limite précise : elle confirme qu’une preuve établit bien l’énoncé tel qu’il est écrit dans le code. Trois questions lui échappent : le code correspond-il à ce qu’Erdős voulait dire ? Quelqu’un avait-il déjà répondu à la question ? Et cette réponse apporte-t-elle quelque chose aux mathématiques ?

Le problème de 1970 montre pourquoi les deux dernières questions comptent. Sa seconde partie implique la première : une seule preuve suffit donc à régler les deux. Après la diffusion des démonstrations de l’agent, des chercheurs ont constaté qu’une légère modification d’une construction de l’article original de 1970 permettait elle aussi de répondre aux deux questions (arXiv). Les preuves de l’agent étaient correctes ; l’étiquette « ouverte » masquait simplement un problème plus proche de sa résolution qu’on ne le pensait.

Repérer ce genre de nuance suppose de connaître le domaine. Gergely Bérczi, mathématicien à Aarhus University, au Danemark, et coauteur de l’étude, a contribué au choix des problèmes et à la validation des solutions (Aarhus University). Il a aussi aidé à rédiger des versions des preuves accessibles aux lecteurs. Lean certifiait chaque étape ; Bérczi et ses collègues jugeaient ce que l’ensemble apportait.

Cette répartition du travail distingue l’étude d’un résultat présenté le mois précédent : Claude, le modèle d’Anthropic, avait alors formalisé dans Lean une démonstration déjà connue du dernier théorème de Fermat (To Brief). La formalisation d’une preuve célèbre ne soulève pas de doute sur sa nouveauté. En revanche, une recherche parmi des énoncés réputés ouverts pose précisément cette question, qui devient alors centrale.

L’équipe a publié les fichiers des démonstrations afin que d’autres puissent les soumettre au même arbitre (GitHub). Le résultat est précis : un agent d’IA a produit des preuves vérifiables par ordinateur pour des énoncés que les mathématiciens tenaient pour ouverts, tels qu’ils sont formulés dans Lean. Il revenait encore aux mathématiciens qui les lisaient de déterminer ce que ces preuves ajoutaient aux connaissances.