El 4 de septiembre de 2026, Anthropic dio a conocer una noticia que causó un fuerte impacto en la comunidad académica: una flota de agentes de inteligencia artificial completó la formalización y verificación íntegra del último teorema de Fermat en tan solo 11 días. En contraste, un equipo de matemáticos de primer nivel del Imperial College London había obtenido una financiación de un millón de libras y planificado un plazo de cinco años para culminar idéntica tarea.
Este enigma, que desconcertó a la humanidad durante más de 350 años, ya había sido demostrado en 1995 por el matemático británico Andrew Wiles. Por ello, el duelo entre 11 días y cinco años de trabajo no traslada las fronteras conceptuales de las matemáticas en sí.
Lo que este hito desmonta verdaderamente es el modelo tradicional de confiar en comités de expertos humanos para validar el conocimiento. La revisión de una demostración de máximo nivel ha pasado de «años de evaluación por pares humanos expuestos a errores» a «una máquina que comprueba la coherencia lógica en cuestión de minutos».
Un enigma de 350 años expone la fragilidad de la revisión humana
La historia de la demostración del último teorema de Fermat es también una crónica de los tropiezos continuos de los sistemas de arbitraje humano. En 1908, el Premio Wolfskehl ofreció en Alemania 100.000 marcos de oro a quien aportara una prueba válida. Estimulado por la recompensa, el jurado recibió 621 propuestas de resolución solo en el primer año; sin excepción, en todas ellas se descubrieron errores insubsanables.
El cerebro humano posee puntos ciegos insalvables a la hora de procesar cadenas lógicas de enorme complejidad. En junio de 1993, Wiles impartió tres conferencias en el Instituto Isaac Newton de Cambridge, proclamando ante el mundo que había demostrado el teorema. Sin embargo, apenas dos meses después, los revisores plantearon una objeción incisiva durante las comprobaciones rutinarias que reveló una grieta crítica en el andamiaje de la prueba.
Wiles dedicó un año entero de angustiosa labor a reparar el fallo, llegando a contemplar la posibilidad de rendirse, hasta que en mayo de 1995 publicó formalmente el artículo definitivo de 129 páginas. Depender de un puñado de mentes brillantes encerradas a examinar más de un centenar de páginas de denso manuscrito representaba una práctica artesanal que ya rozaba el límite físico de la cognición humana.
Imagen: Cabecera del anuncio oficial de Anthropic. Fuente: Anthropic
13 millones de líneas de código máquina en 11 días
¿Cómo se logra que una máquina compruebe una intrincada malla de símbolos matemáticos? La respuesta reside en la «formalización»: traducir una demostración redactada en prosa, repleta de saltos intuitivos humanos, a código informático riguroso donde no se tolera la más mínima discrepancia de sintaxis o tipos. En el pasado, esta era una tarea titánica reservada a un número muy reducido de especialistas.
El profesor Kevin Buzzard, del Imperial College London, encabezaba un proyecto comunitario con un horizonte de cinco años para formalizar el teorema. Su equipo llegó a redactar un documento guía de 86 páginas únicamente para definir la hoja de ruta de la traducción.
El modelo de investigación interna de Anthropic, Claude, ejecutado en la plataforma Prove2Me, redujo ese calendario a menos de dos semanas. Siguiendo la ruta argumental simplificada establecida en 1995, generó más de 13 millones de líneas de código, un volumen que quintuplica la totalidad de la biblioteca matemática oficial de dicha plataforma.
El código resultante integró la prueba formal de 30.300 lemas y teoremas, de los cuales 29.500 quedaron incorporados en el grafo final de la demostración. Decenas de agentes de IA colaboraron en paralelo como engranajes incansables, fragmentando la intuición humana en secuencias lógicas procesables paso a paso por una máquina.
300.000 dólares para adquirir certeza absoluta
La entrada en juego del cómputo a escala industrial ha transformado los elevados costes del trabajo humano en una factura neta de computación. El proyecto a cinco años del equipo de Buzzard contemplaba un presupuesto de un millón de libras, absorbido por sueldos, dedicación intelectual y prolongados debates entre investigadores.
En cambio, la verificación ejecutada por Claude consumió alrededor de 6.000 millones de tokens de salida. A las tarifas comerciales actuales de las API públicas, dicho gasto ronda los 300.000 dólares. Obtener por 300.000 dólares de potencia computacional la certeza irrefutable que antes exigía un lustro de dedicación científica altera de forma irreversible la estructura económica de la investigación de vanguardia.
Las máquinas no estuvieron exentas de contratiempos. En las fases preliminares, los agentes sufrieron desajustes de coordinación y extraviaron el estado del proyecto. No obstante, el sistema corrigió el rumbo de manera autónoma mediante prueba y error; de hecho, los intentos fallidos aportaron aproximadamente el 7 % de las líneas no genéricas del código final. Los investigadores de Anthropic se limitaron a fijar las directrices de alto nivel, dejando el diagnóstico y la corrección técnica en manos del enjambre de agentes.
Imagen: Grafo DAG en la plataforma Prove2Me que muestra cómo Claude descompone los subteoremas hacia FLT. Fuente: Anthropic
La confianza científica se traslada al compilador
El profesor Kevin Buzzard verificó personalmente la colosal base de código, que superó la compilación sin advertencias ni errores. Las herramientas automatizadas de comparación confirmaron asimismo que los enunciados de los teoremas coinciden de manera idéntica con los registros de las bibliotecas matemáticas formales reconocidas. Con ello se dio por culminada la lista de referencia de los «100 desafíos de formalización», planteada hace dos décadas.
Tal como señaló el propio Buzzard, no se ha formulado ninguna teoría matemática inédita, pero en el campo de la formalización automatizada se ha establecido una demostración empírica contundente. Cuando una prueba de 129 páginas puede compilarse con la misma naturalidad que el código fuente de un proyecto de software, la red de confianza de la comunidad académica queda profundamente transformada.
Históricamente, un teorema se aceptaba cuando figuras de incuestionable prestigio avalaban su solidez. Hoy en día, esa intermediación de autoridades consagradas pierde relevancia. Si el código supera el compilador con éxito, la verdad matemática no precisa de avalistas humanos. El compilador se ha erigido en la línea de defensa definitiva.
Enlaces de referencia:
- Anthropic Research
- Discusión en HN
