Ce que dit l’article
Une équipe de Google DeepMind a publié un compte rendu évalué par les pairs d’un système d’IA qui trouve des démonstrations mathématiques et les fait vérifier par la machine au fil de l’eau. L’article, “Advancing Mathematics Research with AI-Driven Formal Proof Search”, de Tsoukalas et ses collègues, est paru dans Science le 8 octobre.
Le système, AlphaProof Nexus, est bâti autour de Gemini 3.1 Pro. Il rédige une démonstration en Lean, un langage formel où chaque étape logique est vérifiée par un logiciel, et les messages d’erreur du vérificateur orientent le brouillon suivant. Pour les sous-problèmes plus coriaces, il peut passer la main à AlphaProof, l’outil spécialisé de DeepMind.
Les chercheurs ont retenu 353 problèmes ouverts de la collection d’Erdős et les ont encodés en Lean. Le système en a clos neuf — environ 2,5 % — dont deux restaient ouverts depuis 56 ans. Il a aussi démontré 44 conjectures de l’Encyclopédie en ligne des suites d’entiers, tranché une question ouverte de géométrie algébrique et amélioré une borne connue en optimisation min-max, une technique employée pour entraîner certains modèles d’IA.
L’ablation est la partie intéressante
DeepMind indique que le système a résolu les mêmes neuf problèmes d’Erdős sans AlphaProof. Une analyse d’ablation montre qu’une configuration plus simple, que l’article appelle Agent A, atteint les mêmes neuf, un point soulevé par Josep Curto, de l’Université ouverte de Catalogne, dans les commentaires d’experts réunis par le Science Media Centre España. Curto y voit un signe de sur-ingénierie et soutient que l’article comporte des incohérences méthodologiques.
Son objection la plus tranchante porte sur ce que la vérification formelle garantit et ne garantit pas. Lean, relève-t-il, assure qu’une démonstration est logiquement valide. Il n’assure pas que l’énoncé formalisé soit bien le problème que l’on voulait poser. La traduction d’une conjecture informelle vers Lean reste une étape humaine, et une erreur à cet endroit traverse le vérificateur intacte.
Comment lire neuf sur 353
Le dénominateur compte. Ce sont neuf succès sur un ensemble défini que l’équipe a choisi et formalisé, et non une capacité générale à abattre des conjectures célèbres. Pablo Haya Coll, de l’Université autonome de Madrid, dans le même ensemble de commentaires, pointe la méthode plutôt que le compte : la valeur tient à une manière reproductible de produire des découvertes mathématiques, pas aux neuf eux-mêmes.
Javier Aramayona, qui dirige l’Institut espagnol des sciences mathématiques, soulève le problème qui découle de démonstrations vérifiées arrivant plus vite que quiconque ne les lit : beaucoup de résultats produits par IA sont vérifiés sans être pleinement compris. Teodoro Calonge, de l’Université de Valladolid, y voit un article de grande qualité et une tentative précoce, avec une marge de progrès considérable.
Le contraste avec l’autre laboratoire
Le chemin emprunté par ce travail fait partie de l’histoire. DeepMind a publié les solutions d’Erdős avant la parution de l’article, puis a soumis le travail à l’évaluation par les pairs. OpenAI a pris l’autre chemin, en déposant des centaines de démonstrations produites par IA sur un dépôt, ce qui a conduit un groupe de mathématiciens à appeler au boycott de l’entreprise plus tôt ce mois-ci.
Ce qu’il faut surveiller, c’est si les fichiers Lean résistent à l’examen extérieur, et si l’une des neuf formalisations énonce finalement autre chose que le problème d’Erdős dont elle porte l’étiquette. Cette vérification est désormais à la portée de tous, ce qui est l’argument pratique en faveur de la voie choisie par DeepMind.
