Resuelto por ordenador: famosos problemas matemáticos que las máquinas ayudaron a resolver (1976–2026)

En 1976, dos matemáticos de Illinois anunciaron que habían demostrado que cuatro colores bastan para colorear cualquier mapa, y que parte de su demostración solo podía comprobarla un ordenador. Muchos matemáticos se sintieron muy incómodos: ¿es de verdad una demostración si ningún humano puede leerla entera? Cincuenta años después, la pregunta se ha invertido. En 2026, sistemas de IA encontraron las ideas clave de resultados que los expertos no habían encontrado en décadas. Este artículo cuenta la historia en orden y, para cada problema famoso, dice exactamente qué hizo la máquina, porque «resuelto por ordenador» puede significar cosas muy distintas.

1976: cuatro colores y una demostración que nadie podía leer

Núcleo GCSE

La pregunta es tan sencilla que vale para primaria: colorear un mapa de modo que dos países vecinos nunca compartan color. ¿Cuántos colores podrías necesitar? Francis Guthrie apostó por cuatro en 1852. Es fácil ver que puedes necesitar cuatro (mira la imagen de abajo), pero demostrar que cuatro bastan siempre, para cualquier mapa posible, se resistió a los matemáticos durante 124 años.

Kenneth Appel y Wolfgang Haken encontraron la forma de demostrar que cualquier mapa que necesitara cinco colores tendría que contener uno de casi dos mil patrones especiales, y que cada uno de esos patrones se puede «reducir». Comprobarlos todos a mano era imposible, así que lo hizo un ordenador, con más de mil horas de cálculo. El teorema quedó demostrado, pero de una manera que cambió lo que «demostración» significaba en la práctica.

Cómo se despejó la duda: en 1996 llegó una demostración por ordenador más corta, y en 2005 Georges Gonthier y Benjamin Werner verificaron todo el argumento en el asistente de demostración Coq. Hoy es uno de los teoremas más minuciosamente verificados de las matemáticas.

1996: la primera demostración que un ordenador encontró por sí solo

Ampliación de grado

La conjetura de Robbins preguntaba si tres reglas cortas describen exactamente la misma álgebra que el álgebra de Boole, la lógica de verdadero o falso que hay dentro de cada chip. Lógicos de primer nivel, entre ellos Alfred Tarski, no habían logrado resolverla en sesenta años. En 1996, el demostrador automático EQP de William McCune exploró cadenas de razonamiento posibles durante unos ocho días y encontró una demostración. Era algo de otra naturaleza que lo de 1976: nadie le había dicho al ordenador cómo debía ser el argumento.

1998–2014: las naranjas de Kepler

En 1611, Johannes Kepler afirmó que la forma en que los fruteros apilan las naranjas (cada capa en los huecos de la de abajo) es el empaquetamiento más denso posible de esferas iguales. Llena alrededor del 74 % del espacio (exactamente π/√18).

Thomas Hales, con Samuel Ferguson, convirtió la pregunta en miles de problemas de optimización, los resolvió por ordenador y anunció una demostración en 1998. Los revisores de la revista dijeron estar «seguros al 99 %» de que era correcta, pero no podían comprobar cada cálculo. Hales respondió dirigiendo el proyecto Flyspeck para volver a verificarlo todo con software de asistente de demostración; terminó en 2014.

2016: la demostración de 200 terabytes

Núcleo GCSE

Aquí tienes un rompecabezas para probar. Colorea cada número entero de rojo o de azul. ¿Puedes hacerlo sin que ninguna terna pitagórica (tres números con a² + b² = c², como 3, 4, 5) sea de un solo color?

Ronald Graham ofreció 100 dólares por la respuesta. En 2016, Marijn Heule, Oliver Kullmann y Victor Marek usaron un solucionador SAT (software que resuelve enormes rompecabezas lógicos de verdadero o falso) en el superordenador Stampede durante unos dos días. La respuesta: todos los números del 1 al 7824 se pueden colorear sin problema, pero del 1 al 7825 no. La demostración de que ningún coloreado de 7825 números funciona ocupaba 200 terabytes, y Nature la presentó como la mayor demostración matemática de la historia hasta entonces. La misma técnica resolvió en 2019 la conjetura de Keller sobre teselar el espacio con cubos en siete dimensiones.

2025–2026: la IA empieza a encontrar las ideas

Ampliación de máster

Todo lo anterior usaba el ordenador para comprobar o para buscar dentro de un marco diseñado por personas. A partir de 2025, sistemas basados en grandes modelos de lenguaje empezaron a proponer ellos mismos las ideas matemáticas y a combinarlas con el asistente de demostración Lean, para que el resultado pudiera verificarlo una máquina en lugar de simplemente creerlo.

La conjetura de la distancia unidad (mayo de 2026). En 1946, Paul Erdős preguntó: si colocas n puntos en una superficie plana, ¿cuántos pares pueden estar exactamente a 1 unidad de distancia? Creía que la respuesta crece solo un poquito más rápido que n. Un modelo interno de OpenAI encontró una familia infinita de conjuntos de puntos que lo supera en una potencia real de n, con herramientas profundas de teoría algebraica de números. Nueve matemáticos de primer nivel, entre ellos los medallistas Fields Tim Gowers y Jacob Tsimerman, lo comprobaron y escribieron un artículo complementario, y Will Sawin hizo explícita la ganancia. Gil Kalai comparó su importancia con la demostración de los cuatro colores de 1976.

AlphaProof Nexus (mayo de 2026). Google DeepMind puso a su agente, que combina el modelo Gemini con Lean, a trabajar en 353 problemas abiertos de la base de datos de problemas de Erdős. Resolvió 9, incluidos dos abiertos desde hacía 56 años, y demostró 44 conjeturas de la Enciclopedia en Línea de Sucesiones de Enteros (OEIS). Cada demostración compila en Lean. Fíjate, eso sí, en la tasa de éxito: alrededor del 2,5 %.

Astra (agosto de 2026). OpenAI anunció diez resultados de su próximo modelo, aún no publicado, entre ellos la primera construcción de un grupo no sófico (respuesta a una pregunta que Mikhail Gromov planteó en 1999), tres problemas de Erdős y la primera mejora desde 1978 de una cota general sobre empaquetamiento de esferas. Cada uno iba acompañado de un certificado de Lean. Una auditoría humana independiente no encontró errores sustanciales confirmados en los resultados principales, aunque uno recibió de un especialista una petición de revisión importante, y la revisión por pares en revistas no había terminado cuando se escribió esto.

Cincuenta años en una cronología

Qué significa esto si estás aprendiendo matemáticas

Cada resultado de este artículo dependió todavía de personas: alguien tuvo que plantear el problema con precisión, decidir qué enfoque merecía la pena, comprobar que el teorema que demostró el ordenador era el que importaba y explicar por qué es cierto. Esa es justo la habilidad que construyen las matemáticas del colegio cuando te piden mostrar tu razonamiento, y es el tema de nuestro artículo ¿Puede la IA hacer matemáticas de verdad?. Para los problemas que siguen abiertos, y una lista ficha por ficha de estos problemas resueltos, consulta nuestro centro de misterios matemáticos sin resolver.