⏱️ Lectura: 11 min
Claude tardó once días en escribir lo que la comunidad matemática estimaba que tomaría años: una demostración completa del Último Teorema de Fermat que una computadora puede verificar paso por paso, sin depender de la palabra de ningún humano.
📑 En este artículo
Anthropic anunció el resultado el 4 de septiembre de 2026: agentes de Claude, trabajando en gran parte de forma autónoma, tradujeron el razonamiento matemático completo al lenguaje del asistente de pruebas Lean, generando 13 millones de líneas de código verificado.
TL;DR
- Claude escribió la primera demostración del Último Teorema de Fermat verificable automáticamente por una computadora.
- El trabajo tomó 11 días de agentes Claude operando en gran parte de forma autónoma.
- La demostración final usa 29.500 teoremas intermedios de un total de 30.300 probados en el proceso.
- El código Lean generado suma 13 millones de líneas, más de 5 veces el tamaño de Mathlib.
- La prueba sigue una versión simplificada del argumento de Wiles según Darmon, Diamond y Taylor.
- Kevin Buzzard, líder del proyecto de formalización de FLT en Lean desde 2024, validó el resultado.
- Anthropic publicó el anuncio el 4 de septiembre de 2026 en su sitio de investigación.
Introducción
El teorema de Fermat es la afirmación que Pierre de Fermat garabateó alrededor de 1637 en el margen de su copia de la Arithmetica de Diofanto: no existen enteros positivos a, b y c que cumplan a^n + b^n = c^n para ningún n mayor que 2. Fermat agregó una nota que se volvió legendaria, donde decía haber descubierto una demostración verdaderamente maravillosa que el margen era demasiado angosto para contener. Esa frase alimentó 358 años de intentos, la mayoría fallidos.
Lo que anunció Anthropic no es una demostración matemática nueva. Es la formalización de una demostración ya existente: convertir el razonamiento de Andrew Wiles, publicado en 1995, a un formato que un programa llamado asistente de pruebas puede comprobar de forma mecánica, sin dar nada por sentado. A diferencia de trabajos recientes de IA sobre la hipótesis de Riemann, que buscaban matemáticas inéditas, acá el objetivo era la verificación: confirmar que cada eslabón lógico de una cadena ya conocida es correcto.
Qué pasó
Tianyi Peng, investigador de Anthropic cuyo grupo en Columbia University desarrolla herramientas de formalización con IA, decidió probar si Claude podía avanzar en la formalización del Último Teorema de Fermat. El resultado superó lo esperado: en 11 días, trabajando en gran parte de forma autónoma, Claude produjo la primera demostración de principio a fin, verificada por computadora, de todo el teorema.
En el proceso, Claude escribió 13 millones de líneas de código en Lean y generó demostraciones verificables de 30.300 teoremas intermedios, de los cuales 29.500 terminaron formando parte de la demostración final. Docenas de agentes de Claude colaboraron para definir conceptos matemáticos, probar teoremas intermedios y usarlos como base para enunciados cada vez más difíciles.
Anthropic compartió la demostración resultante con Kevin Buzzard, matemático de Imperial College London que lidera desde 2024 un esfuerzo comunitario para formalizar este mismo teorema en Lean. Su reacción fue contundente: calificó el logro de extraordinario y señaló que la prueba no asume nada más que los axiomas de las matemáticas, y que a lo largo del camino se ve autoformalización de álgebra, análisis armónico, geometría y teoría de números.
Contexto e historia
Durante más de 350 años, generaciones enteras de matemáticos buscaron una demostración del teorema, maravillosa o no. En 1908 se anunció un premio de 100.000 marcos de oro alemanes (el equivalente a 1 o 2 millones de dólares actuales) para quien lograra probarlo, y solo en el primer año se presentaron 621 intentos incorrectos.
En junio de 1993, Andrew Wiles presentó lo que creía era la primera demostración correcta, en una serie de conferencias de tres días. Dos meses después, en medio de una revisión intensiva, un revisor le hizo una pregunta que expuso un vacío crítico en el argumento. Wiles pasó un año tratando de corregirlo, primero solo y después junto a su exalumno Richard Taylor. Estuvo a punto de abandonar el proyecto hasta que se dio cuenta de que un enfoque que había descartado antes podía resolver el problema. La demostración corregida se publicó en mayo de 1995 y se apoyaba en técnicas muy posteriores a la época de Fermat, motivo por el cual hoy se cree que la demostración maravillosa original de Fermat era, en realidad, incorrecta.
Una década más tarde, el informático neerlandés Jan Bergstra propuso formalizar la demostración de Wiles. Desde entonces, los matemáticos fueron desarrollando los métodos necesarios para codificar una prueba tan compleja, incluido el esfuerzo comunitario de varios años que Kevin Buzzard puso en marcha en 2024 para completar la formalización usando el asistente de pruebas Lean. Solo el blueprint (el plano que describe la fase inicial del proyecto) ocupa 86 páginas.
Detalles técnicos y rendimiento
Un asistente de pruebas como Lean verifica algorítmicamente la lógica de una demostración, mostrando su corrección más allá de cualquier duda. Lo difícil para los humanos es reescribir la prueba para que Lean pueda entenderla: mientras una demostración pensada para lectores humanos se salta pasos obvios, Lean necesita ver cada paso, por trivial que parezca. Además, una prueba humana se apoya en siglos de trabajo publicado, mientras que una formalización parte de la fracción diminuta de las matemáticas que ya fue formalizada.
Para dimensionar el logro: se esperaba que formalizar el Último Teorema de Fermat tomara años. Claude lo hizo en 11 días, con 13 millones de líneas de Lean, más de cinco veces el tamaño de Mathlib, la biblioteca comunitaria de demostraciones sobre la que se construye esta prueba. La demostración de Claude sigue una versión simplificada del argumento de Wiles a partir del trabajo de Darmon, Diamond y Taylor. Según Anthropic, el aporte matemático humano se limitó a intervenciones puntuales, no a guiar cada paso del proceso.
| Aspecto | Prueba de Wiles (1995) | Formalización de Claude (2026) |
|---|---|---|
| Formato | 129 páginas en papel, para lectores humanos | 13 millones de líneas de código en Lean |
| Verificación | Revisión manual por matemáticos durante meses | Verificación automática por el kernel de Lean |
| De la presentación a la publicación | De junio de 1993 a mayo de 1995, tras corregir un vacío crítico | 11 días de trabajo, en gran parte autónomo |
| Nivel de detalle exigido | Omite pasos que un matemático da por obvios | Cada paso, sin importar cuán trivial, debe quedar explícito |
💭 Clave: Claude no descubrió matemáticas nuevas: verificó que la demostración de Wiles, adaptada por Darmon, Diamond y Taylor, es lógicamente correcta hasta el nivel de los axiomas.
Cómo empezar a probarlo
No hace falta ser matemático profesional para tocar un asistente de pruebas como Lean. El punto de entrada estándar es elan, el gestor de versiones de Lean, disponible en Linux, macOS y Windows.
En Linux y macOS:
curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh
elan --versionEn Windows (PowerShell):
Invoke-WebRequest -Uri "https://raw.githubusercontent.com/leanprover/elan/master/elan-init.ps1" -UseBasicParsing | Invoke-Expression
elan --versionCon Lean instalado, un primer ejemplo trivial verifica que la suma es conmutativa:
theorem suma_conmutativa (a b : Nat) : a + b = b + a := by
ringEste bloque define un teorema y lo prueba con la táctica ring, que resuelve automáticamente igualdades algebraicas. Un ejemplo más cercano al espíritu del proyecto de Fermat es enunciar el teorema como una proposición general, tal como aparece planteado en Mathlib antes de tener demostración:
def UltimoTeoremaFermatPara (n : Nat) : Prop :=
∀ a b c : Nat, 0 < a → 0 < b → 0 < c → a ^ n + b ^ n ≠ c ^ n
theorem ultimo_teorema_fermat : ∀ n : Nat, 2 < n → UltimoTeoremaFermatPara n := by
sorry -- aca es donde entraban los 13 millones de lineas de ClaudeLa palabra clave sorry le dice a Lean confía en mí, esto es cierto, y es exactamente lo que un proyecto de formalización tiene que eliminar por completo. Para confirmar que una demostración terminada no depende de atajos ni de axiomas no deseados, Lean ofrece un comando de verificación directo:
#print axioms ultimo_teorema_fermat💡 Tip: corré#print axioms nombre_del_teoremasobre cualquier demostración en Lean y revisá que solo aparezcan los axiomas esperados de la teoría de conjuntos: si aparecesorryAx, la prueba todavía tiene huecos.
Impacto y análisis
El valor de este trabajo no está en resolver un problema abierto, sino en demostrar que la verificación automática puede escalar a pruebas de cientos de páginas escritas por humanos. Entender un resultado matemático nuevo lo suficiente como para confiar en su corrección puede tomar meses o años de trabajo de revisión por pares. Kevin Buzzard remarcó que los artefactos de autoformalización de IA ya son lo bastante robustos como para construir sobre ellos, algo que hasta hace poco no era evidente.
La limitación honesta es que este enfoque no genera matemáticas nuevas por sí solo: necesita una demostración humana ya publicada para traducir. Tampoco elimina la necesidad de confianza, simplemente la desplaza: en vez de confiar en cientos de revisores humanos, hay que confiar en el kernel de Lean y en sus axiomas, un conjunto de software mucho más pequeño y auditable. Y una demostración de 13 millones de líneas, aunque verificable paso por paso, sigue siendo enorme para que un humano la lea de punta a punta.
Qué sigue
Si la formalización de una prueba de esta magnitud pasó de tomar años estimados a 11 días, el cuello de botella para verificar resultados matemáticos importantes podría dejar de ser el tiempo de los revisores humanos. Buzzard planteó que este avance es un paso significativo hacia un futuro en el que toda la matemática pueda revisarse fácilmente, y que a medida que la IA produzca más demostraciones, la capacidad de formalizarlas con rapidez podría aliviar la carga de evaluar resultados nuevos.
📖 Resumen en Telegram: Ver resumen
Probalo vos: instalá elan, cloná el repositorio de Mathlib y corré #print axioms sobre un lema propio para ver al kernel de Lean verificar tu primer paso hoy mismo.
Preguntas frecuentes
¿Qué es el Último Teorema de Fermat?
Es la afirmación, escrita por Pierre de Fermat en 1637, de que no existen enteros positivos a, b y c que cumplan a^n + b^n = c^n para ningún n mayor que 2. Andrew Wiles publicó la primera demostración aceptada en 1995.
¿Qué significa formalizar una demostración matemática?
Significa reescribir el razonamiento en un lenguaje que un asistente de pruebas, como Lean, pueda verificar de forma mecánica, sin saltarse ningún paso, por más obvio que parezca para un lector humano.
¿Claude descubrió matemáticas nuevas con este trabajo?
No. Claude verificó una demostración ya existente, la de Andrew Wiles simplificada según Darmon, Diamond y Taylor. El logro está en la escala y la velocidad de la verificación, no en un resultado matemático inédito.
¿Cuánto código en Lean escribió Claude?
13 millones de líneas, generando demostraciones verificables de 30.300 teoremas intermedios, de los cuales 29.500 se usaron en la demostración final.
¿Por qué importa la opinión de Kevin Buzzard?
Buzzard lidera desde 2024 el esfuerzo comunitario para formalizar el Último Teorema de Fermat en Lean, con un blueprint de 86 páginas. Su validación confirma que el resultado de Claude es coherente con ese proyecto de referencia.
¿Se puede revisar el trabajo de formalización?
El anuncio original de Anthropic describe el proceso y comparte la reacción de Buzzard; para entender cómo se construye una formalización de este tipo, se puede explorar directamente el código y la documentación de Lean y Mathlib.
Referencias
- Formalizing Fermat’s Last Theorem: el anuncio original de Anthropic, con la cronología del proyecto y la cita de Kevin Buzzard.
- Mathlib4 en GitHub: la biblioteca comunitaria de demostraciones en Lean sobre la que se construyó la formalización.
- Documentación oficial de Lean: referencia del lenguaje y el asistente de pruebas usado en el proyecto.
- Último Teorema de Fermat en Wikipedia: contexto histórico completo, incluida la demostración de Andrew Wiles.
📱 ¿Te gusta este contenido? Únete a nuestro canal de Telegram @programacion donde publicamos a diario lo más relevante de tecnología, IA y desarrollo. Resúmenes rápidos, contenido fresco todos los días.
Imagen destacada: Foto de Vitaly Gariev en Unsplash
0 Comentarios