Claude formaliza el Último Teorema de Fermat: la primera demostración completa verificada por ordenador

Qué se ha anunciado exactamente

Anthropic publicó el 4 de septiembre de 2026 una página de investigación, un post de blog y un repositorio abierto en GitHub con la formalización completa del Último Teorema de Fermat en Lean 4. El teorema en sí lleva demostrado desde 1995, cuando Andrew Wiles cerró un enunciado que había resistido 358 años. Lo nuevo no es el resultado matemático, sino que por primera vez la demostración entera está escrita en un lenguaje que un programa puede comprobar paso a paso, sin dejar nada a la interpretación del lector.

El Último Teorema de Fermat afirma algo que se explica en una línea: la ecuación x elevado a n más y elevado a n igual a z elevado a n no tiene soluciones con números enteros positivos cuando n es mayor que 2. Para n igual a 2 sobran soluciones (3, 4 y 5, por ejemplo). A partir de ahí, ninguna. Esa simplicidad aparente es la que convirtió el problema en una obsesión durante tres siglos y medio, y la que contrasta con las cientos de páginas de matemáticas avanzadas que hicieron falta para cerrarlo.

Qué significa formalizar una demostración

Una formalización consiste en traducir una demostración escrita en el lenguaje habitual de los matemáticos —prosa, notación y una buena dosis de pasos que se dan por evidentes— al lenguaje de un asistente de pruebas, un programa que verifica mecánicamente cada inferencia. Lean 4 es uno de esos asistentes: si acepta un teorema, es porque ha comprobado que se deduce de los axiomas de partida sin ningún salto. El teorema formalizado, es decir verificado paso a paso por un programa, ofrece una garantía de corrección que ninguna revisión humana puede igualar.

La formalización de Claude se apoya en Mathlib, la biblioteca comunitaria de matemáticas de Lean 4, y utiliza únicamente los tres axiomas estándar del sistema. Tampoco contiene ningún sorry, la instrucción con la que Lean permite dejar un hueco pendiente de demostrar: si hubiera uno solo, el edificio no se sostendría. Dos verificadores externos independientes, comparator y nanoda, revisaron el resultado.

Once días, agentes en paralelo y ninguna línea humana

El trabajo se hizo entre el 7 y el 17 de agosto de 2026 sobre Prove2Me, una plataforma desarrollada por el grupo de Tianyi Peng en la Universidad de Columbia. Varios agentes de Claude trabajaron en paralelo repartiéndose tres funciones: escribir los enunciados de los teoremas intermedios, revisarse esos enunciados entre ellos y demostrarlos. Los humanos del equipo de Anthropic aportaron el enunciado de una línea del teorema objetivo y, de vez en cuando, comentarios sobre qué priorizar o simples mensajes de ánimo. Ni una línea de matemáticas, ni una línea de Lean.

Las cifras dan la medida del esfuerzo: 29.511 teoremas en el árbol final del que depende el enunciado principal y unos 30.300 demostrados en total en la plataforma, con unos 533.000 lemas de apoyo locales repartidos por los ficheros. En conjunto, unos 13 millones de líneas de código Lean, que bajan a unos 10,5 millones si se descuenta el boilerplate, el código repetitivo generado automáticamente. Ciento seis ficheros se adaptaron, con crédito, del proyecto de formalización de Fermat del Imperial College London y del proyecto flt-regular.

Ese proyecto del Imperial College, financiado por el EPSRC (el consejo británico de investigación en ingeniería y ciencias físicas), lleva años trabajando en la misma meta con equipos humanos. Claude no partió de cero: se apoyó en su blueprint, el plan detallado que descompone la demostración en piezas manejables. La ruta seguida es la clásica de Wiles y Taylor-Wiles, tal como la expusieron Darmon, Diamond y Taylor: se construye una curva de Frey a partir de una hipotética solución, se invoca el teorema de Mazur, se pasa por Langlands-Tunnell en el primo 3, se cambia del primo 3 al 5, se aplica el paso de elevación de modularidad conocido como R=T y se remata con el teorema de Ribet, que rebaja el nivel hasta 2, donde sencillamente no existen las formas que harían falta. La contradicción cierra el argumento.

Por qué importa y qué no demuestra

Es el ejemplo más ambicioso hasta la fecha de una inteligencia artificial haciendo matemáticas verificadas de forma autónoma y sostenida en el tiempo. No se trata de resolver un problema de examen en segundos, sino de mantener durante once días un proyecto de miles de piezas encajadas, con varios agentes coordinándose y corrigiéndose. Si esa capacidad se generaliza, la demostración formal deja de ser un lujo reservado a resultados célebres y se convierte en una herramienta rutinaria, primero en matemáticas y a la larga en software crítico, donde un error verificable a tiempo vale mucho dinero y a veces vidas.

Conviene también acotar el alcance. La garantía que aporta Lean es de corrección lógica, no de comprensión: la máquina ha producido una cadena de deducciones que el verificador acepta, y el debate sobre si eso equivale a entender las matemáticas sigue tan abierto como antes. La propia Anthropic añade una cautela: no ha verificado de forma independiente las afirmaciones matemáticas que aparecen en los extractos del razonamiento de Claude incluidos en su documento técnico. Lo verificado es el código Lean; los comentarios sobre lo que Claude creía estar haciendo son otra cosa.