Anthropic formaliza el teorema de Fermat con Claude en 11 días

Anthropic cierra en 11 días un reto matemático de dos décadas

Claude, el modelo insignia de Anthropic, formalizó una demostración completa del Teorema de Fermat en el asistente de pruebas Lean, según anunció la propia compañía el 4 de septiembre de 2026. El trabajo, desarrollado sobre la plataforma prove2.me, produjo más de 13,4 millones de líneas de código Lean y cerca de 29.500 teoremas intermedios en apenas 11 días, según reportó Crypto Briefing. Con esto se completa la lista de los 100 retos de formalización que el matemático Freek Wiedijk propuso hace dos décadas: el último teorema pendiente era, precisamente, el Último Teorema de Fermat (FLT, por sus siglas en inglés).

La noticia fue confirmada en primera persona por Kevin Buzzard, profesor del Imperial College London y responsable del proyecto Xena, en una entrada de blog titulada "Fermat's Last Theorem: Anthropic has beaten me to it". Buzzard dirigía desde hace un año una iniciativa financiada por el EPSRC del Reino Unido con £1 millón a cinco años para formalizar la misma demostración. Anthropic resolvió el núcleo técnico en 11 días.

Qué hizo exactamente Claude (y qué no)

La formalización sigue la exposición de Darmon, Diamond y Taylor de 1995 del argumento original de Wiles-Taylor-Wiles, apoyándose en el teorema de Langlands-Tunnell y en el descenso de nivel de Ribet. Para llegar al resultado, el modelo tuvo que desarrollar:

🤖 La IA no es solo para leer sobre ella

En la comunidad la aplicamos: automatización, agentes IA y herramientas reales para emprender, no solo para informarte.

👥 Aplicarla en la comunidad

Teoría de Fontaine, usada para estudiar deformaciones planas de representaciones de Galois.
Suficiente trabajo de Mazur sobre el ideal de Eisenstein para demostrar que ninguna curva de Frey puede tener un punto de cierto orden.

La demostración resultante cubre los exponentes primos regulares (todos los primos impares excepto un conjunto finito). Buzzard aclara en su blog que los casos irregulares ya estaban cubiertos por el trabajo previo de Best, Birkbeck, Brasca y Rodríguez, y que el primo irregular más pequeño es el 37, así que la combinación de ambas formalizaciones cierra FLT de forma completa.

Lo que el código no hace, según Buzzard, es aportar nada matemáticamente nuevo: "la formalización sigue fielmente la literatura existente y no añade nada". Lo que sí demuestra es la capacidad del sistema: un modelo interno de Anthropic, operando con recursos de cómputo masivo (la compilación se realizó en una máquina con 96 núcleos y 500 GB de RAM, aportada también al equipo de Buzzard), pudo leer, sintetizar y reescribir miles de páginas de teoría de números moderna.

Por qué este hito importa más allá de las matemáticas

El proyecto mathlib de Lean —la biblioteca de teoremas formalizados que sirve de base a la demostración de FLT— acumulaba hacia marzo de 2026 más de 260.000 teoremas verificados y más de 120.000 definiciones, con más de USD 10 millones de financiamiento, en su mayoría del inversor Alex Gerko, según un reportaje de Quanta Magazine. Es la mayor base de conocimiento matemático verificada por computadora que existe.

El avance de Anthropic muestra tres cosas que incumben a cualquier persona que trabaje con software o IA:

Los modelos de razonamiento ya pueden sostener cadenas largas de trabajo autónomo. No se trata de responder una pregunta: durante 11 días, el modelo produjo un artefacto de más de 13 millones de líneas que compila y verifica. Buzzard confirmó haberlo compilado y ejecutado un comparador: pasa.
La velocidad cambia la economía de la verificación. Buzzard recibió £1 millón para hacerlo en cinco años. Anthropic lo hizo en 11 días. Aunque la cifra exacta gastada por Anthropic no se hizo pública, Buzzard bromea en su blog: "me pregunto si gastaron más dinero".
El ciclo de revisión matemática puede automatizarse de extremo a extremo. "Si miles de páginas de literatura pueden formalizarse de punta a punta por un enjambre de IA en 11 días", escribe Buzzard, "entonces empezaremos a ver la formalización de la investigación moderna haciéndose sobre la marcha".

Qué significa esto para tu startup

Lo que demuestra Claude con FLT es una capacidad operativa nueva: IA capaz de producir durante días, sin intervención humana, un artefacto verificable extremadamente grande y técnicamente denso. Esa capacidad se traduce directamente a tres áreas donde founders hispanohablantes están construyendo producto hoy:

Verificación formal de software crítico. Empresas de fintech, salud o defensa ya usan asistentes de pruebas como Lean, Coq o Isabelle para auditar código. Un modelo que produce 13 millones de líneas en 11 días abarata drásticamente auditorías que antes costaban meses de ingeniería.
Migración y refactorización masiva de código legacy. El mismo patrón (leer mucho, sintetizar, reescribir, verificar) se aplica a traducir un monolito COBOL a un stack moderno, actualizar dependencias con breaking changes, o reescribir una API pública preservando comportamiento.
Síntesis de corpus regulatorios o legales extensos. Documentación tributaria de varios países, normativas GDPR + LATAM, prospectos financieros: formalizarlos en estructuras consultables es exactamente el mismo problema que el que resolvió Claude con FLT.

Tres acciones concretas que puedes tomar esta semana:

Audita qué parte de tu producto podría pasar de "revisión manual" a "revisión formal asistida por IA". Sectores como pagos, salud y compliance regulatorio son los primeros candidatos. Un POC con Lean o con herramientas de verificación basadas en LLMs hoy se monta en días, no en meses.
Construye sobre Lean o sobre bases equivalentes en lugar de empezar desde cero. Anthropic eligió Lean porque mathlib ya tenía 260.000 teoremas verificados. Tu equipo no necesita tener todo el conocimiento: necesita saber a qué corpus consultar y cómo encadenar sobre él.
Prepárate para que "verificable" sea un argumento de venta. En mercados donde la confianza cuesta (banca, seguros, salud), poder demostrar que tu código pasó una verificación formal va a pasar de curiosidad técnica a ventaja comercial. Empieza a mapear qué partes de tu stack podrían certificarse primero.

Lo que Buzzard aún tiene por hacer (y por qué el proyecto humano sigue vivo)

Buzzard aclara en su blog que no se queda sin trabajo. Su proyecto con EPSRC no consistía solo en cerrar FLT: incluía hacer pull requests a mathlib añadiendo objetos fundamentales de la teoría de números moderna, y —lo que él considera más importante— construir un documento dinámico que permita a humanos explorar la demostración moderna paso a paso. "Mi conjetura es que es poco probable que Anthropic haga esto", escribe; "sentirán que su trabajo terminó con la formalización".

Esa segunda parte, la de hacer la matemática legible y navegable para personas, sigue siendo un trabajo profundamente humano. Y es, probablemente, donde la mayoría de startups que estén construyendo herramientas de IA para conocimiento técnico deberían mirar: no a sustituir al experto, sino a darle a su cliente una forma de entender lo que el modelo produjo.

Conclusión

El cierre de FLT en Lean es, sobre todo, una demostración de fuerza operativa: Claude ejecutó durante 11 días un trabajo técnico monumental y produjo un artefacto verificable. Para los matemáticos no cambia casi nada —la demostración ya se conocía desde 1995—, pero para quien construye productos sobre IA cambia el techo de lo que se puede delegar. La pregunta para el próximo año no es si la IA puede formalizar teoremas; es qué otros corpus enormes y técnicamente densos se vuelven tratables cuando un modelo puede dedicar 11 días seguidos a producirlos.