Hemos visto que las computadoras han invadido cotos que pensábamos profundamente humanos. En los años setenta(de hecho en 1968) el Maestro Internacional y experto en computación David Levy lanzó un famoso reto señalando que ninguna computadora podría vencerlo en una partida de ajedrez. En aquella época, a pesar de la participación de genios del ajedrez y la ingeniería como Shannon y Botvinnik, el nivel de juego de las computadoras era escasamente el de un principiante avanzado. La situación cambio rápidamente. Ya en 1989 Levy fue derrotado por un computador. Recuerdo en el año 90 correr en un computador 286 mi copia de Chessmaster 3.0 y sufrir para poder ganarle en el máximo nivel. La situación ahora es muy distinta. Los programas que corremos en nuestras computadoras sólo pueden ser derrotados por jugadores de extraordinario nivel. El mejor jugador de todos los tiempos Garry Kasparov fue humillado por Deep Blue en 1997, finalizando el dominio del hombre en el juego ciencia. IBM, quien construyó Deep Blue, la picó en pedazos para evitar que Kasparov tuviese la revancha, es decir, IBM fue la versión corporativa de Alekhine quien evitó volver a ver a Capablanca en un match despues de derrotarlo en Buenos Aires en el año 1927. Pero, ¿pueden ser exitosas las computadoras en matemática? El ajedrez es un juego y es un juego finito, las computadoras con su extraordinaria rapidez de cálculo pueden moverse en el árbol de variantes buscando la mejor opción. La matemática es más rica y pensamos que la demostración en matemática es más cercana al arte que a la lógica. Por eso sorprendió cuando un venerable problema no resuelto fue demostrado por medio de un computador. Se trata del problema del mapa de los cuatro colores. Los matemáticos habían observado que cualquier mapa, por intrincada que fuera la ubicación de los países, podía ser coloreado con 4 colores(cada país usando uno de los colores) de forma que dos países con regiones adyacentes siempre tuvieran distintos colores. El problema es demostrar que con 4 colores basta. Por mucho que los matemáticos lo pensaban, el problema se resistía. Finalmente en 1976 Appel y Haken usaron una computadora para ¡demostrar! el resultado. Por supuesto, la computadora verificó todas las configuraciones posibles, reduciendo las mismas, a ciertos casos básicos. Esta implementación usaba teoremas anteriores que permitían la clasificación de los mapas y después una verificación por fuerza bruta realizada por la máquina. Distintas voces se opusieron a esta manera de hacer matemáticas. ¿Como verificar los cientos de líneas del programa? Esta objeción me parece absurda. Todos recordamos que hacia la mitad de los años 90,
Andrew Wiles dio con la prueba del último teorema de Fermat, dicha prueba consistía en cientos de páginas de las matemáticas más abstractas que podemos imaginar, que tenían un error inicial que fue subsanado en otro artículo igual de abstracto y de otras cien páginas(escrito con Richard Taylor). Me temo que ver esto con cuidado(¿lo habrá hecho alguien?) es más pesado que ver el código de un programa. La aceptación de la prueba de Wiles tiene mucho del visto bueno de la cofradía de expertos.
Las demostraciones con computadora no han parado y otro venerable problema, el del empacado de esferas, ha sido tratado igualmente, usando una computadora, por Hales en 1998. El veredicto de los árbitros que recibieron el artículo es que ellos están seguros en un casi 99% de que el resultado de Hales es correcto, como vemos cuando se trata de pruebas asistidas por un computador la lógica se vuelve probabilidad.
