Anthropic ha publicado en GitHub una demostración completa del último teorema de Fermat verificada por máquina en el asistente de pruebas Lean 4, un hito que combina más de tres décadas de matemáticas avanzadas con las técnicas más recientes de verificación formal automatizada. El repositorio, presentado como artefacto de investigación sin mantenimiento activo, formaliza el argumento clásico de Frey, Serre, Ribet, Wiles y Taylor–Wiles sobre la imposibilidad de que existan soluciones enteras positivas a la ecuación aⁿ + bⁿ = cⁿ para n mayor o igual a 3.
El núcleo del proyecto es el teorema fermat_last_theorem, declarado en Theorems/Thm_fermat_last_theorem.lean, que enuncia exactamente la propiedad esperada: para cualquier número natural n ≥ 3 y cualesquiera enteros positivos a, b y c, la suma aⁿ + bⁿ es distinta de cⁿ. El archivo FinalCheck.lean obliga a que la prueba descanse únicamente sobre tres axiomas estándar de Lean (propext, Classical.choice y Quot.sound), sin uso de sorry, axiomas añadidos o native_decide; de lo contrario, la construcción falla. Además, FinalCheck.lean deriva la formulación de Mathlib, FermatLastTheorem, a partir de este teorema, garantizando la equivalencia entre ambas.
La construcción se realizó desde cero con Lean 4.33.1, que incorpora las correcciones de solidez del kernel de 2026, compilando Mathlib a partir del código fuente. Los 60.475 módulos del repositorio fueron verificados por el kernel de Lean. La auditoría se completó con dos herramientas adicionales. Por un lado, el comparador leanprover/comparator v4.33.0 confirmó que la declaración probada y todas las constantes mencionadas son idénticas a las del reto de verificación, que no se utiliza ningún axioma ajeno y que toda la prueba, incluida Mathlib, se reproduce a través del kernel de Lean. Por otro lado, nanoda 0.4.13, un kernel de Lean independiente escrito en Rust, aceptó una exportación del mismo entorno con 1.052.234 declaraciones comprobadas sin errores.
En conjunto, las verificaciones establecen que el enunciado se deduce exclusivamente de los tres axiomas mencionados, confiando en el kernel de Lean o en nanoda y en sus herramientas de apoyo. La demostración se apoya únicamente en los números naturales, la suma, el orden, la desigualdad y la exponenciación de Lean, esta última redefinida en Mathlib como la exponenciación nativa del lenguaje. Lo que ninguna herramienta puede comprobar es que cada teorema intermedio signifique lo que su nombre sugiere; esa interpretación queda a juicio del lector, y el archivo PROOF-PATH.md identifica el teorema de Lean asociado a cada paso del razonamiento matemático clásico.
El repositorio incluye además una carpeta html de unos 390 MB que presenta la demostración como páginas web navegables sin conexión: la ruta de la prueba paso a paso, una página por cada uno de los 29.511 teoremas y de los 1.450 módulos de definiciones, un buscador sobre todos los nombres y un grafo de los teoremas clave. Los textos en inglés y las referencias sugeridas se generan automáticamente, mientras que la declaración en Lean constituye la fuente autorizada.
Requisitos técnicos y atribuciones. La construcción exige Linux o macOS —las rutas son demasiado largas para Windows—, la herramienta elan y conexión de red, ya que Lake descarga Mathlib desde GitHub y la compila en unos 13 minutos con 96 trabajos. El proceso necesita alrededor de 5 GB de memoria por trabajo paralelo y unos 67 GB de disco en .lake/, más ficheros C que pueden borrarse durante la compilación. El proceso completo de Anthropic tardó 5 horas y 32 minutos con un pico de 153 GB de memoria. El comparador requiere unas 15 horas y 230 GB de pico, mientras que la exportación para nanoda consume unos 90 GB durante una hora y la comprobación unos 40 GB durante media hora.
El proyecto se distribuye bajo licencia Apache 2.0 con copyright de Anthropic, PBC, correspondiente a 2026, e incorpora material de tres proyectos previos también bajo Apache 2.0: el proyecto FLT del Imperial College London liderado por Kevin Buzzard, que aporta el paquete Frey, representaciones de Galois, teoría de deformaciones y técnicas de parcheo; flt-regular, que aporta el teorema de Kummer; y la propia Mathlib. ATTRIBUTION.md enumera los 106 ficheros con material de los dos primeros proyectos y los 23 ficheros que reproducen texto de Mathlib.
El avance marca un nuevo estándar en la verificación formal de resultados matemáticos de gran profundidad. Demostraciones que durante años solo se conocían en formato de artículo y cuya revisión dependía del juicio de expertos se convierten ahora en artefactos verificables byte a byte por un kernel independiente. La consecuencia es doble: por un lado, refuerza la confianza en la corrección lógica del teorema; por otro, abre la puerta a que el resto de la literatura matemática pueda someterse a procesos análogos de formalización y auditoría automatizada. Anthropic presenta el trabajo como un artefacto de investigación, sin vocación de mantenimiento, lo que sugiere que el siguiente paso será observar si la comunidad matemática adopta Lean como infraestructura estándar para la verificación de pruebas de gran envergadura.