Claude formaliza el último teorema de Fermat en Lean en solo 11 días
Índice de contenidos
Claves de la noticia
- La prueba publicada es verificable por Lean y no introduce axiomas distintos de los tres estándares que usa su biblioteca matemática.
- Decenas de agentes Claude trabajaron durante once días y generaron 13 millones de líneas, más de cinco veces el tamaño de Mathlib.
- El logro formaliza una demostración conocida; no sustituye la prueba de Wiles ni constituye una demostración matemática nueva.
Anthropic ha publicado el primer desarrollo completo del último teorema de Fermat comprobado por ordenador. Un sistema de agentes Claude escribió 13 millones de líneas de Lean y encadenó 29.500 resultados intermedios durante once días.
Una verificación completa, no un nuevo teorema
Anthropic ha abierto el código de la primera formalización integral y comprobable por máquina del último teorema de Fermat. El resultado traduce a Lean 4 la cadena matemática que parte de Frey, Serre y Ribet y culmina en el trabajo de Andrew Wiles y Richard Taylor. La distinción es esencial: Claude no descubrió que la ecuación carece de soluciones para exponentes mayores que dos, algo demostrado en 1995, sino que convirtió el argumento en objetos lógicos que un núcleo pequeño puede revisar paso a paso.
El repositorio incluye una sentencia explícita para números naturales positivos y obliga a que la compilación falle si la prueba depende de un axioma añadido, de una admisión temporal o de un atajo nativo. Anthropic también utilizó un comparador para confirmar que su formulación coincide con la de Mathlib. La comprobación automática no garantiza que el código sea elegante ni pedagógico, pero sí reduce la confianza necesaria en una lectura humana de millones de pasos.
Trece millones de líneas explican la escala
El sistema produjo 30.300 teoremas auxiliares y conservó 29.500 en la prueba final. Sus 13 millones de líneas superan en más de cinco veces el tamaño de Mathlib, la biblioteca comunitaria sobre la que se apoya. Esa desproporción no significa que la IA haya creado cinco bibliotecas nuevas: Mathlib está condensada y revisada durante años, mientras el artefacto de Anthropic prioriza llegar a una ruta verificable y contiene abundante desarrollo que después podría simplificarse.
Claude trabajó con una versión interna de capacidad parecida a Fable 5.1 y consumió alrededor de 6.000 millones de tokens de salida. Decenas de agentes se repartieron definiciones y lemas, pero los primeros intentos se descoordinaron. Cerca del 7 % de las líneas útiles procede de esas vías fallidas. La cifra revela que el avance no fue una única respuesta brillante: necesitó una infraestructura que mantuviera el estado, repartiera objetivos y permitiera reutilizar resultados.
Prove2Me convirtió la prueba en un grafo
El cambio decisivo fue Prove2Me, una plataforma colaborativa desarrollada por Tianyi Peng y colegas de Columbia. En vez de pedir a cada agente que recordara la campaña completa, el sistema conservó un grafo acíclico de teoremas pendientes y demostrados. Separó en archivos las declaraciones y las pruebas, aceleró la compilación y añadió descripciones en lenguaje natural para facilitar búsquedas. Esa arquitectura atacó el problema operativo de la memoria degradada y la duplicación de trabajo.
La intervención humana se limitó, según Anthropic, a indicaciones ocasionales de alto nivel sobre prioridades matemáticas. Kevin Buzzard, responsable del proyecto académico de formalización iniciado en 2024, revisó el artefacto y destacó que solo descansa en los axiomas habituales. Su evaluación aporta una comprobación externa relevante, aunque no equivale a una auditoría independiente de cada decisión de ingeniería ni resuelve cómo integrar una masa tan grande de código en una biblioteca mantenible.
La comparación histórica evita exagerar el anuncio
Wiles presentó en 1993 una prueba que contenía una laguna y necesitó cerca de un año, junto a Taylor, para repararla. Una formalización exige aún más detalle que una exposición humana porque no puede saltarse pasos considerados obvios. El proyecto de Imperial esperaba años de trabajo. Completar una ruta en once días cambia la escala temporal, pero se beneficia de esa literatura, de Mathlib, del plano académico existente y de una demostración simplificada de Darmon, Diamond y Taylor.
Un recuento directo de los datos publicados muestra una productividad media de unos 1,18 millones de líneas y 2.680 teoremas intermedios por día. Esa división no describe un ritmo constante ni calidad editorial, pero dimensiona por qué la coordinación automática importa tanto como el modelo. El resultado sugiere que la formalización masiva puede pasar de proyecto artesanal a proceso computacional, mientras la comprensión humana continúa siendo necesaria para decidir qué merece demostrarse y cómo comunicarlo.
Lean ofrece una salida al cuello de botella científico
Los modelos ya producen conjeturas y argumentos a una velocidad que puede desbordar a revisores. Una prueba formal adjunta permite verificar consistencia lógica sin delegar la confianza en el propio modelo que la escribió. Anthropic sostiene que esto puede descubrir errores en el corpus matemático y aligerar el arbitraje. También probó tres suscripciones personales de Claude Max y completó en tres días una formalización relacionada con el teorema de los tres primos de Vinogradov, señal de que el método no depende únicamente de un clúster cerrado.
Persisten límites prácticos. Una prueba gigantesca puede ser difícil de mantener, reutilizar o enseñar; un núcleo correcto no valida que la especificación refleje exactamente la pregunta informal; y el coste de 6.000 millones de tokens está lejos de una tarea cotidiana. El valor inmediato del repositorio reside en que cualquiera puede inspeccionarlo y recompilarlo. Esa reproducibilidad separa este anuncio de una afirmación de laboratorio imposible de contrastar y ofrece material concreto para que la comunidad evalúe dónde termina la automatización y empieza la curaduría.
