Claude d'Anthropic réalise une preuve formelle du dernier théorème de Fermat en 11 jours

Le modèle d'IA d'Anthropic, Claude, a atteint un jalon significatif en formalisant de manière autonome le dernier théorème de Fermat en un remarquable délai de 11 jours. Cet accomplissement a nécessité la génération de 13 millions de lignes de code Lean et la vérification de 29 500 théorèmes intermédiaires, une tâche qui était auparavant censée prendre des années.

Le théorème, initialement proposé par Pierre de Fermat en 1637, stipule qu'aucun trio d'entiers positifs a, b et c ne peut satisfaire l'équation a^n + b^n = c^n pour toute valeur entière de n supérieure à 2. Bien qu'Andrew Wiles ait prouvé le théorème en 1995, la formalisation de Claude traduit cette preuve dans un format vérifiable par machine, garantissant que chaque étape logique est codée et vérifiée indépendamment par un ordinateur.

Cette formalisation repose sur les bases solides établies par la communauté de la preuve interactive, en particulier les efforts continus de Kevin Buzzard au Imperial College de Londres. Le travail de Claude suit l'approche moderne de la courbe de Frey et du relèvement de modularité, qui se distingue des méthodes antérieures et met en lumière le potentiel de l'IA à assister dans le raisonnement mathématique rigoureux.

Les implications de cet accomplissement vont au-delà des mathématiques, car il démontre la capacité de l'IA à gérer des tâches de raisonnement logique complexes qui dépassent les références traditionnelles. Les observateurs notent que ce succès pourrait améliorer la position concurrentielle d'Anthropic dans le paysage de l'IA, les prix du marché reflétant une confiance accrue dans les capacités de Claude.

En regardant vers l'avenir, la communauté mathématique aspire à un futur où chaque théorème majeur dispose d'une preuve vérifiée par machine, réduisant ainsi le risque d'erreur humaine dans les preuves acceptées. L'accomplissement de Claude est un pas vers la réalisation de cette vision, bien que l'écart entre la formalisation des preuves existantes et la découverte de nouvelles reste significatif.