La ETH es una conjetura sobre la dificultad inherente de los problemas de satisfacibilidad: en términos generales, plantea que k-SAT (para k ≥ 3) no puede resolverse en tiempo 2o(n), donde n es el número de variables; es decir, ningún algoritmo puede resolver en tiempo subexponencial en n todas las instancias. En la práctica, la ETH sirve como referencia para establecer la dureza de los problemas: muchos límites inferiores condicionales para problemas de grafos, consultas a bases de datos y reducciones de biología computacional suponen que la ETH se cumple para argumentar que sería sorprendente superar ciertos tiempos de ejecución. Cuando los investigadores dicen que un problema es difícil según la ETH, quieren decir que cualquier mejora drástica supondría avances frente a esta referencia.

La afirmación de OpenAI se refiere a SAT de ancho fijo: instancias SAT restringidas por la estructura de las cláusulas o las interacciones entre variables. Si alguien construyera un algoritmo que resolviera todas las instancias de SAT de ancho fijo en tiempo 2o(n) —subexponencial en n—, contradiría la afirmación general de la ETH sobre los límites exponenciales para las familias de k-SAT. Eso invalidaría muchos resultados condicionales de dureza que parten explícitamente de la ETH. Es fundamental entender que refutar la ETH no equivale a demostrar que P = NP: la ETH es una conjetura más fuerte y específica sobre la dependencia exponencial exacta de los tiempos de ejecución. P = NP eliminaría la brecha entre el tiempo polinómico y el tiempo polinómico no determinista; un algoritmo subexponencial para una familia concreta de SAT mostraría mejores cotas asintóticas para esa familia, pero no afirmaría que todos los problemas de NP pueden resolverse en tiempo polinómico.

Formalizar una demostración en Lean es un paso importante: obliga a definir los conceptos con precisión, subsana muchas lagunas informales y produce un artefacto verificable por máquina que ayuda a prevenir ciertas clases de errores humanos. El equipo de OpenAI informa que la formalización en Lean se completó en las 24 horas siguientes a la refutación en lenguaje natural. Aun así, la verificación formal confirma la corrección sintáctica con respecto a los axiomas y definiciones formales; no sustituye la interpretación colectiva de los supuestos del modelo, las constantes ocultas de las cotas asintóticas, los regímenes de parámetros ni la cuestión de si el algoritmo tiene una aplicación amplia o está diseñado para familias de instancias patológicas.

OpenAI invitó a un grupo de revisión dirigido por Russell Impagliazzo y Ramamohan Paturi —dos de los proponentes originales de la ETH— y Ryan Williams, del MIT. El trío combina el contexto histórico y la autoridad técnica adecuados: Impagliazzo y Paturi pueden determinar si la posible refutación contradice realmente la formulación original de la ETH, mientras que Williams puede evaluar sus implicaciones para los límites inferiores algorítmicos y otros resultados condicionales relacionados. Su labor debería facilitar una evaluación transparente del artefacto, dirigida por expertos, y destaca un modelo constructivo de colaboración entre empresas de IA y el ámbito académico.

Este episodio ilustra una nueva forma de investigar: los modelos generativos pueden proponer conjeturas e incluso producir demostraciones verificables por máquina, acortando el trayecto entre una idea y un artefacto formal. Para los grupos de investigación, los financiadores y los responsables de producto, la implicación inmediata es invertir en infraestructura de verificación, repositorios abiertos de artefactos y auditorías comunitarias con financiación. Persisten los riesgos: los modelos pueden alucinar lemas incorrectos que aun así superan la comprobación de tipos, aplicar mal las definiciones o aprovechar supuestos demasiado restrictivos sobre las instancias. La respuesta adecuada no es ni el entusiasmo ciego ni el rechazo automático, sino una validación estructurada y transparente dirigida por expertos en el campo.