Los principales teoremas del siglo XX y su formalización

PorJosé A. Alonso

Como comentaba en la entrada anterior, un gran reto para el razonamiento formalizado podría consistir en la formalización de los principales teoremas del siglo XX.

Este reto es análogo a Formalizing 100 Theorems que consiste en la formalización de los 100 principales teoremas de todos los tiempos.

El punto de partida ha de ser la determinación de cuáles son los principales teoremas del siglo XX y en qué punto se encuentra su formalización.

Algunos candidadatos de la lista de los principales teoremas del siglo XX son
Read More “Los principales teoremas del siglo XX y su formalización”

Reto de formalización: El proyecto Wiles-Fermat

PorJosé A. Alonso

Una de las líneas de desarrollo de la Lógica Computacional es abordar formalizaciones de resultados matemáticos complejos. El intento de formalización produce como efectos laterales la formalización del conocimiento implícito en el resultado (el mathware) y el desarrollo de nuevos procedimientos de decisión.

Uno de los grandes retos actuales es la formalización de la demostración de Andrew Wiles del último teorema de Fermat. Una descripción detallada del reto se encuentra en el artículo Computer verification of Wiles’ proof of Fermat’s Last Theorem de Wim H. Hesselink. En el artículo se traza la hoja de ruta de la formalización describiendo la estructura de la demostración de Wiles. Una de las principales dificultades radica en comentando la necesidad de disponer de sistemas de razonamiento que incorporen cálculo simbólico. Hesselink estima que se tardarán unos 50 años en conseguirse la formalización del teorema de Wiles.