Claude Formaliza el Último Teorema de Fermat en Lean con una Prueba de 13 Millones de Líneas

Anthropic ha publicado lo que describe como la primera formalización completa y verificable por ordenador del Último Teorema de Fermat. Un conjunto de agentes de Claude trabajó durante 11 días para convertir una ruta matemática basada en la demostración moderna del teorema en código Lean que puede ser comprobado automáticamente por un asistente de pruebas.

El resultado no constituye una nueva demostración matemática del teorema. Claude siguió una versión simplificada del camino desarrollado a partir de los trabajos de Frey, Serre, Ribet, Andrew Wiles y Richard Taylor, utilizando como referencia una exposición de Henri Darmon, Fred Diamond y Taylor. La novedad está en haber trasladado ese razonamiento a una prueba formal completa que un ordenador puede verificar paso a paso.

Claude produjo 13 millones de líneas de Lean en 11 días

Según Anthropic, el proyecto generó aproximadamente 13 millones de líneas de código Lean y pruebas de 30.300 teoremas durante el proceso. Unos 29.500 de esos resultados intermedios forman parte de la demostración final.

La escala es considerable: Anthropic señala que el resultado tiene más de cinco veces el tamaño de Mathlib, la principal biblioteca comunitaria de matemáticas formalizadas sobre la que se apoya el proyecto. La propia compañía reconoce que parte de esa diferencia se debe a que Mathlib está muy optimizada y revisada, mientras que la prueba producida por los agentes probablemente contiene bastante más código del estrictamente necesario.

El trabajo fue realizado por decenas de agentes que dividieron el problema en definiciones y teoremas intermedios. La intervención humana se limitó principalmente a instrucciones matemáticas de alto nivel proporcionadas por Tianyi Peng, investigador de Anthropic y miembro de un grupo de Columbia University dedicado a herramientas de formalización mediante IA.

Prove2Me permitió coordinar a decenas de agentes

Los primeros intentos no funcionaron correctamente. Anthropic explica que los agentes perdían la visión del estado global del proyecto y dejaban de colaborar de forma eficaz a medida que la prueba crecía.

El avance llegó al utilizar Prove2Me, una plataforma abierta desarrollada por Peng y colaboradores de Columbia University. El sistema representa los teoremas pendientes mediante un grafo dirigido, permitiendo que múltiples agentes identifiquen qué resultados necesitan demostrarse y trabajen sobre diferentes partes de la prueba en paralelo.

Prove2Me también separa las declaraciones de los teoremas de sus demostraciones para acelerar la compilación de Lean y mantiene descripciones en lenguaje natural que facilitan encontrar y reutilizar resultados ya obtenidos.

Anthropic combinó esta plataforma con una infraestructura multiagente basada en Claude Code. En total, el experimento consumió alrededor de 6.000 millones de tokens de salida utilizando un modelo interno de propósito general que la compañía describe como aproximadamente comparable a Claude Fable 5.1.

Lean comprobó toda la cadena de la demostración

La diferencia entre una demostración matemática tradicional y una formalización está en el nivel de detalle exigido. Los textos escritos para matemáticos suelen omitir pasos considerados evidentes, mientras que un asistente como Lean necesita que todas las inferencias estén expresadas de una forma que su núcleo pueda comprobar.

El repositorio publicado por Anthropic utiliza Lean 4.33.1 y Mathlib 4.33.0. La comprobación final establece que el teorema depende únicamente de los tres axiomas estándar utilizados por Lean en este contexto: propext, Classical.choice y Quot.sound.

El proyecto también fue validado con Comparator, una herramienta del ecosistema Lean que confirmó que el enunciado demostrado coincide con la definición del Último Teorema de Fermat incluida en Mathlib. Además, una segunda implementación independiente del núcleo de Lean escrita en Rust, denominada nanoda, aceptó más de un millón de declaraciones del mismo entorno sin detectar errores.

La prueba puede volver a verificarse de forma independiente

Anthropic ha publicado el código completo bajo licencia Apache 2.0. El repositorio incluye la demostración, la ruta de dependencias entre resultados y las herramientas utilizadas para repetir las comprobaciones.

Reproducir todo el proceso requiere, sin embargo, recursos informáticos importantes. La compilación realizada por Anthropic utilizó hasta 153 GB de memoria y tardó aproximadamente cinco horas y media empleando 96 trabajos en paralelo. La comprobación con Comparator necesitó cerca de 15 horas y alcanzó un máximo aproximado de 230 GB de memoria.

El repositorio también contiene páginas estáticas para explorar unas 29.500 demostraciones y alrededor de 1.450 módulos de definiciones, junto con gráficos que muestran cómo los distintos resultados se conectan hasta llegar al teorema final.

El proyecto de Imperial College llevaba años trabajando en la misma meta

La formalización del Último Teorema de Fermat no comenzó con Anthropic. Desde 2024 existe un proyecto abierto dirigido por Kevin Buzzard en Imperial College London que busca formalizar el resultado utilizando Lean y Mathlib.

Ese proyecto está diseñado como un esfuerzo matemático colaborativo de varios años y utiliza una variante moderna de la demostración de Wiles y Taylor-Wiles. Anthropic reconoce que su propio resultado reutiliza partes del trabajo abierto producido por el proyecto de Imperial College London, además de componentes procedentes de Mathlib y de otro proyecto denominado flt-regular.

Buzzard revisó el resultado de Anthropic y valoró especialmente que la prueba dependa únicamente de los axiomas matemáticos utilizados por Lean. También considera que el experimento muestra que la formalización automática de grandes cantidades de literatura matemática puede haberse convertido en una posibilidad práctica.

No es una nueva solución al Último Teorema de Fermat

El Último Teorema de Fermat afirma que no existen enteros positivos a, b y c que satisfagan la ecuación a elevado a n más b elevado a n igual a c elevado a n cuando n es superior a 2.

Andrew Wiles consiguió la primera demostración aceptada del resultado en la década de 1990, posteriormente completada junto con Richard Taylor tras detectarse un problema en la versión presentada inicialmente. La formalización de Anthropic no sustituye ni descubre una alternativa a ese trabajo, sino que convierte una ruta basada en esas matemáticas en una cadena lógica que un ordenador puede comprobar automáticamente.

Para Anthropic, el interés del experimento está precisamente en esa capacidad de verificación. A medida que los sistemas de inteligencia artificial produzcan más resultados matemáticos, formalizarlos en herramientas como Lean podría permitir detectar errores y reducir parte del trabajo requerido para revisar demostraciones extremadamente extensas.

La propia compañía advierte de que una prueba formal tampoco reemplaza una explicación matemática comprensible para humanos. El código garantiza que las declaraciones formales se derivan correctamente unas de otras bajo los axiomas utilizados, pero interpretar el significado matemático y la relevancia de los pasos continúa siendo una tarea para los investigadores.