Claude verificó el teorema de Fermat en 11 días, pero no halló otra prueba

Anthropic publicó el 4 de septiembre de 2026 una formalización completa y comprobable por ordenador del último teorema de Fermat. El informe técnico de Anthropic documenta que decenas de agentes Claude trabajaron de forma mayormente autónoma durante 11 días, escribieron 13 millones de líneas en Lean y generaron pruebas verificables para 30.300 teoremas intermedios, 29.500 de ellos utilizados en el resultado final.

Claude no encontró una solución matemática diferente de la construida por Andrew Wiles y Richard Taylor. Una noticia de Nature del 7 de septiembre describe el resultado como la primera conversión completa del teorema en código verificado por ordenador: el avance consiste en automatizar la formalización de una demostración conocida, no en sustituirla por otra.

De la literatura matemática a 13 millones de líneas

El sistema no inició una investigación sobre el teorema desde cero. La formalización sigue la exposición de Henri Darmon, Fred Diamond y Richard Taylor de una versión simplificada del argumento de Wiles y convierte sus definiciones, referencias y pasos implícitos en una cadena que Lean puede procesar.

La enorme extensión del repositorio no equivale a una cantidad semejante de ideas nuevas. Los artículos dirigidos a especialistas omiten operaciones rutinarias, emplean convenciones compartidas y remiten a resultados repartidos por la literatura; un asistente de pruebas exige que cada definición, dependencia y transición quede expresada con precisión.

Los primeros intentos de coordinación tuvieron dificultades porque los agentes perdían de vista el estado global del trabajo. El proyecto avanzó al adoptar Prove2Me, una plataforma que organiza los enunciados pendientes mediante un grafo dirigido, separa enunciados y demostraciones para agilizar la compilación y conserva descripciones en lenguaje natural con las que localizar resultados reutilizables.

Sobre esa infraestructura, un sistema multiagente basado en Claude Code distribuyó las obligaciones formales. La aportación matemática humana se concentró principalmente en indicaciones ocasionales de alto nivel, mientras los agentes definían conceptos, resolvían resultados intermedios y conectaban esos resultados con la conclusión.

Qué valida Lean y qué queda fuera de su veredicto

Lean no juzga una demostración como lo haría un comité editorial ni determina si una idea es original o esclarecedora. Su núcleo comprueba que cada término de prueba tenga el tipo correcto y que las conclusiones se deriven de las definiciones, los axiomas y los resultados previamente declarados.

La prueba terminada utiliza los tres axiomas estándar de Lean. Además, un comparador cotejó el enunciado final del repositorio con la formulación del último teorema de Fermat incluida en Mathlib, la biblioteca matemática comunitaria en la que se apoyan numerosas formalizaciones.

La compilación certifica la coherencia de la cadena dentro de ese entorno formal: si falta una dependencia o un paso no es válido, Lean no lo acepta. No certifica por sí misma que el código sea breve, fácil de mantener o pedagógicamente útil, una distinción importante también en otros usos de la verificación formal.

La revisión independiente separó logro técnico y novedad matemática

Kevin Buzzard, matemático del Imperial College London y responsable de otro proyecto para formalizar el teorema, descargó el repositorio, compiló el código y ejecutó el comparador. En su revisión técnica del 4 de septiembre registró más de 13,4 millones de líneas, una compilación casi veinte veces más lenta que la de Mathlib en una máquina con 96 núcleos y un resultado correcto del comparador.

Su valoración distingue dos planos. La formalización sigue fielmente la literatura temprana de la prueba y no agrega un argumento matemático esencial; al mismo tiempo, demuestra que un conjunto coordinado de agentes puede convertir miles de páginas de matemáticas avanzadas en una prueba procesable de extremo a extremo en muy poco tiempo.

El proyecto de Imperial tampoco queda reemplazado porque persigue objetivos distintos. Entre ellos figuran incorporar a Mathlib objetos fundamentales de teoría de números y construir un documento dinámico con el que las personas puedan explorar una versión moderna de la demostración. El artefacto generado por Claude prioriza que una máquina pueda comprobar la cadena completa.

Por qué la formalización no es otra prueba de Fermat

Formalizar significa traducir un razonamiento matemático a un lenguaje con reglas que un verificador pueda revisar mecánicamente. Esa traducción puede descubrir huecos de detalle, dependencias omitidas o incompatibilidades entre definiciones, pero no convierte automáticamente el razonamiento de partida en un descubrimiento diferente.

En este caso no apareció un camino alternativo al argumento de Wiles y Taylor ni una prueba elemental perdida. Claude desarrolló y conectó de forma explícita una ruta conocida, basada en resultados profundos de teoría de números y campos relacionados, hasta lograr que Lean aceptara la conclusión.

Por eso «verificó» describe el resultado con mayor precisión que «resolvió». El conocimiento matemático central no cambió; lo novedoso es la velocidad y el grado de autonomía con que una demostración extensa pasó a convertirse en un objeto formal comprobable paso a paso.

El reto pasa ahora por revisar y mantener el artefacto

El resultado muestra que la automatización puede abordar formalizaciones cuya escala parecía exigir proyectos humanos prolongados. Todavía no demuestra que el mismo procedimiento vaya a producir siempre código compacto, legible o listo para integrarse en Mathlib, donde las contribuciones se someten a revisión comunitaria.

También queda por determinar hasta qué punto el flujo puede reproducirse fuera de la infraestructura utilizada y cómo se depurarán y mantendrán repositorios de este tamaño. A fecha del 8 de septiembre, el balance es concreto: Claude convirtió una demostración conocida en una cadena aceptada por Lean y reproducida en una revisión independiente, pero no aportó una nueva solución matemática al último teorema de Fermat.

Lee también:

• Verificación formal: una prueba matemática no garantiza software perfecto
• Tu empresa puede vigilar el correo, pero debe explicar por qué lo hace
• YouTube contará una vista desde el primer fotograma, pero no pagará por ella