El último teorema de Fermat formalizado por agentes de IA en solo 11 días

La empresa de IA Anthropic ha creado una demostración formalizada del último teorema de Fermat. Solo les llevó 11 días a un grupo de agentes de IA completar la tarea, confirmando que la demostración encontrada por humanos propuesta en la década de 1990 es correcta.

El último teorema de Fermat desconcertó a los matemáticos durante siglos hasta que fue demostrado en 1995 por Andrew Wiles. Establece que no existen números enteros a, b y c que satisfagan la ecuación aⁿ + bⁿ = cⁿ, donde n es un número entero mayor que 2.

El teorema, aunque fácil de enunciar, era endiabladamente difícil de demostrar. El matemático Pierre de Fermat planteó el enigma en el siglo 17 y famosamente aludió a una demostración que afirmaba haber descubierto, diciendo que era demasiado extensa para caber en los márgenes del libro de texto en el que estaba escribiendo.

Muchos matemáticos intentaron y no lograron encontrar una demostración. Wiles trabajó en el problema durante siete años en secreto antes de anunciar su avance en 1993. Las demostraciones a menudo implican largos argumentos lógicos que se construyen unos sobre otros. Si un solo paso contiene un error, entonces todo puede colapsar. Esto le sucedió a Wiles cuando se encontró un fallo en su demostración que les llevó a él y a su colaborador Richard Taylor alrededor de un año solucionar.