Claude formaliza el último teorema de Fermat

Anthropic afirma que Claude ha completado la primera formalización informática del último teorema de Fermat: una versión escrita en Lean que un ordenador puede revisar paso a paso. El proceso duró 11 días y produjo unos 13 millones de líneas de código matemático.

El resultado no es un nuevo descubrimiento sobre el teorema. El matemático Andrew Wiles ya lo demostró en 1995, en una prueba de 129 páginas que necesitó años de trabajo y revisión. Lo que Claude ha hecho es convertir esa demostración en instrucciones tan precisas que un sistema informático puede comprobar su lógica.

De una anotación en un libro a millones de líneas

El último teorema de Fermat afirma que no existen números enteros positivos que cumplan aⁿ + bⁿ = cⁿ cuando n > 2. Fermat escribió la afirmación alrededor de 1637 y dejó una frase famosa: aseguraba tener una demostración demasiado larga para el margen del libro.

Durante más de 350 años nadie encontró esa prueba. Wiles presentó una demostración en 1993, pero los matemáticos detectaron después un fallo importante. Tardó otro año en corregirlo junto con Richard Taylor. La versión definitiva se publicó en 1995 y utilizaba herramientas matemáticas que ni siquiera existían en la época de Fermat.

Formalizar una prueba significa traducirla a un lenguaje que no permite saltarse pasos. Anthropic utilizó Lean, un asistente de pruebas que verifica automáticamente si cada afirmación se deduce de las anteriores. Un texto matemático puede decir “es evidente” y seguir adelante. Lean exige demostrar también esa parte.

Qué hizo Claude

El proyecto partió de una versión simplificada de la prueba de Wiles desarrollada por Henri Darmon, Fred Diamond y Richard Taylor. Decenas de agentes de Claude colaboraron para definir conceptos, resolver problemas intermedios y conectar los resultados hasta llegar al teorema final.

El sistema produjo pruebas verificables para 30.300 teoremas durante el proceso. De ellos, 29.500 se utilizan en la demostración final. El resultado ocupa más de cinco veces el tamaño de Mathlib, la principal biblioteca comunitaria de pruebas matemáticas en Lean sobre la que se apoya el proyecto.

Los primeros intentos fallaron porque los agentes perdían el estado del trabajo y dejaban de coordinarse. El avance llegó al usar Prove2Me, una plataforma colaborativa para formalizar matemáticas creada por Tianyi Peng y sus colaboradores de la Universidad de Columbia.

En total, el equipo consumió alrededor de 6.000 millones de tokens, las unidades con las que los modelos procesan y generan texto. Anthropic asegura que la prueba utiliza únicamente los tres axiomas estándar de Lean y que su formulación coincide con la versión del teorema incluida en Mathlib.

“Si la formalización automática de FLT es posible ahora, hemos dado un gran paso hacia la formalización automática de la literatura matemática moderna”, dijo Kevin Buzzard, de Imperial College London, tras revisar el trabajo.

Qué cambia para ti

La importancia no está en que una IA haya “superado” a Wiles. Está en que puede ayudar a revisar demostraciones complejas con un nivel de precisión que sería muy costoso conseguir solo con matemáticos humanos.

Una prueba tradicional puede tardar meses o años en ser evaluada. Si contiene un error en un solo paso, todo lo que viene después puede quedar invalidado. Una prueba formalizada permite que Lean compruebe la cadena lógica completa, aunque los humanos sigan necesitando una explicación comprensible de las ideas.

Esto podría afectar a tres áreas:

• Revisión científica: comprobar resultados nuevos con menos trabajo manual.
• Matemáticas generadas por IA: distinguir entre una demostración convincente y una que realmente funciona.
• Bibliotecas de conocimiento: construir pruebas reutilizables para que futuros trabajos no tengan que empezar desde cero.

Hay una diferencia importante: Claude no ha encontrado una demostración nueva del último teorema de Fermat. Ha automatizado una parte muy laboriosa de la verificación de una prueba conocida. El próximo paso será comprobar hasta dónde puede llegar esta técnica con otros resultados importantes y si las formalizaciones pueden hacerse más pequeñas, claras y fáciles de mantener.

La matemática no queda reducida a código, pero el código puede convertirse en una segunda capa de confianza. A medida que las IA produzcan más resultados, esa capa podría ser la forma práctica de saber cuáles merecen ser tomados en serio.