Em 26 de outubro de 2026, a OpenAI anunciou que um sistema interno produziu um resultado que, segundo a empresa, refutaria a Exponential Time Hypothesis (ETH), uma conjectura sobre a complexidade, no pior caso, de problemas de satisfatibilidade booleana. A empresa diz que o resultado em linguagem natural foi encontrado em 16 de outubro e formalizado em Lean no dia 17. A afirmação ainda estava sob análise externa: a OpenAI anunciou um grupo de pesquisadores para examinar o trabalho.
O que a documentação do Lean formaliza
A documentação oficial do escopo em Lean descreve um algoritmo determinístico que conta exatamente as atribuições satisfatórias de fórmulas k-CNF codificadas de forma canônica, para k fixo e k ≥ 2. Em uma fórmula desse tipo, cada cláusula combina até k variáveis ou suas negações. O limite de tempo formalizado é (L+1)^{O_k(1)} 2^{O_k(n(log log n)^2/√log n)}, em que L é o comprimento da codificação em bits e n é o número de variáveis. A documentação também limita a (L+1)^{O_k(1)} o total de células de fita visitadas.
Lean é um assistente de provas, um programa que permite formalizar enunciados matemáticos e verificar se uma demonstração segue suas regras. O escopo descrito na documentação se refere à contagem exata de soluções para essa classe de fórmulas; a alegação da OpenAI é que o resultado também refuta a ETH.
O limite atribuído ao manuscrito é diferente
A página de escopo atribui ao manuscrito de 25 de outubro um limite de tempo mais forte: (n+m)^{O_k(1)} 2^{O_k(n log log n/√log n)}, em que m é o número de cláusulas. Para fórmulas com m ≤ Dn, com D > 0 fixo, ela atribui ao manuscrito ainda o limite (n+m)^{O_{k,D}(1)} 2^{O_{k,D}(n/√log n)}.
São expressões distintas da cota que a documentação apresenta para o teorema formalizado em Lean. A diferença importa porque a demonstração formal e as cotas de tempo atribuídas ao manuscrito não devem ser tratadas como se fossem o mesmo enunciado.
O que a afirmação significa na prática
O anúncio da OpenAI não apresenta uma solução para P versus NP. A empresa afirma que transformar avanços teóricos em melhorias práticas exigirá pesquisa significativa; uma cota assintótica, por si só, não informa que computadores ou programas de SAT já ficaram mais rápidos.
Em 28 de outubro de 2026, a ExplainX informou que nenhuma confirmação independente havia sido relatada até aquela data. A OpenAI anunciou que Russell Impagliazzo, Ramamohan Paturi e Ryan Williams liderariam um grupo externo para examinar e explicar o resultado.
O vídeo de Adem B10, em inglês, apresenta ETH e discute a diferença entre limites teóricos e desempenho prático. A explicação usa um quebra-cabeça de interruptores como ilustração simplificada, não como descrição do algoritmo da OpenAI.
