Math Demostraciones

Demostraciones con ordenadorEl ordenador ha dejado de ser sólo una herramienta de cálculo o un almacén de memoria, capaz de asombrarnos por su capacidad de ganar al campeón mundial de ajedrez, para convertirse en una máquina inteligente que puede demostrar teoremas.
Davis Mumford, ganador de la medalla Fields en 1974, dijo en una ocasión que “a pesar de todas las exageraciones propagandísticas,la comunidad matemática sigue considerando a los ordenadores como invasores”. Ya han pasado 30 años desde entonces y una gran parte de la comunidad matemática considera que los ordenadores han pasado a ser una herramienta muy valiosa en la investigación matemática.
Desde que aparecieron los logaritmos, los matemáticos han buscado siempre la forma de eludir cálculos que, por su carácter meramentemecánico, fueran una simple pérdida de tiempo a evitar. Fueron bienvenidos la regla de cálculo, las primeras máquinas a las que había que hacer girar a mano para que hicieran sumas y restas y, cómo no, los primeros ordenadores capaces de llevar a término cálculos que se salían ya de la escala humana.
Pero llegó un momento en que las máquinas fueron capaces de llevar a cabo la simulación de unrazonamiento deductivo, algo propio de una mente matemática. Fue entonces cuando algunos científicos tuvieron la sensación de que se estaba profanando un terreno prohibido para cualquier tipo de máquina. ¿Era juicio o prejuicio? El desarrollo de la Informática es extraordinariamente veloz y en unos pocos años podría cambiar mentalidades forjadas durante siglos.
Cálculos inteligentesEn 1976 dosmatemáticos, Appel y Haken, sorprendieron a la comunidad matemática anunciando que habían conseguido demostrar el Teorema de los Cuatro Colores (dicho teorema afirma que cuatro colores son suficientes para colorear cualquier mapa de forma que dos colores iguales nunca coincidan en dos países que tengan una frontera en común). La sorpresa había sido por partida doble; por un lado, por el hecho de haberdemostrado una conjetura que se había resistido a todos los intentos durante más de cien años, y por el otro lado, porque la demostración se había hecho con un ordenador, concretamente el IBM 370-160, que para llevarla a cabo estuvo realizando cálculos durante más de 1.200 horas.
Trece años después, el ordenador CRAY corrió un programa durante cientos de horas para demostrar que no existen planosproyectivos finitos de orden 10. El ordenador examinó para ello todos los casos posibles (unos doscientos billones).
Habían sido demostrados dos teoremas por un ordenador. Algo estaba cambiando.
El razonamiento automáticoEl razonamiento automático (RA) es un área de la Inteligencia Artificial (IA) cuyo objetivo es crear programas de ordenador que permitan resolver problemas matemáticos en losque intervienen razonamientos. Todas las técnicas propias de esta área, como son la representación del conocimiento, las estrategias para controlar las reglas establecidas, las implementaciones, etc, están encaminadas a conseguir lo que se denomina un asistente de razonamiento automático.
Una vez establecido un conjunto de axiomas, el razonamiento automático debe ser capaz de demostrar unaconjetura como una consecuencia lógica de los mismos. Existen alrededor de una docena de programas informáticos de estas características. EQP (equational prover) es uno de los más famosos porque, gracias a él, L. Wos y McCunne consiguieron demostrar en 1996 que toda Álgebra de Robins es un Álgebra de Boole, algo que hasta entonces no había podido ser demostrado por los métodos convencionales. La novedades que este tipo de programas no está basado en los cálculos directos, sino en un proceso de reducción al absurdo.
El quehacer matemáticoLos detractores de las demostraciones con ordenador aducen básicamente dos razones para poner en tela de juicio este procedimiento. La primera es que no son verificables, ya que contienen etapas en el programa que nunca podrán ser comprobadas por ningún...