Algunas reflexiones sobre las pruebas asistidas por computadora.
Ponente(s): Favio Ezequiel Miranda Perea
El advenimiento de los programas de computadora conocidos como asistentes de
prueba o demostradores interactivos de teoremas, así como su aplicación en el
desarrollo y verificación formal de teoremas matemáticos, ha traido consigo una noción
de prueba formalizada que, como es de esperarse, no coincide con las pruebas informales, si bien
rigurosas, con las que convive diariamente el matemático pero que tampoco
corresponde al concepto de prueba formal surgido en, y estudiado por la lógica
matemática. El objetivo de esta charla es presentar algunas cuestiones
generadas por esta novel idea de prueba, abriendo así la puerta a lo que
podemos llamar filosofía de las matemáticas asistidas por computadora.
Este trabajo se realiza con el apoyo del proyecto UNAM PAPIME PE102117.