31 de octubre de 2026 | Investigación y computación. La inteligencia artificial ha entrado de lleno en uno de los debates más delicados de la informática teórica. OpenAI y Anthropic han publicado, con pocos días de diferencia, resultados generados con ayuda de sistemas de IA que afirman refutar la Hipótesis del Tiempo Exponencial (ETH). Ambos equipos ofrecen textos técnicos y formalizaciones en Lean para que especialistas independientes puedan analizar el trabajo. La existencia de esos materiales es verificable; la aceptación científica definitiva de las conclusiones sigue siendo otra cuestión.

Qué se ha anunciado y cuándo

OpenAI explica en su comunicado del 26 de octubre que sus modelos obtuvieron una refutación en lenguaje natural el 16 de octubre y la formalizaron en Lean el 17. Su manuscrito, fechado el 17 y revisado el 25, aparece en el repositorio público de investigación. Anthropic ha publicado también un trabajo independiente titulado A 2^{o(n)} Time Algorithm for 3-SAT con código Lean 4. Que dos organizaciones presenten resultados coincidentes no equivale automáticamente a que se hayan validado mutuamente.

¿Qué es la Hipótesis del Tiempo Exponencial?

La ETH es una conjetura de complejidad computacional formulada a comienzos de este siglo. Simplificando, sostiene que para resolver en el peor caso 3-SAT, un problema fundamental de lógica booleana, no existe un algoritmo cuya duración sea subexponencial respecto al número de variables. SAT pregunta si es posible asignar valores verdadero o falso a variables de forma que todas las condiciones de una fórmula resulten satisfechas.

Imaginemos un sistema de decisiones binarias con restricciones. La exploración exhaustiva de n decisiones tiene 2 elevado a n combinaciones; algoritmos mejores pueden evitar muchos intentos, pero ETH sostiene que no se puede atravesar cierta barrera asintótica en 3-SAT. Es una hipótesis, no un teorema demostrado, aunque se utiliza para demostrar resultados condicionales sobre otros problemas.

Qué afirma exactamente OpenAI

El manuscrito presenta un algoritmo determinista para contar exactamente las asignaciones satisfactorias de fórmulas k-CNF, para un número fijo de literales por cláusula. La cota asintótica anunciada tiene la forma de un factor polinómico multiplicado por 2 elevado a n dividido por una potencia creciente del logaritmo de n. Esto es subexponencial en n. Contar soluciones es, en principio, una tarea más informativa que comprobar si existe al menos una: si el recuento es mayor que cero, la fórmula es satisfacible.

Su resultado, si resiste la validación, contradice ETH porque produciría un procedimiento determinista de tiempo 2^{o(n)} para 3-SAT. El equipo también discute consecuencias condicionales para otras conjeturas relacionadas y determinados problemas de recuento. Esas afirmaciones deben leerse dentro de las definiciones exactas y las reducciones utilizadas.

Qué presenta Anthropic

El README público de Anthropic describe igualmente un algoritmo determinista subexponencial para 3-SAT y una solución para el problema más exigente de contar satisfacibilidad (#3-SAT). Da una cota de tiempo aproximada de 2 elevado a O(n log log n / raíz de log n). El propio material advierte expresamente que el resultado es puramente asintótico y no supone que estas fórmulas puedan resolverse de manera útil en instancias prácticas actuales.

¿Por qué importa que las pruebas estén en Lean?

Lean es un asistente de demostración que comprueba si los pasos formalizados se siguen de axiomas y definiciones aceptados. Reduce la posibilidad de errores lógicos omitidos en una explicación informal. Sin embargo, la revisión humana debe comprobar que el teorema formalizado corresponde realmente a la afirmación del artículo, que no se han introducido supuestos inadecuados y que las formalizaciones reproducen todas las partes relevantes del argumento. OpenAI publica un documento sobre el alcance concreto de su prueba formal, una referencia crucial para distinguir la versión Lean de las cotas más precisas descritas en el manuscrito.

Qué NO se ha demostrado

  • No equivale a P = NP: subexponencial no significa polinómico.
  • No significa que todos los problemas NP tengan ahora algoritmos subexponenciales: las reducciones polinómicas pueden aumentar el tamaño de la entrada.
  • No significa que un ordenador actual pueda resolver inmediatamente las instancias difíciles: una mejora asintótica puede seguir siendo demasiado costosa.
  • No demuestra que las contraseñas o la criptografía estén rotas: los sistemas criptográficos utilizan problemas y supuestos específicos; cualquier consecuencia debe analizarse por separado.
  • No implica que la comunidad haya certificado ya las pruebas: es necesario reproducir y examinar los resultados.

La revisión científica importa más que el titular

OpenAI señala que especialistas de la comunidad de complejidad, entre ellos Russell Impagliazzo, Ramamohan Paturi y Ryan Williams, participan en la organización de una evaluación abierta. El anuncio de esa revisión no supone la aprobación del teorema. En investigación matemática conviene diferenciar el manuscrito publicado, una comprobación formal de un enunciado preciso y un consenso independiente tras examinar todas las hipótesis.

¿Qué supondría para la investigación?

Si se valida el resultado, habría que revisar una larga cadena de consecuencias construidas sobre ETH y estudiar qué mejoras reales se trasladan a otros problemas combinatorios. También se abriría una conversación sobre cómo atribuir contribuciones entre investigadores y modelos, cómo revisar pruebas extensas generadas por IA, qué herramientas de formalización deben compartirse y cómo financiar la verificación externa.

Para la industria, la lección inmediata es más metodológica que comercial. Los modelos de IA pueden formular conjeturas, construir argumentos y ayudar a formalizarlos, pero los titulares extraordinarios requieren pruebas extraordinarias y evaluación externa. La automatización de la demostración no hace desaparecer el rigor científico: lo vuelve aún más importante.

Preguntas frecuentes

¿La IA ha demostrado que ETH es falsa?

Dos laboratorios afirman haber obtenido resultados que implicarían su falsedad y han publicado material técnico para comprobarlo. La validación comunitaria sigue siendo esencial.

¿Es un algoritmo nuevo o solo una redacción convincente?

Los manuscritos describen algoritmos y cotas matemáticas concretas, y existen artefactos Lean. No es una simple respuesta de un chatbot, aunque el alcance correcto de las pruebas requiere revisión.

¿Podría afectar a seguridad informática?

Las implicaciones criptográficas no se deducen automáticamente de una refutación de ETH. Hay que analizar cada esquema y supuesto de seguridad independientemente.

¿Podemos utilizar ya esos algoritmos en aplicaciones?

No se ha demostrado que sus constantes y sus costes reales resulten competitivos en tareas prácticas. Anthropic advierte que su trabajo es asintótico.

Fuentes primarias y materiales de verificación

Nota editorial: este reportaje informa de los resultados anunciados y disponibles públicamente a 31 de octubre de 2026. No presenta las demostraciones como un descubrimiento definitivamente aceptado por la comunidad científica.