Le dernier théorème de Fermat formalisé par des agents IA en onze jours

En onze jours seulement, des agents de l'intelligence artificielle Claude, développés par Anthropic, ont produit la première démonstration informatiquement vérifiée du dernier théorème de Fermat, une prouesse que la communauté mathématique estimait nécessiter plusieurs années de travail collectif.

Rappelons le contexte : vers 1637, le mathématicien français Pierre de Fermat avait griffonné dans la marge d'un livre qu'il n'existe aucun triplet d'entiers positifs vérifiant l'équation an + bn = cn pour un exposant n supérieur à 2, en précisant détenir une « merveilleuse démonstration » que la marge était trop étroite pour contenir. Ce défi est resté sans réponse pendant plus de trois siècles. En 1995, le mathématicien britannique Andrew Wiles en publia enfin une preuve, longue de 129 pages, qui avait elle-même failli échouer : un défaut critique y avait été découvert dès 1993, obligeant Wiles et son collaborateur Richard Taylor à travailler une année supplémentaire avant de le corriger.

Vérifier une telle démonstration à la main est long et faillible. C'est pourquoi les mathématiciens recourent de plus en plus à des « assistants de preuve » comme Lean, un logiciel capable de contrôler chaque étape d'un raisonnement mathématique avec la rigueur d'une machine, à condition que la preuve soit entièrement traduite dans son langage — un processus appelé formalisation. Cette traduction est particulièrement laborieuse : là où une preuve humaine omet les étapes « évidentes », Lean exige que chacune soit explicitée. Depuis 2024, une équipe menée par Kevin Buzzard à l'Imperial College de Londres s'attaquait à cette formalisation dans le cadre d'un effort collaboratif pluriannuel.

L'équipe de Tianyi Peng, chercheur chez Anthropic et professeur assistant à l'université Columbia, a décidé de tester si Claude pouvait accélérer ce travail. Le résultat a largement dépassé les attentes : en onze jours, plusieurs dizaines d'agents Claude ont collaboré de manière quasi autonome, produisant 13 millions de lignes de code Lean et démontrant 30 300 théorèmes intermédiaires — dont 29 500 retenus dans la preuve finale. Ce volume représente plus de cinq fois la taille de Mathlib, la principale bibliothèque communautaire de mathématiques formalisées. L'intervention humaine s'est limitée à quelques instructions de haut niveau, du type « accorder la priorité au théorème de Mazur ».

La clé du succès résidait dans l'utilisation de Prove2Me, une plateforme collaborative open source conçue par Peng et ses collaborateurs, qui a permis aux agents de coordonner efficacement leurs efforts. Les premières tentatives s'étaient en effet soldées par un échec : les agents perdaient le fil du projet et cessaient de coopérer. Kevin Buzzard, dont l'équipe travaillait sur le même chantier, a qualifié le résultat d'« extraordinaire », soulignant que la preuve ne repose que sur les axiomes fondamentaux des mathématiques et couvre des domaines aussi variés que l'algèbre, la géométrie, l'analyse harmonique et la théorie des nombres.

Au-delà de l'exploit symbolique, Anthropic voit dans cette réalisation un modèle pour l'avenir : systématiser la vérification formelle des preuves générées par l'IA afin de décharger les experts humains d'un travail de contrôle qui peut prendre des années, sans pour autant remplacer les démonstrations lisibles par les mathématiciens.