La lógica al servicio de las matemáticas, o cómo es que mi computadora puede entender álgebra

Cuando uno piensa en las matemáticas en relación a la computadora por lo general uno apunta hacia las calculadoras o hacia los sistemas como Maple o Mathematica, que nos permiten automatizar cómputos tediosos, numéricos o simbólicos. Sin embargo, la lógica matemática ha posibilitado la implementación de programas conocidos como asistentes de prueba, los cuales permiten hacer demostraciones matemáticas complicadas, por ejemplo del teorema de Feith-Thompson en teoría de los grupos, ganando la certeza de que dichas demostraciones son correctas.

En esta plática hablaremos brevemente de los fundamentos lógicos de esta clase de programas, su relevancia en matemáticas y además haremos una breve demostración de su uso mediante ciertos ejemplos en el ámbito de las estructuras algebraicas.