Claude formalise la preuve du dernier théorème de Fermat

Anthropic a annoncé le 4 septembre que ses modèles Claude avaient formalisé une preuve complète et vérifiable par ordinateur du dernier théorème de Fermat, une tâche que la communauté mathématique estimait nécessiter plusieurs années de travail humain.

Le projet, dirigé par le chercheur Tianyi Peng, a mobilisé des dizaines d'agents Claude travaillant en parallèle sur Prove2Me, une plateforme de traduction d'arguments mathématiques dans le langage de preuve Lean. En 11 jours, les agents ont produit environ 13 millions de lignes de code Lean, démontrant environ 29 500 théorèmes intermédiaires, une formalisation environ cinq fois plus grande que l'ensemble de la bibliothèque mathématique existante de Lean, Mathlib. Anthropic a indiqué que ce travail avait consommé environ 6 milliards de tokens de sortie d'un modèle de recherche interne à usage général, aux capacités comparables à Claude Fable 5.1.

Le dernier théorème de Fermat, énoncé pour la première fois en 1637, affirme qu'aucun triplet d'entiers positifs ne peut satisfaire l'équation a^n + b^n = c^n pour un entier n supérieur à 2. Andrew Wiles l'a démontré en 1995 après des années de travail, mais sa preuve, comme la plupart des mathématiques avancées, était rédigée en langage naturel et reposait sur les lecteurs et relecteurs pour repérer les erreurs. La formalisation convertit ce raisonnement dans une forme qu'un assistant de preuve comme Lean peut vérifier ligne par ligne, en n'utilisant que les trois axiomes logiques standard de Lean, supprimant toute dépendance à une relecture humaine pour confirmer l'exactitude.

Pourquoi maintenant : Anthropic a publié la formalisation sur GitHub et a indiqué qu'un outil de comparaison indépendant avait confirmé que l'énoncé final du théorème correspond à la formulation mathématique standard, répondant à une crainte courante qu'un système d'IA formalise un énoncé plus facile et subtilement différent de celui qu'il prétend démontrer.

Pourquoi c'est important : Kevin Buzzard, mathématicien à l'Imperial College de Londres et voix marquante de la communauté de la formalisation, a déclaré que ce résultat montre que l'autoformalisation réussit désormais en algèbre, analyse harmonique, géométrie et théorie des nombres, et non plus seulement sur des problèmes isolés et simples. Vérifier à la main une preuve mathématique majeure peut prendre des années aux mathématiciens, comme ce fut le cas pour le travail original de Wiles. Si les systèmes d'IA peuvent convertir de manière fiable des preuves humaines denses en formalisations vérifiables par machine, cela pourrait offrir au domaine un moyen plus rapide et plus fiable de confirmer l'exactitude de nouveaux résultats, et permettre aux systèmes d'IA de s'attaquer à des problèmes non résolus avec des résultats que d'autres mathématiciens peuvent vérifier rapidement plutôt que de se fier à la seule réputation.

Divulgation : le processus éditorial de NewUJ utilise les modèles Claude d'Anthropic.