El 15 de julio de 2026, en el subreddit de matemáticas de Reddit apareció un hilo con un título anodino: algo así como “Después de ver el método de OpenAI para la conjetura CDC, probé con GPT-5.6 y cerré un hueco de 30 años”.
Tres días después, el hilo llegó a Hacker News con 477 votos positivos y 308 comentarios. Los matemáticos que leyeron línea por línea el código en Lean tenían una postura sorprendentemente unánime: esta vez se trata de una verdadera contribución matemática.
Tras recorrer las discusiones, la fuerza del asunto radica en que tocó una tarea que los matemáticos humanos consideran especialmente espinosa: demostrar cotas inferiores. Y GPT-5.6 lo hizo con un solo prompt y 148 minutos.
Qué pasó: un prompt, 148 minutos y un hueco de 30 años
Phillip Kerger es profesor asistente de matemáticas aplicadas en UC Berkeley, doctorado en teoría de optimización por Johns Hopkins, y trabajó antes en el laboratorio de inteligencia artificial cuántica de la NASA. Desde el año pasado ha venido masticando, de forma intermitente, un problema: un vacío de complejidad en el campo de la optimización convexa que llevaba sin resolverse desde 1996.
En pocas palabras: en 1996 alguien diseñó un algoritmo cuya complejidad resultó ser \(O(d^2 \log^2 d)\). Todos saben que no puede ser mejor que \(O(d)\) (porque al menos hay que mirar cada dimensión). Pero el vacío de 30 años entre \(O(d)\) y \(O(d^2 \log^2 d)\) nadie lo había llenado —¿es que aún se podía ir más rápido, o aquel algoritmo viejo ya estaba en el límite?
Kerger había probado antes con GPT-5.4 y GPT-5.5, y ambos fallaron. Incluso cuando él encauzaba manualmente el razonamiento hacia la familia de funciones correcta, el modelo no completaba los últimos pasos.
Luego llegó GPT-5.6.
Siguiendo la estructura del prompt de la “conjetura de la doble cobertura cíclica” que OpenAI publicó hace unas semanas, escribió un prompt de unas 10 páginas: especificaba el marco matemático, enumeraba las vías de demostración viables, metía sus experiencias de intentos fallidos previos y definía explícitamente qué resultados no contaban como solución válida. Primero usó GPT-5.6 para ayudar a organizar la bibliografía relevante y pulir el esquema argumental del prompt, y luego le pasó la versión final al modelo en una sesión continua.
148 minutos después, GPT-5.6 escupió la construcción completa de la demostración.
Crédito de la imagen: Unsplash / GuerrillaBuzz — ilustración de la convergencia de métodos de optimización convexa. Lo que GPT-5.6 demostró es precisamente que la curva de cota inferior ya no puede bajarse más: aquel algoritmo de 1996 ya está pisando el límite teórico.
El resultado: una cota inferior de \(\Omega(d^2 / \log(d+1))\), que solo difiere de la cota superior conocida \(O(d^2 \log^2 d)\) en un factor logarítmico. Esto descarta la posibilidad de “que exista un método mucho más rápido que aquel algoritmo viejo de 30 años”.
Por qué “demostrar la cota inferior” es mucho más difícil: una analogía con correr
Para entender el peso del asunto, primero planteo una analogía cotidiana.
Demostrar la cota superior es como demostrar que puedes correr 100 metros: solo tienes que correr una vez, apretar el cronómetro y la conclusión queda firmada.
Demostrar la cota inferior es como demostrar que no puedes correr más rápido: para eso tienes que descartar todos los métodos de entrenamiento posibles. ¿Zapatillas nuevas? Inútil. ¿Cambiar la postura de salida? Inútil. ¿Dieta especial? Sigue sin servir. Para que la conclusión “no puedes bajar de 9 segundos” se sostenga, tienes que agotar todas las formas imaginables y demostrar una por una que ninguna te ayuda.
En matemáticas, demostrar la cota superior (“encontré un método que al menos llega hasta aquí”) es relativamente fácil: das un algoritmo, calculas su complejidad y listo. Pero demostrar la cota inferior (“no existe ningún método más rápido que este”) exige acotar todos los algoritmos posibles. Tienes que demostrar: pase lo que pase, por mucho que otros diseñen algoritmos nuevos, por cualquier truco que usen, por muchos rodeos que den — nada, el límite está ahí.
Por eso aquel comentarista de HN llamado alternator —quien se describió como alguien “que sabe un poco del área”— dijo:
“Proving upper bounds is easy, it’s just how long your algorithm runs for. Proving nontrivial lower bounds is much harder because it requires you to bound all possible algorithms.”
Y justo eso es lo que GPT-5.6 logró esta vez. No solo demostró que el algoritmo que construyó Kerger funciona bien: demostró que aquel método viejo de 1996 ya tocó el techo teórico. Durante 30 años nadie pudo descartar la posibilidad de “a lo mejor hay algo mejor”, y GPT-5.6 la descartó en 148 minutos.
Dos formas de hacer matemáticas con IA: no las confundas
Al hablar de IA haciendo matemáticas, conviene distinguir dos cosas. Parecen parecidas, pero son esencialmente distintas.
Primera: la IA como ayudante de conjeturas. Esto lleva años ocurriendo. Los investigadores dejan que el modelo busque patrones entre resultados conocidos, genere conjeturas “prometedoras” y luego el humano las verifica. El modelo dice “creo que esta desigualdad podría valer”, y el humano lo comprueba con papel y lápiz o con una computadora. En este escenario la IA es un asistente muy listo, pero la última palabra la tiene el humano.
Segunda: la IA completa una demostración rigurosa por sí misma — y pasa la verificación formal. Esto es lo que hizo GPT-5.6. El modelo no solo soltó un argumento “plausible”, sino que ese argumento se tradujo íntegramente a Lean 4 —un asistente de demostraciones matemáticas— y compiló línea por línea. Lean no acepta “obviamente se sigue”, “fácil de ver” ni retórica parecida. En el mundo de Lean, o cada paso es lógicamente impecable o directamente da error; no hay término medio.
Kerger subió todo el código Lean de la demostración a GitHub. Cualquiera que instale un gestor de versiones llamado elan, clone el repositorio y ejecute una línea, lake build, puede ver con sus propios ojos que el compilador no da error de principio a fin. Y al correr #print axioms, confirma que no hay sorryAx (el marcador de Lean que significa “este paso aún no lo demuestro”) —lo que significa que en toda la cadena lógica no hay ni un hueco.
El preprint de 36 páginas de Kerger, el prompt completo, el registro de la conversación con el modelo, el código Lean y las instrucciones de compilación —todo está público. Este estándar de divulgación está varios escalones por encima de esos artículos que solo mencionan de pasada, en los agradecimientos, “gracias al sistema de IA por su ayuda”.
Crédito de la imagen: Unsplash / Bozhin Karaivanov — interfaz del código del asistente de demostraciones Lean. La demostración de GPT-5.6 se tradujo íntegramente a Lean 4 y compiló sin errores; en toda la cadena lógica no hay ningún sorry (paso sin demostrar).
A decir verdad: las voces críticas también merecen oírse
No pienso escribir esto como un “la IA aplasta a los humanos”. Tanto en r/math como en HN hay bastantes dudas razonables, y esas voces son clave para entender el cuadro completo.
Primera, el área es bastante de nicho. Varios comentaristas señalaron que esta cota inferior de optimización convexa es mucho menos conocida que la “conjetura de la doble cobertura cíclica” que resolvió OpenAI. Esta última es un problema famoso de teoría de grafos colgado durante 50 años, mientras que la conjetura de cota inferior se mueve sobre todo en un círculo relativamente pequeño de teoría de la optimización. Su valor académico es real, pero su alcance “más allá del gremio” es limitado.
Segunda, su transferibilidad es dudosa. El patrón de razonamiento que exige demostrar cotas inferiores —acotar todos los algoritmos posibles— es sin duda una categoría muy difícil, y GPT-5.6 mostró capacidad aquí. Pero ¿puede esa capacidad transferirse de la optimización convexa a otras ramas de las matemáticas? Hasta ahora nadie lo sabe.
Tercera, la disputa por la prioridad. En la discusión de r/math, alguien estuvo rebuscando en la literatura de optimización rusa de los años 90 y sospecha que el lema central de la demostración de Kerger ya pudo haber sido publicado por matemáticos soviéticos, solo que en revistas poco indexadas por las bases de datos occidentales. Si se confirma, la contribución de GPT-5.6 sería “reconstruir un argumento desde una literatura casi olvidada y formalizarlo de una forma que nadie había usado”. Los pesos de ambas contribuciones son distintos.
Cuarta, los “148 minutos” no son todo. Kerger había dedicado a este problema, de forma intermitente, un año entero. Esas 10 páginas del prompt condensan su comprensión del problema, sus intentos fallidos, los callejones sin salida que ya descartó. Antes de GPT-5.6, GPT-5.4 y GPT-5.5 habían fracasado en el mismo problema. Los 148 minutos fueron la última búsqueda de demostración ininterrumpida —no magia desde cero. Como decía la cobertura de RuntimeWire: “el prompt envuelve un año de trabajo en el área”.
Crédito de la imagen: RuntimeWire / Gemini — ilustración generada por IA del flujo de demostración matemática. Vale la pena recordar: detrás del prompt hay un año de acumulación en el área, y los 148 minutos son solo el tiempo de búsqueda del último paso.
Lo realmente importante es este modo de trabajo
Dejando las polémicas a un lado, lo que a mí me parece más digno de atención no es el teorema concreto.
El flujo de trabajo humano + IA + verificación formal, como trío, ha demostrado ser reproducible.
El procedimiento de Kerger es claro: parte el gran problema en lemas pequeños, traduce primero cada lema a las sentencias estrictas de Lean, y luego deja que el modelo rellene la demostración. Si algún lema no compila, itera sobre ese solo —sin que un cambio en un sitio tire abajo toda la demostración. Este proceso no exige ser medalla Fields; el umbral está en que seas capaz de definir tu problema con precisión.
En otras palabras, la IA ya tiene una receta operativa para ir comiéndose los problemas matemáticos de “dificultad media”. Esto no va a dejar a los matemáticos sin trabajo —definir el problema, construir el prompt, juzgar si la salida es basura, eso hoy sigue siendo cosa de humanos—, pero cambiará el día a día de la investigación matemática: los investigadores se parecerán cada vez más a directores, y la IA cada vez más a un equipo de ejecución.
Un comentarista de HN lo dijo sin rodeos: a veces leer estas discusiones es como leer jeroglíficos. Pero no te asustes por la jerga —la esencia es simple. Durante 30 años, los humanos supieron hasta qué punto rápido podía correr un algoritmo, pero no se atrevieron a decir “este es el límite”. Una IA, guiada por una persona que acumuló un año de trabajo, demostró en 148 minutos que “este es el límite”. Luego, otra máquina llamada Lean revisó su tarea línea por línea y confirmó que no había tomado atajos.
Esta es la frontera de las matemáticas en 2026: humanos, IA y un compilador de demostraciones empiezan a trabajar juntos en un mismo proyecto.
Enlaces de referencia:
- Reddit r/math: After OpenAI’s CDC proof announcement, GPT-5.6 used a prompt to close a 30-year gap in convex optimization
- HN discussion (item?id=48957779)
