Seminario "Razones para formalizar matemáticas"

CONFERENCIANTE: María Inés de Frutos Fernández (UAM)

TÍTULO: Razones para formalizar matemática

DÍA Y HORA: Jueves 14 de marzo, 11:30

LUGAR: Sala 520, módulo 17.

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) o 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.