¿Ha "resuelto" la IA el último teorema de Fermat? La demostración de 13 millones de líneas completada en 11 días que cambia las matemáticas

Un problema de 350 años "demostrado" en 11 días

Uno de los problemas más famosos en la historia de las matemáticas ha vuelto a captar la atención mundial.

En septiembre de 2026, Anthropic anunció que su IA "Claude" había creado una demostración formal completa, verificable por computadora de principio a fin, del último teorema de Fermat. El trabajo tomó 11 días. El código Lean generado alcanzó aproximadamente 13 millones de líneas, y durante el proceso se demostraron 33,000 teoremas, de los cuales 29,500 se utilizaron en la demostración final.

Mirando solo estos números, podría parecer que la IA resolvió en solo 11 días un problema que ha desconcertado a la humanidad durante siglos. Sin embargo, hay una distinción importante aquí. Claude no descubrió un método de solución desconocido. Lo que hizo fue traducir la demostración, completada en la década de 1990 por Andrew Wiles y Richard Taylor y reconocida como correcta por la comunidad matemática, a un lenguaje que una computadora pueda verificar lógicamente, llenando las vastas partes intermedias que faltaban.

No es un "descubrimiento de una nueva demostración", sino una "verificación mecánica completa de una demostración existente". Sin entender esta diferencia, se corre el riesgo de sobrevalorar el logro. Por otro lado, considerar la formalización como una mera tarea de traducción subestima su dificultad y el impacto de este logro.

La línea que Fermat dejó en el margen

El último teorema de Fermat afirma que no existen números enteros positivos a, b, c y un entero n mayor que 2, tales que "a elevado a n más b elevado a n igual a c elevado a n".

Alrededor de 1637, Pierre de Fermat escribió esta afirmación en el margen de un libro de matemáticas griego antiguo llamado 'Arithmetica', y dejó una nota diciendo que había encontrado una demostración maravillosa, pero que el margen era demasiado pequeño para contenerla. Sin embargo, esa demostración nunca fue encontrada.

Desde entonces, generaciones de matemáticos intentaron resolverlo, y aunque se lograron avances para exponentes individuales, el caso general permaneció sin resolver durante más de 350 años. El punto de inflexión llegó en 1993, cuando Wiles anunció una demostración tras años de investigación secreta, pero se encontró un defecto significativo durante la revisión. Wiles, junto con Taylor, trabajó en una corrección y superaron el problema en 1994. El artículo fue publicado en 1995.

Esta historia muestra que en matemáticas, "demostrado" no se establece en el momento en que alguien escribe la respuesta. La demostración debe ser leída por otros expertos, revisada en sus premisas y teoremas citados, y debe verificarse que la cadena lógica no tenga rupturas. El hecho de que incluso la demostración de un matemático del calibre de Wiles tuviera un defecto tras su publicación inicial simboliza su dificultad.

Lo que es "obvio para los humanos" no lo es para las computadoras

Los artículos matemáticos convencionales están escritos para ser leídos por expertos humanos. Los autores omiten transformaciones obvias, se refieren a resultados conocidos y no explicitan partes que pueden entenderse por el contexto. Los lectores también utilizan su conocimiento de fondo para seguir la lógica, llenando los espacios entre líneas.

Sin embargo, las computadoras no hacen suposiciones como "esto es obvio". Es necesario especificar rigurosamente las definiciones, premisas, tipos, teoremas utilizados y las conclusiones derivadas de ellos, mostrando que cada paso sigue las reglas. Para esta tarea se utilizó el sistema de asistencia de pruebas Lean.

En Lean, las demostraciones se escriben en un formato cercano a un programa. Un pequeño núcleo verifica si la demostración ingresada sigue las reglas lógicas y no acepta si hay saltos en el proceso. En ese sentido, una demostración formal es similar a una prueba automática muy estricta de una afirmación matemática.

Lo difícil es que no basta con simplemente traducir el artículo de Wiles a lenguaje de máquina. Las demostraciones para humanos se basan en vastos sistemas de conocimiento como álgebra, geometría, análisis armónico y teoría de números. Si los conceptos necesarios y los teoremas auxiliares no existen en la biblioteca compartida de Lean, también deben definirse y demostrarse. La escala de 13 millones de líneas es el resultado de construir esta "base invisible" paso a paso.

Múltiples IAs compartieron la carga de una enorme demostración

En el experimento de Anthropic, decenas de agentes Claude trabajaron en paralelo. Un agente definía conceptos, otro demostraba teoremas auxiliares, y otro más los combinaba para avanzar hacia teoremas de nivel superior. Fue una división del trabajo a gran escala por parte de un grupo de IAs, similar a cómo los humanos realizan investigaciones colaborativas.

Sin embargo, no todo fue fluido desde el principio. En los intentos iniciales, los agentes perdieron de vista el progreso del proyecto en su conjunto y no pudieron utilizar eficazmente los logros de los demás. En trabajos a largo plazo, no solo la capacidad de razonamiento de cada IA era crucial, sino también un sistema para gestionar qué tareas estaban completas y qué debía demostrarse a continuación.

Para ello, se utilizó la plataforma de formalización colaborativa Prove2Me, que gestiona las relaciones de dependencia entre teoremas como un gráfico acíclico dirigido. Los elementos a demostrar se disponen como un mapa, permitiendo a cada agente elegir tareas no resueltas y reutilizar resultados completados por otros agentes. El diseño también soportó la carga de compilación de Lean y permitió el uso de explicaciones en lenguaje natural para la búsqueda, apoyando la división del trabajo a gran escala.

Finalmente, el grupo de IAs consumió aproximadamente 6 mil millones de tokens de salida y alcanzó la raíz de la demostración en poco menos de 11 días. Según Anthropic, además de la verificación por Lean, también se confirmó mediante herramientas de comparación que la descripción final del teorema coincidía con el último teorema de Fermat en la biblioteca existente Mathlib. Es decir, no terminaron demostrando un problema diferente con un nombre similar, sino que confirmaron haber alcanzado la afirmación buscada.

No se puede comparar directamente los 5 años de los humanos con los 11 días de la IA

Un contraste frecuente es con el proyecto de formalización centrado en humanos liderado por el matemático Kevin Buzzard del Imperial College London. Este proyecto comenzó en 2024 y tiene como objetivo formalizar el último teorema de Fermat en Lean durante varios años.

La descripción de que "un trabajo que tomaría 5 años a los humanos fue completado por la IA en 11 días" es impactante, pero los objetivos de ambos no son completamente los mismos. El logro de Anthropic priorizó hacer el teorema completamente verificable por máquina de principio a fin. Por otro lado, Buzzard y su equipo también buscan desarrollar teorías básicas que puedan incorporarse en una biblioteca compartida y crear documentos dinámicos que permitan a los humanos explorar y aprender demostraciones modernas.

Crear un código gigantesco que "pase" en un corto período de tiempo y organizarlo de manera que los matemáticos puedan entenderlo, reutilizarlo y conectarlo con investigaciones futuras son tareas diferentes. Anthropic también explicó que utilizaron la base establecida por proyectos humanos y la Mathlib existente. No es preciso describir esta competencia como una simple carrera de velocidad entre IA y matemáticos.

Aun así, el hecho de que la formalización de principio a fin sea posible en días en lugar de años es significativo. Buzzard comentó en su blog que, aunque no se aprendió casi nada nuevo matemáticamente de este logro, el hecho de que un grupo de IAs pudiera formalizar el equivalente a miles de páginas de literatura en 11 días demuestra el potencial de la formalización automática. También señaló que, mientras antes se consideraba que una demostración era 99.9% correcta, ahora se puede estar 100% seguro después de la formalización, lo cual se percibe como un símbolo de este logro.

Las redes sociales se dividen entre "asombro" y "no es un nuevo descubrimiento"

Tras el anuncio, hubo una gran reacción en X, Reddit, Hacker News y otros. La cuenta oficial de Lean presentó el logro como la primera demostración completamente verificada por computadora. En Hacker News, cientos de comentarios se reunieron en publicaciones relacionadas, y en Reddit, hubo expresiones de asombro como "algo impensable hace unos años", "impresionante el tamaño de 13 millones de líneas" y "¿realmente se necesitan más de 29,000 teoremas intermedios?".

Por otro lado, la advertencia más repetida fue sobre cómo se interpretaron los titulares. Frente a expresiones como "la IA resolvió el último teorema de Fermat", hubo numerosas correcciones diciendo "quienes lo resolvieron fueron Wiles y Taylor, Claude formalizó la demostración existente en Lean" y "no es un nuevo descubrimiento matemático". Entre las reacciones, hubo opiniones que veían la formalización como una simple conversión de formato, pero también hubo respuestas señalando que el hecho de completar la base faltante de una demostración extensa y hacer verificables por máquina decenas de miles de teoremas intermedios es un logro significativo en la investigación.

Además, el debate se extendió al papel de los investigadores y la distribución de fondos. Algunos ven la llegada de la IA a un trabajo que había sido llevado a cabo con grandes subvenciones y planes de varios años como un salto en la productividad de la investigación. Sin embargo, también se expresaron preocupaciones sobre la posibilidad de que las temáticas de investigación de jóvenes investigadores sean anticipadas por la IA, o que se pierda la motivación para pensar matemáticamente a mano. En la sección de comentarios del blog de Buzzard, se intercambiaron opiniones que veían esto como "el triste final de las matemáticas" y respuestas diciendo "el contenido matemático no ha cambiado, solo han avanzado los medios de verificación".

Estas no son encuestas de opinión aleatorias, sino tendencias observadas en publicaciones en cada red social. Aun así, ilustran bien por qué este logro es propenso a malentendidos y al mismo tiempo evoca emociones fuertes. La reacción de las personas no es solo hacia un teorema, sino hacia la pregunta más amplia de "¿hasta dónde se puede automatizar el trabajo intelectual?".

Una demostración correcta y una demostración útil no son lo mismo

Este logro también tiene debilidades claras. La escala de 13 millones de líneas supera cinco veces el tamaño de la biblioteca matemática principal Mathlib. Aunque la máquina pueda verificar su corrección, no es fácil para los humanos comprender la imagen completa, encontrar las partes necesarias y reutilizarlas en otras demostraciones.

El desarrollo de las matemáticas requiere no solo conclusiones correctas, sino también explicaciones que permitan entender por qué son así, abstracciones adecuadas para organizar conceptos y lemas que puedan usarse en otros campos. Si cada vez que se crea una teoría básica se hace como un código masivo y especializado, las demostraciones formales pueden aumentar, pero el sistema de conocimiento no crecerá fácilmente. Existe la posibilidad de que las demostraciones verificables se produzcan en masa, pero cada una se convierta en una isla con poca compatibilidad.

Por lo tanto, el próximo desafío será acortar y organizar el código creado por la IA, reducirlo a Mathlib y vincularlo con explicaciones comprensibles para los humanos. La IA abre el camino de manera abrupta, y los humanos y la IA juntos lo convierten en un mapa. Este logro es más un punto de partida para esta nueva división del trabajo que una meta.

Un "segundo lector" incansable que complementa los límites de la revisión por pares

El mayor significado no reside en haber demostrado nuevamente un teorema famoso, sino en mostrar la posibilidad de realizar verificaciones mecánicas a gran escala, algo que antes no era realista debido al costo y tiempo.

La verificación de artículos matemáticos requiere mucho tiempo de expertos. Especialmente cuando una nueva teoría se extiende a cientos de páginas y depende de numerosos estudios previos, es difícil para los revisores reconstruir todo. Si la IA puede ayudar en la formalización, podría extenderse el hábito de presentar certificados verificables en Lean junto con artículos dirigidos a humanos.

Esto se vuelve aún más importante en una era en la que la IA comienza a generar logros matemáticos en masa. Si la IA genera candidatos a artículos a una velocidad superior a la que los humanos pueden leer, la revisión por pares tradicional no será suficiente. Combinando una IA que genera, otra que formaliza y un pequeño núcleo de verificación que confirma la lógica, al menos se puede verificar eficientemente si "la conclusión se deriva lógicamente".

Por supuesto, las demostraciones formales no determinan todo el valor de un artículo. Quedan juicios sobre si las definiciones representan adecuadamente problemas reales, si el tema de investigación es importante, si la demostración ofrece nuevas ideas y si la explicación es educativa. También son inevitables problemas como la confianza en el software de verificación y las bibliotecas base, la auditoría de códigos masivos y la distribución desigual de los recursos computacionales.

Aun así, el significado de que las matemáticas tengan un "segundo lector" que no se cansa, no respeta la autoridad y no pasa por alto las lagunas lógicas es enorme.

¿Reemplazará la IA a los matemáticos?

Este acontecimiento no trata de que la IA haya sustituido de un plumazo el trabajo de los matemáticos. Fue necesario el ingenio humano que creó la demostración original, los investigadores que durante décadas desarrollaron la teoría, la comunidad que cultivó Mathlib y Lean, y los desarrolladores que diseñaron la plataforma para dividir la demostración, para que los 11 días de Claude fueran posibles.

Sin embargo, también es prematuro concluir que "la IA es simplemente una herramienta". El hecho de que múltiples agentes se recuperaron de fallos, siguieron las relaciones de dependencia y acumularon decenas de miles de teoremas para completar un objetivo gigantesco, es cualitativamente diferente de la automatización tradicional. No fue que los humanos dieran instrucciones detalladas paso a paso, sino que un grupo de IAs, al que se le dieron un objetivo y un entorno de trabajo, llevó a cabo una gran parte de un proyecto a largo plazo.

En el futuro, el valor de los matemáticos podría desplazarse aún más de "la velocidad para escribir código de demostración a mano" hacia la habilidad de elegir qué problemas abordar, cómo organizar los conceptos y explicar qué significan los resultados. La IA puede acelerar la verificación, pero no termina automáticamente el trabajo de editar las matemáticas como conocimiento humano.

No hay nuevas conclusiones sobre el último teorema de Fermat en sí. La demostración de Wiles y Taylor fue correcta. Sin embargo, el hecho de que el trabajo de convertir esa corrección en una forma que una máquina pueda verificar de principio a fin se haya completado en 11 días, cambia la forma en que se crean, leen y creen las matemáticas.

La demostración de Fermat, que no cabía en el margen, se ha expandido a 13 millones de líneas unos 360 años después. Y el próximo desafío podría ser comprimir esa enorme demostración nuevamente en conocimiento comprensible para los humanos.