Anthropic a vu Claude achever de manière autonome la première preuve formelle de la conjectation de Fermat vérifiée par un ordinateur en utilisant Lean. Pendant 11 jours, l'IA a généré 13 millions de lignes de code et 30 300 théorèmes grâce à une collaboration multi-agents. Le système a formalisé la preuve d'Andrew Wiles de 1995, qui a ensuite été vérifiée par Lean en utilisant seulement trois axiomes. Cette étape importante démontre la capacité de l'IA à effectuer une formalisation mathématique à grande échelle, réduisant potentiellement les coûts de vérification manuelle et établissant une nouvelle norme pour combiner la supervision humaine avec la génération automatique de preuves.