Nous partageons la première preuve complète vérifiée par ordinateur du dernier théorème de Fermat. Claude a travaillé en grande partie de manière autonome pendant 11 jours pour écrire la preuve dans le langage de programmation Lean. Ci-dessous, nous décrivons comment la formalisation a été réalisée et partageons quelques réflexions sur ce que ce travail pourrait signifier pour les mathématiques de recherche.

Vers 1637, Pierre de Fermat a noté une affirmation dans la marge de son exemplaire de l'Arithmétique de Diophante qui deviendrait l'une des conjectures mathématiques les plus célèbres de tous les temps : aucun entier positif a, b, c ne satisfait aⁿ + bⁿ = cⁿ pour tout n > 2. Le dernier théorème de Fermat (FLT), comme la conjecture est devenue connue, s'est avéré incroyablement difficile à prouver. La première preuve, de Sir Andrew Wiles en 1995, comptait 129 pages et a nécessité des mois de travail minutieux pour être vérifiée.

Une décennie plus tard, l'informaticien néerlandais Jan Bergstra a proposé de « formaliser » la preuve de Wiles : convertir le raisonnement mathématique en une forme que les ordinateurs peuvent vérifier automatiquement. Depuis lors, les mathématiciens développent les méthodes nécessaires pour encoder une preuve aussi complexe, y compris un effort communautaire pluriannuel lancé en 2024 par Kevin Buzzard à l'Imperial College de Londres pour achever la formalisation à l'aide de l'assistant de preuve Lean.

Récemment, Tianyi Peng, chercheur chez Anthropic dont le groupe à l'Université de Columbia construit des outils pour la formalisation par IA, a entrepris de tester si Claude pouvait progresser dans la formalisation de FLT. Le résultat est allé plus loin qu'il ne l'espérait. En 11 jours, travaillant en grande partie de manière autonome, Claude a produit la première preuve de FLT de bout en bout, vérifiée par ordinateur. En cours de route, il a écrit 13 millions de lignes de Lean et prouvé 29 500 théorèmes intermédiaires.