La primera vez que los ordenadores superaron a los matemáticos: el teorema de los cuatro colores

Claro, hoy tienes la inteligencia artificial para pedirle que resuelva cualquier problema matemático o tarea que te envían de la universidad, pero antes no existía ni ChatGPT. Ciertas fórmulas y ejercicios por resolver resultaban realmente complicados para los expertos que se dedicaban de lleno al área. Incluso mucho antes de que Windows se hiciera realidad, alrededor de los 70, las pruebas asistidas por ordenador eran realmente impresionantes.

Sin embargo, había algo que era muy complicado de lograr y se pudo salir de ello gracias al teorema de los cuatro colores. Lo que parecía un problema relativamente simple acabó desencadenando un debate que todavía hoy sigue presente en la filosofía de las matemáticas. Sin buscar en Internet ni tener que depender de un asistente virtual, este método de resolución fue el más efectivo para la época y definitivamente le dio un giro completo a la historia de la informática.

El problema centenario que una computadora consiguió resolver

El teorema de los cuatro colores plantea una afirmación sorprendente porque cualquier mapa plano puede colorearse utilizando un máximo de cuatro colores de forma que dos regiones adyacentes nunca compartan el mismo color.

La cuestión fue propuesta en el siglo XIX y mantuvo ocupadas a generaciones de matemáticos durante más de cien años. Su aparente simplicidad resultaba engañosa. Aunque el enunciado podía entenderse en pocos segundos, encontrar una demostración rigurosa se convirtió en uno de los desafíos más persistentes de la disciplina.

La situación cambió en julio de 1976, cuando los matemáticos Kenneth Appel y Wolfgang Haken, de la Universidad de Illinois, anunciaron una demostración que utilizaba ayuda informática a gran escala. Con la colaboración del programador John Koch, emplearon algoritmos capaces de analizar miles de configuraciones distintas.

El sistema realizó alrededor de 1.200 horas de cálculo y evaluó una enorme cantidad de casos que habrían resultado impracticables para cualquier investigador trabajando únicamente con papel y lápiz. Posteriormente, Appel y Haken llegaron a reconocer que el ordenador «comenzó a enseñarnos cosas sobre cómo proceder que nunca esperábamos» y que había llegado a «superar a sus creadores» en determinadas tareas intelectuales.

La prueba no solo resolvía un problema histórico. También dejaba una pregunta incómoda sobre la mesa: ¿puede considerarse plenamente válida una demostración matemática que ningún ser humano es capaz de verificar por completo sin la ayuda de una máquina?

La reacción de la comunidad matemática estuvo lejos de ser unánime. Para muchos investigadores, el resultado era correcto y representaba una evolución natural de las herramientas matemáticas. Otros, en cambio, consideraban que una prueba dependiente de millones de comprobaciones computacionales rompía con la tradición de las demostraciones elegantes y comprensibles para cualquier experto.

Las críticas fueron especialmente duras. El matemático Herbert Wilf llegó a bromear afirmando: «¡Dios no permitiría que el teorema se demostrara mediante un método tan terrible como ese!». Paul Halmos fue aún más directo al escribir: «la presente prueba se basa en efecto en un Oráculo, ¡y digo abajo con Oráculos! No son matemáticas». También aparecieron voces que sostenían que una solución fundamentada en verificaciones informáticas no pertenecía realmente al campo de las matemáticas tradicionales.

Sin embargo, con el paso del tiempo la prueba fue ganando aceptación. Matemáticos de gran prestigio, entre ellos William Tutte y Heinrich Heesch, terminaron reconociendo la validez del trabajo. El debate dejó de centrarse en si la demostración era correcta y pasó a enfocarse en una cuestión más profunda: el papel que deben desempeñar los ordenadores en la generación del conocimiento científico.

El filósofo Thomas Tymoczko argumentó años después que nadie había visto realmente una demostración completa del teorema en el sentido clásico. Frente a esa postura, Ted Swart defendió que una computadora no era más que una extensión de las herramientas matemáticas tradicionales y resumió su visión con una frase que se hizo célebre: «Considero que la prueba asistida por computadora es simplemente una extensión del lápiz y el papel».

Hoy, casi medio siglo después, el teorema de los cuatro colores sigue siendo recordado no solo por resolver un problema histórico. Su verdadero legado consiste en haber marcado la primera gran ocasión en la que una máquina realizó una parte esencial del trabajo intelectual necesario para alcanzar una demostración matemática.

Aquella decisión abrió la puerta a las pruebas verificadas por ordenador, a los sistemas formales modernos y a una nueva forma de colaboración entre seres humanos y computadoras. Lo que en 1976 muchos consideraron una herejía académica acabó convirtiéndose en una práctica cada vez más habitual en algunos de los campos más avanzados de las matemáticas contemporáneas.