Claude formaliza la demostración del teorema de Fermat en Lean

Anthropic anunció el 4 de septiembre de 2026 que su inteligencia artificial Claude había producido la primera demostración del último teorema de Fermat verificable por ordenador de principio a fin. El teorema afirma que no existen enteros positivos a, b, c que cumplan a^n + b^n = c^n para ningún entero n mayor que 2. Más de treinta años después de que el matemático Andrew Wiles publicara su demostración de 129 páginas en 1995, nadie había verificado mecánicamente su lógica desde cero. Claude trabajó de forma en gran parte autónoma durante 11 días y produjo cerca de 13 millones de líneas de código en Lean, un asistente de pruebas informático.

El proyecto lo dirigió Tianyi Peng, investigador de Anthropic especializado en formalización matemática con IA. Durante el proceso, Claude demostró de forma verificable por ordenador unos 30.300 teoremas intermedios, de los cuales aproximadamente 29.500 se usaron en la demostración final. El código resultante supera cinco veces el tamaño de Mathlib, la principal biblioteca matemática comunitaria de Lean. Decenas de agentes Claude trabajaron en paralelo definiendo conceptos y demostrando teoremas intermedios antes de abordar enunciados más difíciles. Los primeros intentos fracasaron: los agentes perdían de vista el estado general del proyecto y dejaban de reutilizar eficazmente los resultados de los demás. Cerca del 7% de las líneas no repetitivas de la demostración final proceden de esos intentos fallidos.

Qué es una demostración formal verificada por ordenador

Un artículo matemático escrito para lectores humanos suele omitir pasos considerados "evidentes". Un asistente de pruebas como Lean no puede: cada paso, por trivial que sea, debe quedar explícito. Reescribir una demostración existente en esa forma se llama "formalización". Como un solo eslabón lógico roto puede invalidar todo lo que viene después, una demostración formalizada solo obtiene una garantía de corrección independiente de la revisión humana cuando supera el control mecánico de Lean. La de Claude solo depende de los tres axiomas estándar de Lean, sin ningún uso de "sorry", el marcador que permite dejar un paso temporalmente sin demostrar. Una herramienta de comparación confirmó que el enunciado demostrado coincide con el del último teorema de Fermat en Mathlib, y un núcleo Lean independiente escrito en Rust, llamado "nanoda", verificó más de un millón de declaraciones sin errores.

Por qué el teorema de Fermat es un caso tan emblemático

El teorema debe su nombre a una nota que el matemático francés Pierre de Fermat garabateó hacia 1637 en el margen de un ejemplar de la Aritmética de Diofanto, donde afirmaba haber hallado "una demostración verdaderamente maravillosa" que el margen era demasiado estrecho para contener. Durante más de 350 años, generaciones de matemáticos buscaron esa demostración sin éxito. En 1908 se ofreció un premio equivalente hoy a uno o dos millones de dólares por una demostración correcta; solo en el primer año llegaron 621 intentos erróneos. En junio de 1993, Andrew Wiles anunció su demostración en una serie de conferencias de tres días, pero unos dos meses después, durante la revisión, un evaluador detectó un fallo crítico. A Wiles le costó casi un año, junto a su antiguo alumno Richard Taylor, corregirlo antes de publicar la versión definitiva en mayo de 1995: 129 páginas que la comunidad matemática tardó meses en verificar. Un dato notable para un lector internacional: la conjetura de Taniyama-Shimura, en la que se apoya la demostración de Wiles, fue formulada en los años 50 por los matemáticos japoneses Yutaka Taniyama y Goro Shimura. Lo que Claude formalizó es una versión simplificada de la demostración de Wiles, debida a Darmon, Diamond y Taylor.

Este extraordinario logro de autoformalización, que según los investigadores de Anthropic solo llevó 11 días, demuestra el teorema de Fermat sin más hipótesis que los axiomas de las matemáticas. En el proceso vemos la autoformalización del álgebra, el análisis armónico, la geometría y la teoría de números, y aprendemos que los artefactos de autoformalización producidos por IA ya son lo bastante robustos como para construir sobre ellos: la demostración tiene varias capas.

• Duración del trabajo: 11 días, en gran parte de forma autónoma
• Código Lean producido: unos 13 millones de líneas, más de 5 veces Mathlib
• Teoremas demostrados: unos 30.300, de los cuales 29.500 usados en la demostración final
• Tokens de salida consumidos: unos 6.000 millones, con un modelo de investigación comparable a Claude Fable 5.1
• Axiomas utilizados: solo los 3 axiomas estándar de Lean, cero usos de "sorry"

Lo que Claude hizo realmente, y sus límites

Conviene subrayar que Claude no "descubrió" por sí solo la demostración original de Wiles. El razonamiento matemático lo establecieron Wiles y sus colaboradores en 1995; el trabajo de Claude consistió en reescribir una versión simplificada de ese razonamiento en la forma simbólica rigurosa que Lean puede verificar, y luego someterla a un control mecánico: eso es formalización, no descubrimiento. Es distinto de los trabajos recientes de IA sobre la hipótesis de Riemann, orientados a producir matemáticas realmente nuevas. Anthropic sitúa explícitamente la novedad de este trabajo en la verificación, no en el descubrimiento. El proyecto se apoyó en Prove2Me, una plataforma colaborativa de formalización matemática creada por Tianyi Peng, que gestiona las dependencias entre teoremas mediante un grafo dirigido acíclico para que varios agentes Claude sepan qué teorema abordar a continuación. La intervención humana se limitó a instrucciones de alto nivel de Peng, como "priorizar el jacobiano como esquema".

A medida que la IA produce más demostraciones matemáticas, aumenta la carga de revisarlas a mano. Anthropic espera que producir una demostración formalizada y verificable por ordenador, junto a un artículo pensado para lectores humanos, se convierta en algo habitual. Kevin Buzzard, que desde 2024 dirige un proyecto comunitario plurianual para formalizar el teorema de Fermat en Lean en el Imperial College de Londres —cuyo plan de trabajo inicial ya alcanza las 86 páginas—, calificó el logro como un gran paso hacia la autoformalización de la literatura matemática moderna: detectar errores en el corpus existente, aliviar la carga de los revisores y permitir verificar rigurosamente matemáticas generadas por IA.

Para una empresa española o latinoamericana de tecnología, la lección va más allá del logro matemático en sí. Los mismos asistentes de pruebas que verificaron este teorema ya se usan para verificar protocolos criptográficos, compiladores y código crítico en aeronáutica o diseño de semiconductores. Que un agente de IA pueda producir millones de líneas de prueba verificada en días, y no en años, es una señal concreta de que la verificación formal, considerada durante mucho tiempo demasiado lenta y especializada, podría volverse mucho más accesible para equipos de ingeniería ajenos a las matemáticas puras, siempre que, como recalca la propia Anthropic, esta capacidad de verificación no se confunda con una capacidad de descubrir matemáticas nuevas de forma autónoma.