Una IA completa en 11 días la verificación formal del Último Teorema de Fermat
Anthropic publicó la primera demostración del teorema comprobada de punta a punta por computador, escrita en el lenguaje Lean.
Anthropic informó que su modelo Claude produjo, trabajando de forma mayoritariamente autónoma durante once días, la primera demostración del Último Teorema de Fermat verificada íntegramente por computador. El resultado son unos 13 millones de líneas en Lean y alrededor de 29.500 teoremas intermedios utilizados en la prueba final: la demostración formal más extensa escrita hasta ahora en ese lenguaje.
El teorema fue demostrado por Andrew Wiles en 1995, más de 350 años después de ser enunciado. Formalizarlo —traducirlo a un lenguaje que un asistente de pruebas pueda verificar línea por línea— era un trabajo que la comunidad matemática estimaba en varios años. Con esto se cierra además el último punto pendiente de la lista de 100 desafíos de formalización de Freek Wiedijk.
Por qué importa
Verificar que una demostración compleja es correcta puede llevar años de revisión humana. Que un modelo produzca una prueba que una máquina puede comprobar cambia la escala del problema: el resultado no depende de confiar en la IA, sino de que el verificador acepte cada paso.
Anthropic · Formalizing Fermat's Last Theorem · anthropic.com
Comentado por Kevin Buzzard en el blog del Xena Project.
Leer fuente originalEl texto de esta página es un resumen propio elaborado por PixaWeb Tech. No reproduce el artículo original: para leerlo completo, sigue el enlace a la fuente.