Anthropic afirma que su IA Claude produjo la primera demostración totalmente verificada por computadora del Último Teorema de Fermat, completando el trabajo en 11 días en gran medida por sí sola y generando lo que ahora es la demostración matemática más larga jamás construida.

Un proyecto liderado por humanos en el Imperial College London ha estado trabajando en exactamente la misma tarea desde 2024 y no está cerca de terminar. Claude llegó primero a la meta. Kevin Buzzard, el matemático que lidera el proyecto del Imperial, revisó la demostración de Claude y confirmó que se sostiene usando únicamente las reglas lógicas más básicas de las matemáticas.

Según Anthropic, Claude escribió la demostración matemática más larga jamás creada y la usó para probar formalmente el Último Teorema de Fermat, un problema que desconcertó a los matemáticos durante 358 años. La IA lo logró en 11 días, en su mayoría por sí sola, produciendo 13 millones de líneas de código que una computadora puede verificar línea por línea, en lugar de requerir confiar en la palabra de un matemático.

El Último Teorema de Fermat establece que no existen tres números enteros positivos que, elevados cada uno a una potencia mayor que 2, hagan que los dos primeros sumen el tercero. Pierre de Fermat anotó esa afirmación al margen de un libro de matemáticas en 1637, añadiendo que tenía una "demostración verdaderamente maravillosa" que el margen era demasiado pequeño para contener. Luego murió. Los matemáticos pasaron los siguientes 358 años intentando reconstruir lo que él creía tener.

Probar algo y verificarlo son dos tareas distintas

Una demostración matemática es una cadena de pasos lógicos, y si un eslabón se rompe, todo se derrumba. Encontrar ese único eslabón roto, enterrado en algún lugar de cien páginas de argumentación densa, puede costarles a otros matemáticos años de sus vidas.

Formalizar una demostración significa traducirla a un lenguaje tan literal que una computadora pueda verificar cada paso por sí sola, sin caer en subjetividades.

Los matemáticos han luchado con la verificación durante mucho tiempo. Un premio alemán de 1908 —valorado en aproximadamente entre 1 y 2 millones de dólares actuales, ofrecido por la primera demostración válida del teorema— recibió 621 propuestas incorrectas solo en su primer año.

Como escribió Anthropic en X:

Verificar que una demostración matemática importante sea correcta puede tomar años. La formalización —convertir el razonamiento matemático a una forma que asistentes de demostración como Lean puedan verificar— puede ayudar. El mes pasado, Claude completó la primera demostración formalizada del Último Teorema de Fermat, uno de… pic.twitter.com/pdT8zwlV4A

— Anthropic (@AnthropicAI) September 4, 2026

La verdadera demostración no apareció hasta 1995, de la mano del matemático británico Andrew Wiles, y llegó con un giro inesperado. Wiles anunció su solución en tres conferencias en junio de 1993, solo para que un revisor encontrara después un fallo en ella. Pasó casi un año corrigiéndolo junto a un exestudiante, Richard Taylor, estuvo a punto de rendirse y finalmente publicó una demostración corregida de 129 páginas en mayo de 1995. Se apoyaba en matemáticas que no existían en la época de Fermat, razón principal por la que los matemáticos ahora dudan de que la "demostración maravillosa" del propio Fermat haya funcionado realmente.

Las matemáticas verificadas por computadora tienen ya décadas de historia. El primer caso famoso fue la demostración asistida por computadora del Teorema de los Cuatro Colores en 1976, que encendió un debate permanente sobre si una demostración que ningún humano puede leer por completo a mano debería contar como tal. Los lenguajes de demostración formal como Lean —creado por Leonardo de Moura, originalmente en Microsoft Research— nacieron precisamente de esa tensión, permitiendo que el software haga la verificación para que los humanos puedan confiar en el resultado de todos modos.

En 2024, el matemático del Imperial College London Kevin Buzzard inició un proyecto para hacer exactamente lo que Claude acaba de hacer: traducir la demostración de Wiles a Lean, un lenguaje que las computadoras pueden verificar. Es el tipo de trabajo que requiere un ejército de matemáticos voluntarios: el propio esquema del proyecto abarca 86 páginas y su financiamiento está asegurado hasta 2029. Claude terminó todo el trabajo en 11 días.

Cómo lo logró Claude realmente

Anthropic explica en una publicación más detallada que Tianyi Peng, quien desarrolla herramientas de formalización con IA junto a un equipo en Columbia, decidió ver hasta dónde podía llegar Claude por sí sola. Decenas de agentes de Claude trabajaron en paralelo, escribiendo definiciones, demostrando resultados pequeños y apilándolos en otros mayores, con casi ninguna intervención humana más allá de ocasionales indicaciones como "prioriza este teorema a continuación".

Al principio no todo fue fluido. En las etapas iniciales, los agentes perdían el rastro de lo que ya habían demostrado y dejaban de colaborar; esos falsos arranques todavía constituyen alrededor del 7% de las líneas de la demostración final.

Lo que lo solucionó fue una herramienta llamada Prove2Me, también creada por el equipo de Peng, que dio a cada agente la misma lista de tareas en vivo indicando qué demostraciones menores seguían pendientes, de modo que nadie duplicara trabajo ni se desviara. También organizó los archivos para que Lean pudiera verificar todo más rápido, y mantuvo notas en lenguaje sencillo sobre cada resultado para que los agentes pudieran reutilizar el trabajo de los demás en lugar de reinventarlo.

Al terminar, Claude había demostrado más de 30.000 teoremas de apoyo y consumido miles de millones de tokens, ejecutándose en un modelo de investigación que, según Anthropic, es aproximadamente comparable a Claude Fable 5.1, la versión que luego lanzó al público. La demostración terminada abarca 13 millones de líneas, más de cinco veces el tamaño de Mathlib, la biblioteca compartida que los matemáticos ya utilizan para este tipo de trabajo.

Una novela típica tiene unas 80.000 palabras. La demostración de Claude equivale a 160 novelas de pura argumentación lógica.

¿Y esto realmente importa?

Buzzard —cuya propia versión de este proyecto sigue financiada hasta 2029— revisó la demostración de Claude y le dio su respaldo, afirmando que prueba el teorema "sin más supuestos que los axiomas de las matemáticas".

Esto no equivale a que Claude haya descubierto matemáticas nuevas, algo que Anthropic también afirmó con su investigación criptográfica a principios de este año. Wiles ya demostró el teorema de Fermat hace tres décadas; Claude construyó un comprobante verificable por máquina de ese resultado. Eso importa porque los matemáticos están cada vez más desbordados por demostraciones no verificadas, incluidas las escritas por IA, que llegan más rápido de lo que los humanos pueden revisarlas a mano. Además, este tipo de demostraciones formalizadas son deterministas y no propensas a errores humanos, lo cual es muy importante en matemáticas.

No es un problema nuevo. Una demostración asistida por computadora de la conjetura de Kepler tardó cuatro años antes de que un panel de revisión solo se comprometiera a estar "99% seguro", y la demostración de Grigori Perelman de la conjetura de Poincaré tardó aproximadamente lo mismo en ser asimilada por completo.

Quien no quiera tomar la palabra de Anthropic no tiene por qué hacerlo. La demostración completa de 13 millones de líneas está disponible en GitHub, libre para que cualquier matemático con suficiente tiempo libre la examine, línea por línea.