OpenAI afirma que uno de sus sistemas ha refutado la hipótesis del tiempo exponencial, una conjetura utilizada durante 25 años para razonar sobre la dificultad de miles de problemas informáticos. La empresa ha publicado un manuscrito en lenguaje natural y una formalización en Lean, y ha pedido a un grupo de especialistas —entre ellos dos de los autores que formularon la hipótesis— que examine, explique y contextualice el resultado.
La noticia es extraordinaria, pero exige precisión. Una prueba comprobada por un asistente formal no equivale automáticamente a consenso científico, no demuestra que P sea igual a NP y no convierte de repente todos los problemas difíciles en tareas rápidas. Sí plantea una posibilidad importante: que ciertos problemas de satisfacibilidad booleana puedan resolverse en tiempo subexponencial, contradiciendo el supuesto central de la hipótesis.
La forma responsable de leer el anuncio es separar tres capas: lo que OpenAI asegura haber demostrado, lo que el código de Lean verifica y lo que la comunidad todavía debe revisar sobre definiciones, supuestos, alcance e implicaciones. Esa separación permite entender el avance sin convertir una afirmación matemática en una promesa tecnológica inmediata.
Qué es la hipótesis del tiempo exponencial
La hipótesis del tiempo exponencial, conocida por sus siglas inglesas ETH, se formuló para describir la dificultad de k-SAT. En este problema se recibe una fórmula lógica con variables que pueden ser verdaderas o falsas y se pregunta si existe una asignación que satisfaga todas las restricciones. Para un valor fijo de k igual o superior a tres, la hipótesis sostiene esencialmente que no existe un algoritmo que resuelva todos los casos en tiempo subexponencial respecto al número de variables.
El artículo de Russell Impagliazzo y Ramamohan Paturi de 2001 formalizó esta idea y estudió cómo cambia la complejidad de k-SAT cuando aumenta k. Desde entonces, ETH se ha utilizado como supuesto condicional: si fuera cierta, numerosos problemas de grafos, geometría computacional, bases de datos o biología computacional tampoco admitirían determinados algoritmos rápidos.
Un resultado que refute ETH no invalida automáticamente cada artículo que la emplea. Cambia la lectura de sus conclusiones condicionales. Una afirmación del tipo «este problema no puede resolverse más rápido salvo que ETH sea falsa» dejaría de ofrecer la barrera esperada; habría que buscar otro supuesto o analizar directamente el problema.
Qué afirma OpenAI haber conseguido
La publicación oficial de OpenAI del 26 de octubre de 2026 presenta tres resultados generados con modelos internos: uno sobre suavizado local y la conjetura de Kakeya, otro sobre ETH y un tercero sobre la existencia matemática de ciertas teorías cuánticas de campos. La empresa describe esos materiales como datos de investigación en bruto que necesitan comprensión y revisión por especialistas.
Para ETH, OpenAI sitúa la obtención de la prueba en lenguaje natural el 16 de octubre y la formalización en Lean el día 17. El manuscrito publicado en su repositorio lleva fecha del 25 de octubre. La empresa sostiene que el algoritmo obtiene un tiempo subexponencial para contar exactamente asignaciones satisfactorias de fórmulas k-CNF y, por tanto, también para decidir si existe al menos una.
El resumen de la formalización en Lean concreta el alcance: para k fijo igual o superior a dos, la máquina determinista cuenta las asignaciones satisfactorias de una codificación canónica en un tiempo cuyo exponente crece más lentamente que de forma lineal con n. El manuscrito declara una cota más afinada cuando se expresa también el número de cláusulas.
La precisión de «codificación canónica» y de cada dependencia asintótica importa. En complejidad teórica, una diferencia pequeña en el modelo de máquina, el tamaño de entrada o la uniformidad del algoritmo puede cambiar el significado de una conclusión. Por eso el resultado no debe resumirse únicamente como «la inteligencia artificial ha hecho fácil SAT».
Quién va a revisar el resultado
OpenAI ha formado un grupo encabezado por Russell Impagliazzo y Ramamohan Paturi, de la Universidad de California en San Diego, y Ryan Williams, del MIT. Los dos primeros están directamente vinculados a la formulación original de ETH; Williams ha trabajado durante años en algoritmos y límites inferiores relacionados.
La empresa afirma que publicará los datos en bruto solicitados por el grupo y financiará una conferencia para estudiar las consecuencias. Los participantes son independientes, no están sujetos a acuerdos de confidencialidad y no hablan en nombre de OpenAI. Esa estructura busca evitar que la propia compañía sea la única intérprete de una prueba producida por sus modelos.
La existencia de especialistas no debe presentarse como aprobación previa. Su tarea es verificar, explicar y situar el trabajo. Hasta que existan análisis públicos, réplicas y una exposición que otros investigadores puedan seguir, lo correcto es hablar de una refutación anunciada y formalizada, no de una conclusión aceptada universalmente.
Qué aporta Lean y qué no puede decidir por sí solo
Lean es un asistente de demostración. Convierte definiciones, teoremas y pasos lógicos en objetos que un núcleo pequeño comprueba según reglas formales. La documentación oficial sobre validación de pruebas explica que una prueba exportada puede reproducirse con el núcleo de Lean y con verificadores externos.
Si el archivo compila sin axiomas indebidos y la declaración formal representa correctamente el teorema deseado, el sistema ofrece una garantía muy fuerte de que los pasos lógicos encajan. Evita errores humanos típicos como omitir un caso, aplicar mal una regla o depender de una intuición no demostrada.
Pero Lean comprueba lo que se ha escrito, no lo que el autor pretendía escribir. Los revisores deben confirmar que las definiciones de máquina, tiempo, entrada y satisfacibilidad corresponden al concepto estándar de ETH. También deben comprobar que no haya una traducción demasiado débil, un supuesto escondido o una diferencia entre la cota del manuscrito y la que realmente cubre el código.
La formalización tampoco explica por sí sola por qué funciona el método, qué ideas son reutilizables o qué resultados previos dependen de la hipótesis. Convertir una prueba formal en conocimiento científico requiere una exposición comprensible, comparaciones con la literatura y evaluación comunitaria.
Por qué refutar ETH no resuelve P frente a NP
ETH y P frente a NP están relacionadas, pero no son la misma pregunta. La descripción oficial del Clay Mathematics Institute resume P frente a NP así: si una solución puede comprobarse rápidamente, ¿también puede encontrarse rápidamente? Un algoritmo subexponencial puede ser mucho mejor que explorar todas las combinaciones y seguir siendo demasiado lento para pertenecer a P.
Por ejemplo, una función con un exponente como n dividido por la raíz de log n crece más lentamente que c elevado a n para una constante c mayor que uno, pero sigue creciendo mucho más deprisa que un polinomio. La refutación de ETH abriría espacio entre «exponencial» y «polinómico» sin cerrar el problema P frente a NP.
Tampoco implica que un ordenador doméstico pueda resolver de inmediato cualquier fórmula grande. Las cotas asintóticas describen el comportamiento cuando la entrada crece; pueden ocultar constantes, factores polinómicos y estructuras de datos costosas. Para saber si hay utilidad práctica haría falta implementar el algoritmo, medir memoria y tiempo y compararlo con los solucionadores SAT modernos.
Qué podría cambiar en algoritmos y seguridad
El impacto más inmediato sería teórico. Cientos de resultados usan ETH o su versión fuerte para demostrar que, bajo ese supuesto, no existe cierto algoritmo eficiente. Si ETH es falsa, algunas barreras condicionadas tendrían que revisarse. Eso no proporciona automáticamente el algoritmo que cada aplicación necesita.
La satisfacibilidad aparece en planificación, verificación de software, diseño de circuitos, optimización y análisis combinatorio. Una técnica realmente general podría inspirar algoritmos más rápidos o nuevas descomposiciones. Sin embargo, transformar una demostración asintótica en código competitivo puede requerir años y quizá no sea viable para los tamaños habituales.
No debe confundirse con una ruptura automática de la criptografía. La seguridad de un sistema concreto depende de problemas, parámetros y modelos de ataque específicos. Nuestro análisis sobre Magnetar y las pruebas criptográficas de programas muestra otra distinción: demostrar que un cálculo se ejecutó correctamente no equivale a acelerar todos los problemas computacionales.
El precedente reciente de la conjetura KLS resuelta con ayuda de inteligencia artificial permite comparar procesos. Una afirmación matemática gana solidez cuando existen una formulación precisa, una prueba revisable, especialistas independientes y tiempo para detectar errores o consecuencias no previstas.
Cómo debería verificarse una afirmación de este tamaño
- Reproducir la compilación. Fijar versiones de Lean, dependencias, archivos y opciones, y comprobar que el teorema se construye desde cero.
- Auditar los axiomas. Identificar todas las hipótesis utilizadas y descartar atajos que debiliten la conclusión.
- Comparar definiciones. Verificar que k-SAT, codificación, tamaño y modelo de cómputo coinciden con la literatura de ETH.
- Traducir la idea. Producir una explicación humana que permita a especialistas seguir el argumento sin depender únicamente del archivo formal.
- Buscar contraejemplos. Examinar casos pequeños y límites donde una reducción o una estimación podría fallar.
- Implementar el algoritmo. Separar la existencia asintótica de su rendimiento real en memoria y tiempo.
- Revisar consecuencias. Catalogar qué resultados eran condicionales a ETH y cuáles mantienen otras barreras.
Este protocolo también ofrece una lección práctica para el uso cotidiano de modelos. Quien aprende a organizar una producción con el Taller IA Content o a estructurar un proyecto con IA Autor trabaja en un contexto de riesgo mucho menor, pero necesita la misma separación básica: propuesta generada, revisión humana y resultado comprobado. Son recursos comerciales independientes y no guardan relación con la investigación de OpenAI.
Hechos, inferencias y previsiones
Hechos confirmados: OpenAI publicó el 26 de octubre de 2026 una afirmación de refutación de ETH, un manuscrito y archivos de Lean. El resumen formal declara un algoritmo subexponencial para contar soluciones de k-CNF bajo una codificación especificada. Un grupo de expertos independientes ha aceptado organizar la revisión y explicación.
Inferencia razonable: la formalización reduce de forma importante el riesgo de un fallo lógico local, pero el principal trabajo pendiente está en comprobar que la declaración formal corresponde exactamente a la hipótesis conocida y en entender el método. Que los autores originales de ETH participen en el proceso aumenta la calidad potencial de la revisión, no sustituye sus conclusiones futuras.
Previsión: si el resultado se sostiene, aparecerán estudios que revisen barreras condicionales y busquen versiones implementables del algoritmo. También es probable que se consoliden nuevos protocolos para publicar descubrimientos generados por inteligencia artificial: artefactos formales, datos abiertos, grupos independientes y reconocimiento separado para quienes producen comprensión y exposición.
Preguntas frecuentes
¿OpenAI ha demostrado que P es igual a NP?
No. El resultado anunciado ofrece un algoritmo subexponencial para k-SAT, no un algoritmo polinómico. P frente a NP continúa siendo una pregunta distinta.
¿Lean demuestra que el anuncio es indiscutible?
Lean comprueba la validez formal de una declaración bajo definiciones y axiomas concretos. Los especialistas aún deben validar que esa declaración representa correctamente ETH y explicar la prueba.
¿Los ordenadores serán ahora mucho más rápidos?
No de forma inmediata. Una mejora asintótica puede ser impracticable por constantes, memoria o complejidad de implementación. Todavía no se han publicado comparaciones prácticas con solucionadores SAT.
¿Puede afectar a la criptografía?
No existe una consecuencia automática. Cada sistema criptográfico depende de supuestos concretos; sería necesario demostrar una reducción y un algoritmo aplicable a sus parámetros reales.
Una prueba formal abre el debate, no lo cierra
La afirmación de OpenAI merece atención porque combina tres elementos poco habituales: un resultado que contradice una conjetura central, una formalización pública y un proceso de revisión encabezado por especialistas directamente vinculados al problema. Es una base más sólida que una demostración cerrada o una nota publicitaria sin artefactos.
Al mismo tiempo, la prudencia forma parte del método científico. Hoy puede afirmarse que existe un manuscrito y que Lean verifica una declaración concreta. Todavía no puede afirmarse que todas sus interpretaciones hayan sido aceptadas, que P frente a NP esté resuelto o que haya un algoritmo práctico listo para usarse. Si la revisión confirma el alcance, el cambio será profundo; hasta entonces, la noticia correcta es que una gran afirmación acaba de entrar en un proceso público de comprobación.
Fuentes primarias y oficiales consultadas el 28 de octubre de 2026. Las explicaciones y previsiones editoriales están identificadas como tales.