Anthropic publicó el 4 de septiembre una formalización verificada por máquina de el último teorema de Fermat en Lean 4; la API de GitHub sitúa la creación del repositorio a las 14:21:04 UTC. La afirmación que circuló fue que Claude demostró el último teorema de Fermat en 11 días. Los propios archivos del repositorio describen algo más limitado y, en un sentido, más interesante.
Lo que dice el archivo de atribución
El repositorio incluye un ATTRIBUTION.md que registra 106 archivos con material del proyecto FLT de Imperial College London, liderado por Kevin Buzzard, y del proyecto flt-regular — "54 en Definitions/, 52 en P2M/Sol/; y los 23 archivos que reproducen texto de Mathlib". Decenas de filas indican "whole file (100%)". El archivo NOTICE fecha el préstamo: "Material was taken from the project's main branch as of 2026-05-21". En el port a Lean 4.33, el archivo de atribución señala que "left the other 41 byte-identical".
La verificación es real
Nada de eso invalida la comprobación. El README informa de que se construyeron los 60.475 módulos, de que #print axioms fermat_last_theorem está limitado a los tres axiomas estándar y de que ningún módulo contiene axiom, sorry, native_decide, unsafe ni partial def. La compilación tardó 5 horas y 32 minutos con 96 tareas y alcanzó un pico de 153 GB de memoria. Según las cifras de Anthropic: 13 millones de líneas de Lean, 29.500 teoremas intermedios utilizados en la demostración final, y unos seis mil millones de tokens de salida.
Lo que falla en el encuadre recibido
Tres cosas. Claude no demostró nada nuevo — se trata de una autoformalización de la exposición de 1995 de Darmon, Diamond y Taylor del argumento de Wiles, Taylor y Wiles, una prueba que los humanos завершaron hace treinta y un años. No es un trabajo sin ayuda: según el propio recuento de Anthropic, una novena parte del repositorio contiene texto humano en Lean, parte de él literal. Y Buzzard, el matemático cuya reseña cita Anthropic, escribió en su propio blog ese mismo día que "mathematically this work of anthropic tells us essentially nothing" y que la formalización "just faithfully follows the early literature on the proof and adds nothing." Varios medios también lo llamaron el mayor archivo de este tipo; son 60.475 módulos, no un archivo.
La afirmación honesta sigue siendo grande
Las máquinas ya pueden traducir miles de páginas de literatura matemática existente a una forma comprobable por el núcleo en menos de dos semanas, apoyadas en varios años de trabajo voluntario en Lean. Ese es un resultado real sobre velocidad de traducción. No es un resultado sobre descubrimiento matemático, y el propio README reconoce la brecha residual: "What no tool can check is that each intermediate theorem means what its name suggests."