Claude recrea la prueba formal del Último Teorema de Fermat en solo 11 días

Miércoles 09 Septiembre 2026 - 16:49

Anthropic afirma que su modelo de inteligencia artificial Claude ha completado un proyecto de formalización matemática altamente ambicioso, reproduciendo una versión verificable por computadora del Último Teorema de Fermat en solo 11 días con intervención humana limitada.

El proyecto generó alrededor de 13 millones de líneas de código en el lenguaje de programación Lean y casi 29,500 teoremas intermedios. Ese volumen es aproximadamente cinco veces el tamaño de Mathlib, una importante biblioteca de código abierto que contiene matemáticas formalmente verificadas.

El Último Teorema de Fermat fue propuesto por primera vez por el matemático francés Pierre de Fermat en el siglo XVII. El problema permaneció sin resolver durante más de 300 años hasta que el matemático británico Andrew Wiles finalmente estableció una prueba en 1994, con la versión definitiva publicada en 1995 después de que se identificara y corrigiera un error en el argumento original.

La formalización es diferente de descubrir una nueva prueba matemática. Implica traducir un argumento matemático existente a un lenguaje informático preciso para que un asistente de prueba pueda verificar cada paso lógico y confirmar que el razonamiento sigue de los axiomas subyacentes y resultados previamente establecidos.

Según el relato del proyecto, el matemático Kevin Buzzard del Imperial College London pasó varios años trabajando en el esfuerzo de formalización, mientras que Claude completó la tarea en 11 días. El resultado se diseñó para confiar únicamente en axiomas matemáticos y razonamiento formalmente establecido en lugar de suposiciones informales.

Se informa que el sistema de IA dividió el trabajo entre múltiples agentes que recibieron instrucciones generales a intervalos regulares. Una herramienta conocida como Prove2Me, desarrollada originalmente para ayudar a matemáticos humanos, ayudó a coordinar partes del proceso.

El logro ilustra el creciente papel de la IA en las matemáticas formales, donde incluso un pequeño vacío lógico puede invalidar una prueba sofisticada. La verificación asistida por computadora ofrece una forma de examinar cadenas largas de razonamiento de manera sistemática e identificar inconsistencias que pueden ser difíciles de detectar a través de una revisión matemática convencional.

Mathlib, el repositorio central utilizado por los matemáticos que trabajan con Lean, contiene millones de líneas de matemáticas formalizadas y continúa expandiéndose a medida que los investigadores convierten resultados establecidos en formas verificables por máquina.

Si el resultado de Claude puede ser reproducido de manera independiente y demostrado como confiable, los sistemas de IA podrían acelerar significativamente la formalización de las matemáticas modernas. Tales herramientas no necesariamente reemplazarían a los matemáticos, sino que podrían ayudar a transformar argumentos complejos desarrollados por humanos en estructuras precisas que las computadoras pueden verificar.