Teorema de los 4 colores: así lo probó una máquina en 1976

El día que una máquina resolvió lo que un siglo de matemáticos no pudo

En julio de 1976, Kenneth Appel y Wolfgang Haken anunciaron que habían resuelto el teorema de los cuatro colores, un enigma que la matemática arrastraba desde 1852, cuando Francis Guthrie lo formuló al colorear un mapa de los condados ingleses. Lo revolucionario no fue el resultado, sino el método: un computador hizo el trabajo pesado, con 1.200 horas de cómputo y 10.000 millones de decisiones.

Los propios autores lo describieron con una frase que hoy suena sospechosamente actual: el sistema "empezó a enseñarnos cosas sobre cómo proceder que nunca esperábamos" y admitieron que había "superado a sus creadores" en ciertas tareas intelectuales.

Para un founder que hoy usa IA para programar, analizar datos o redactar propuestas, esa frase no es una curiosidad histórica. Es el acta de nacimiento de una discusión que sigue abierta: qué hacemos cuando la herramienta produce algo que no podemos revisar a mano.

Por qué los matemáticos se negaron a aceptarlo

La reacción de la comunidad fue todo menos entusiasta. Las objeciones no apuntaban a que el resultado fuera falso, sino a que el camino no era "matemática de verdad".

• Herbert Wilf, de la Universidad de Pensilvania: "¡Dios no permitiría que el teorema se probara con un método tan terrible como ese!"
• Paul Halmos, de UC Santa Barbara: "la prueba actual depende en efecto de un Oráculo, y yo digo abajo los Oráculos. No son matemática".
• Frank Bonsall, de la Universidad de Edimburgo: "si la solución implica verificación por computadora de casos especiales, esa solución no pertenece a la ciencia matemática en absoluto".
• Daniel Cohen, de Hunter College: "admitir las artimañas computacionales de Appel y Haken en las filas de la matemática solo nos dejaría intelectualmente insatisfechos".

Hubo algo más duro que el escepticismo: negación. George Spencer-Brown, de Cambridge, escribió que no había "nada que siquiera empiece a parecerse a una prueba" y lo llamó "el caso más ridículo de 'El traje nuevo del emperador' que jamás haya deshonrado la historia de la matemática".

Un jefe de departamento llegó a prohibir que Appel y Haken se reunieran con sus estudiantes de posgrado, con un argumento que cualquier líder de equipo reconoce: si el problema ya estaba resuelto "por un medio totalmente inapropiado", ningún matemático de primera línea volvería a trabajarlo, porque ya no sería el primero. La consecuencia, decía, era que una prueba decente podría retrasarse indefinidamente.

La grieta generacional que hoy se repite con la IA

El detalle más revelador es cómo se dividió la audiencia. Después de una presentación del hijo de Haken sobre la prueba, los asistentes se partieron en dos: los mayores de 40 no se convencían de que una prueba por computadora fuera correcta, y los menores de 40 no se convencían de que una prueba con 700 páginas de cálculos a mano pudiera serlo.

Esa grieta es exactamente la que se ve hoy en las empresas. El equipo que creció escribiendo cada línea de código desconfía del output del modelo; el que creció usándolo desconfía del proceso manual que nadie puede auditar.

La defensa más lúcida de 1976 no vino de un informático, sino del matemático Ted Swart, que había estado cerca de una prueba asistida por computadora al mismo tiempo que Appel y Haken. Swart sostuvo que la prueba por computadora era "solo una extensión del lápiz y el papel" y atacó la supuesta infalibilidad humana: "los seres humanos se cansan, su atención se distrae y son muy propensos a todo tipo de deslices. Las computadoras no se cansan".

En 1979 el filósofo Thomas Tymoczko llevó el debate al terreno formal en The Journal of Philosophy: una prueba que ningún humano puede recorrer completa no es una prueba matemática tradicional. No dudaba de que probara lo que decía probar; dudaba de que pudiéramos llamarla conocimiento verificable.

El nuevo capítulo: 8.202 casos y la misma pregunta

Cincuenta años después, el debate no se cerró: se mudó. En marzo de 2026, un equipo integrado por Ken-ichi Kawarabayashi, Mikkel Thorup, Carsten Thomassen, Bojan Mohar, Yuta Inoue y Atsuyuki Miyashita publicó una nueva prueba del teorema, que se presentará en noviembre en la conferencia Foundations of Computer Science, según reportó Quanta Magazine.

La nueva prueba es, en apariencia, más compleja: usa 8.202 configuraciones, contra las 633 de la prueba de 1997 liderada por Neil Robertson. Pero el punto no es el tamaño, sino que esas configuraciones se pueden reducir en paralelo. El algoritmo de coloreado pasó de necesitar n² pasos a n(log n) para un grafo de n vértices.

Thomassen, que lleva décadas con el problema, lo dijo sin rodeos: "lo que me gustaría es una prueba sin usar una computadora. Y nunca dejaré de pensar en eso".

¿Qué significa esto para tu startup?

La historia del teorema de los cuatro colores no es sobre matemática. Es sobre cómo una organización reacciona cuando aparece una herramienta que produce resultados correctos por caminos que nadie puede auditar a mano. Tres lecciones concretas:

1. La resistencia no mide si la herramienta funciona; mide quién la usa. En 1976, el rechazo vino de los matemáticos con más años de método manual. La prueba de 1997, con solo 633 configuraciones, fue aceptada de inmediato porque para entonces el uso de computadoras ya era común. Si tu equipo rechaza una herramienta nueva, pregúntate si la objeción es técnica o generacional.

2. La verificación es el nuevo cuello de botella, y hay que diseñarla. El problema de 1976 no fue generar la prueba, sino comprobarla. Hoy pasa lo mismo: en octubre de 2026, OpenAI publicó 722 manuscritos matemáticos producidos por un modelo interno no lanzado, organizados en 372 familias, y advirtió que algunos resultados sin formalizar podrían tener problemas. La respuesta de la industria es la misma que insinuó la matemática: verificación formal. Herramientas como Lean permiten que un computador revise si una prueba se sigue de axiomas definidos, y el AI for Math Fund de Renaissance Philanthropy y XTX Markets financió en 2026 un proyecto de Işil Dillig, de UT Austin, para aprender estructuras matemáticas reutilizables en pruebas formales. Si tu equipo produce con IA, necesitas un paso equivalente: tests, evals, revisión por muestreo. Sin eso, estás publicando sin verificar.

3. Documenta el proceso, no solo el resultado. The New York Times se negó a cubrir el anuncio de 1976 por miedo a una falsa alarma; cuando la prueba se consideró legítima, los editores argumentaron que ya no era noticia. La credibilidad no se recupera después. Si usas IA en un entregable, deja registro de qué modelo, qué prompts y qué revisión humana hubo. Es lo que en septiembre de 2026 recomendó el grupo asesor sobre Matemática e IA del Institute for Advanced Study: publicar el nombre del modelo, los prompts, el tiempo y el costo de cómputo de cada resultado.

Conclusión

El teorema de los cuatro colores se probó tres veces: en 1976, en 1997 y en 2026. Las tres veces hizo falta una computadora, y las tres veces alguien preguntó si eso contaba como matemática. La herramienta cambió; la pregunta no.

Para un founder, la lección es incómoda y liberadora a la vez: la ventaja competitiva no está en tener acceso al modelo, porque todos lo tienen. Está en saber qué hacer con su output, cómo verificarlo y cómo defenderlo ante quien todavía no confía en él. Eso es lo que separó a Appel y Haken de sus críticos, y es lo que va a separar a tu equipo del resto.

Fuentes

• The Four Colour Theorem: The first time machines mogged mathematicians (fuente original)
• The Four-Color Theorem Gets a Rare New Proof - Quanta Magazine
• A new proof of the Four Color Theorem has been discovered - Gigazine
• OpenAI Releases 722 Math Manuscripts From an Unreleased AI Model - Unite.AI
• Işil Dillig Receives AI for Math Fund Grant - UT Austin