Anthropic afirma haber alcanzado un hito histórico en la matemática asistida por inteligencia artificial: Claude produjo una formalización completa y verificable por computadora del último teorema de Fermat. El trabajo se desarrolló durante 11 días y generó unos 13 millones de líneas de código en Lean, un lenguaje diseñado para expresar y comprobar pruebas matemáticas.
La noticia no significa que Claude haya descubierto un teorema nuevo. Su logro está en convertir una demostración matemática extremadamente compleja en una estructura que un asistente de pruebas puede revisar paso a paso. ¿Por qué importa tanto? Porque verificar una prueba puede tomar meses o años cuando depende únicamente de la lectura cuidadosa de otros matemáticos.
Qué demuestra el último teorema de Fermat
El último teorema de Fermat sostiene que no existen números enteros positivos a, b y c que cumplan:
aⁿ + bⁿ = cⁿ
para ningún exponente entero n > 2.
Pierre de Fermat escribió esta afirmación alrededor de 1637 en el margen de un libro y añadió que había encontrado una demostración extraordinaria, pero que el margen era demasiado pequeño para contenerla. La supuesta prueba nunca apareció y, durante más de tres siglos, generaciones de matemáticos intentaron resolver el problema.
La primera demostración aceptada llegó en 1995, cuando Andrew Wiles publicó una prueba basada en herramientas avanzadas de teoría de números. El trabajo, desarrollado junto con Richard Taylor después de corregir un problema crítico, ocupó 129 páginas y conectó áreas como las curvas elípticas, las formas modulares y la geometría algebraica.
De una prueba humana a una prueba verificable
Una demostración escrita para personas suele omitir pasos considerados obvios. Un matemático puede afirmar que una consecuencia se obtiene fácilmente de un resultado anterior y continuar con el argumento. Lean, en cambio, necesita recibir cada conexión lógica de forma explícita.
Lean es un asistente de pruebas. No intenta comprender una demostración como lo haría un lector humano, sino comprobar que cada afirmación se desprende correctamente de definiciones, teoremas previos y axiomas aceptados. Si falta un paso o una regla se aplica de manera incorrecta, el sistema rechaza la prueba.
Formalizar una prueba no reemplaza la explicación matemática para humanos, pero ofrece una forma extremadamente rigurosa de comprobar su estructura lógica.
El desafío consiste en traducir décadas de conocimiento matemático a un formato que la computadora pueda procesar. Para el último teorema de Fermat, la comunidad esperaba que ese proceso tomara años. Solo el esquema inicial utilizado por el proyecto de formalización desarrollado en el Imperial College London tenía 86 páginas.
Cómo trabajaron Claude y los agentes de IA
Según Anthropic, Claude trabajó con decenas de agentes coordinados mediante Prove2Me, una plataforma colaborativa para formalizar matemáticas desarrollada por Tianyi Peng y sus colaboradores en la Universidad de Columbia.
Los agentes se repartieron tareas como definir conceptos, demostrar resultados intermedios y conectar esos resultados con afirmaciones cada vez más complejas. En total, produjeron pruebas verificables para 30.300 teoremas, de los cuales 29.500 fueron utilizados en la demostración final.
El sistema consumió aproximadamente seis mil millones de tokens de salida de un modelo interno de investigación comparable, según la descripción de Anthropic, con Claude Fable 5.1. La prueba final supera cinco veces el tamaño de Mathlib, la biblioteca principal de resultados matemáticos sobre la que se apoya este trabajo.
El proceso no fue exitoso desde el comienzo. Los primeros intentos perdieron el estado del proyecto y los agentes dejaron de colaborar de manera eficaz. Esos esfuerzos fallidos aportaron cerca del 7 % de las líneas no repetitivas de la versión final, una muestra de que la autonomía de los agentes todavía depende mucho de la organización del entorno de trabajo.
Qué aporta realmente este avance
La parte novedosa no es una nueva demostración del teorema. Claude siguió una versión simplificada de la estrategia de Wiles, basada en el trabajo de Henri Darmon, Fred Diamond y Richard Taylor, además de apoyarse en formalizaciones previas de otros proyectos matemáticos.
Lo nuevo es la velocidad y el alcance de la verificación automática. Anthropic asegura que Lean comprobó la prueba utilizando únicamente sus tres axiomas estándar y que un comparador confirmó que el enunciado empleado coincide con la formulación del último teorema de Fermat disponible en Mathlib.
Kevin Buzzard, matemático del Imperial College London y uno de los impulsores del proyecto comunitario de formalización de Fermat, revisó el resultado y señaló que el trabajo representa un paso importante hacia la formalización automática de grandes partes de la literatura matemática.
Esto puede cambiar la revisión académica. Cuando una inteligencia artificial produce una prueba, un investigador humano todavía debe entender la estrategia, evaluar su relevancia y revisar que el resultado responda a la pregunta correcta. Pero una prueba formalizada puede encargarse de una parte especialmente pesada: verificar que la cadena lógica no contiene errores.
La diferencia entre descubrir y verificar
En los últimos años, algunos sistemas de IA han intentado producir resultados matemáticos nuevos, como avances relacionados con la hipótesis de Riemann. Formalizar el último teorema de Fermat pertenece a una categoría distinta.
Aquí la IA no está presentando una idea matemática inédita. Está realizando una tarea comparable a comprobar un cálculo con una calculadora, aunque a una escala muchísimo mayor. La prueba debe estar expresada en un lenguaje formal y superar las verificaciones del sistema.
Eso no vuelve innecesarios a los matemáticos. La formalización todavía requiere decisiones humanas sobre qué estrategia seguir, qué bibliotecas utilizar y cómo dividir el problema. En este caso, Tianyi Peng ofreció instrucciones de alto nivel, como priorizar la construcción de un jacobiano como esquema o avanzar con el teorema de Mazur.
La diferencia es que una parte considerable del trabajo de traducción, búsqueda de lemas y conexión entre resultados pudo ser delegada a agentes de IA. ¿Podría este flujo convertirse en una herramienta habitual para investigar? Anthropic cree que sí.
Hacia una matemática más fácil de auditar
El equipo también informa de un experimento más pequeño: tres suscripciones personales de Claude Max fueron utilizadas para formalizar aplicaciones del método del círculo de Hardy y Littlewood. Los agentes colaboraron en Prove2Me y completaron la formalización del teorema de los tres primos de Vinogradov en tres días.
Estos resultados apuntan a una posible evolución del trabajo matemático. En lugar de publicar únicamente una explicación en lenguaje natural, los investigadores podrían entregar también una versión formalizada que cualquier persona pueda volver a comprobar con las herramientas correspondientes.
La formalización podría ayudar a detectar errores antiguos en el corpus matemático, reducir la carga de los revisores y evaluar con más confianza las pruebas generadas por modelos de lenguaje. También parece funcionar como una herramienta de autocontrol para la propia IA: al intentar expresar cada paso en Lean, el modelo se ve obligado a comprobar si sus hipótesis realmente conducen al resultado.
Aun así, quedan límites importantes. Una prueba formal puede confirmar que una conclusión se deriva de sus premisas y axiomas, pero no decide por sí sola si el problema elegido era interesante, si la estrategia es comprensible o si una definición refleja correctamente la intención original del investigador.
La historia del último teorema de Fermat nació con una nota en el margen de un libro y terminó conectando matemáticas desarrolladas durante siglos con millones de líneas de código. El logro de Claude no elimina esa historia humana. La convierte en un nuevo tipo de objeto: una demostración que no solo puede leerse, sino también ejecutarse y auditarse paso a paso.
Fuente original
https://www.anthropic.com/research/formalizing-fermats-last-theorem