Un bond dans la preuve formelle assistée par IA

Des chercheurs issus de plusieurs institutions (dont les noms figurent sur le document déposé sur arXiv) présentent une évaluation inédite de l’utilisation de grands modèles de langage (LLM) combinés à un vérificateur formel pour résoudre des problèmes mathématiques ouverts. Leur agent le plus performant est parvenu à démontrer neuf des 353 problèmes non résolus de la collection d’Erdős — un ensemble de défis posés par le mathématicien hongrois Paul Erdős — ainsi que 44 conjectures issues de l’Encyclopédie en ligne des suites de nombres entiers (OEIS). Le coût par problème est estimé à quelques centaines de dollars.

Fonctionnement de l’agent

L’approche repose sur un cycle alternant génération de preuves par un LLM et vérification automatique via le langage de preuve formelle Lean. Un agent simple appliquant cette boucle de base a reproduit les succès obtenus sur les problèmes d’Erdős, mais avec un coût plus élevé pour les défis les plus difficiles. Les auteurs qualifient l’agent le plus performant de « plus capable » et précisent qu’il est déjà déployé dans des domaines tels que la combinatoire, l’optimisation, la théorie des graphes, la géométrie algébrique et la recherche en optique quantique.

Contexte et portée

Les grands modèles de langage montrent des capacités croissantes en raisonnement mathématique, mais leur manque de fiabilité (hallucinations, erreurs logiques) limite leur usage direct en recherche. La vérification formelle dans Lean permet de certifier chaque étape d’une preuve, éliminant ce risque. Cette étude constitue la première évaluation à grande échelle de cette méthode sur des problèmes vraiment ouverts — non pas des exercices ou des problèmes déjà résolus, mais des questions anciennes sur lesquelles les mathématiciens butent depuis des décennies.

Implications

Ces résultats suggèrent que l’IA peut désormais contribuer directement à l’avancement des mathématiques fondamentales, en accélérant très fortement la recherche de preuves et en réduisant les coûts. Le fait que neuf problèmes d’Erdős sur 353 aient été résolus en quelques mois (ou années d’effort algorithmique) montre que la méthode est opérationnelle. Les auteurs notent que l’agent est actuellement en usage dans plusieurs branches des mathématiques, élargissant le champ de la preuve formelle assistée au-delà de la simple vérification de théorèmes connus.

Limites et perspectives

L’article ne précise pas quels problèmes d’Erdős ont été résolus, ni la date exacte de soumission (21 mai 2026). Toutefois, le dépôt sur arXiv rend l’étude accessible à la communauté scientifique. Les auteurs soulignent que l’agent simple, bien que moins efficace, démontre la robustesse de l’approche. La recherche ouvre la voie à des assistants mathématiques capables de proposer des conjectures et de les prouver formellement, transformant potentiellement la pratique de la recherche en mathématiques.

Équipe et contributions

Les premiers auteurs (George Tsoukalas, Anton Kovsharov, Sergey Shirobokov) et le dernier auteur (Swarat Chaudhuri) ont contribué de manière équitable, selon la note des auteurs. Les 19 coauteurs incluent des chercheurs de Google DeepMind (Pushmeet Kohli, Aja Huang) et d’autres institutions. Le code et les données associées à l’article sont disponibles en ligne, et la licence de l’article est Creative Commons BY-NC-ND 4.0.