Anthropic afirma que un prototipo avanzado de Claude convirtió por primera vez la demostración del último teorema de Fermat en código verificable por computadora. El sistema acabó en 11 días un proyecto que se esperaba que llevara diez años a humanos y apunta a un papel mayor de la IA al revisar pruebas matemáticas.
Formalizar una prueba implica traducir argumentos escritos en lenguaje natural a un código que una computadora puede certificar, por lo común en Lean. El resultado contiene 13 millones de líneas. Anthropic anunció el avance el 4 de septiembre.
La prueba original, completada en 1994 por Andrew Wiles y Richard Taylor, establece que no existen números enteros x, y y z que cumplan xⁿ + yⁿ = zⁿ cuando n es mayor que 2. Pierre de Fermat había planteado esa afirmación en 1637 sin dejar una demostración.
Kevin Buzzard, del Imperial College London, considera que este trabajo tiene un nivel de complejidad muy superior al de una formalización lograda en febrero sobre el empaquetamiento de esferas. Daniel Litt, de la Universidad de Toronto, dijo que, si pueden formalizar este teorema, quizá puedan formalizar cualquier cosa.
✅ El avance sugiere que la IA puede ayudar a revisar el trabajo de matemáticos y a convertir pruebas complejas en código certificable. El límite es que la información procede del anuncio de Anthropic y el artículo no detalla una verificación independiente del resultado ni del proceso seguido por el modelo.
