Claude formalizó el último teorema de Fermat en 11 días

La carrera de 11 días que debería haber tomado años

Kevin Buzzard, matemático del Imperial College London, comenzó en 2024 un proyecto para formalizar el Último Teorema de Fermat en Lean. Su documento inicial de planificación solo tenía 86 páginas. La estimación de tiempo: varios años de trabajo por parte de un equipo de matemáticos y formalizadores expertos.

Claude, de Anthropic, completó la misma tarea en 11 días.

El anuncio llegó el 4 de septiembre de 2026, y es más grande de lo que sugieren las cifras principales. Claude generó aproximadamente 13 millones de líneas de código en Lean 4, verificó 33 000 teoremas y utilizó cerca de 29 500 de ellos en la demostración final. Esa base de código es más de cinco veces el tamaño de Mathlib, la biblioteca estándar de matemáticas en Lean que representa décadas de esfuerzo humano por codificar las matemáticas modernas en un formato que las computadoras pueden verificar.

Para dar contexto, la demostración original de Andrew Wiles del Último Teorema de Fermat ocupaba 129 páginas. Un equipo de humanos que leyera cada paso dedicaría meses a buscar posibles vacíos. Formalizar esa demostración —el proceso de traducir el razonamiento matemático a un lenguaje que una computadora pueda verificar— es un tipo de empresa completamente diferente. Cada paso que para un lector humano resulta “obvio” debe hacerse explícito para Lean. Esa es la razón por la que se esperaba que el proyecto de Buzzard tomara años.

Cómo lo logró Claude

El truco no consistió simplemente en ejecutar Claude una vez y esperar. Docenas de agentes de Claude trabajaron en paralelo, cada uno responsable de definiciones, lemas intermedios y, finalmente, las proposiciones más difíciles. Pero la paralelización por sí sola casi no funcionó.

Tianyi Peng, investigador de Anthropic que ha estudiado la formalización matemática impulsada por IA, describió intentos iniciales en los que los agentes perdían de vista el estado general del proyecto. Sin coordinación, cada agente no sabía qué habían completado los demás, y el progreso se estancó.

La solución fue Prove2Me, una plataforma colaborativa desarrollada por el equipo de Peng específicamente para este tipo de trabajo. Representa los teoremas como un grafo acíclico dirigido, de modo que cada agente puede ver qué dependencias se han satisfecho y qué metas quedan pendientes. El sistema también separa las declaraciones de teoremas de las demostraciones en archivos diferentes, acelerando la compilación. Cada teorema lleva una descripción en lenguaje natural, lo que lo hace searchable para resultados reutilizables.

Este detalle de infraestructura importa. Las 13 millones de líneas de código no son solo una medida de generación bruta: reflejan una nueva forma de organizar el trabajo colectivo de verificación formal. El plan de Buzzard, de haberse llevado a cabo al estilo humano, habría sido una secuencia lineal de definiciones y lemas. El enfoque de Claude es distribuido, gestionado por grafos e iterativo.

La demostración está realmente verificada

Existe una razón para que esto se verifique repetidamente. En la verificación formal, un único supuesto falso se propaga a todo lo construido sobre él. Los primeros borradores de contenido matemático generado por IA a veces contenían errores que solo aparecían después de trabajos posteriores considerables.

La demostración de Fermat pasó la verificación del propio kernel de Lean sin objetivos abiertos ni subobjetivos pendientes. Depende únicamente de los tres axiomas estándar de Lean. No hay marcadores temporales —los temidos comandos sorry que señalan demostraciones inconclusas en proyectos Lean—. Una implementación de kernel independiente llamada nanoda, escrita en Rust, también verificó más de un millón de declaraciones sin errores. Una herramienta de comparación confirmó que la declaración formalizada coincide exactamente con la descripción existente en Mathlib del Último Teorema de Fermat.

La demostración es pública en GitHub bajo la organización de Anthropic. Cualquier persona con Lean instalado puede cargarla y ejecutar la verificación por su cuenta.

Lo que esto significa para las matemáticas

La implicación más inmediata no es que la IA ahora pueda resolver el Último Teorema de Fermat —Wiles lo resolvió en la década de 1990—. La implicación es que la IA ahora puede tomar una demostración existente y traducirla a una forma verificable por máquina más rápido de lo que cualquier equipo humano ha logrado, y hacerlo a una escala que supera con creces los intentos anteriores.

El propio trabajo de Buzzard, cuando se complete, será un punto de referencia. Los formalizadores humanos han logrado avances impresionantes en teoremas importantes, pero el ritmo sigue siendo lento porque el cuello de botella es fundamentalmente humano: leer, comprender, reinterpretar y verificar. Claude no reemplazó la necesidad de rigor. Reemplazó el cuello de botella.

Esto genera una tensión. A medida que la IA genera más y más demostraciones formalizables, aumenta la carga sobre los humanos para verificarlas. Anthropic prevé que, de aquí en adelante, las formalizaciones verificadas por computadora acompañarán a los artículos legibles por humanos como práctica estándar. Eso sería un cambio estructural en la forma en que se producen y validan las matemáticas.

También plantea una pregunta sobre el crédito y la atribución. Cuando una demostración es formalizada por agentes de IA distribuidos en lugar de un matemático humano con nombre, ¿qué significa para la cultura de la autoría matemática? Buzzard dedicó años a planificar este proyecto. Claude lo completó en 11 días. La demostración es la misma. La diferencia está en quién recibe el crédito por hacerla verificable por máquina —y si esa distinción importará menos en los años venideros—.

El verdadero hito

El Último Teorema de Fermat es famoso, pero no es el teorema más difícil que existe. El significado de este resultado no radica en el teorema en sí. Rodea la escala. Trece millones de líneas de código Lean verificado. Treinta y tres mil teoremas. Un sistema de agentes distribuidos coordinado por una herramienta de planificación basada en grafos. Todo ello producido en menos de dos semanas.

Proyectos de formalización a gran escala previos —como la demostración del Teorema del Orden Impar— requirieron años de trabajo de equipos de especialistas. Este anuncio sugiere que esos plazos ahora se miden contra una nueva base. La pregunta para la comunidad matemática ya no es si la IA puede formalizar teoremas importantes. Es qué tan rápido se cerrará la brecha entre el ritmo humano y el máquina, y qué le ocurrirá a la práctica matemática cuando la verificación sea más barata que la intuición.