Claude completa en 11 días la primera demostración formal del Último Teorema de Fermat
La inteligencia artificial de Anthropic, Claude, ha logrado en apenas 11 días lo que la comunidad matemática llevaba años intentando: la primera demostración completa, verificada por ordenador, del Último Teorema de Fermat. El resultado, publicado en el repositorio de GitHub de la compañía, fue posible gracias al trabajo autónomo del modelo de lenguaje, que escribió 13 millones de líneas de código en el lenguaje formal Lean y demostró 29.500 teoremas intermedios en el proceso.
El Último Teorema de Fermat, formulado por Pierre de Fermat en 1637 al margen de su ejemplar de la Aritmética de Diofanto, afirma que no existen enteros positivos a, b, c que satisfagan la ecuación aⁿ + bⁿ = cⁿ para ningún valor de n mayor que 2. Durante más de 350 años, el problema desafió a generaciones de matemáticos. En 1908 se ofreció un premio de 100.000 marcos de oro alemanes —equivalente a entre uno y dos millones de dólares actuales— y solo en el primer año se registraron 621 intentos fallidos de demostración. La primera prueba correcta fue presentada por el matemático británico Andrew Wiles en 1995, tras un laborioso proceso de verificación que incluyó un error inicial detectado meses después de su anuncio original en 1993. La demostración de Wiles, de 129 páginas, se apoyaba en técnicas matemáticas muy posteriores a la época de Fermat, lo que llevó a la comunidad a concluir que la famosa «demostración maravillosa» que el francés aseguró poseer nunca existió realmente.
El avance de Claude no consiste en descubrir una nueva demostración, sino en formalizar la existente: traducir la prueba de Wiles a un lenguaje que un ordenador pueda verificar de forma automática. En 2004, el informático holandés Jan Bergstra propuso por primera vez esta idea, pero el proyecto cobró verdadero impulso en 2024, cuando el matemático Kevin Buzzard, del Imperial College de Londres, inició una iniciativa comunitaria para completar la formalización utilizando el asistente de pruebas Lean. Los expertos estimaban que esta tarea tomaría años; solo el «blueprint» inicial que guía el proyecto ocupa 86 páginas.
La investigación fue liderada por Tianyi Peng, investigador de Anthropic vinculado a la Universidad de Columbia, cuyo grupo desarrolla herramientas de formalización con IA. Peng planteó a Claude el desafío de avanzar en la formalización del teorema, y el resultado superó sus expectativas. Según Anthropic, la intervención humana se limitó a instrucciones de alto nivel como «el jacobiano como esquema suena prioritario» o «empujar el teorema de Mazur para que se complete pronto». Decenas de agentes de Claude colaboraron de forma autónoma para definir conceptos, demostrar teoremas intermedios y encadenarlos hasta completar la prueba final, que sigue una versión simplificada de la demostración de Wiles elaborada por Darmon, Diamond y Taylor.
El proceso no estuvo exento de dificultades. Los primeros intentos del modelo fracasaron porque los agentes perdían el seguimiento del estado del proyecto y dejaban de colaborar de manera efectiva. El cambio estratégico llegó al incorporar Prove2Me, una plataforma abierta de colaboración en formalización matemática diseñada por el propio Peng y sus colegas de Columbia. Los intentos fallidos, sin embargo, no fueron en vano: contribuyeron con aproximadamente el 7% de las líneas no boilerplate de la prueba final.
Buzzard, la principal referencia académica en el proyecto comunitario, calificó el logro como «un extraordinario avance en autoformalización» y destacó que la prueba cubre áreas tan dispares como álgebra, análisis armónico, geometría y teoría de números, lo que demuestra que los artefactos de autoformalización mediante IA son ya lo suficientemente robustos como para servir de base a nuevos trabajos. Con 13 millones de líneas de código Lean, la prueba de Claude quintuplica en tamaño a Mathlib, la principal biblioteca comunitaria de demostraciones matemáticas sobre la que se construye.
La trascendencia del avance radica en sus implicaciones para el futuro de las matemáticas. A diferencia de trabajos recientes de IA sobre la hipótesis de Riemann, que produjeron matemáticas genuinamente novedosas, aquí la novedad es la verificación. Como señala Anthropic, demostrar teoremas requiere encadenar complejas cadenas lógicas en las que un solo eslabón roto puede invalidar todo lo posterior; evaluar un resultado nuevo puede tomar meses o incluso años. La formalización automática aligera esa carga y podría hacer que el cuerpo de conocimiento matemático sea más fácil de revisar, confiar y ampliar.
Por ahora, el siguiente paso será la revisión exhaustiva por parte de la comunidad matemática. El propio sistema registra el momento histórico con mensajes como «el nodo raíz de FLT aparece como DEMOSTRADO», aunque los autores insisten en que toda verificación final corresponde a los humanos. De confirmarse plenamente, estaríamos ante un punto de inflexión: la demostración más célebre de las matemáticas, que tardó siglos en probarse y meses en validarse, ha podido ser verificada formalmente por una inteligencia artificial en menos de dos semanas.