OpenAI Diz Que a Hipótese do Tempo Exponencial É Falsa: O Que Muda em 2026

Olá HaWkers, no dia 26 de outubro de 2026 a OpenAI publicou no repositório público openai/math um preprint com um título que parece provocação: "The Exponential Time Hypothesis is False". O documento é datado de 25 de outubro, vem assinado apenas como "OpenAI" e chega acompanhado de uma formalização em Lean. Junto com ele, a empresa anunciou mais dois resultados, um em análise matemática ligado à conjectura de Kakeya e outro em física teórica, sobre a existência de teorias quânticas de campos em quatro dimensões.

A Hipótese do Tempo Exponencial, conhecida pela sigla ETH, é uma das suposições que sustentam boa parte da teoria de algoritmos moderna. Se ela cair, dezenas de resultados que dizem "este problema não pode ser resolvido mais rápido do que X, assumindo a ETH" perdem a base.

Mas o que exatamente foi afirmado? Isso quebra criptografia? Resolve P versus NP? E por que tanta gente séria está tratando o anúncio com cautela? Neste artigo você vai entender a ETH do zero, ver em código por que SAT é tão difícil, comparar as curvas de crescimento envolvidas e separar o que já foi checado do que ainda é só alegação.

O Que É a Hipótese do Tempo Exponencial

Para entender a ETH, comece pelo problema SAT. Você recebe uma fórmula lógica com variáveis booleanas e precisa responder: existe alguma atribuição de verdadeiro e falso que torne a fórmula inteira verdadeira?

A versão mais estudada é o 3-SAT, em que a fórmula é uma conjunção de cláusulas e cada cláusula tem no máximo três literais. Algo como:

(x1 OU NÃO x2 OU x3) E (NÃO x1 OU x2) E (x2 OU NÃO x3 OU x4)

O 3-SAT é NP-completo. Isso significa que, se alguém encontrasse um algoritmo polinomial para ele, teria provado P = NP. Quase ninguém acredita nisso, mas "não ser polinomial" ainda deixa muito espaço. Um algoritmo que roda em 2^(n^0.5) passos não é polinomial, mas é absurdamente mais rápido que 2^n.

Foi aí que Russell Impagliazzo e Ramamohan Paturi entraram, no fim dos anos 1990. Eles formularam a Hipótese do Tempo Exponencial, que diz, de forma simplificada:

Existe uma constante c > 0 tal que nenhum algoritmo resolve 3-SAT com n variáveis em tempo 2^(c·n) ou menos.

Em outras palavras, a ETH aposta que o 3-SAT exige tempo genuinamente exponencial no número de variáveis. Não é só "não polinomial": é exponencial de verdade, sem atalho subexponencial.

Por que a ETH importa tanto

A ETH virou uma ferramenta de trabalho. Pesquisadores de algoritmos usam reduções para dizer coisas como "se você resolver o problema Y em tempo 2^o(n), você também resolve 3-SAT nesse tempo, contrariando a ETH". Assim, a ETH serve de base para limites inferiores condicionais em grafos, otimização, algoritmos parametrizados e muito mais.

Existe também uma versão mais forte, a SETH (Strong Exponential Time Hypothesis), que afirma que para k-SAT com k grande o expoente se aproxima de 2^n. Muitos limites inferiores de "complexidade fina" dependem da SETH. Como a SETH implica a ETH, se a ETH for falsa, a SETH também cai.

O Que a OpenAI Afirma Ter Provado

Segundo o anúncio e as primeiras análises do preprint, o resultado central é um algoritmo determinístico que conta exatamente quantas atribuições satisfazem uma fórmula k-CNF com largura de cláusula fixa, rodando em tempo subexponencial e espaço polinomial.

Três detalhes chamam atenção:

É contagem, não só decisão. Contar quantas soluções existem (o problema #SAT) costuma ser mais difícil do que só responder se existe alguma. Um algoritmo de contagem rápido resolve a decisão de brinde.
É determinístico. Não depende de sorte nem de aleatoriedade.
Usa espaço polinomial. Não troca tempo por uma montanha de memória.

Como 3-SAT é um caso particular, um algoritmo assim refutaria a ETH. A própria OpenAI escreveu: "Surprisingly, our system has recently proved that the ETH is false".

Qual é o tempo de execução

Aqui as fontes ainda divergem nos detalhes. Comentários na discussão do Hacker News e análises publicadas descrevem o limite como algo da ordem de 2^(n/√log n), com fatores extras envolvendo log log n no expoente. Para o nosso raciocínio, o que importa é a forma geral: o expoente cresce como n dividido por algo que também cresce. Isso é menor que qualquer 2^(c·n) para n suficientemente grande, que é exatamente o que a ETH diz ser impossível.

Ao mesmo tempo, o algoritmo continua sendo superpolinomial. Ele não prova P = NP. A ETH é uma suposição mais forte que P ≠ NP, então derrubá-la deixa a pergunta do milênio exatamente onde estava.

Na Prática: Por Que SAT Explode

Antes de olhar para curvas, vale sentir o problema com código. O jeito ingênuo de contar soluções de uma fórmula é testar todas as 2^n atribuições:

// Uma fórmula CNF é uma lista de cláusulas.
// Cada cláusula é uma lista de literais: 3 significa x3, -3 significa NÃO x3.
const formula = [
  [1, -2, 3],
  [-1, 2],
  [2, -3, 4],
];

// Conta quantas atribuições satisfazem a fórmula testando todas elas.
function contarSolucoes(clausulas, n) {
  let total = 0;
  // Cada número de 0 a 2^n - 1 representa uma atribuição diferente.
  for (let mask = 0; mask < 1 << n; mask++) {
    const valor = (v) => ((mask >> (v - 1)) & 1) === 1;
    const satisfaz = clausulas.every((clausula) =>
      clausula.some((lit) => (lit > 0 ? valor(lit) : !valor(-lit)))
    );
    if (satisfaz) total++;
  }
  return total;
}

console.log(contarSolucoes(formula, 4)); // número de soluções com 4 variáveis

Com 4 variáveis, são 16 testes. Com 40, já passam de um trilhão. Com 100, o número de atribuições tem 31 dígitos. Esse é o muro que todo algoritmo de SAT tenta contornar.

Os algoritmos que já existiam

Ninguém resolve SAT na força bruta. Solvers reais usam variações do DPLL e do CDCL, que propagam consequências lógicas e podam ramos inteiros da busca. Uma versão mínima de DPLL fica assim:

// Simplifica as cláusulas assumindo que o literal `lit` é verdadeiro.
function atribuir(clausulas, lit) {
  return clausulas
    .filter((c) => !c.includes(lit)) // cláusula satisfeita some
    .map((c) => c.filter((l) => l !== -lit)); // literal falso é removido
}

// DPLL: decide se a fórmula tem solução.
function dpll(clausulas) {
  if (clausulas.length === 0) return true; // tudo satisfeito
  if (clausulas.some((c) => c.length === 0)) return false; // conflito

  // Propagação unitária: cláusula com um literal só força o valor dele.
  const unitaria = clausulas.find((c) => c.length === 1);
  if (unitaria) return dpll(atribuir(clausulas, unitaria[0]));

  // Ramificação: escolhe um literal e tenta os dois valores.
  const lit = clausulas[0][0];
  return dpll(atribuir(clausulas, lit)) || dpll(atribuir(clausulas, -lit));
}

console.log(dpll([[1, -2, 3], [-1, 2], [2, -3, 4]])); // true

Na prática, solvers CDCL resolvem instâncias industriais com milhões de variáveis. Mas, no pior caso teórico, todos os algoritmos conhecidos para 3-SAT continuavam exponenciais. O melhor limite clássico vinha da família de algoritmos PPSZ (Paturi, Pudlák, Saks e Zane), que roda em algo próximo de 1,307^n. Ainda é 2^(c·n), com c em torno de 0,386. Rápido para um algoritmo exponencial, mas exponencial.

Comparando as Curvas de Crescimento

A melhor forma de enxergar a diferença entre "exponencial" e "subexponencial" é colocar os números lado a lado. O código abaixo compara os expoentes (em base 2) da força bruta, do PPSZ e de um limite no formato n/√log n, ignorando as constantes escondidas na notação O:

// Expoente em base 2 de cada limite, para comparar sem estourar o Number.
const limites = {
  forcaBruta: (n) => n, // 2^n
  ppsz: (n) => n * Math.log2(1.307), // aproximadamente 1,307^n
  subexponencial: (n) => n / Math.sqrt(Math.log2(n)), // 2^(n / √log n)
};

for (const n of [16, 64, 256, 1024, 65536, 1e9]) {
  const linha = Object.entries(limites)
    .map(([nome, f]) => `${nome}: 2^${f(n).toFixed(1)}`)
    .join(" | ");
  console.log(`n=${n} -> ${linha}`);
}

Rodando, você percebe duas coisas. Primeiro, para n pequeno, o PPSZ ganha, porque √log n cresce devagar demais. Segundo, para n grande, a razão entre o expoente subexponencial e n vai para zero, enquanto a do PPSZ fica parada em 0,386. É essa diferença assintótica que derruba a ETH.

O que significa "galáctico"

Na discussão do Hacker News, um especialista em SAT resumiu: o resultado não tem aplicação imediata, os algoritmos são "galácticos". Esse é um termo técnico informal para algoritmos que são assintoticamente melhores, mas só ganham dos métodos existentes em tamanhos de entrada que nunca vão aparecer no mundo real.

Dá para ilustrar isso calculando quando a curva nova passa a ganhar do PPSZ. Com os fatores de log log n que aparecem no limite real, esse ponto de virada fica muito mais longe do que no exemplo simplificado:

// Procura o menor k tal que, para n = 2^k, o limite com fator (log log n)^2
// no expoente fica abaixo do PPSZ. Trabalhamos com k = log2(n) para não
// estourar o Number do JavaScript. Ilustrativo: constantes ignoradas.
function pontoDeVirada() {
  const razaoPpsz = Math.log2(1.307); // expoente do PPSZ dividido por n
  // Expoente do limite novo dividido por n, em função de k = log2(n).
  const razaoNova = (k) => Math.log2(k) ** 2 / Math.sqrt(k);
  for (let k = 4; k <= 1e8; k *= 1.01) {
    if (razaoNova(k) < razaoPpsz) return `n ≈ 2^${Math.round(k).toLocaleString("pt-BR")}`;
  }
  return "acima de 2^100000000";
}

console.log(pontoDeVirada());

Mesmo nessa versão sem constantes, o ponto de virada fica perto de n = 2 elevado a cerca de um milhão: um número de variáveis com centenas de milhares de dígitos, muito além de qualquer fórmula que um computador vá processar. Por isso a importância do resultado é teórica: ele muda o mapa do que é possível, não o desempenho do seu solver.

E a Criptografia? Seus Dados Estão Seguros?

Essa foi a primeira pergunta de muita gente, e faz sentido: se um problema NP-completo ficou "mais fácil", será que a criptografia não vai junto?

Ryan Williams, um dos pesquisadores convidados para examinar o resultado, respondeu diretamente em uma declaração reproduzida na discussão do Hacker News: "In fact, one of the first things I wanted OpenAI to check is that no existing cryptosystems are compromised by the result." E completou que, aparentemente, eles estão seguros.

Há bons motivos para isso:

Ganho subexponencial pequeno não quebra chaves. Esquemas como RSA, curvas elípticas e os algoritmos pós-quânticos já são dimensionados contra ataques subexponenciais conhecidos. O ataque clássico mais forte contra RSA, o General Number Field Sieve, já é subexponencial há décadas.
Reduções não preservam o ganho. O próprio preprint observa que limites de tempo do tipo 2^o(n) não se transferem sob reduções polinomiais gerais. Converter um problema criptográfico em SAT costuma inflar muito o número de variáveis, e o ganho evapora.
O algoritmo é galáctico. Mesmo que houvesse uma redução eficiente, o ponto de virada fica longe demais para ter efeito prático.

Os Outros Dois Resultados: Kakeya e Yang–Mills

O anúncio de 26 de outubro não era só sobre ETH. A OpenAI apresentou três resultados de uma vez.

Matemática: suavização local e Kakeya

A empresa afirma que seus modelos produziram uma prova da conjectura de suavização local (local smoothing) de Sogge para a equação da onda euclidiana, em toda dimensão espacial a partir de 2. Segundo a OpenAI, isso implicaria as conjecturas de Kakeya (maximal e de dimensão) e as estimativas de restrição esférica de Stein, "throughout the interior of the conjectured range".

Para dar contexto: em 2025, Hong Wang e Joshua Zahl publicaram a prova da conjectura de Kakeya em três dimensões, considerada um dos grandes resultados da análise na década. Uma prova que cobrisse todas as dimensões seria um salto enorme. Vale notar uma tensão nas próprias palavras da OpenAI: o resumo fala em "todas as dimensões", enquanto o texto técnico restringe ao interior da faixa conjecturada. Nesses casos, quem manda é o artigo técnico.

Física: existência de teorias quânticas de campos

O terceiro resultado é o mais ambicioso. A OpenAI diz que seus modelos produziram uma prova em linguagem natural da existência de Yang–Mills em 9 de setembro de 2026 e da cromodinâmica quântica (QCD) em 18 de setembro de 2026, além de uma extensão para algo que a empresa chama de completamento unificado do Modelo Padrão.

O grupo de especialistas que acompanha esse trabalho é liderado por David Gross, Nobel de Física de 2004 pelo trabalho sobre a força forte, e inclui Michael Douglas, Arthur Jaffe, Igor Klebanov e Nikita Nekrasov. Os materiais completos ainda não foram liberados: segundo a cobertura, o grupo preferiu escrever a própria interpretação antes de publicar.

Um ponto importante para não cair em manchete: o Problema do Prêmio do Milênio do Clay Institute sobre Yang–Mills exige provar a existência e a lacuna de massa (mass gap). A alegação da OpenAI fala em existência; ela não reivindica o prêmio.

O Que Já Foi Verificado e o Que Ainda Não Foi

Esta é a parte que mais importa, e a que as manchetes costumam pular. Até 27 de outubro de 2026, nenhum dos três resultados tem confirmação independente.

O processo montado pela OpenAI funciona com "shepherds": especialistas externos que organizam grupos para entender, checar e explicar cada resultado. No caso da ETH, o grupo é formado por Russell Impagliazzo, Ramamohan Paturi e Ryan Williams. A ironia é evidente: Impagliazzo e Paturi são justamente os autores da hipótese que o preprint diz refutar. Em carta aberta, eles deixaram claro que a participação deles não deve ser lida como certificação do resultado. Foi a pedido do grupo que a OpenAI tornou os materiais públicos.

O papel do Lean

A formalização em Lean é o ponto mais forte da alegação de ETH. Lean é um assistente de provas: se a prova compila, cada passo lógico foi checado por máquina. Mas há uma armadilha conhecida, e vale entender como desenvolvedor:

-- Esboço ilustrativo, NÃO é o enunciado da OpenAI.
-- O Lean garante que a prova está correta em relação ao enunciado formal.
-- Ele não garante que o enunciado formal diz o que o artigo diz em português.
theorem algoritmo_subexponencial :
    ∃ alg : Algoritmo, ResolveKSAT alg ∧ TempoSubexponencial alg := by
  sorry -- a prova real ficaria aqui

Se a definição de TempoSubexponencial ou de ResolveKSAT estiver sutilmente errada, a prova compila e mesmo assim não prova o que se queria. Por isso revisores humanos ainda precisam conferir se o enunciado formalizado bate com a afirmação informal. Na física, não há formalização citada, e os materiais nem estão públicos.

O Que Isso Muda Para Quem Desenvolve Software

Na prática, no curto prazo, nada muda no seu código. Seu solver SAT, seu compilador e seu banco de dados vão continuar rodando os mesmos algoritmos amanhã. Mas há três lições que valem para o dia a dia.

1. Limites inferiores condicionais são suposições, não leis. Muita gente lê "este problema não tem algoritmo melhor que X" sem perceber o "assumindo a ETH" no rodapé. Se você trabalha com otimização, agendamento ou verificação, vale saber em quais hipóteses o seu "impossível" se apoia.

2. Verificação formal ganhou um caso de uso enorme. Se IAs vão produzir provas longas demais para humanos lerem linha por linha, ferramentas como Lean viram o filtro de confiança. Para devs, é um sinal de que assistentes de prova e tipos dependentes podem sair do nicho acadêmico. Se o tema te interessa, vale também olhar como a computação quântica está mexendo com outras suposições clássicas no post sobre o avanço dos qubits criptografados em 2026.

3. Desconfie de manchete, confie em processo. O anúncio foi feito por uma empresa sobre o próprio produto, e os revisores foram convidados por ela. Isso não invalida nada, mas é exatamente o motivo pelo qual a revisão independente importa. O jeito certo de acompanhar é esperar o relatório do grupo de Impagliazzo, Paturi e Williams.

Perspectivas: IA Como Coautora da Ciência

Se a refutação da ETH se sustentar, 2026 vai ficar marcado como o ano em que uma IA derrubou uma das hipóteses centrais da teoria da computação, um problema em aberto desde o fim dos anos 1990. E, se cair, o processo de revisão aberto que está acontecendo agora vai ter mostrado o valor de checar antes de comemorar.

Seja qual for o desfecho, algumas coisas já mudaram. A conversa saiu de "IA consegue resolver exercício de olimpíada?" para "quem revisa uma prova que nenhum humano escreveu?". A comunidade de complexidade vai precisar reconstruir parte do mapa de limites inferiores se o resultado for confirmado. E ferramentas de verificação formal ganharam um protagonismo que poucos previam há dois anos.

Para quem gosta de algoritmos, é um ótimo momento para revisitar fundamentos: entender SAT, reduções e notação assintótica nunca foi tão útil para ler as notícias de tecnologia. E, se você curte a ideia de algoritmos que exploram espaços de busca enormes, o post sobre algoritmos genéticos mostra outra forma de atacar problemas difíceis.

Bora pra cima! 🦅

📚 Quer Acompanhar o Que Vem Por Aí?

Este artigo cobriu a alegação da OpenAI de que a Hipótese do Tempo Exponencial é falsa, mas o ecossistema muda toda semana e nem tudo vira artigo aqui.

No X eu compartilho o que estou testando, os bastidores dos projetos e as novidades que aparecem antes de virarem post.

Me Segue Lá

👉 Seguir @jeffbruchado no X

💡 Conteúdo diário sobre desenvolvimento, carreira e as ferramentas que eu realmente uso