Claude de Anthropic completó de forma autónoma la primera demostración formal verificada por ordenador del Último Teorema de Fermat utilizando Lean. Durante 11 días, la IA generó 13 millones de líneas de código y 30.300 teoremas mediante colaboración multiagente. El sistema formalizó la demostración de Andrew Wiles de 1995, que luego fue verificada por Lean utilizando únicamente tres axiomas. Este hito demuestra la capacidad de la IA para la formalización matemática a gran escala, lo que podría reducir los costes de verificación manual y establecer un nuevo estándar para combinar la supervisión humana con la generación automatizada de demostraciones.