Anthropic affirme que Claude a accompli la première preuve formelle complète du dernier théorème de Fermat. Il ne s'agit pas de redécouvrir ce théorème, mais de retranscrire la preuve existante en code logique vérifiable ligne par ligne par un ordinateur. L'entreprise indique que ce travail a pris 11 jours et a généré environ 13 millions de lignes.
La signification de la preuve formelle réside dans la transcription d'arguments mathématiques dans un langage vérifiable par machine. Les preuves traditionnelles publiées dans des articles nécessitent souvent une révision prolongée par des pairs ; si une étape intermédiaire présente une faille, le processus de correction peut durer des mois, voire des années. Le grand théorème de Fermat a été démontré par le mathématicien britannique Andrew Wiles en 1995, mais convertir entièrement cette preuve en une version vérifiable par machine a longtemps été considéré comme un projet d'ingénierie intensif.
11 jours pour atteindre l'objectif à long terme
Le mathématicien de l'Imperial College London, Kevin Buzzard, a lancé le projet en 2024, avec pour objectif de retranscrire la démonstration de Wiles dans l'assistant de preuve Lean. Selon le plan initial, ce travail nécessite une collaboration à long terme, et les financements sont prévus jusqu'en 2029.
Anthropic affirme que Claude a accompli plus tôt que prévu les objectifs similaires. Après examen par Buzzard, il a été constaté que cette preuve peut être établie sans recourir à des hypothèses supplémentaires, c'est-à-dire en s'appuyant uniquement sur le système d'axiomes les plus fondamentaux des mathématiques.
Effectué en parallèle par plusieurs agents
Selon Anthropic, l'équipe de Tianyi Peng de l'Université Columbia a fait travailler plusieurs agents Claude en parallèle, chacun chargé d'écrire des définitions et de démontrer des conclusions plus petites, puis de les assembler progressivement pour former des structures de preuve plus grandes. L'intervention humaine était minimale et consistait principalement à définir des ordres de priorité intermédiaires.
Les progrès initiaux n'ont pas été faciles. Anthropic a indiqué que certains agents étaient momentanément incapables de partager le contenu terminé et redoublaient parfois leurs efforts. Par la suite, l'équipe a utilisé un outil appelé Prove2Me pour fournir à chaque agent une liste de tâches unifiée et une organisation des fichiers cohérente, tout en conservant des commentaires en langage naturel afin de faciliter la réutilisation des résultats des autres agents.
- Plus de 30 000 théorèmes de soutien
- La consommation totale atteint des milliards de tokens
- En fin de compte, environ 13 millions de lignes
Focus on verifiability rather than new theorems
L'accent de ce résultat ne repose pas sur la découverte de nouveaux théorèmes mathématiques, mais sur la transformation de preuves majeures existantes en versions vérifiables étape par étape par un ordinateur. Avec l'augmentation des articles mathématiques et des contenus générés par l'IA, le coût de la vérification manuelle des preuves augmente également, ce qui accroît l'intérêt pour les outils de formalisation.
Anthropic a également déclaré que cette preuve dépasse de plus de cinq fois la taille de la bibliothèque partagée couramment utilisée dans la communauté mathématique, Mathlib. Le fichier complet a été téléchargé sur GitHub, permettant aux chercheurs de continuer à examiner ligne par ligne sa structure et sa correction.