OpenAI meldet formalisierten Beweis gegen die Exponential Time Hypothesis

Posted on Oct 27 • Originally published at elsolitario.org

El 18 de octubre de 2026, un modelo de OpenAI produjo una prueba que, según la empresa, refuta una conjetura de complejidad computacional vigente desde 1999: la Hipótesis del Tiempo Exponencial.

La prueba quedó formalizada en Lean un día después y forma parte de tres descubrimientos que OpenAI presentó el 26 de octubre junto a un nuevo protocolo para trabajar con comunidades académicas.

La Hipótesis del Tiempo Exponencial es una conjetura de teoría de la complejidad formulada en 1999 por Russell Impagliazzo y Ramamohan Paturi. Afirma que ningún algoritmo puede resolver 3-SAT, el problema de satisfacibilidad booleana con cláusulas de tres literales, en tiempo subexponencial en el peor caso.

El acrónimo ETH aparece en cientos de papers de teoría de grafos, bases de datos, biología computacional y geometría computacional, que la citan para justificar por qué ciertos problemas no admiten algoritmos rápidos. Es una suposición más fuerte que asumir simplemente que P es distinto de NP: fija un piso exponencial concreto, no solo la ausencia de un algoritmo polinomial.

OpenAI anunció el 26 de octubre de 2026 tres resultados producidos por sus modelos: una prueba de análisis armónico que resuelve de paso la conjetura de Kakeya, una refutación de la ETH en teoría de la complejidad y un tercer resultado de teoría cuántica de campos que la empresa todavía no detalló en público. Los tres pasaron por el mismo filtro antes de salir: un experto externo, actuando como 'shepherd' (pastor), recomendó cómo presentar cada hallazgo a la comunidad académica correspondiente, en lugar de que OpenAI decidiera sola.

Cada área recibió una estrategia distinta de publicación: ÁreaEstrategia de publicaciónQué se liberóMatemáticas (suavizado local y Kakeya)Publicación abierta; los investigadores se organizan por su cuentaEscrito en lenguaje natural y prueba formal en Lean, en GitHubComplejidad computacional (ETH)Un grupo externo explica el resultado mientras la salida del modelo queda públicaEscrito en lenguaje natural y formalización en Lean, en GitHubFísica (teoría cuántica de campos)Un grupo externo decide qué liberar; por ahora prefiere escribirlo ellos mismosNada publicado todavía OpenAI dice no saber todavía cuál de las tres estrategias funciona mejor y pide feedback sobre cómo ampliar la participación. El proceso se apoya en cuatro principios que la empresa fijó para estas colaboraciones:

flowchart TD A [ "Modelo de OpenAI" ] -- > B [ "Nuevo resultado: matematico, de complejidad o de fisica" ] B -- > C [ "Un experto externo actua como shepherd" ] C -- > D [ "Se elige una estrategia de lanzamiento" ] D -- > E [ "Matematicas: salida libre en GitHub" ] D -- > F [ "Complejidad (ETH): grupo explica, salida publica" ] D -- > G [ "Fisica: grupo decide, salida contenida" ] Enter fullscreen mode Exit fullscreen mode Contexto e historia La ETH no nació con OpenAI. La propusieron Russell Impagliazzo y Ramamohan Paturi en 1999 como una hipótesis más fina que la pregunta abierta de P contra NP: fija un piso exponencial concreto para el peor caso de 3-SAT, no solo la ausencia de un algoritmo polinomial. Desde entonces, cientos de papers en teoría de grafos, bases de datos, biología computacional y geometría computacional usaron la ETH como supuesto de partida para probar que sus propios problemas también son difíciles, mediante reducciones que heredan la dureza de 3-SAT.

El resultado matemático tiene una historia paralela igual de larga. En 1991, Christopher Sogge propuso la conjetura de suavizado local, sobre cómo se enfoca una onda en el peor momento posible frente a lo que ocurre en un instante típico. Esa conjetura implica, entre otras cosas, la conjetura de Kakeya y la conjetura de restricción de Stein.

En 2019, Larry Guth, Hong Wang y Ruixiang Zhang probaron el caso de suavizado local en dos dimensiones; en 2025, Hong Wang y Joshua Zahl resolvieron Kakeya en tres dimensiones. El modelo de OpenAI, según la empresa, prueba el caso de suavizado local en todas las dimensiones y resuelve de paso Kakeya y la de Stein para cualquier número de dimensiones, apoyándose en una ecuación diferencial parcial auxiliar distinta de las usadas en las pruebas anteriores.

Este no es el primer resultado matemático que OpenAI libera de esta manera: la empresa dice haber aplicado la misma estrategia de publicación abierta en un anuncio del 6 de octubre de 2026. La diferencia esta vez es que el resultado de complejidad sí pasó antes por un grupo de colaboradores externos. La prueba de Kakeya en todas las dimensiones llega siete años después del caso bidimensional de Guth, Wang y Zhang.

La Hipótesis del Tiempo Exponencial no dice que 3-SAT sea irresoluble: dice que cualquier algoritmo correcto necesita tiempo exponencial en el peor caso, sin importar cuán ingenioso sea. Formalmente, afirma que no existe ningún algoritmo que resuelva 3-SAT en tiempo 2^o(n), es decir, estrictamente menor que exponencial en el número de variables n. Refutarla exige mostrar, aunque sea sin construirlo explícitamente, que un algoritmo así existe.

OpenAI no detalló públicamente la técnica usada para la prueba de complejidad: el anuncio solo confirma que la demostración fue producida por el modelo y verificada formalmente en Lean. Donde sí hay más detalle es en el resultado matemático, que según la empresa se apoya en una ecuación diferencial parcial auxiliar novedosa, distinta de las herramientas de análisis armónico que usaron Guth, Wang y Zhang para el caso bidimensional.

La verificación en Lean es lo que distingue este anuncio de una afirmación sin respaldo. Un verificador de tipos como Lean rechaza cualquier paso lógico inválido, así que una compilación exitosa confirma que la cadena de inferencias es correcta dentro del sistema formal declarado. Eso no elimina todo riesgo: Lean valida que la prueba es internamente consistente, no que la manera de traducir '3-SAT' o 'tiempo subexponencial' a axiomas de Lean capture exactamente lo que la comunidad de complejidad entiende por esos términos. Esa traducción, la formalización del enunciado y no solo de la prueba, es justamente lo que el grupo de colaboradores externos de la ETH está revisando antes de que el resultado se considere confirmado por la comunidad.

📌 Nota: que Lean acepte una prueba confirma que es lógicamente válida dentro de los axiomas declarados, no que esos axiomas describan correctamente el problema real que se quería resolver.

Las implicaciones no son automáticas. Los cientos de papers que asumieron la ETH para probar dureza condicionada en sus propios problemas siguen siendo lógicamente correctos: demostraron que si la ETH es cierta, entonces su problema es difícil. Lo que cambia es que esa premisa, si la refutación resiste el escrutinio, ya no es cierta, así que la conclusión deja de estar garantizada. Cada uno de esos resultados necesitará revisarse para ver si sigue valiendo con otro supuesto, o si en verdad era más débil de lo que parecía.

La refutación tampoco entrega todavía un algoritmo utilizable. Mostrar que existe un algoritmo subexponencial para 3-SAT no es lo mismo que publicarlo con una constante razonable: muchas pruebas de existencia en complejidad son no constructivas o producen algoritmos con constantes tan grandes que no sirven en la práctica. El propio anuncio de OpenAI lo plantea con cautela: la refutación reabre preguntas sobre cuánto más rápidas pueden volverse esas tareas, pero guiar la búsqueda de mejores algoritmos no es lo mismo que haberla terminado.

Hay además una asimetría que OpenAI reconoce en su propio anuncio: elegir a los primeros shepherds define quién se entera primero y quién arma el relato inicial de cada hallazgo. La empresa dice estar abierta a sugerencias sobre cómo ampliar esa participación, pero por ahora el criterio de selección de esos expertos no es público. OpenAI dice no saber todavía cuál de sus tres estrategias de publicación funciona mejor.

El grupo de colaboradores de ciencias de la computación ya decidió hacer público de inmediato el escrito en lenguaje natural y la formalización en Lean del resultado sobre la ETH, y ambos están en el repositorio de GitHub de OpenAI. El trabajo que falta es externo a la empresa: que especialistas en teoría de la complejidad repasen la formalización del enunciado, no solo la prueba, y que la comunidad empiece a mapear qué resultados condicionados a la ETH quedan en pie y cuáles no.

Para el resultado de física, en cambio, no hay nada que revisar todavía: el grupo externo optó por escribir su propio material antes de publicar los artefactos que generó el modelo. OpenAI no dio fecha para esa publicación.

Si querés revisarlo de primera mano, el escrito en lenguaje natural y la formalización en Lean del resultado sobre la ETH ya están publicados en el repositorio de GitHub de OpenAI, abiertos para que cualquiera los lea o intente encontrarles un error.

Es la conjetura, formulada en 1999, de que ningún algoritmo resuelve 3-SAT en tiempo subexponencial en el peor caso. Sirve de base para pruebas de dureza condicionada en decenas de problemas relacionados con la satisfacibilidad booleana.

Porque cientos de papers la usaron como supuesto de partida para demostrar que sus propios problemas, en áreas como bases de datos o biología computacional, también son computacionalmente difíciles.

En principio implica que existe un algoritmo capaz de resolver 3-SAT en tiempo subexponencial, aunque la prueba no lo construye explícitamente ni dice si sería útil en la práctica.

Es un problema de geometría sobre el tamaño mínimo que debe tener un conjunto que contiene segmentos de línea en todas las direcciones posibles; se resolvió en tres dimensiones en 2025 y ahora, según OpenAI, en todas las dimensiones.

El escrito en lenguaje natural y la formalización en Lean del resultado sobre la ETH están publicados en el repositorio de GitHub de OpenAI, disponibles para cualquiera que quiera auditarlos.

📱 ¿Te gusta este contenido? Únete a nuestro canal de Telegram @programacion donde publicamos a diario lo más relevante de tecnología, IA y desarrollo. Resúmenes rápidos, contenido fresco todos los días.

Expand Stefan Stefan Stefan Follow Senior Software Engineer | Product Engineering & Architecture | AI & Security Location VC, Australia Joined Feb 10, 2026 • Oct 27 Dropdown menu Copy link Hide Could you add a direct link to the ETH proof files? The article says the proof doesn't explicitly construct an algorithm, but I'd like to see whether that's stated in the manuscript or inferred from the announcement. That seems worth pinning down before drawing conclusions about practical applications.