AIREITERCuando un titular dice que «Claude ha resuelto el último teorema de Fermat», conviene fijarse en una palabra: formalizado. Anthropic ha publicado un artefacto de Lean que, según la compañía, comprueba el teorema de principio a fin. Pero el recorrido matemático es el ya conocido —el argumento de Frey–Serre–Ribet–Wiles–Taylor-Wiles—, no una demostración recién descubierta.
La diferencia entre las dos afirmaciones
La respuesta estricta es sí: Anthropic ha publicado un repositorio con una formalización en Lean 4 del último teorema de Fermat (FLT), junto con instrucciones para compilarla y verificarla. Lo que no es correcto es decir que Claude resolvió por su cuenta este famoso problema; el avance matemático fundamental lo lograron Andrew Wiles y Richard Taylor hace décadas.
El FLT afirma que no existen soluciones en enteros positivos para a^n + b^n = c^n cuando n > 2. La demostración de Wiles se publicó en 1995; el trabajo de Anthropic convierte ese recorrido ya establecido en un artefacto comprobable por máquina. Para conocer el contexto histórico, consulta el anuncio del proyecto FLT de Lean Community.
Una demostración en Lean responde a una pregunta distinta de la que plantea un artículo matemático informal. Puede demostrar que una proposición codificada con precisión se deduce de definiciones, dependencias y axiomas comprobados en un entorno concreto. No demuestra que una IA haya inventado las matemáticas subyacentes ni que los nombres de los teoremas coincidan con lo que describen.
Qué ha publicado realmente Anthropic
En su artículo de investigación del 4 de septiembre de 2026, Anthropic afirma que Claude produjo la primera formalización completa de principio a fin del FLT en Lean, comprobada por ordenador, en 11 días. El artículo habla de aproximadamente 13 millones de líneas de Lean, 30.300 enunciados de teoremas demostrados y 29.500 utilizados en la prueba final. También cifra en unos 6.000 millones los tokens generados.
El trabajo se apoyó en Prove2Me, una plataforma que Anthropic describe como un sistema que mantiene un grafo dirigido acíclico de enunciados matemáticos y coordina varios agentes. Según la compañía, la formalización sigue una exposición simplificada del recorrido clásico asociado a Frey, Serre, Ribet, Wiles y Taylor-Wiles.
Para comprobar la afirmación, el repositorio público de GitHub resulta más útil que el anuncio. Su objetivo predeterminado es FinalCheck.lean, y la declaración del teorema es:
theorem fermat_last_theorem (n : ℕ) (hn : 3 ≤ n) (a b c : ℕ)
(ha : 0 < a) (hb : 0 < b) (hc : 0 < c) :
a ^ n + b ^ n ≠ c ^ nEl propio repositorio se define como un artefacto de investigación que no recibe mantenimiento ni acepta contribuciones. Fija Lean 4.33.1 y Mathlib v4.33.0, incluye PROOF-PATH.md y ofrece una versión HTML navegable sin conexión del grafo de teoremas y definiciones.
La comprobación final del repositorio está diseñada para fallar si la prueba depende de un axioma añadido, sorry, native_decide, unsafe o algún recurso de escape parecido. Así, el artefacto se puede inspeccionar sin tener que confiar únicamente en una captura de pantalla o en un resumen redactado.
Cómo verificarlo de forma reproducible
Una comprobación seria empieza por el entorno fijado por el repositorio, no por copiar un archivo .lean aislado en otro proyecto. La guía de verificación de Lean Community explica el motivo: Lean se publica mensualmente, Mathlib cambia con frecuencia y la compatibilidad hacia atrás no está garantizada.
Fija el entorno antes de compilar
El repositorio indica que la compilación está pensada para Linux o macOS y requiere elan, Git, Python, GNU coreutils y conexión a Internet para que Lake pueda descargar y compilar las dependencias fijadas. También calcula unos 67 GB dentro de .lake, además de aproximadamente 220 GB de archivos C generados que pueden borrarse después.
El repositorio calcula asimismo unos 5 GB de memoria por trabajo paralelo, aunque algunos módulos pueden requerir hasta 36 GB. Con 96 trabajos, su propia compilación tardó 5 horas y 32 minutos y alcanzó un pico de 153 GB de memoria. Son cifras comunicadas por el repositorio, no mediciones realizadas en este artículo; tómalas como una advertencia para planificar, no como un tiempo de ejecución garantizado.
Elige una vía de verificación
- Solo inspección: lee
FinalCheck.lean,PROOF-PATH.mdyATTRIBUTION.mdsin compilar. - Compilación completa de Lean: utiliza la cadena de herramientas fijada y ejecuta
lake build. - Reproducción independiente: después de una compilación y exportación correctas, ejecuta los scripts de comparator y nanoda.
Tras clonar el repositorio desde cero, sus instrucciones proponen esta secuencia general:
git clone https://github.com/anthropics/fermats-last-theorem.git flt
cd flt
# Reduce el número si tu máquina no puede proporcionar la memoria necesaria.
LEAN_NUM_THREADS=96 lake build
# Comprueba el resultado frente a un enunciado de desafío que solo utiliza Mathlib.
verification/comparator/run.sh
# Ejecútalo después de la comprobación de comparator.
verification/nanoda/run.shCada etapa cumple una función distinta:
| Etapa | Detalle comunicado por el repositorio | Para qué sirve |
|---|---|---|
lake build | 60.475 módulos; 5 h 32 min con 96 trabajos en la ejecución comunicada | Compila el proyecto desde el código fuente y permite que el kernel de Lean compruebe las declaraciones incluidas en la compilación |
| Comparator | 14 h 46 min en la ejecución comunicada; pico de memoria de 230 GB | Comprueba que el teorema expuesto y las constantes referenciadas coinciden con el enunciado de desafío previsto en Mathlib |
nanoda | Unos 30 minutos con 16 hilos después de la exportación | Reproduce un entorno exportado mediante un kernel de Lean independiente escrito en Rust |
Comparator no sustituye la lectura del enunciado del teorema. Ayuda a detectar el riesgo de que un proyecto demuestre una proposición debilitada o ligeramente distinta. El PROOF-PATH.md del repositorio relaciona los pasos matemáticos con nombre con sus declaraciones en Lean, mientras que las páginas HTML generadas permiten inspeccionar las dependencias sin tener que poner en marcha una aplicación web.
El repositorio informa de costes adicionales para estas comprobaciones: escribir una exportación de 37,8 GB puede requerir unos 90 GB de memoria, y el flujo de trabajo de nanoda puede necesitar unos 40 GB durante la comprobación.
Qué demuestra la evidencia —y qué no—
| Capa de evidencia | Lo que establece | Lo que no establece |
|---|---|---|
| Compilación del kernel de Lean | Que los términos de prueba enviados son válidos en el entorno de Lean fijado | Que Claude haya descubierto las matemáticas, o que la explicación informal coincida con cada nombre de teorema |
FinalCheck.lean y la protección contra axiomas | Que el teorema final del repositorio se comprueba frente a la lista de axiomas indicada y rechaza varios atajos concretos | Que el teorema sea el enunciado histórico del FLT si no se inspecciona el propio enunciado |
Salida de #print axioms | Que las dependencias incluyen los tres axiomas estándar de Lean —propext, Classical.choice y Quot.sound— en lugar de un axioma de usuario oculto, cuando la comprobación esperada pasa | Que toda la cadena de suministro de software haya sido validada de forma independiente |
| Comparator | Que el resultado demostrado y las constantes referenciadas coinciden con el desafío que solo utiliza Mathlib empleado por el repositorio | Que todas las descripciones en lenguaje natural del proyecto sean claras o pedagógicamente adecuadas |
| Reproducción con nanoda | Que un segundo kernel de Lean implementado en Rust aceptó un entorno exportado | Que la exportación, los scripts o el sistema operativo estén más allá de cualquier posible error |
PROOF-PATH.md y atribución | Una ruta para que los humanos inspeccionen la correspondencia matemática y las fuentes previas | Que los nombres de teoremas generados por máquina describan correctamente sus enunciados sin revisión humana |
La lista «Did you prove it?» de Lean Community resume la regla esencial: la compilación valida la proposición codificada, no que el nombre de un teorema coincida con la afirmación informal que pretendía representar. En este artefacto, Comparator y su uso de Mathlib reducen ese riesgo, pero no eliminan la necesidad de leer la declaración del teorema y el recorrido de la prueba.
Qué muestra el artefacto —y qué queda fuera—
El sistema ha producido un artefacto de Lean comprobado formalmente y de una escala poco habitual. Eso no demuestra que exista un nuevo recorrido hacia el FLT, una nueva demostración elemental ni un descubrimiento matemático independiente por parte de Claude.
Anthropic afirma que la prueba sigue una versión simplificada del recorrido de Wiles. El repositorio también reconoce trabajos previos: su ATTRIBUTION.md identifica 106 archivos que contienen material del proyecto FLT del Imperial College London o de flt-regular, además de Mathlib. Esa procedencia es importante para describir con precisión sobre qué se construye el artefacto publicado.
El proyecto informa de 30.300 enunciados de teoremas demostrados durante la ejecución y unos 29.500 utilizados en la prueba final, mientras que el repositorio habla de 29.511 páginas de teoremas. Son declaraciones formales y dependencias, no 29.511 resultados matemáticos nuevos. Una prueba formal hace explícitos pasos, tipos, coerciones, definiciones y dependencias de bibliotecas que una demostración humana puede dejar implícitos porque confía en los conocimientos del lector experto.
El repositorio explica que sus fuentes se escribieron para ser comprobadas, no para leerse cómodamente: los nombres se generan automáticamente, etiquetas como P2M identifican etapas del flujo de trabajo y el enunciado, no el nombre, es la autoridad. Por eso el recorrido de la prueba y Comparator importan tanto como el teorema que aparece en el titular.
Los trabajos anteriores en Lean no deben mezclarse con la afirmación de 2026. Un artículo de 2023 sobre el último teorema de Fermat para primos regulares comunicó una formalización completa y sin sorry del Caso I del teorema de Kummer para primos regulares, aunque señalaba que el Caso II y el lema de Kummer todavía requerían un trabajo sustancial. Una revisión de 2025 describió la formalización para primos regulares como una demostración completa de ese caso más limitado.
| Trabajo | Alcance | Función práctica |
|---|---|---|
Investigación de flt-regular | Resultados sobre primos regulares e infraestructura de apoyo en teoría algebraica de números | Bloque formal previo y material de partida |
| Proyecto FLT del Imperial | Formalización reutilizable y a largo plazo de la teoría moderna de números relacionada con el FLT | Infraestructura de bibliotecas y colaboración |
| Repositorio de Anthropic | Un teorema FLT de principio a fin en Lean 4, según se afirma, con comprobaciones de compilación y reproducción | Un gran artefacto de investigación optimizado para obtener un resultado comprobado, no para mantenerlo a largo plazo |
El proyecto FLT de Imperial/Lean describe la formalización de la teoría moderna de números como un esfuerzo de infraestructura más amplio, no como la simple traducción de un teorema. La publicación de Anthropic se entiende mejor como una evidencia complementaria sobre lo que pueden hacer agentes de IA coordinados dentro de un ecosistema formal ya existente, no como una prueba de que los objetivos del proyecto anterior hayan dejado de ser relevantes.
Qué se puede dar por demostrado
| Si quieres saber… | La respuesta responsable es… | Siguiente paso |
|---|---|---|
| Si Anthropic ha publicado un artefacto real | Sí; existe un anuncio oficial y un repositorio público con el entorno fijado | Lee conjuntamente el artículo de investigación y el repositorio |
| Si el teorema codificado es el FLT | El repositorio proporciona una declaración concreta, Comparator y un recorrido de la prueba | Inspecciona FinalCheck.lean, Comparator y PROOF-PATH.md |
| Si el código compila correctamente | El repositorio documenta una compilación desde cero y comunica su propio resultado | Vuelve a compilar con Lean 4.33.1 y Mathlib v4.33.0 si dispones del hardware necesario |
| Si Claude inventó una prueba nueva | No hay pruebas que respalden esa descripción; el recorrido utiliza las matemáticas establecidas de Wiles/Taylor-Wiles | Descríbelo como una formalización asistida por IA o como ingeniería de pruebas |
| Si el artefacto es fácil de mantener | No; el repositorio se define explícitamente como no mantenido y su código se genera automáticamente | Trátalo como un artefacto de investigación, no como una biblioteca de Mathlib lista para usar |
| Si demuestra una autonomía matemática general | No; muestra resultados en un objetivo de formalización muy especificado y con una infraestructura considerable | Distingue entre capacidad de verificación formal y descubrimiento abierto de teoremas |
Si solo necesitas conocer la noticia, el anuncio oficial y el repositorio bastan para confirmar que el proyecto existe. Si necesitas auditarlo, reproduce la compilación fijada e inspecciona el enunciado. Si estás evaluando investigación en IA, incluye en el análisis la orquestación, las bibliotecas existentes, la formalización previa y el coste computacional del sistema.
Preguntas frecuentes
¿Descubrió Claude una nueva demostración del último teorema de Fermat?
No. El artefacto de Anthropic formaliza un recorrido ya establecido, asociado a Frey, Serre, Ribet, Wiles y Taylor-Wiles. El logro está en la escala y la velocidad con que se ha producido un artefacto de Lean comprobable por máquina, no en una nueva solución matemática.
¿Una compilación correcta en Lean demuestra el teorema informal?
Demuestra que la proposición codificada se deduce de las dependencias comprobadas en ese entorno de Lean. Aun así, debes verificar que la proposición y sus definiciones se corresponden con el teorema informal que quieres afirmar.
¿Utiliza el repositorio sorry o axiomas adicionales?
El repositorio afirma que su comprobación final rechaza sorry, los axiomas añadidos, native_decide, unsafe y varios atajos relacionados. La lista de axiomas esperada contiene los tres axiomas estándar de Lean: propext, Classical.choice y Quot.sound; reproduce la comprobación en lugar de confiar únicamente en el anuncio.
¿Puedo reproducir el resultado en un portátil normal?
Es posible que puedas inspeccionar y compilar parcialmente el repositorio, pero la verificación completa no es una tarea ligera habitual. El repositorio informa de un pico de 153 GB de memoria durante la compilación, hasta 230 GB para Comparator y unas necesidades de almacenamiento considerables, así que el hardware es una limitación central.
Para comprobar la afirmación con precisión, empieza por el artefacto fijado de GitHub, lee la declaración del teorema antes de quedarte con el titular y describe el resultado como una gran formalización, asistida por IA, de matemáticas conocidas.