Los principales teoremas del siglo XX y su formalización
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
- 1910: La demostración de Brouwer del teorema del punto fijo. Está formalizado en HOL Light (por John Harrison), en Mizar (por Artur Korniłowicz y Yasunari Shidama) y en Isabelle (por Robert Himmelmann).
- 1928: La demostración de John von Neumann del teorema minimax.
- 1930: La demostración de Casimir Kuratowski de inexistencia de solución del problema de las tres casas.
- 1930: La demostración del teorema de Ramsey. Está formalizado en HOL Light (por John Harrison), en Mizar (por Marco Riccardi), en Isabelle (por Tom Ridge), en ProofPower (por Rob Arthan y Roger Bishop Jones), en PVS (por Natarajan Shankar), en Nqthm (por Matt Kaufmann) y en NuPRL (por David Basin).
- 1931: La demostración de Kurt Gödel de los teoremas de incompletitud. Está formalizado en HOL Light (por John Harrison), en Coq (por Russell O’Connor) y en Nqthm (por Natarajan Shankar).
- 1963: La demostración de Paul Cohen de la indecidibilidad de la hipótesis del continuo
- 1966: demostración de Paul Erdos, Alfred Renyi y Vera Sos del teorema de la amistad. Está formalizado en HOL Light (por John Harrison).
- 1976: La demostración de Kenneth Appel y Wolfgang Haken de 1976 del teorema de los cuatros colores. En 2005 Benjamin Werner y Georges Gonthier formalizaron una demostración del teorema en Coq.
- 1983: La clasificación de los grupos finitos. Su formalización se está realizando en el proyecto Mathematical Components. El estado de la formalización puede consultarse en Mathematical Component: Group Theory.
- 1993: La demostración de Andrew Wiles del último teorema de Fermat, que se comentó en la entrada Reto de formalización: El proyecto Wiles-Fermat.
- 1998: La demostración de Thomas C. Hales de la conjetura de Kepler. Su formalización se está realizando dentro del proyecto Flyspeck.
Más candidatos pueden extraerse de las siguientes referencias:
- Timeline of mathematics (20th century)
- Algunos descubrimientos y acontecimientos destacables de la matemática del siglo XX
- Algunos de los avances más importantes en la matemática del siglo XX.
- La matemática del siglo XX.
¿Cuáles son vuestros candidatos para la lista de los principales teoremas del siglo XX?