En 11 jours, les agents de Claude ont produit la première version entièrement vérifiée par ordinateur de la preuve du dernier théorème de Fermat. Cela a été rapporté le 4 septembre dans Anthropic.
Vérifier qu’une preuve mathématique majeure est correcte peut prendre des années. La formalisation, c'est-à-dire la conversion du raisonnement mathématique en une forme que des assistants informatiques comme Lean peuvent vérifier, peut aider.
Le mois dernier, Claude a complété la première preuve formalisée du dernier théorème de Fermat, l'un des… pic.twitter.com/pdT8zwlV4A
– Anthropique (@AnthropicAI) 4 septembre 2026
Le dernier théorème de Fermat déclare : l'égalité aⁿ + bⁿ = cⁿ est impossible pour les entiers positifs a, b et c pour les entiers n supérieurs à deux. Pierre Fermat a formulé cette affirmation en 1637.
Le résultat concerne une formalisation d'une preuve déjà connue publiée par Andrew Wiles en 1995. Claude a traduit le raisonnement mathématique en code que le système de vérification de la preuve Maigre peut vérifier étape par étape.
Comment fonctionnaient les agents de Claude ?
L'expérience a été organisée par le chercheur Anthropic Tianyi Peng, dont le groupe de l'Université de Columbia développe des outils pour formaliser les mathématiques. Selon le rapport technique, les gens ont précisé le théorème cible et parfois les priorités.
Les agents ont rédigé indépendamment des déclarations intermédiaires, vérifié les formulations de chacun et construit des preuves.
Le système utilisait la bibliothèque Mathlib et le matériel de l'Imperial College London FLT et des projets flt-regular. Dans le code final, 106 fichiers sont adaptés des deux derniers projets avec attribution.
La plateforme Prove2Me a aidé à coordonner les agents. L'article de ses développeurs décrit le principe de la collaboration : un gros problème est divisé en énoncés intermédiaires liés, et les participants ajoutent des preuves et utilisent les résultats déjà obtenus. La structure globale permet à plusieurs agents de travailler en parallèle.
Selon Anthropic, Claude a prouvé environ 30 300 théorèmes intermédiaires, dont environ 29 500 ont été inclus dans l'ouvrage final. Le volume de code a atteint 13 millions de lignes.
L'entreprise a qualifié le résultat de la plus grande preuve de Lean, précisant que le code est probablement beaucoup plus long que nécessaire.
L'expérience a utilisé un modèle de recherche interne à peu près comparable à Claude Fable 5.1. Le travail a nécessité environ 6 milliards de jetons de sortie.
Comment vérifier le résultat
Le code complet et les instructions de revalidation sont publiés sur GitHub. Selon la documentation, la preuve a été vérifiée par Lean et le noyau de vérification indépendant nanoda. L'outil de comparaison a confirmé que l'énoncé final correspond à la formulation du théorème de Fermat de Mathlib.
Les auteurs ont également établi que la preuve utilise uniquement les trois axiomes Lean standards et ne contient pas de bouts non prouvés. Le référentiel précise : la fiabilité du résultat présuppose la confiance dans les programmes de vérification.
Kevin Buzzard, mathématicien de l'Imperial College de Londres, qui dirige son propre projet pour formaliser le théorème, a confirmé séparément le résultat sur son blog.
« J'ai compilé la base de code et exécuté le comparateur dessus et le test a réussi », a-t-il écrit.
Buzzard a associé l'importance de l'œuvre aux possibilités de formalisation automatique. Selon lui, de tels outils permettront de vérifier les articles scientifiques et d'identifier les lacunes du raisonnement.
Le chercheur poursuivra son propre projet. En plus de la formalisation, ses objectifs incluent l'expansion de Mathlib et la création d'un document qui permettra aux utilisateurs d'étudier la version moderne de la preuve. Claude a travaillé en décrivant une approche antérieure.
Rappelons qu'en juillet, Claude Mythos Preview a aidé les chercheurs d'Anthropic à trouver des attaques cryptanalytiques sur le schéma de signature post-quantique HAWK et une version raccourcie à sept tours d'AES-128. Le résultat AES ne s’appliquait pas à la version complète à dix tours du chiffre.
Vous avez trouvé une erreur dans le texte ? Sélectionnez-le et appuyez sur CTRL+ENTRÉE
Voir l’article original en russe
