Ordenadores para hacer matemáticas: ¿competición o cooperación?

La partida de ajedrez en la que la supercomputadora Deep Blue ganó a Kasparov dio un vuelco a las ciencias de la computación. Lo que parecía imposible se volvió realidad: una máquina había vencido a un ser humano en inteligencia. Mientras tanto, los ordenadores llevan tiempo usándose para hacer matemáticas. ¿Podrán vencernos también aquí?

Está claro que, para hacer cálculos, los ordenadores son mucho más rápidos que los humanos. La película Figuras Ocultas mostraba salas llenas de mujeres afroamericanas rellenando hoja tras hoja de papel para calcular la trayectoria de la nave espacial de la NASA Friendship 7, matemáticas que ya en los años sesenta empezaban a ser reemplazadas por ordenadores. Pero el reto de desarrollar nuevas matemáticas es mucho mayor: se trata de demostrar teoremas.

Apilando naranjas

Los ingredientes para demostrar un teorema son dos: afirmaciones previamente establecidas (pueden ser axiomas, si son tan básicos que no necesitan demostración, o bien otros teoremas ya demostrados) y reglas lógicas. La receta consiste en combinar las afirmaciones utilizando las reglas lógicas para deducir así el teorema. Dar con la manera de combinar las afirmaciones y la elección de reglas lógicas para conseguir demostrar el teorema con éxito no es tarea fácil. De hecho, es mucho más difícil que hacer cálculos, porque requiere creatividad. Ante este desafío, ¿tienen algo que hacer las máquinas?

La respuesta es afirmativa: ya hay ejemplos de teoremas donde los ordenadores han sido clave para su demostración. Uno de ellos parte de la famosa conjetura de Kepler. Según esta conjetura, la mejor manera de apilar esferas es en forma de pirámide, tal y como se colocan las naranjas en cualquier frutería. Aunque Kepler predijo hace cuatro siglos que esta era la manera de reducir al mínimo el hueco entre las esferas, hasta 1998 no se había logrado dar con una demostración rigurosa. Fue entonces cuando Thomas Hales consiguió, primero, reducir las infinitas formas de apilar esferas a una lista de unos cuantos miles, las maneras más densas. Esta reducción la hizo a mano y, después, analizó una a una las maneras de la lista, utilizando un ordenador, hasta obtener la colocación mejor. Una vez demostrada, la conjetura se convirtió en teorema.

Hales envió su trabajo a la revista más prestigiosa de matemáticas: Annals of Mathematics. Tras cuatro años de revisión, le devolvieron el artículo. La revista alegaba que había sido imposible comprobar el código en el que se había apoyado Hales para demostrar el teorema. No fue hasta 2005 cuando accedieron a publicar una versión abreviada del artículo, centrándose solamente en las partes de la demostración que se habían realizado a mano.

La necesidad de entender

La reticencia de Annals a dar por válida una demostración por ordenador refleja el sentimiento de una parte de la comunidad matemática. Es cierto que, muchas veces, se necesitan códigos larguísimos que es imposible verificar a mano. Por eso hay quien cuestiona la validez de este tipo de demostraciones, argumentando que dependen del proceso empírico que es la computación antes que de la deducción lógica a partir de axiomas. Como cualquier proceso empírico, la computación puede verse afectada por errores en el código, defectos físicos en el ordenador en sí… Errores y defectos que podrían resolverse utilizando diferentes máquinas, diferentes lenguajes de programación, etc., aunque es cierto que la transparencia de la deducción hecha a mano la hace inmune a estos fallos.

Sin embargo, hay otros usos de las computadoras para demostrar teoremas que son menos controvertidos. Se trata de los sistemas de verificación formal. En lugar de utilizar otros teoremas ya establecidos como ingredientes en las demostraciones, estos sistemas exigen que se parta únicamente de los axiomas. Equipados con las reglas lógicas más básicas, los ordenadores son capaces de verificar cada paso de la demostración. Carecen de la intuición que a veces se deja llevar por la tentación muy humana de sacar la conclusión deseada a toda costa, de forma que no dejan escapar ni un solo detalle. Además, validar una demostración siempre es más fácil que encontrarla, con lo que estos códigos son más sencillos y por tanto más comprensibles por seres humanos.

Ante el rechazo parcial de Annals, Hales se propuso verificar formalmente su propia demostración. El equipo Flyspeck, que él lideró, logró completar la validación en 2017. Por eso uno de los usos más prometedores de los ordenadores en matemáticas es precisamente la revisión de artículos científicos. La labor de revisión, a pesar de ser tan necesaria para el progreso científico, no es un trabajo remunerado ni reconocido para progresar en la carrera investigadora, y esta carga se podría reducir utilizando ordenadores. No podemos ignorar la encomiable tarea de traducir la demostración de un teorema al lenguaje formal que pueda entender un ordenador. Sin embargo, los teoremas ya verificados formalmente serían ingredientes legítimos en futuras verificaciones, aligerando el trabajo de revisión al menos a largo plazo.

Intuición y elegancia muy humanas

Podríamos admitir que los teoremas verificados formalmente sí son válidos, o, al menos, que lo son si es posible comprobar que el código de verificación sea correcto. Pero la demostración de un teorema va más allá de darlo por cierto: también da la clave de por qué se cumple. Cuando entendemos los pilares sobre los que se sostienen los teoremas ya establecidos, podemos desarrollar la intuición necesaria para proponer nuevos teoremas y demostrarlos. En este sentido, las demostraciones por ordenador como la de Hales no son nada esclarecedoras, y esta es una de las críticas principales al uso de ordenadores en matemáticas.

A pesar de todo, el propio ejercicio de formalizar una demostración para que sea verificable por ordenador ayuda a destapar posibles huecos en la estructura lógica, contribuyendo así a que pensemos de manera clara y rigurosa. Como apoyo a nuestro razonamiento, las computadoras son una poderosa herramienta y seguramente cobrarán cada vez más protagonismo. Pero la comunidad matemática tardará en renunciar a la elegancia de una buena demostración hecha a mano.

QUE NO TE LA CUELEN:

• Aunque los ordenadores juegan un papel fundamental en aeronáutica, la NASA sigue contratando a profesionales de las matemáticas. Sus conocimientos son clave para programar los ordenadores y hacer los cálculos de manera eficiente.

REFERENCIAS (MLA):

• Hales, Thomas. “A Proof Of The Kepler Conjecture”. Annals Of Mathematics, vol 162, no. 3, 2005, pp. 1065-1185. Annals Of Mathematics, Princeton U, doi:10.4007/annals.2005.162.1065. Accessed 11 July 2021. https://doi.org/10.4007/annals.2005.162.1065

Hales, Thomas et al. “A Formal Proof of the Kepler Conjecture”. Forum Of Mathematics, Pi, vol 5, 2017. Cambridge University Press (CUP), doi:10.1017/fmp.2017.1. Accessed 11 July 2021. https://doi.org/10.1017/fmp.2017.1