A Anthropic publicou uma pré-publicação em 27 de outubro de 2026 alegando um algoritmo determinístico de tempo subexponencial para 3-SAT, um resultado que refutaria a Hipótese do Tempo Exponencial se passar pela revisão.
Na pré-publicação da Anthropic, o tempo de execução alegado é 2^o(n), e o artigo afirma que a mesma abordagem também produz um resultado subexponencial para #3-SAT. A Anthropic diz que o algoritmo central foi encontrado em 16 de outubro por um modelo interno de pesquisa Claude, usando 14M tokens de saída sem intervenção humana, antes de pesquisadores trabalharem com o Claude para desenvolver o artigo.
A Anthropic também lançou um artefato em Lean 4 junto da pré-publicação. O README afirma que o Lean verifica as provas, mas nenhuma máquina verifica se as declarações em Lean correspondem exatamente ao artigo. O mesmo repositório também diz que o resultado é puramente assintótico, não uma alegação sobre resolução prática de SAT.
A principal ressalva é que isso ainda é uma alegação sem revisão. O artigo e a formalização são artefatos públicos, mas não substituem o escrutínio externo de teóricos da complexidade.
