M¨¢quinas para fabricar teoremas matem¨¢ticos

Uno de los temores recurrentes ante el avance de la inteligencia artificial es la posible sustituci¨®n de los seres humanos por m¨¢quinas, dej¨¢ndoles sin prop¨®sito m¨¢s all¨¢ de las labores de mantenimiento de los robots. Por el momento, sigue habiendo tareas en las que la inteligencia humana no puede ser igualada por la artificial. ?Es as¨ª en el quehacer matem¨¢tico? Si se introdujera todo el conocimiento disponible en una m¨¢quina, ?podr¨ªa resolver los grandes misterios de la disciplina, operando de forma mec¨¢nica a partir de las ideas ya conocidas? Hoy en d¨ªa los ordenadores est¨¢n muy lejos de ser capaces de combinar con creatividad e ingenio las ideas matem¨¢ticas de la forma que se requiere para obtener nuevos teoremas, pero su incorporaci¨®n en la resoluci¨®n de problemas lleva siendo una realidad desde hace d¨¦cadas.?

M¨¢s informaci¨®n

Bernard Morin, haciendo matem¨¢ticas a ciegas

Galileo y Kepler en Laputa

Uno de los primeros ejemplos se dio a mediados de los setenta, cuando los matem¨¢ticos Kenneth Appel y Wolfgang Haken demostraron el llamado teorema de los cuatro colores. Este, planteado en 1850, dec¨ªa m¨¢s o menos que cualquier mapa geogr¨¢fico puede ser coloreado usando un m¨¢ximo de cuatro colores diferentes, de forma que no queden regiones adyacentes con el mismo color. Appel y Haken fueron capaces de reducir el problema general a un n¨²mero finito de casos concretos que hab¨ªa que comprobar haciendo una serie de c¨¢lculos. Pero, para verificar a mano los alrededor de 2.000 mapas, hubieran necesitado varias vidas, por lo que hicieron uso de la potencia de c¨¢lculo de un ordenador.?

Las computaciones se supon¨ªan correctas, pero su comprobaci¨®n fue una fuente de controversia en aquella ¨¦poca. El lenguaje de los c¨®digos era oscuro y pr¨¢cticamente ilegible, y, adem¨¢s, todos los mapas se introdujeron manualmente. ?Qui¨¦n pod¨ªa garantizar que no se hubiera cometido un error introduciendo tant¨ªsimas instrucciones? ?Qui¨¦n pod¨ªa comprobar que los c¨®digos fueran correctos? Esto plante¨® serias dificultades para aceptar este trabajo de acuerdo con el procedimiento de revisi¨®n por pares de la ciencia, que consiste en la verificaci¨®n-comprobaci¨®n del trabajo mediante uno o varios expertos an¨®nimos. Sin embargo, la dificultad de verificar una demostraci¨®n no es algo exclusivo del uso de ordenadores. La comprensi¨®n por terceras personas de resultados muy reconocidos y celebrados, como el ¨²ltimo teorema de Fermat (demostrado por Andrew Wiles), la conjetura de Poincar¨¦ (por Grigory Perelman) o la conjetura de Kepler (por Thomas Hales, y que tambi¨¦n contiene una parte asistida mediante ordenador), ha sido un verdadero quebradero de cabeza.?

La clasificaci¨®n requiere considerar muchos casos especiales y su discurso dista de la s¨ªntesis que podemos encontrar en la poes¨ªa

Tambi¨¦n se plantearon cr¨ªticas en un sentido est¨¦tico, de falta de elegancia: ¡°una buena prueba matem¨¢tica es similar a un poema ¡ª?pero esto es una gu¨ªa telef¨®nica!¡±, dijeron. Pero, de nuevo, este comentario tambi¨¦n se puede hacer a algunas demostraciones tradicionales. Un ejemplo es la clasificaci¨®n de grupos simples finitos, cuya demostraci¨®n recoge el trabajo de numerosos autores y se extiende a lo largo de m¨¢s de 10 000 p¨¢ginas. La clasificaci¨®n requiere considerar muchos casos especiales y su discurso dista de la s¨ªntesis que podemos encontrar en la poes¨ªa.?

En 1996, Neil Robertson, Daniel Sanders, Paul Seymour y Robin Thomas presentaron una nueva demostraci¨®n asistida por ordenador del teorema de los cuatro colores. El art¨ªculo ocupaba 40 p¨¢ginas, la implementaci¨®n se realiz¨® en c¨®digo C (mucho m¨¢s habitual y legible), y los mapas no se introduc¨ªan de forma manual. En esta ocasi¨®n, otros investigadores s¨ª pudieron reproducir la implementaci¨®n de forma independiente, y fue aceptado. Por tanto, la verificaci¨®n de este tipo de demostraciones no contradice el principio de revisi¨®n por pares.?

El uso del ordenador est¨¢ lejos de ser una caja negra para producir incomprensibles demostraciones que se limitan a certificar la veracidad de un enunciado

De hecho, la comprobaci¨®n de demostraciones asistidas por ordenador no es tan diferente de las tradicionales: se tienen que comprender todas las l¨ªneas de c¨®digo de ordenador, y en caso de que el c¨¢lculo computacional requiera realizar aproximaciones que produzcan una fuente de error, es necesario controlar rigurosamente la magnitud de dicho error para tenerlo en cuenta. El uso del ordenador est¨¢ lejos de ser una caja negra para producir incomprensibles demostraciones que se limitan a certificar la veracidad de un enunciado. Es, simplemente, una herramienta m¨¢s de la que se dispone y que, hoy en d¨ªa, como toda t¨¦cnica en matem¨¢ticas, puede ser usada y verificada tras el debido proceso de aprendizaje. Permite automatizar tareas rutinarias, ahorrando al matem¨¢tico c¨¢lculos triviales (aunque numerosos). Pero, m¨¢s all¨¢ de eso, dise?ar e implementar con ¨¦xito estos m¨¦todos requiere una gran comprensi¨®n del problema, y, en muchas ocasiones, plantea dudas y nuevos puntos de vista que refuerzan el conocimiento sobre el tema. Una demostraci¨®n asistida por ordenador de un nuevo teorema eventualmente puede contener una idea inesperada o una nueva estrategia para inspirar investigaciones futuras.

?gata A. Tim¨®n y Alejandro Luque son miembros del ICMAT.?

Caf¨¦ y Teoremas es una secci¨®n dedicada a las matem¨¢ticas y al entorno en el que se crean, coordinado por el Instituto de Ciencias Matem¨¢ticas (ICMAT), en la que los investigadores y miembros del centro describen los ¨²ltimos avances de esta disciplina, comparten puntos de encuentro entre las matem¨¢ticas y otras expresiones sociales y culturales, y recuerdan a quienes marcaron su desarrollo y supieron transformar caf¨¦ en teoremas. El nombre evoca la definici¨®n del matem¨¢tico h¨²ngaro Alfred R¨¦nyi: ¡°Un matem¨¢tico es una m¨¢quina que transforma caf¨¦ en teoremas¡±.