Claude lleva el Último Teorema de Fermat a una prueba verificable
Anthropic logró que Claude construyera una formalización completa y verificable por computadora del Último Teorema de Fermat, uno de los resultados más célebres de la historia de las matemáticas.
Durante 11 días, múltiples agentes de IA trabajaron en gran medida de forma autónoma para traducir una versión de la demostración de Andrew Wiles al lenguaje Lean, utilizado para comprobar rigurosamente cada paso lógico. El proyecto generó alrededor de 13 millones de líneas de código y utilizó cerca de 29,500 teoremas intermedios en la prueba final.
La aportación no es una nueva demostración matemática, sino algo distinto: convertir una prueba extremadamente compleja en una estructura que una computadora puede validar de principio a fin.
El avance apunta hacia sistemas capaces de ayudar a revisar investigaciones, detectar errores y verificar matemáticas generadas por humanos o por otras inteligencias artificiales con un nivel de rigor difícil de alcanzar mediante revisión manual.
ALXN PXVEL
