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.