La IA de Anthropic verifica el Último Teorema de Fermat en 11 días
Una inteligencia artificial acaba de reescribir cómo se verifica la matemática
El 4 de septiembre de 2026, Anthropic anunció que su modelo Claude completó la primera formalización íntegra y verificable por máquina del Último Teorema de Fermat en el lenguaje Lean 4. Lo hizo en unos 11 días, produciendo más de 13 millones de líneas de código — la mayor demostración jamás escrita en Lean, más de cinco veces el tamaño de Mathlib, la biblioteca comunitaria de referencia. No es una noticia de un teorema nuevo: es una señal de que la manera en que la humanidad certifica la verdad matemática está cambiando de raíz.
El resultado fue revisado por Kevin Buzzard, matemático del Imperial College London, quien lideraba desde 2024 un proyecto financiado para lograr exactamente esto mismo con trabajo humano coordinado, con fondos asegurados hasta 2029. Claude llegó primero.
Qué se demostró exactamente (y qué no)
Conviene ser precisos, porque la diferencia importa. El Último Teorema de Fermat afirma que la ecuación x^n + y^n = z^n no tiene soluciones con enteros positivos cuando n es mayor que 2. Para n=2 las soluciones abundan (3² + 4² = 5², el clásico teorema de Pitágoras); pero Pierre de Fermat conjeturó en 1637, en el margen de un libro, que más allá del exponente 2 no existe ninguna terna, y afirmó tener "una demostración verdaderamente maravillosa" que no cabía en ese margen.
El teorema ya fue demostrado por Sir Andrew Wiles en 1995, tras más de 350 años. Lo que Claude produjo no es matemática nueva: es una formalización — la traducción de las 129 páginas del argumento de Wiles-Taylor (vía curvas de Frey y elevación de modularidad) a un lenguaje que una computadora puede verificar línea por línea, sin ambigüedad y sin depender del juicio de un revisor humano.
Las cifras del trabajo, según el informe de investigación de Anthropic:
- Más de 13 millones de líneas de código Lean generadas.
- Alrededor de 30.300 teoremas de apoyo demostrados (29.500 usados en la prueba final), muchos en áreas de las matemáticas nunca antes formalizadas.
- Cerca de 6.000 millones de tokens consumidos durante la ejecución.
- Lean verificó el resultado usando únicamente sus tres axiomas estándar, sin supuestos adicionales.
Por qué esto le importa a la ciberseguridad
Podría parecer un logro puramente académico, pero toca fibras directas de nuestro mundo. La verificación formal es la misma disciplina que se usa para probar matemáticamente que un protocolo criptográfico, un kernel o un contrato inteligente se comportan como deben y no tienen fallos lógicos. Que un modelo de IA pueda autoformalizar demostraciones de esta escala abre la puerta a auditar software crítico con un rigor antes impensable.
El propio Buzzard lo resumió tras revisar la prueba: "Si la formalización automática del Último Teorema de Fermat es posible ahora, hemos dado un gran paso hacia la formalización automática de la literatura matemática moderna." Trasladado a la seguridad, significa que las herramientas para demostrar la ausencia de vulnerabilidades —no solo buscarlas— podrían dejar de ser un lujo artesanal para volverse escalables.
El otro lado de la moneda: confianza y verificación
Hay un matiz que la comunidad Lean subrayó de inmediato. La prueba se apoya en el andamiaje matemático que Buzzard y decenas de voluntarios llevaban años construyendo; Claude no partió de cero. Y una demostración de 13 millones de líneas plantea una paradoja: ¿quién verifica al verificador? La respuesta, precisamente, es la fortaleza del enfoque: a diferencia de un argumento en prosa que un humano tarda años en revisar (el proyecto de la conjetura de Kepler necesitó cuatro años para que un panel se atreviera a decir "99% seguro"), una prueba en Lean la comprueba la máquina en minutos, de forma determinista y reproducible.
Anthropic publicó la demostración completa de 13 millones de líneas en GitHub, abierta para que cualquier matemático la escrutine. Esa transparencia es la que separa un anuncio de marketing de un resultado científico verificable — un principio que en CiberPlaneta defendemos también para la seguridad: lo que no se puede auditar, no se puede confiar.
Lo que viene
Este hito cierra el último problema pendiente de la célebre lista de 100 desafíos de formalización de Freek Wiedijk, un benchmark de 20 años. Pero su verdadero peso está en la tendencia: los modelos de IA no solo escriben código, ahora generan pruebas matemáticas verificables a escala industrial. Para quienes trabajamos en ciberseguridad, la pregunta ya no es si la verificación formal asistida por IA llegará a nuestras herramientas, sino qué tan rápido y con qué garantías. Conviene estar atentos: la misma capacidad que hoy certifica un teorema de 358 años podría mañana certificar —o comprometer— el software del que dependemos.
Fuentes
- Anthropic (@AnthropicAI) — anuncio oficial, 4 de septiembre de 2026.
- Decrypt — "AI Just Solved a 350-Year-Old Math Problem By Writing the Longest Proof Ever" (5-sep-2026).
- Kevin Buzzard, Xena Project — "FLT: Anthropic has beaten me to it" (4-sep-2026).
- ExplainX / AI Weekly — cobertura técnica de la formalización en Lean 4 (5-sep-2026).