IA da OpenAI e da Anthropic diz ter refutado conjectura de 1999 sobre complexidade computacional

Em 26 de outubro de 2026, a OpenAI anunciou que um modelo interno da empresa havia refutado a Hipótese do Tempo Exponencial (ETH, na sigla em inglês para Exponential Time Hypothesis), uma conjectura de 1999 sobre a qual se apoiam centenas de resultados de teoria da computação. Menos de seis horas depois, a Anthropic publicou sua própria refutação: um artigo de 49 páginas chamado "A 2^o(n) Time Algorithm for 3-SAT", assinado por "Claude". As duas empresas datam a descoberta do mesmo dia, 16 de outubro, segundo reportagem da ActuIA.

Na Anthropic, o algoritmo central foi encontrado por um modelo Claude de pesquisa interna, que produziu 14 milhões de tokens sem intervenção humana na descoberta em si, segundo relato do matemático da empresa Levent Alpöge, citado pela ActuIA a partir de uma publicação dele na rede X.

O problema que a hipótese protegia

O 3-SAT é um problema clássico de satisfatibilidade lógica: decidir se existe uma forma de atribuir verdadeiro ou falso a um conjunto de variáveis que satisfaça uma lista de restrições. Cada variável nova dobra o número de combinações possíveis, e testar tudo (força bruta) já fica impraticável perto de cem variáveis.

Em 1999, Russell Impagliazzo e Ramamohan Paturi, da Universidade da Califórnia em San Diego, formularam a ETH: nenhum algoritmo escaparia dessa explosão exponencial além de uma constante. Desde então, pesquisadores usam a ETH como régua. Quando querem provar que um problema de planejamento, grafos ou verificação jamais será resolvido rapidamente, reduzem esse problema a 3-SAT e invocam a hipótese. Mais de 800 artigos dependem da ETH ou de hipóteses correlatas, segundo o próprio artigo da Anthropic.

Se a refutação se confirmar, os limites inferiores desses 800 artigos perdem o fundamento, e problemas conhecidos como clique máxima ou cobertura por vértices passam a admitir, em teoria, algoritmos mais rápidos do que se supunha.

Duas provas, um mesmo limite, nenhuma revisão humana concluída

Os dois algoritmos chegam a limites muito próximos, da ordem de 2^(n/√log n), a menos de fatores secundários. É pouco menos que exponencial, mas a ETH proibia justamente esse "pouco menos".

Lean é uma linguagem em que cada passo de uma demonstração matemática é checado por um programa, não só lido por um humano. Isso garante que o teorema enunciado decorre logicamente dos axiomas usados. Não garante que o enunciado formalizado diga exatamente o que os autores afirmam que ele diz: essa ponte entre a matemática em prosa e o código formal ainda depende de leitura humana especializada, e é justamente o que falta aqui.

A anexação da Anthropic registra que o desenvolvimento em Lean foi escrito por modelos de IA, revisado por outras instâncias dos mesmos modelos e que, no momento da redação, nenhuma pessoa havia verificado o trabalho de ponta a ponta.

A OpenAI pediu aos próprios formuladores da conjectura, Impagliazzo e Paturi, além de Ryan Williams, do MIT, para organizar um exame aberto do resultado. Em carta pública à comunidade, os três avisam que participar do exame não equivale a certificar a prova. Em troca, obtiveram da OpenAI a publicação dos dados brutos e o financiamento de uma conferência sobre o tema. O teórico da complexidade Lance Fortnow, que diz não ter verificado a prova ele mesmo, escreveu em seu blog em 28 de outubro que já dá para considerar a hipótese como superada.

Criptografia e solvers industriais seguem intocados, por enquanto

Ryan Williams perguntou a Dan Roberts, responsável científico da OpenAI, se algum sistema criptográfico seria afetado. Segundo relato reproduzido pela ActuIA a partir da TechCrunch, a OpenAI verificou e disse estar "razoavelmente confiante" de que nenhum sistema foi quebrado. O RSA depende da fatoração de inteiros, um problema que não é conhecido por ser tão difícil quanto o 3-SAT. Ainda assim, Williams pondera que refinamentos futuros do algoritmo poderiam um dia afetar sistemas dimensionados para tamanhos de chave específicos.

Solvers de SAT usados na indústria, que verificam projetos de chips ou planejam cadeias logísticas, também não ganham nada com a mudança: eles lidam com milhões de variáveis usando heurísticas que a ETH nunca governou. O próprio artigo da Anthropic deixa isso explícito: o resultado nada diz sobre a resolução prática de fórmulas. P versus NP continua em aberto, e um tempo pouco abaixo do exponencial ainda está longe de um tempo polinomial.

Não foi o único anúncio do dia

No mesmo 26 de outubro, a OpenAI também reivindicou uma prova da conjectura de suavização local de Christopher Sogge em todas as dimensões, o que resolveria a conjectura de Kakeya, e uma prova da existência da teoria de Yang-Mills pura em quatro dimensões, que resolve apenas parte de um dos sete problemas do milênio do Clay Mathematics Institute. Para a parte de física, o grupo liderado pelo laureado com o Nobel David Gross optou por não publicar ainda o material produzido pela IA.

Esse volume de resultados não é isolado. No começo de outubro, a OpenAI já havia divulgado de uma vez 722 artigos de matemática gerados por seus modelos. Ryan Williams chamou aquela entrega de um ataque de negação de serviço contra os matemáticos (no original em inglês, "DDoS attack against mathematicians"). Mesmo assim, ele aceitou organizar o exame do caso da ETH, e classifica partes da prova como rotineiras, mas aponta dois ou três elementos que considera bem incomuns.

O que muda para quem constrói e avalia IA

Para quem monta benchmark de raciocínio lógico ou usa prova formal como critério de avaliação, o episódio separa duas coisas que costumavam andar juntas: gerar uma demonstração e confirmar que ela é válida. Um checker como o Lean garante consistência interna, não garante que a tradução do enunciado em prosa para código formal captura a intenção certa. É exatamente esse elo, chamado de autoformalização, que ainda depende de revisão humana especializada e que nenhum dos dois laboratórios terminou.

Isso tem peso prático para quem avalia agentes de raciocínio: um resultado "verificado por Lean" não é sinônimo de "correto e relevante". Times que constroem pipelines de avaliação com prova formal como sinal de qualidade precisam somar uma etapa de checagem de fidelidade da formalização, não só do êxito do verificador.

O caso também deixa mais claro o limite atual da IA em teoria da computação: ela já produz candidatos a resultado em escala (722 artigos em um único lote, 14 milhões de tokens para um único algoritmo), mas o gargalo migrou da descoberta para a verificação, que continua custando meses de trabalho de especialistas humanos. Para quem planeja usar modelos de raciocínio para acelerar pesquisa interna, esse é o número que importa: quantos revisores humanos por resultado publicado, não quantos tokens por resultado gerado.

Fonte: ActuIA