Théorème de Fermat : Claude le formalise en onze jours

En juillet dernier, un prix Nobel de physique avait raconté s'être fait aider par l'intelligence artificielle Claude pour résoudre un problème de physique. Anthropic annonce à présent qu'un modèle expérimental de Claude a formalisé en onze jours, dans le langage Lean, la démonstration du dernier théorème de Fermat. Il s'agit de la traduction d'une démonstration mathématique complexe en un code qu'un ordinateur peut vérifier étape par étape.

Pour parvenir à ce résultat, Claude a généré environ 13 millions de lignes de code et 30 300 théorèmes intermédiaires. La comparaison avec le travail humain donne la mesure de l'exploit : le projet dirigé par le mathématicien Kevin Buzzard pour formaliser entièrement le théorème avait été estimé à environ dix ans.

Le dernier théorème de Fermat a été formulé en 1637 par Pierre de Fermat. Il affirme que, pour tout entier n supérieur à 2, l'équation xⁿ + yⁿ = zⁿ n'admet aucune solution entière positive non nulle. Le problème est resté non résolu pendant plus de trois siècles, jusqu'à la démonstration d'Andrew Wiles dans les années 1990, complétée par la contribution de Richard Taylor.

Ce que Claude a réellement accompli

Le travail de l'intelligence artificielle ne consiste pas à avoir trouvé une nouvelle démonstration : celle de Wiles reste valable et n'a pas été remise en cause. Claude a plutôt transformé la démonstration existante en une séquence formelle d'étapes qu'un ordinateur peut contrôler. C'est précisément la fonction de Lean, le langage et l'environnement utilisés pour formaliser les mathématiques.

Le résultat comporte toutefois une limite. Le code produit par l'intelligence artificielle ne peut pas encore être intégré à Mathlib, la bibliothèque de référence utilisée par la communauté scientifique pour les mathématiques formelles. La formalisation est donc achevée, mais elle n'est pas encore prête à entrer durablement dans l'écosystème partagé par les mathématiciens.

L'expérience indique néanmoins une direction pour l'intelligence artificielle appliquée aux mathématiques : ne pas se limiter à fournir des réponses, mais construire des démonstrations vérifiables de manière formelle. Le prochain défi, selon l'annonce, consistera à rendre ces résultats non seulement rapides à obtenir, mais aussi lisibles et réutilisables par les mathématiciens.