A ETH é uma conjectura sobre a dificuldade inerente dos problemas de satisfatibilidade: em termos gerais, propõe que k-SAT (para k ≥ 3) não pode ser resolvido em tempo 2o(n), sendo n o número de variáveis — ou seja, que não existe um algoritmo que resolva todas as instâncias em tempo subexponencial em n. Na prática, a ETH serve de referência para a dificuldade computacional: muitos limites inferiores condicionais para problemas de grafos, consultas a bases de dados e reduções em biologia computacional partem da ETH para sustentar que seria surpreendente melhorar certos tempos de execução. Quando os investigadores dizem que um problema é difícil segundo a ETH, querem dizer que qualquer melhoria significativa implicaria avanços que desafiam esta referência.

A afirmação da OpenAI diz respeito a SAT de largura fixa: instâncias SAT sujeitas a restrições na estrutura das cláusulas ou nas interações entre variáveis. Se alguém construir um algoritmo que resolva todas as instâncias de SAT de largura fixa em tempo 2o(n) (subexponencial em n), isso contradiz a afirmação geral da ETH sobre limites inferiores exponenciais para famílias de k-SAT. Essa refutação invalidaria muitos resultados condicionais de dificuldade computacional que assumem explicitamente a ETH. É fundamental perceber que refutar a ETH não é o mesmo que provar P = NP: a ETH é uma conjectura mais forte e específica sobre a dependência exponencial exata dos tempos de execução. P = NP eliminaria a diferença entre o tempo polinomial e o tempo polinomial não determinístico; um algoritmo subexponencial para uma família específica de SAT demonstra uma complexidade assintótica mais favorável para essa família, sem afirmar que todos os problemas NP têm soluções em tempo polinomial.

Formalizar uma prova em Lean é um passo importante: obriga a usar definições precisas, elimina muitas lacunas informais e cria um artefacto verificável por máquina, capaz de prevenir algumas formas de erro humano. A equipa da OpenAI afirma que a formalização em Lean foi concluída nas 24 horas seguintes à refutação em linguagem natural. Ainda assim, a verificação formal trata da correção sintática relativamente aos axiomas e às definições formais; não substitui a interpretação da comunidade sobre as hipóteses do modelo, as constantes ocultas na análise assintótica, os regimes dos parâmetros ou se o algoritmo é amplamente aplicável ou se foi concebido para famílias patológicas de instâncias.

A OpenAI convidou um grupo de análise liderado por Russell Impagliazzo e Ramamohan Paturi — dois dos proponentes originais da ETH — e por Ryan Williams, do MIT. Este trio reúne o contexto histórico e a autoridade técnica adequados: Impagliazzo e Paturi podem determinar se a refutação proposta contradiz efetivamente a formulação original da ETH, enquanto Williams pode avaliar as implicações para os limites inferiores algorítmicos e outros resultados condicionais relacionados. A sua orientação deverá ajudar a garantir uma avaliação transparente e conduzida por especialistas, além de dar um exemplo construtivo de colaboração entre empresas de IA e meios académicos.

Este episódio ilustra um novo fluxo de trabalho de investigação: os modelos generativos podem propor conjecturas e até produzir provas verificáveis por máquina, encurtando o caminho entre uma ideia e um artefacto formal. Para as partes interessadas — equipas de investigação, financiadores e responsáveis de produto —, a consequência imediata para as políticas é investir em infraestruturas de verificação, repositórios abertos de artefactos e auditorias comunitárias financiadas. Os riscos mantêm-se: os modelos podem alucinar lemas incorretos que ainda assim passam na verificação de tipos, aplicar definições indevidamente ou explorar hipóteses demasiado restritas sobre as instâncias. A resposta adequada não é nem o entusiasmo irrefletido nem a rejeição automática, mas sim uma validação estruturada e transparente, liderada por especialistas na área.