Anthropic affirme que Claude a rédigé la première preuve vérifiée par ordinateur du dernier théorème de Fermat

Anthropic a annoncé jeudi que son modèle d'IA Claude a complété la première preuve de bout en bout, vérifiée par ordinateur, du dernier théorème de Fermat, l'un des résultats les plus célèbres en mathématiques. Travaillant de manière largement autonome pendant 11 jours, Claude a rédigé la preuve dans le langage de programmation Lean, produisant 13 millions de lignes de code et prouvant 29 500 théorèmes intermédiaires en cours de route.anthropic+1

Un sprint de 11 jours à travers des siècles de mathématiques

Le dernier théorème de Fermat stipule qu'aucun entier positif a, b et c ne satisfait l'équation aⁿ + bⁿ = cⁿ pour tout entier n supérieur à 2. Conjecturé pour la première fois par Pierre de Fermat vers 1637, il n'a été prouvé qu'en 1995, lorsque Andrew Wiles a publié une preuve de 129 pages ayant nécessité des mois d'examen par des experts pour être vérifiée.anthropic

La formalisation de cette preuve, c'est-à-dire sa réécriture pour qu'un ordinateur puisse vérifier chaque étape logique, devait prendre des années. Kevin Buzzard, mathématicien à l'Imperial College de Londres qui dirige un effort indépendant pour formaliser ce théorème en utilisant Lean, a confirmé que le code compile et est correct. Dans un article de blog vendredi, Buzzard a qualifié cela d'"exploit extraordinaire d'auto-formalisation" et a noté que la preuve est "multicouche", couvrant l'algèbre, l'analyse harmonique, la géométrie et la théorie des nombres.xenaproject.wordpress+1

La preuve de Claude suit l'exposition de Darmon-Diamond-Taylor de l'argument de Wiles-Taylor-Wiles, une version simplifiée de la preuve originale. L'intervention humaine s'est limitée à des instructions occasionnelles de haut niveau du chercheur d'Anthropic, Tianyi Peng, dont l'équipe à l'Université Columbia a construit la plateforme Prove2Me qui a permis cet effort.anthropic+1

Comment la preuve a été construite

Plusieurs tentatives initiales ont échoué car les agents de Claude perdaient le fil de l'état du projet et cessaient de collaborer efficacement. La percée est survenue lorsque l'équipe est passée à Prove2Me, une plateforme collaborative ouverte qui maintient un graphe dirigé des énoncés de théorèmes, permettant à plusieurs agents de travailler en parallèle et de décider quelles preuves tenter ensuite. En utilisant un système multi-agents basé sur Claude Code, des dizaines d'agents ont consommé environ six milliards de jetons de sortie provenant d'un modèle de recherche interne qu'Anthropic décrit comme comparable à Claude Fable 5.1.siliconangle+1

La preuve terminée a été vérifiée par Lean en utilisant uniquement ses trois axiomes standards, et un comparateur a confirmé que l'énoncé du théorème correspond à la propre formulation du théorème dans Mathlib. Avec 13 millions de lignes, elle est plus de cinq fois plus grande que Mathlib, la principale bibliothèque communautaire de mathématiques formalisées.anthropic+1

Ce que cela signifie pour les mathématiques

Buzzard, qui a été informé du résultat par e-mail alors qu'il était dans un festival de musique et qui avait pris l'expéditeur pour un plaisantin, a écrit que cet accomplissement marque une nouvelle ère : "Si la formalisation automatique du théorème est possible maintenant, alors nous avons fait un grand pas vers la formalisation automatique de la littérature mathématique moderne". Il a noté que de telles techniques pourraient éliminer les erreurs dans le corpus mathématique existant et alléger la charge des relecteurs évaluant les nouveaux travaux.anthropic+1

Cette étape fait suite à une série d'avancées en mathématiques pilotées par l'IA. Anthropic a utilisé Claude le mois dernier pour découvrir de nouvelles informations sur la fonction zêta de Riemann, tandis que son rival OpenAI a utilisé son dernier modèle pour résoudre plusieurs problèmes d'Erdős. Anthropic a également utilisé récemment Claude pour réfuter la conjecture jacobienne en trois dimensions et plus. Buzzard, pour sa part, a fait une remarque typiquement sobre : "On m'a donné 1 million de livres sterling pour mener mon projet sur 5 ans ; Anthropic n'a pris que 11 jours, mais je me demande s'ils ont dépensé plus d'argent".xenaproject.wordpress+2