Viernes 01/09/2023, 14.30 hs. Aula 27
Titulo: Formalización de Matemática, una tarea (in)necesaria pero (in)viable
Resumen:
La matemática como disciplina científica tiene un estatus especial porque, se supone, sus métodos son rigurosos. Si bien no lo hacemos todos los días (ni mucho menos) asumimos que, si nos fuerzan a ello, podríamos transformar nuestras pruebas (que surgieron de nuestra intuición) en deducciones formales dentro de un sistema lógico con axiomas aceptados por la comunidad del área en cuestión. Bourbaki dedicó todo un capítulo para sentar su sistema formal pero en el prefacio se aclara que tampoco es tan necesario por eso mismo que decíamos: es algo tedioso, poco informativo y muy demandante. Siendo que la matemática trata con estructuras cada vez más complejas es posible que debamos aceptar que la traducción es cada vez más difícil pero cada vez más necesaria. Para facilitarnos la vida podemos aprovechar la tecnología de los asistentes de prueba (de la misma manera que usamos GAP, Mathematica, o Geogebra para calcular cosas) y escribir nuestras pruebas en programas que no sólo verifican la validez de nuestras deducciones sino también nos asisten en la construcción de las derivaciones.
En esta charla repasaré algunas de las cuestiones mencionadas más arriba citando a gente que sabe más que yo e intentaré mostrar algún ejemplo concreto de uso de asistentes de prueba.