La IA de Anthropic formaliza el último teorema de Fermat en Lean

Anthropic ha publicado una prueba completa y verificada por máquina del último teorema de Fermat, escrita en Lean. La empresa afirma que un modelo de investigación interno la generó en 11 días. El resultado ocupa unas cinco veces lo que ocupa Mathlib, la principal biblioteca abierta de matemáticas formalizadas.

Lean es un asistente de pruebas. Escribes matemáticas como código, y un programa pequeño llamado núcleo comprueba cada paso. El último teorema de Fermat dice que no hay tres enteros positivos a, b y c que cumplan a^n + b^n = c^n cuando n es mayor que 2. Andrew Wiles lo demostró en 1995. Hasta ahora nadie había escrito esa prueba de una forma que un ordenador pudiera verificar de principio a fin.

Qué contiene realmente el repositorio

El artículo de investigación de Anthropic se publicó el 4 de septiembre de 2026. El código está en GitHub bajo licencia Apache 2.0.

Su archivo README enuncia el teorema formal. Para enteros positivos a, b y c, y cualquier n de al menos 3, a^n + b^n nunca es igual a c^n.

Elemento	Valor
Cadena de herramientas Lean	4.33.1
Revisión de Mathlib	v4.33.0
Teoremas	29.511
Módulos	60.475
Tiempo de compilación	5,5 horas con 96 trabajos en paralelo
Pico de memoria	230 GB
Tamaño de la exportación	37,8 GB

Dos afirmaciones del README pesan más que el tamaño. La prueba no contiene ningún sorry, el marcador de Lean para un paso que nadie terminó. Y se apoya en solo tres axiomas: propext, Classical.choice y Quot.sound. Esos tres vienen con el propio Lean. No se supuso nada más para cerrar el argumento.

Anthropic dice que el modelo demostró 30.300 teoremas en total. Unos 29.500 acabaron en la prueba final. La empresa cita 6.000 millones de tokens de salida y 13 millones de líneas de Lean generadas. El trabajo pasó por Prove2Me, una plataforma que parte una formalización en enunciados pequeños y los reparte entre agentes que trabajan en paralelo.

Cómo se comprobó la prueba

Se hicieron tres comprobaciones separadas, y esta es la parte que merece entenderse.

Primero el propio núcleo de Lean aceptó la prueba. Después una herramienta llamada comparator, en la versión 4.33.0, la volvió a comprobar en unas 15 horas. Por último Nanoda, un núcleo independiente escrito en Rust, verificó 1.052.234 declaraciones en unos 30 minutos.

Nanoda importa porque no comparte código con Lean. Un fallo en el núcleo de Lean no lo detectaría el núcleo de Lean. Una segunda implementación, en otro lenguaje, es un control real sobre ese riesgo.

Qué opinan los matemáticos

Kevin Buzzard dirige el Proyecto Xena. Tiene una subvención de un millón de libras del financiador de investigación británico EPSRC, repartida en cinco años, para formalizar justo este teorema. Escribió en su blog que Anthropic llegó antes.

Buzzard no discute el resultado. "Estoy seguro al 99,9 % de que la prueba de FLT está bien", escribió. En la página de Anthropic califica el trabajo de "logro extraordinario de autoformalización".

También traza un límite. La formalización "sigue fielmente la literatura temprana sobre la prueba y no añade nada", escribió. Sigue la exposición de Darmon, Diamond y Taylor de 1995 sobre el argumento de Wiles. Aquí no se encontraron matemáticas nuevas. Lo nuevo es que las viejas ya se pueden comprobar con una máquina.

Buzzard señala que la prueba cubre los primos de al menos 17. Los primos irregulares más pequeños ya los habían formalizado otros. Un comentarista de su entrada, David Jao, situó el coste de API de la ejecución en unos 300.000 dólares.

Qué significa esto para los desarrolladores

Si escribes Lean, puedes clonar el repositorio, pero revisa antes tu hardware. Una compilación de 5,5 horas con 96 trabajos, con un pico de 230 GB de memoria, descarta casi cualquier portátil. Lee en su lugar la documentación HTML generada. Ocupa 390 MB y no necesita compilarse.

La lección aprovechable no es que un modelo escribiera 13 millones de líneas. Es que nadie tuvo que leerlas. Un núcleo decidió si el código era correcto, en minutos, sin confiar en lo que lo había producido.

Eso solo funciona donde existe un verificador. Lean tiene uno. Tu servicio web no. Antes de tomar esto como plantilla, pregunta qué haría el papel del núcleo en tu propia pila. Un sistema de tipos, una prueba de propiedades o un fuzzer son los candidatos habituales.

Si revisas Lean escrito por una IA, dos comprobaciones mecánicas cubren casi todo. Busca sorry, e imprime la lista de axiomas. La afirmación de Anthropic se apoya en esos dos hechos, y ambos son baratos de confirmar por tu cuenta.

La diferencia de coste es lo último que conviene notar. Producir la prueba costó 11 días y miles de millones de tokens. Volver a verificarla en otro lenguaje costó media hora. Anthropic ya ha dirigido modelos de investigación al trabajo de laboratorio, y aquí se repite el patrón. Generar sale caro. Comprobar sale barato.