Mais um laboratório de ponta afirma que a sua IA derrubou um dos pressupostos de trabalho da teoria da complexidade. A 27 de outubro, a Anthropic integrou no repositório público formal-math, no GitHub, uma pasta com um artigo atribuído ao Claude e um desenvolvimento em Lean 4 que, segundo a empresa, demonstra que a Hipótese do Tempo Exponencial (ETH) é falsa. A publicação aconteceu poucas horas depois de a OpenAI divulgar a sua própria refutação da mesma conjetura, e os dois trabalhos apresentam-se como independentes.
Formulada por Russell Impagliazzo e Ramamohan Paturi em 1999, a ETH sustenta que o 3-SAT, ou seja, decidir se uma fórmula booleana com cláusulas de três literais tem solução, exige um tempo exponencial no número de variáveis para alguma constante fixa. O artigo da Anthropic descreve um algoritmo determinístico que vai além da decisão: conta as atribuições que satisfazem a fórmula, em tempo 2 elevado a O(n log log n a dividir pela raiz quadrada de log n). Como esse expoente cresce mais devagar do que qualquer múltiplo constante de n, a conclusão é que o 3-SAT pode ser resolvido em tempo 2^o(n).
A forma como o resultado terá surgido é invulgar. De acordo com a nota de proveniência na página do artigo na plataforma Hexagon, um modelo interno de investigação do Claude encontrou o núcleo do algoritmo a 16 de outubro, consumindo cerca de 14 milhões de tokens de saída sem intervenção humana; só depois os investigadores da Anthropic trabalharam com o modelo na redação. A mesma página classifica o texto como gerado sobretudo por IA. O README do repositório acrescenta que o Claude Opus 5.5, em esforço elevado, consegue reconstruir a versão de decisão da refutação a partir de uma pista condensada ali publicada.
A parte formal foi pensada para ser verificada por terceiros. Um ficheiro curto, MainResults.lean, enuncia dois teoremas sobre o modelo de máquinas de Turing do Mathlib: que a ETH é falsa e o principal limite de contagem do artigo. Segundo o README, ambos dependem apenas dos três axiomas padrão do Lean, o projeto compila em cerca de oito minutos com 24 CPU virtuais e a integração contínua usa a ferramenta Comparator para voltar a verificar as provas com um segundo núcleo, escrito de forma independente, chamado nanoda. O código está sob licença Apache 2.0.
A Anthropic é clara sobre o que a verificação automática deixa de fora. O Lean confirma que as provas decorrem das definições enunciadas, mas nenhum programa garante que MainResults.lean diz o mesmo que o artigo, e uma análise do SXZ.io cita o próprio texto para notar que ninguém, ao que se sabe, conferiu o código Lean escrito pela IA. A mesma análise observa que o teorema apenas garante a existência de uma constante e que, pelas contas do próprio artigo, o limite só supera a pesquisa exaustiva em fórmulas com mais de 10^10 000 variáveis, no caso de cinco cláusulas por variável.
A comparação com o trabalho da OpenAI já está a ser feita. O SXZ.io indica que o enunciado em Lean da Anthropic abrange o limite completo do artigo e declara diretamente a falsidade da ETH, ao passo que o teorema formal da OpenAI cobre um expoente mais fraco do que o do manuscrito; a configuração da Anthropic ativa ainda o segundo núcleo, que a da OpenAI deixa desligado. O TechCrunch, que noticiou as duas publicações, citou Ryan Williams, do MIT, segundo o qual, a confirmarem-se as alegações, muitos artigos que assumem a ETH terão de ser revistos, e a comunidade deverá dar um pouco mais de peso à hipótese de P = NP.
A revisão por especialistas mal começou. Williams, Impagliazzo e Paturi estão a organizar a resposta da comunidade de ciência da computação à alegação da OpenAI e escreveram que a sua participação não equivale a uma certificação; não foi anunciada qualquer revisão equivalente do artigo da Anthropic. Para já, o impacto prático é reduzido. A Anthropic sublinha que o resultado é puramente assintótico e não acelera a resolução de fórmulas reais, pelo que o interesse está na teoria e no que revela sobre sistemas de IA capazes de produzir matemática verificável.