Claude formalizó el Último Teorema de Fermat en 11 días: 13 millones de líneas de Lean
Un modelo de Anthropic trabajó once días seguidos, sin supervisión humana intermedia, y salió con algo que ningún sistema automático había logrado antes: la primera demostración completa del Último Teorema de Fermat verificada por computadora. Trece millones de líneas de código Lean. Treinta mil trescientos teoremas demostrados por el camino. Y un verificador que, al final, aceptó la prueba usando solo sus tres axiomas estándar.
Qué hizo el modelo con el Último Teorema de Fermat
El proyecto terminó el 18 de agosto y Anthropic lo publicó el 4 de septiembre de 2026. El sistema fue un modelo interno de investigación que la compañía describe como aproximadamente comparable a Claude Fable 5.1, y funcionó de forma autónoma durante los once días.
Las cifras dan la escala del esfuerzo: unos 6.000 millones de tokens de salida, 30.300 teoremas demostrados y 29.500 de ellos efectivamente utilizados en la prueba final. El resultado es una formalización en Lean, el asistente de demostración que permite que una máquina revise cada paso lógico sin confiar en la intuición de nadie.
La verificación es la parte que importa. Lean validó la demostración completa apoyándose únicamente en sus tres axiomas estándar, y un comparador independiente confirmó que el enunciado formalizado coincide con el del Último Teorema de Fermat tal como está registrado en Mathlib, la biblioteca matemática de referencia. No es una prueba que haya que creerle a un modelo de lenguaje: es una prueba que otro programa puede revisar línea por línea.
Quién revisó la prueba del Último Teorema de Fermat
Kevin Buzzard, matemático del Imperial College London y una de las figuras centrales de la formalización moderna, revisó el trabajo. Del lado de Anthropic, Tianyi Peng lideró el uso de Prove2Me, una plataforma desarrollada con Columbia University que organiza los enunciados en un grafo acíclico dirigido, de modo que el modelo pueda atacar subproblemas en paralelo y reutilizar lo ya demostrado.
Ese detalle explica cómo se sostiene un proyecto de once días: no es un modelo escribiendo trece millones de líneas de corrido, sino un sistema que descompone, prueba, verifica y ensambla.
Lo que Anthropic reconoce que salió mal
Conviene la honestidad aquí, y la compañía la tuvo. Cerca del 7% de las líneas no repetitivas provienen de intentos fallidos que quedaron en el código. La demostración, admiten, es probablemente mucho más larga de lo necesario. Y el proceso fue intensivo en tokens de una forma que hoy no escala a cualquier problema abierto.
Traducido: esto no significa que la matemática esté resuelta. Significa que un sistema automático puede sostener un razonamiento formal durante días y producir algo verificable, aunque sea desprolijo.
Qué significa para América Latina
Hay una lectura que va mucho más allá de la teoría de números.
La verificación formal deja de ser un lujo académico. Lo que se demostró con el Último Teorema de Fermat es que un modelo puede generar pruebas que una máquina revisa sin necesidad de confiar en el modelo. Ese es exactamente el problema que tiene cualquier entidad que quiera usar IA en algo crítico: no se trata de creerle al sistema, sino de poder auditarlo. Para un banco, una entidad de salud o un operador de infraestructura en la región, la ruta de la verificación formal es más interesante que cualquier benchmark de conversación.
El cómputo sigue siendo la barrera. Seis mil millones de tokens de salida no los paga un departamento de matemáticas latinoamericano. La región tiene matemáticos de primer nivel —en Bogotá, Ciudad de México, Buenos Aires, São Paulo— y presupuestos de cómputo que no dan para once días de inferencia continua. La ventaja de estos proyectos es que el resultado queda público en Mathlib: cualquiera puede construir encima sin repetir el gasto.
Y hay una oportunidad concreta de nicho. Formalizar matemáticas en Lean es una habilidad que se aprende con tiempo y disciplina, no con acceso a GPU. Es de los pocos frentes donde un investigador de la región puede competir de igual a igual, y donde la demanda va a crecer conforme más laboratorios intenten replicar este tipo de trabajo.
El punto de fondo
El Último Teorema de Fermat le tomó a Andrew Wiles siete años en los noventa, y a la comunidad matemática tres siglos y medio antes de eso. Formalizarlo en Lean era un proyecto que se estimaba en años de trabajo humano coordinado. Un modelo lo hizo en once días, con desperdicio y todo.
Lo interesante no es la velocidad. Es que el resultado se puede verificar sin confiar en quien lo produjo. Eso es lo que la industria lleva dos años sin poder ofrecer.
Sitio oficial:
Investigación publicada por Anthropic ·
Lean
Reportado por: Anthropic Research — Mathlib Community
Lee también:
