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”.