Eva Miranda - Universitat Politècnica de Catalunya

De Alan Turing a Navier-Stokes: entre la indecibilidad y el caos

 

Día y hora: 14 de marzo de 2023 - 13:00

Lugar: Aula Miguel de Guzmán - Facultad de CC. Matemáticas (UCM)

Resumen

En 1992, 29000 patitos de goma se perdieron en el océano Pacífico durante una tormenta.
Algunos de estos patitos de goma aparecieron muchos años después en lugares inesperados.
¿Se podía prever dónde aparecerían?

El día 19 de septiembre de 2021 se inició la erupción del volcán de Cumbre Vieja en la isla de la Palma.
La erupción duró 85 días y no se conocía siempre el camino exacto que seguiría la lava después de salir del cráter.
¿Se podía predecir?

En 1936 Alan Turing, conocido por descifrar la máquina Enigma, demostró que el problema de la parada era indecidible. En otras palabras, no podía existir un "superordenador" que nos dijera si un ordenador arbitrario con unos datos iniciales arbitrarios se pararía o seguiría funcionando indefinidamente.

¿Pero qué tiene que ver Turing con los patitos de goma? Intentaremos dar respuesta a estas preguntas desde las matemáticas. El movimiento del agua y la lava viene descrito por las ecuaciones de Euler y Navier-Stokes. Son ecuaciones con muchos enigmas. Algunos de estos enigmas tienen recompensa: un millón de dólares y la fama eterna para quien consiga demostrar o refutar si las ecuaciones de Navier-Stokes tienen soluciones razonables por todo valor de tiempo.

Terence Tao propuso un interesante programa para abordar el problema del Milenio de Navier-Stokes utilizando máquinas de Turing. Haremos un breve recorrido por estas cuestiones demostrando que se puede asociar una nueva noción de caos (lógico) al movimiento de fluidos dando lugar al concepto de "ordenadores de agua". Estos "ordenadores teóricos" realizan el sueño de Stanisław Lem,en su novela Solaris, immortalizada en el cine por Nirenburg, Tarkovski y Soderbergh sobre un "océano pensante". Sin embargo, ¿servirán algún día para realizar el sueño de Terence Tao?

 

 

María Inés de Frutos - Universidad Autónoma de Madrid

¿Por qué formalizar matemáticas?

 

Día y hora: 14 de marzo de 2023 - 17:00

Lugar: Aula Miguel de Guzmán - Facultad de CC. Matemáticas (UCM)

Resumen

La formalización matemática consiste en digitalizar definiciones y resultados matemáticos utilizando un programa informático, conocido como "asistente de demostración", capaz de comprobar si una proposición se puede deducir de un conjunto de reglas de inferencia y una colección de axiomas básicos.

En los últimos años, la comunidad de matemáticos que trabajan en formalización ha crecido rápidamente y ha alcanzado hitos que demuestran la capacidad de formalizar resultados en la frontera del conocimiento, como la formalización de la definición de espacio perfectoide (Buzzard, Commelin, Massot, 2019) y la formalización de teoremas recientes de Clausen-Scholze en el área de las matemáticas condensadas (Commelin, Topaz, et. al., 2022).

Aunque la ventaja más obvia de la formalización es que otorga certeza sobrehumana en la corrección de las demostraciones, en esta charla también presentaremos otras formas en las que los asistentes de demostración podrán pronto ser utilizados como parte del proceso de investigación matemática. Asimismo, discutiremos aplicaciones de estas herramientas informáticas a la enseñanza y comunicación de matemáticas.